Theorem Continuous.aestronglyMeasurable_of_compactSpace

Modification history

2026-01-07 14:25
Mathlib/MeasureTheory/Integral/IntegrableOn.lean
feat: more API for ae strongly measurable functions on compact sets (#33670)
Added Continuous.aestronglyMeasurable_of_compactSpaceView on Github →