ae_empty_or_univ — Mathlib

English

If f is PreErgodic with respect to μ, and s is measurable with f⁻¹(s) = s, then s is μ-almost-empty or μ-almost-universal.

Русский

Если f является предергодическим относительно меры μ и множество s измеримо, причём прообраз f⁻¹(s) = s, тогда s является μ-почти-пустым или μ-почти-всепокрывающим.

LaTeX

$$$\\text{PreErgodic } f\\, μ\\;\\rightarrow\\; (s \\text{ measurable and } f^{-1}(s) = s) \\Rightarrow s =^{\\mathbf{ae}}_μ \\varnothing \\lor s =^{\\mathbf{ae}}_μ \\text{univ}$$$

Lean4

theorem ae_empty_or_univ (hf : PreErgodic f μ) (hs : MeasurableSet s) (hfs : f ⁻¹' s = s) :
    s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ := by simpa only [eventuallyConst_set'] using hf.aeconst_set hs hfs

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