Theorems · Theorem · dynamical systems

MonoidHom.ergodic_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] [CompactSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure]
  (f : G →* G), Dense (⋃ n, (⇑f)^[n] ⁻¹' 1) → Continuous ⇑f → Function.Surjective ⇑f → Ergodic (⇑f) μ

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

Defined in

Mathlib.Dynamics.Ergodic.Action.OfMinimal

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceIsTopologicalGroupSecondCountableTopologyMeasurableSpaceBorelSpaceCompactSpaceMeasureTheory.Measure.IsHaarMeasure