We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 86963af commit 3ae40eeCopy full SHA for 3ae40ee
theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
@@ -26,11 +26,11 @@ From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable.
26
(* Detailed contents: *)
27
(* ``` *)
28
(* m1 \x m2 == product measure over T1 * T2, m1 is a measure *)
29
-(* measure over T1, and m2 is a sigma finite *)
30
-(* measure over T2 *)
+(* over T1, and m2 is a sigma finite measure over *)
+(* T2 *)
31
(* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *)
32
-(* measure over T1, and m1 is a sigma finite *)
33
+(* over T1, and m1 is a sigma finite measure over *)
34
35
(* *)
36
(******************************************************************************)
0 commit comments