periodicOrbit_apply_eq — Mathlib

English

For any x in the domain, periodicOrbit(f, f x) equals periodicOrbit(f, x) when x is periodic.

Русский

Для любой точки x, если x периодична, то periodicOrbit(f, f x) = periodicOrbit(f, x).

LaTeX

$$$\\forall x\\in \\operatorname{periodicPts}(f),\\ \\operatorname{periodicOrbit}(f, f(x)) = \\operatorname{periodicOrbit}(f,x)$$$

Lean4

theorem periodicOrbit_apply_eq (hx : x ∈ periodicPts f) : periodicOrbit f (f x) = periodicOrbit f x :=
  periodicOrbit_apply_iterate_eq hx 1

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