Function

📁 Source: Mathlib/Dynamics/Ergodic/Function.lean

Statistics

Metric	Count
Definitions	0
Theorems ae_eq_const_of_ae_eq_comp_ae, ae_eq_const_of_ae_eq_comp₀, eq_const_of_compMeasurePreserving_eq, ae_eq_const_of_ae_eq_comp, ae_eq_const_of_ae_eq_comp_ae, ae_eq_const_of_ae_eq_comp_of_ae_range₀, ae_eq_const_of_ae_eq_comp₀, eq_const_of_compQuasiMeasurePreserving_eq	8
Total	8

Ergodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_const_of_ae_eq_comp_ae 📖	—	Ergodic MeasureTheory.AEStronglyMeasurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass QuasiErgodic.ae_eq_const_of_ae_eq_comp_ae quasiErgodic
ae_eq_const_of_ae_eq_comp₀ 📖	—	Ergodic MeasureTheory.NullMeasurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass QuasiErgodic.ae_eq_const_of_ae_eq_comp₀ quasiErgodic
eq_const_of_compMeasurePreserving_eq 📖	mathematical	Ergodic MeasureTheory.AEEqFun.compMeasurePreserving toMeasurePreserving	MeasureTheory.AEEqFun.const	—	toMeasurePreserving QuasiErgodic.eq_const_of_compQuasiMeasurePreserving_eq quasiErgodic

PreErgodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_const_of_ae_eq_comp 📖	mathematical	PreErgodic Measurable	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Filter.exists_eventuallyEq_const_of_forall_separating MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.instCountableInterFilter MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated ae_mem_or_ae_notMem Set.preimage_comp

QuasiErgodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_const_of_ae_eq_comp_ae 📖	—	QuasiErgodic MeasureTheory.AEStronglyMeasurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range ae_eq_const_of_ae_eq_comp_of_ae_range₀ MeasurableSpace.countablySeparated_of_separatesPoints BorelSpace.countablyGenerated Subtype.borelSpace TopologicalSpace.IsSeparable.secondCountableTopology TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace separatesPointsOfOpensMeasurableSpaceOfT0Space Subtype.opensMeasurableSpace BorelSpace.opensMeasurable Subtype.t0Space T6Space.toT0Space instT6SpaceOfMetrizableSpace AEMeasurable.nullMeasurable MeasureTheory.AEStronglyMeasurable.aemeasurable
ae_eq_const_of_ae_eq_comp_of_ae_range₀ 📖	—	QuasiErgodic Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.NullMeasurable Filter.EventuallyEq	—	—	MeasureTheory.Measure.instOuterMeasureClass Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating MeasureTheory.instCountableInterFilter MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated_subtype ae_mem_or_ae_notMem₀ Filter.Eventually.set_eq Filter.Eventually.mono Set.preimage_comp Set.mem_preimage
ae_eq_const_of_ae_eq_comp₀ 📖	—	QuasiErgodic MeasureTheory.NullMeasurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass ae_eq_const_of_ae_eq_comp_of_ae_range₀ MeasurableSpace.countablySeparated_subtype_of_hasCountableSeparatingOn MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated Filter.univ_mem
eq_const_of_compQuasiMeasurePreserving_eq 📖	mathematical	QuasiErgodic MeasureTheory.AEEqFun.compQuasiMeasurePreserving toQuasiMeasurePreserving	MeasureTheory.AEEqFun.const	—	toQuasiMeasurePreserving MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.trans Filter.EventuallyEq.symm MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving Filter.EventuallyEq.refl ae_eq_const_of_ae_eq_comp_ae MeasureTheory.AEEqFun.aestronglyMeasurable MeasureTheory.AEEqFun.ext MeasureTheory.AEEqFun.coeFn_const

---

← Back to Index