Theorem MeasureTheory.Measure.QuasiMeasurePreserving.restrict

Modification history

2026-09-15 19:08

Mathlib/MeasureTheory/Measure/Restrict.lean

chore(MeasureTheory): break import cycle between `QuasiMeasurePreserving` and `AEMeasurable` (#43190) …

Deleted MeasureTheory.Measure.QuasiMeasurePreserving.restrict View on Github →

2024-08-16 07:51

Mathlib/MeasureTheory/Measure/Restrict.lean

feat(Measure/Restrict): add `QuasiMeasurePreserving.restrict` (#15661)

Added MeasureTheory.Measure.QuasiMeasurePreserving.restrict View on Github →