Theorems · Theorem · dynamical systems

MonoidHom.preErgodic_of_dense_iUnion_preimage_one

∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [SecondCountableTopology G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasure μ]
  [μ.InnerRegular] [μ.IsMulLeftInvariant] (f : G →* G), Dense (⋃ n, (⇑f)^[n] ⁻¹' 1) → PreErgodic (⇑f) μ

Let f : G →* G be a group endomorphism of a topological group with second countable topology. If the preimages of 1 under the iterations of f are dense, then it is pre-ergodic with respect to any finite inner regular left invariant measure.

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

GroupTopologicalSpaceIsTopologicalGroupSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.Measure.InnerRegularMeasureTheory.Measure.IsMulLeftInvariant