iterate_mem_periodicOrbit — Mathlib

English

If x is a periodic point for f, then every iterate f^n x lies in the periodic orbit of x.

Русский

Если x — периодическая точка относительно f, тогда каждый повтор f^n x принадлежит периодической орбите x.

LaTeX

$$$\\text{If }x\\in \\operatorname{periodicPts}(f),\\ \\forall n,\\ f^{n}(x) \\in \\operatorname{periodicOrbit}(f,x)$$$

Lean4

theorem iterate_mem_periodicOrbit (hx : x ∈ periodicPts f) (n : ℕ) : f^[n] x ∈ periodicOrbit f x := by simp [hx]

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