Theorem MeasureTheory.FiniteMeasure.continuous_integral_boundedContinousFunction

Modification history

2024-11-05 19:27
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
chore: fix typo `Continous`-> `Continuous` (#18666)
Deleted MeasureTheory.FiniteMeasure.continuous_integral_boundedContinousFunctionView on Github →
2024-11-03 19:54
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
feat(ProbabilityMeasure): continuity of integral against a bounded continuous function (#18292) …
Added MeasureTheory.FiniteMeasure.continuous_integral_boundedContinousFunctionView on Github →