periodicOrbit_apply_iterate_eq — Mathlib

English

The periodic orbit is invariant under iteration: periodicOrbit f (f^n x) = periodicOrbit f x for all n.

Русский

Периодическая орбита инвариантна относительно итераций: periodicOrbit(f, f^n x) = periodicOrbit(f, x) для всех n.

LaTeX

$$$\\operatorname{periodicOrbit}(f, f^{[n]}(x)) = \\operatorname{periodicOrbit}(f, x)$$$

Lean4

theorem periodicOrbit_apply_iterate_eq (hx : x ∈ periodicPts f) (n : ℕ) :
    periodicOrbit f (f^[n] x) = periodicOrbit f x :=
  Eq.symm <|
    Cycle.coe_eq_coe.2 <|
      .intro n <|
        List.ext_get (by simp [minimalPeriod_apply_iterate hx]) fun m _ _ ↦ by
          simp [List.getElem_rotate, iterate_add_apply]

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