ae_empty_or_univ_of_image_ae_le — Mathlib

English

An ergodic map is quasi-ergodic (re-statement).

Русский

Эргодичное отображение является квазирегодичным.

LaTeX

$$$\mathrm{Ergodic}(f, \mu) \Rightarrow \mathrm{QuasiErgodic}(f, \mu)$$$

Lean4

theorem ae_empty_or_univ_of_image_ae_le (hf : Ergodic f μ) (hs : NullMeasurableSet s μ) (hs' : f '' s ≤ᵐ[μ] s) :
    s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ :=
  ae_empty_or_univ_of_image_ae_le' hf hs hs' <| measure_ne_top μ s

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