Theorem MeasureTheory.Conservative.measureRestrict

Modification history

2024-09-12 18:54

Mathlib/Dynamics/Ergodic/Conservative.lean

feat(Ergodic/Conservative): add `Conservative.measureRestrict` (#16126)

Added MeasureTheory.Conservative.measureRestrict View on Github →