iterate_le_of_le — Mathlib

English

If g is monotone and f ≤ g and g is monotone, then f^[n] ≤ g^[n] for all n.

Русский

Если g монотонна и f ≤ g, то f^[n] ≤ g^[n] для всех n.

LaTeX

$$$\\text{Monotone}(g) \\land f \\le g \\Rightarrow \\forall n, f^{[n]} \\le g^{[n]}.$$$

Lean4

/-- If `f ≤ g` and `f` is monotone, then `f^[n] ≤ g^[n]`. -/
theorem iterate_le_of_le {g : α → α} (hf : Monotone f) (h : f ≤ g) (n : ℕ) : f^[n] ≤ g^[n] :=
  hf.iterate_comp_le_of_le h n

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