Theorems · Theorem · dynamical systems

ErgodicSMul.trans_isMinimal

∀ {M : Type u_1} {X : Type u_2} [inst : Monoid M] [inst_1 : SMul M X] [inst_2 : TopologicalSpace X] [R1Space X]
  [inst_4 : MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ]
  [μ.InnerRegular] (N : Type u_3) [inst_8 : MulAction M N] [inst_9 : Monoid N] [inst_10 : TopologicalSpace N]
  [MulAction.IsMinimal M N] [inst_12 : MulAction N X] [IsScalarTower M N X] [ContinuousSMul N X] [ErgodicSMul N X μ],
  ErgodicSMul M X μ

If N acts continuously and ergodically on X and M acts minimally on N, then the corresponding action of M on X is ergodic.

Defined in

Mathlib.Dynamics.Ergodic.Action.OfMinimal

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidSMulTopologicalSpaceR1SpaceMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.Measure.InnerRegularMulActionMonoidTopologicalSpaceMulAction.IsMinimalMulActionIsScalarTowerContinuousSMulErgodicSMul