iterate — Mathlib

English

If f is locally Lipschitz, then its n-th iterate f^[n] is locally Lipschitz for every n.

Русский

Если f локально липшицево, то его n-й итерат f^[n] тоже локально липшицево.

LaTeX

$$$\\forall n:\\\\mathbb{N},\\ LocallyLipschitz f^{[n]}$$$

Lean4

protected theorem iterate {f : α → α} (hf : LocallyLipschitz f) : ∀ n, LocallyLipschitz f^[n]
  | 0 => by simpa only [pow_zero] using LocallyLipschitz.id
  | n + 1 => by rw [iterate_add, iterate_one]; exact (hf.iterate n).comp hf

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