ae_empty_or_univ_of_preimage_ae_le

English

For ergodic f with finite measure, if f⁻¹' s ≤ᵐ s and s is null-measurable, then s is almost empty or almost univ.

Русский

Для эргодического f с конечной мерой, если f⁻¹' s ≤ᵐ s и s нуль-измеримо, то s почти пусто или почти все пространство.

LaTeX

$$$\mathrm{Ergodic}(f, \mu) \land \mathrm{NullMeasurableSet}(s, \mu) \land (f^{-1}(s) \leq^{\mathrm{ae}} s) \Rightarrow s =^{\mu} \emptyset \lor s =^{\mu} \mathrm{univ}$$$

Lean4

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

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