Theorem MeasureTheory.Conservative.of_absolutelyContinuous

Modification history

2024-09-12 18:54
Mathlib/Dynamics/Ergodic/Conservative.lean
feat(Ergodic/Conservative): add `Conservative.measureRestrict` (#16126)
Added MeasureTheory.Conservative.of_absolutelyContinuousView on Github →