docstring

teorth · Nov 18, 2024 · 4e2da37 · 4e2da37
1 parent c5c6e0c
commit 4e2da37
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/PFR/ForMathlib/ProbabilityMeasureProdCont.lean b/PFR/ForMathlib/ProbabilityMeasureProdCont.lean
@@ -29,7 +29,7 @@ lemma ProbabilityMeasure.tendsto_iff_forall_apply_tendsto {ι α : Type*} {L : F
     simp only [ne_eq, ennreal_coeFn_eq_coeFn_toMeasure]
 
 /-- Probability measures on a finite space tend to a limit if and only if the probability masses
-of all points tend to the corresponding limits. Version in ℝ≥0. -/
+of all points tend to the corresponding limits. Version in ℝ≥0∞. -/
 lemma ProbabilityMeasure.tendsto_iff_forall_apply_tendsto_ennreal
     {ι α : Type*} {L : Filter ι} [Finite α]
     [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] [BorelSpace α]