Commit 2026-01-07 14:25 46bb3906

View on Github →

feat: more API for ae strongly measurable functions on compact sets (#33670)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

added theorem Continuous.aestronglyMeasurable_of_compactSpace

added theorem ContinuousOn.aestronglyMeasurable_of_subset_isCompact

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

added theorem MeasureTheory.Measure.restrict_inter_toMeasurable

modified theorem MeasureTheory.Measure.restrict_toMeasurable

Modified Mathlib/Topology/MetricSpace/Pseudo/Basic.lean

modified theorem ContinuousOn.isSeparable_image

modified theorem IsCompact.isSeparable