iterate — Mathlib

English

If f is RightOrdContinuous, then every iterate f^[n] is RightOrdContinuous for all n ∈ ℕ.

Русский

Если f — правая непрерывность, то все итерации f^[n] являются правой непрерывностью для любого n ∈ ℕ.

LaTeX

$$$ \\forall n \\in \\mathbb{N}, \\ \\text{RightOrdContinuous}(f^{[n]}). $$$

Lean4

protected theorem iterate {f : α → α} (hf : RightOrdContinuous f) (n : ℕ) : RightOrdContinuous f^[n] :=
  hf.orderDual.iterate n

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