English
Let X be a topological space, f: X → X, and x ∈ X. If f is continuous at x and x is a fixed point of f (f(x) = x), then for every n ∈ ℕ the n-th iterate of f is continuous at x.
Русский
Пусть X — топологическое пространство, f: X → X, и x ∈ X. Если f непрерывна в x и x является.fixed точкой функции (f(x) = x), то для каждого n ∈ ℕ f^{[n]} непрерывна в x.
LaTeX
$$$\\forall X [TopologicalSpace\,X], \\forall f:X\\to X, \\forall x\\in X, (\\\\ ContinuousAt\\, f\\ x \\land f\\ x = x) \\Rightarrow \\forall n\\in\\mathbb{N}, \\ ContinuousAt\\,(f^{[n]})\\ x$$$
Lean4
theorem iterate {f : X → X} (hf : ContinuousAt f x) (hx : f x = x) (n : ℕ) : ContinuousAt f^[n] x :=
Nat.recOn n continuousAt_id fun _n ihn ↦ ihn.comp_of_eq hf hx
