English
Let f: α → α and x ∈ α. If x is a fixed point of f (i.e., f(x) = x), then x is a fixed point of every iterate f^n, for all n ∈ ℕ.
Русский
Пусть f: α → α и x ∈ α. Если x является фиксированной точкой f (то есть f(x) = x), то x является фиксированной точкой каждой итерации f^n для всех n ∈ ℕ.
LaTeX
$$$IsFixedPt\, f\, x \rightarrow \forall n:\mathbb{N},\ IsFixedPt\, (f^n)\, x$$$
Lean4
/-- If `x` is a fixed point of `f`, then it is a fixed point of `f^[n]`. -/
protected theorem iterate (hf : IsFixedPt f x) (n : ℕ) : IsFixedPt f^[n] x :=
iterate_fixed hf n