of_iterate — Mathlib

English

If f^n is PreErgodic with μ, then f is PreErgodic with μ.

Русский

Если f^n преэргодично относительно μ, то и f преэргодично относительно μ.

LaTeX

$$$\forall n\,\ \mathrm{PreErgodic}(\mathrm{Nat.iterate}(f,n),\mu) \Rightarrow \mathrm{PreErgodic}(f,\mu).$$$

Lean4

theorem of_iterate (n : ℕ) (hf : PreErgodic f^[n] μ) : PreErgodic f μ :=
  ⟨fun _ hs hs' => hf.aeconst_set hs <| IsFixedPt.preimage_iterate hs' n⟩

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