ae_mem_or_ae_notMem — Mathlib

English

For PreErgodic f and measurable s with invariance, either a.e. all points lie in s or a.e. almost all lie outside s.

Русский

Для PreErgodic f и измеримого s с инвариантностью либо почти все точки в s, либо почти все вне s.

LaTeX

$$$(\forall)\ae_{μ} x:\ x∈s \lor x∉s$ a.e.$$

Lean4

theorem ae_mem_or_ae_notMem (hf : PreErgodic f μ) (hsm : MeasurableSet s) (hs : f ⁻¹' s = s) :
    (∀ᵐ x ∂μ, x ∈ s) ∨ ∀ᵐ x ∂μ, x ∉ s :=
  eventuallyConst_set.1 <| hf.aeconst_set hsm hs

Похожие утверждения