Theorem ContinuousOn.aestronglyMeasurable_of_subset_isCompact

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 ContinuousOn.aestronglyMeasurable_of_subset_isCompactView on Github →