Theorems · Theorem · dynamical systems

aeconst_of_dense_setOf_preimage_smul_ae

Deprecated since 2026-07-09Use aeconst_of_dense_setOfPred_preimage_smul_ae instead.

∀ {M : Type u_1} [inst : TopologicalSpace M] {X : Type u_2} [inst_1 : TopologicalSpace X] [R1Space X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] [inst_5 : SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense {g | (fun x => g • x) ⁻¹' s =ᵐ[μ] s} → Filter.EventuallyConst s (MeasureTheory.ae μ)

Alias of aeconst_of_dense_setOfPred_preimage_smul_ae. Let M act continuously on an R₁ topological space X. Let μ be a finite inner regular measure on X which is ergodic with respect to this action. If a null measurable set s is a.e. equal to its preimages under the action of a dense set of elements of M, then it is either null or conull.

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

TopologicalSpaceTopologicalSpaceR1SpaceMeasurableSpaceBorelSpaceSMulContinuousSMulMeasureTheory.IsFiniteMeasureMeasureTheory.Measure.InnerRegularErgodicSMul