Theorems · Definition · dynamical systems

ErgodicSMul.recOn

{G : Type u_1} →
  {α : Type u_2} →
    [inst : SMul G α] →
      {x : MeasurableSpace α} →
        {μ : MeasureTheory.Measure α} →
          {motive : ErgodicSMul G α μ → Sort u} →
            (t : ErgodicSMul G α μ) →
              ([toSMulInvariantMeasure : MeasureTheory.SMulInvariantMeasure G α μ] →
                  (aeconst_of_forall_preimage_smul_ae_eq :
                      ∀ {s : Set α},
                        MeasurableSet s →
                          (∀ (g : G), (fun x => g • x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)) →
                    motive ⋯) →
                motive t

Defined in

Mathlib.Dynamics.Ergodic.Action.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SMul