inter_frequently_image_mem_ae_eq — Mathlib

English

Under a conservative f, the joint set s ∩ {x | ∃ᶠ n, f^n x ∈ s} is a.e. equal to s.

Русский

При консервативном f множество $s$ пересечения с частыми возвращениями совпадает почти везде с $s$.

LaTeX

$$$s \cap \{x: \exists^{\mathrm{F}} n, f^{n} x \in s\} =_{\text{ae}} s$.$$

Lean4

theorem inter_frequently_image_mem_ae_eq (hf : Conservative f μ) (hs : NullMeasurableSet s μ) :
    (s ∩ {x | ∃ᶠ n in atTop, f^[n] x ∈ s} : Set α) =ᵐ[μ] s :=
  inter_eventuallyEq_left.2 <| hf.ae_mem_imp_frequently_image_mem hs

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