Theorems · Theorem · dynamical systems

ergodic_mul_left_of_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},
  (DenseRange fun x => g ^ x) →
    ∀ (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsMulLeftInvariant],
      Ergodic (fun x => g * x) μ

Defined in

Mathlib.Dynamics.Ergodic.Action.OfMinimal

Cited by

1 results in Mathlib

Foundations

Depth 231 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpaceIsTopologicalGroupMeasurableSpaceSecondCountableTopologyBorelSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.Measure.InnerRegularMeasureTheory.Measure.IsMulLeftInvariant