ae_mem_or_ae_notMem₀ — Mathlib

English

For a quasi-ergodic map, either almost every point lies in s or almost every point lies outside s.

Русский

Для квазирегодной карты либо почти каждый точка принадлежит s, либо почти каждая точка не принадлежит s.

LaTeX

$$$\mathrm{(ae}\,\mu)\EventuallyEq (x \in s) \lor (x \notin s)$$$

Lean4

/-- For a quasi-ergodic map, sets that are almost invariant (rather than strictly invariant) are
still either almost empty or full. -/
theorem ae_mem_or_ae_notMem₀ (hf : QuasiErgodic f μ) (hsm : NullMeasurableSet s μ) (hs : f ⁻¹' s =ᵐ[μ] s) :
    (∀ᵐ x ∂μ, x ∈ s) ∨ ∀ᵐ x ∂μ, x ∉ s :=
  eventuallyConst_set.mp <| hf.aeconst_set₀ hsm hs

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