Commit 2025-11-24 15:11 7cb828c1

View on Github →

feat: universal property of the weak convergence topology (#31964) ... in terms of evaluation against bounded continuous functions.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

added theorem MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_integral

added theorem MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_lintegral

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

added theorem MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_integral

added theorem MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_lintegral