Regular

📁 Source: Mathlib/Dynamics/Ergodic/Action/Regular.lean

Statistics

Metric	Count
Definitions	0
Theorems instErgodicSMulMulOppositeOfIsMulRightInvariant, instErgodicSMulOfIsMulLeftInvariant, instErgodicVAddAddOppositeOfIsAddRightInvariant, instErgodicVAddOfIsAddLeftInvariant	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instErgodicSMulMulOppositeOfIsMulRightInvariant 📖	mathematical	—	ErgodicSMul MulOpposite SemigroupAction.toSMul Monoid.toSemigroup MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toOppositeMulAction	—	MeasureTheory.Measure.IsMulRightInvariant.toSMulInvariantMeasure_op MeasureTheory.Measure.instOuterMeasureClass Filter.Frequently.exists Filter.Frequently.and_eventually MeasureTheory.Measure.ae_ae_comm Measurable.setOf Measurable.iff MeasurableSet.mem MeasurableSet.preimage Measurable.mul measurable_fst measurable_snd MeasureTheory.ae_of_all Filter.EventuallyEq.mem_iff mul_inv_cancel_left MeasureTheory.Measure.QuasiMeasurePreserving.ae MeasureTheory.quasiMeasurePreserving_mul_left or_not_of_imp
instErgodicSMulOfIsMulLeftInvariant 📖	mathematical	—	ErgodicSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction	—	MeasureTheory.Measure.IsMulLeftInvariant.smulInvariantMeasure MeasureTheory.Measure.instOuterMeasureClass Filter.Frequently.exists Filter.Frequently.and_eventually MeasureTheory.Measure.ae_ae_comm Measurable.setOf Measurable.iff MeasurableSet.mem MeasurableSet.preimage Measurable.mul measurable_snd measurable_fst MeasureTheory.ae_of_all Filter.EventuallyEq.mem_iff inv_mul_cancel_right MeasureTheory.Measure.QuasiMeasurePreserving.ae MeasureTheory.quasiMeasurePreserving_mul_right or_not_of_imp
instErgodicVAddAddOppositeOfIsAddRightInvariant 📖	mathematical	—	ErgodicVAdd AddOpposite AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toOppositeAddAction	—	MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op MeasureTheory.Measure.instOuterMeasureClass Filter.Frequently.exists Filter.Frequently.and_eventually MeasureTheory.Measure.ae_ae_comm Measurable.setOf Measurable.iff MeasurableSet.mem MeasurableSet.preimage Measurable.add measurable_fst measurable_snd MeasureTheory.ae_of_all Filter.EventuallyEq.mem_iff Filter.eventually_mem_set add_neg_cancel_left MeasureTheory.Measure.QuasiMeasurePreserving.ae MeasureTheory.quasiMeasurePreserving_add_left Filter.eventuallyConst_set Filter.not_frequently or_not_of_imp
instErgodicVAddOfIsAddLeftInvariant 📖	mathematical	—	ErgodicVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction	—	MeasureTheory.Measure.IsAddLeftInvariant.vaddInvariantMeasure MeasureTheory.Measure.instOuterMeasureClass Filter.Frequently.exists Filter.Frequently.and_eventually MeasureTheory.Measure.ae_ae_comm Measurable.setOf Measurable.iff MeasurableSet.mem MeasurableSet.preimage Measurable.add measurable_snd measurable_fst MeasureTheory.ae_of_all Filter.EventuallyEq.mem_iff Filter.eventually_mem_set neg_add_cancel_right MeasureTheory.Measure.QuasiMeasurePreserving.ae MeasureTheory.quasiMeasurePreserving_add_right Filter.eventuallyConst_set Filter.not_frequently or_not_of_imp

---

← Back to Index