iterate — Mathlib

English

If g is continuous at f(x) and f is continuous at x, then the function x ↦ g(f(x)) is continuous at x.

Русский

Если g непрерывна в f(x) и f непрерывна в x, то x ↦ g(f(x)) непрерывна в x.

LaTeX

$$$\\mathrm{ContinuousAt}(g, f(x)) \\Rightarrow \\mathrm{ContinuousAt}(f, x) \\Rightarrow \\mathrm{ContinuousAt}(\\lambda x. g(f(x)), x)$$$

Lean4

theorem iterate {f : X → X} (h : Continuous f) (n : ℕ) : Continuous f^[n] :=
  Nat.recOn n continuous_id fun _ ihn => ihn.comp h

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