Theorems · Theorem · dynamical systems
MeasureTheory.Conservative.congr_ae
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {μ ν : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ → MeasureTheory.ae μ = MeasureTheory.ae ν → MeasureTheory.Conservative f ν- Defined in
- Mathlib.Dynamics.Ergodic.Conservative
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Filterstatement · cited by 8,121
- MeasureTheory.aestatement and proof · cited by 2,352
- Eq.leproof · cited by 605
- Eq.geproof · cited by 375
- MeasureTheory.Conservativestatement and proof · cited by 19
- MeasureTheory.Measure.QuasiMeasurePreserving.monoproof · cited by 9
- MeasureTheory.Conservative.toQuasiMeasurePreservingproof · cited by 6
- MeasureTheory.Conservative.of_absolutelyContinuousproof · cited by 2
- LE.le.absolutelyContinuous_of_aeproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- MeasureTheory.conservative_congrproof · cited by 0