Theorem MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_lintegral

Modification history

2025-11-28 15:51
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
feat: universal property of weak convergence over a compact space (#32087) …
Modified MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_lintegralView on Github →
2025-11-24 15:11
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
feat: universal property of the weak convergence topology (#31964) …
Added MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_lintegralView on Github →