sequence notation in Fubini

math-comp · Oct 16, 2022 · 409b82b · 409b82b
1 parent 6a6d7e1
commit 409b82b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -4086,8 +4086,8 @@ Hypothesis f_g : {ae mu, forall x n, D x -> `|f_ n x| <= g x}.
 Let g_ n x := `|f_ n x - f x|.
 
 Theorem dominated_convergence : [/\ mu.-integrable D f,
-  (fun n => \int[mu]_(x in D) (g_ n x) ) --> 0 &
-  (fun n => \int[mu]_(x in D) (f_ n x) ) --> \int[mu]_(x in D) (f x) ].
+  [sequence \int[mu]_(x in D) (g_ n x)]_n --> 0 &
+  [sequence \int[mu]_(x in D) (f_ n x)]_n --> \int[mu]_(x in D) (f x) ].
 Proof.
 have [N1 [mN1 N10 subN1]] := f_f.
 have [N2 [mN2 N20 subN2]] := f_g.