Commit 2024-11-03 19:54 b60689e9

View on Github →

feat(ProbabilityMeasure): continuity of integral against a bounded continuous function (#18292) From PFR

Estimated changes

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

added theorem MeasureTheory.FiniteMeasure.continuous_integral_boundedContinousFunction

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

added theorem MeasureTheory.ProbabilityMeasure.continuous_integral_boundedContinuousFunction