iterate — Mathlib

English

If f tends to itself along l, then all iterates f^[n] tend to l along l for every natural n.

Русский

Если f сходится к себе по l, то все повторные применения f^[n] сходятся к l по l для любого натурального n.

LaTeX

$$$\\forall f:\\alpha \\to \\alpha, \\; \\forall l:\\mathrm{Filter}(\\alpha),\\; (\\mathrm{Tendsto} f\\ l\\ l) \\Rightarrow \\forall n:\\mathbb{N},\\; \\mathrm{Tendsto} (f^{[n]})\\ l\\ l$$$

Lean4

protected theorem iterate {f : α → α} {l : Filter α} (h : Tendsto f l l) : ∀ n, Tendsto (f^[n]) l l
  | 0 => tendsto_id
  | (n + 1) => (h.iterate n).comp h

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