Mathlib Changelog
v4
Changelog
About
Github
Theorem
MeasureTheory.Measure.restrict_inter_toMeasurable
Modification history
2026-01-07 14:25
Mathlib/MeasureTheory/Measure/Restrict.lean
feat: more API for ae strongly measurable functions on compact sets (#33670)
Added
MeasureTheory.Measure.restrict_inter_toMeasurable
View on Github →