Theorem MeasureTheory.FiniteMeasure.continuous_integral_boundedContinuousFunction

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_integral_boundedContinuousFunctionView on Github →
2024-11-05 19:27
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
chore: fix typo `Continous`-> `Continuous` (#18666)
Added MeasureTheory.FiniteMeasure.continuous_integral_boundedContinuousFunctionView on Github →