Update theories/lebesgue_integral.v

Co-authored-by: Cyril Cohen <[email protected]>
math-comp · Feb 5, 2025 · 063e6af · 063e6af
1 parent c8beda2
commit 063e6af
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -3497,8 +3497,8 @@ apply: ge0_subset_integral => //=.
 by move=> ? _; rewrite lee_fin f0.
 Qed.
 
-Lemma ge0_cvg_integral :
-  (fun n => \int[mu]_(x in `[0%R, n%:R]) (f x)%:E) @ \oo -->
+Lemma ge0_cvgn_integral :
+  \int[mu]_(x in `[0%R, n%:R]) (f x)%:E @[n --> \oo] -->
   \int[mu]_(x in `[0%R, +oo[) (f x)%:E.
 Proof.
 rewrite -cvg_shiftS/= ge0_integral_ereal_sup//.