Theorems · Theorem · dynamical systems

aeconst_of_dense_aestabilizer_smul

∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [ContinuousInv G] {X : Type u_2}
  [inst_3 : TopologicalSpace X] [R1Space X] [inst_5 : MeasurableSpace X] [BorelSpace X] [inst_7 : MulAction G X]
  [ContinuousSMul G X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular]
  [inst_11 : ErgodicSMul G X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense ↑(MulAction.aestabilizer G μ s) → Filter.EventuallyConst s (MeasureTheory.ae μ)

Defined in

Mathlib.Dynamics.Ergodic.Action.OfMinimal

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceContinuousInvTopologicalSpaceR1SpaceMeasurableSpaceBorelSpaceMulActionContinuousSMulMeasureTheory.IsFiniteMeasureMeasureTheory.Measure.InnerRegularErgodicSMul