isFixedPt — Mathlib

English

If x is periodic with period n for f, then x is a fixed point of the nth iterate f^{∘n}; equivalently, f^{n}(x) = x.

Русский

Если x является периодической точкой f с периодом n, то x является фиксированной точкой n-й итерации f; то есть f^{n}(x) = x.

LaTeX

$$$IsPeriodicPt(f,n,x) \Rightarrow f^{\circ n}(x) = x$$$

Lean4

protected theorem isFixedPt (hf : IsPeriodicPt f n x) : IsFixedPt f^[n] x :=
  hf

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