measure_inter_frequently_image_mem_eq

English

For a conservative f and null-measurable s, μ(s ∩ {x | ∃ᶠ n, f^n x ∈ s}) = μ(s).

Русский

Для консервативного f и нулевоизмеримого s: μ( s ∩ {x | ∃ᶠ n, f^n x ∈ s} ) = μ(s).

LaTeX

$$$\mu\bigl(s \cap \{x: \exists^{\mathrm{F}} n, f^{n} x\in s\}\bigr) = \mu(s).$$$

Lean4

theorem measure_inter_frequently_image_mem_eq (hf : Conservative f μ) (hs : NullMeasurableSet s μ) :
    μ (s ∩ {x | ∃ᶠ n in atTop, f^[n] x ∈ s}) = μ s :=
  measure_congr (hf.inter_frequently_image_mem_ae_eq hs)

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