fix

math-comp · Jan 8, 2024 · 6ff15ac · 6ff15ac
1 parent 2f6c482
commit 6ff15ac
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -20,10 +20,10 @@ Require Import esum measure lebesgue_measure numfun.
 (* Fubini's theorem, etc.                                                     *)
 (*                                                                            *)
 (* Main notation:                                                             *)
-(* | Coq notation          | | Meaning                         |              *)
-(* |-----------------------|-|---------------------------------|              *)
-(* | \int[mu]_(x in D) f x | | $\int_{x\in D} f(x)\mathbf{d}x$ |              *)
-(* | \int[mu]_x f x        | | $\int_x f(x)\mathbf{d}x$        |              *)
+(* | Coq notation          |  | Meaning                         |             *)
+(* |----------------------:|--|:--------------------------------              *)
+(* | \int[mu]_(x in D) f x |==| $\int_D f(x)\mathbf{d}\mu(x)$                 *)
+(* | \int[mu]_x f x        |==| $\int f(x)\mathbf{d}\mu(x)$                   *)
 (*                                                                            *)
 (* Main reference:                                                            *)
 (* - Daniel Li, Intégration et applications, 2016                             *)