Theorem MeasureTheory.ProbabilityMeasure.continuous_integral_boundedContinuousFunction

Modification history

2025-11-28 15:51
Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
feat: universal property of weak convergence over a compact space (#32087) …
Modified MeasureTheory.ProbabilityMeasure.continuous_integral_boundedContinuousFunctionView on Github →
2024-11-03 19:54
Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
feat(ProbabilityMeasure): continuity of integral against a bounded continuous function (#18292) …
Added MeasureTheory.ProbabilityMeasure.continuous_integral_boundedContinuousFunctionView on Github →