AddCircleAdd

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

Statistics

Metric	Count
Definitions	0
Theorems ergodic_add_left, ergodic_add_right	2
Total	2

AddCircle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ergodic_add_left 📖	mathematical	—	Ergodic AddCircle Real Real.instAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroupReal MeasureTheory.MeasureSpace.volume addOrderOf ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	AddSubgroup.normal_of_comm denseRange_zsmul_iff ergodic_add_left_iff_denseRange_zsmul QuotientAddGroup.instIsTopologicalAddGroup instIsTopologicalAddGroupReal QuotientAddGroup.instSecondCountableTopology IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instSecondCountableTopologyReal QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Real.borelSpace AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples isFiniteMeasure MeasureTheory.Measure.instInnerRegularOfIsAddHaarMeasureOfCompactSpace compactSpace MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant instIsAddHaarMeasureRealVolume MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.instNeZeroOfNonempty MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure
ergodic_add_right 📖	mathematical	—	Ergodic AddCircle Real Real.instAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroupReal MeasureTheory.MeasureSpace.volume addOrderOf ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	add_comm

---

← Back to Index