iterate — Mathlib

English

If f is strictly monotone, then every iterate f^{∘ n} is strictly monotone for all natural numbers n.

Русский

Если f строго монотонна, то каждая итерация f^{∘ n} строго монотонна при любом натуральном n.

LaTeX

$$$\text{StrictMono}(f) \Rightarrow \forall n\in\mathbb{N},\ \text{StrictMono}(f^{\circ n}).$$$

Lean4

protected theorem iterate {f : α → α} (hf : StrictMono f) (n : ℕ) : StrictMono f^[n] :=
  Nat.recOn n strictMono_id fun _ h ↦ h.comp hf

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