Theorems · Theorem · dynamical systems

ergodic_mul_left_iff_denseRange_zpow

∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [SecondCountableTopology G] [BorelSpace G] {g : G} (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ]
  [μ.InnerRegular] [μ.IsMulLeftInvariant] [NeZero μ], Ergodic (fun x => g * x) μ ↔ DenseRange fun x => g ^ x

Defined in: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Cited by: 0 results in Mathlib
Foundations: Depth 232 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group TopologicalSpace IsTopologicalGroup MeasurableSpace SecondCountableTopology BorelSpace MeasureTheory.IsFiniteMeasure MeasureTheory.Measure.InnerRegular MeasureTheory.Measure.IsMulLeftInvariant NeZero

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Groupstatement and proof · cited by 6,238
BorelSpacestatement and proof · cited by 1,602
MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
SecondCountableTopologystatement and proof · cited by 750
IsTopologicalGroupstatement and proof · cited by 469
DenseRangestatement and proof · cited by 164
MeasureTheory.Measure.IsMulLeftInvariantstatement and proof · cited by 118
MeasureTheory.Measure.InnerRegularstatement and proof · cited by 49
Ergodicstatement · cited by 48

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.