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_toMeasurableView on Github →