le_iterate_comp_of_le — Mathlib

English

If f is monotone and h ∘ g ≤ f ∘ h, then h ∘ g^[n] ≤ f^[n] ∘ h for every n.

Русский

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

LaTeX

$$$\\text{Monotone}(f) \\Rightarrow (H : h \\circ g \\le f \\circ h) \\Rightarrow \\forall n,\\ h \\circ g^{[n]} \\le f^{[n]} \\circ h.$$$

Lean4

theorem le_iterate_comp_of_le (hf : Monotone f) (H : h ∘ g ≤ f ∘ h) (n : ℕ) : h ∘ g^[n] ≤ f^[n] ∘ h := fun x =>
  by
  apply hf.seq_le_seq n <;> intros <;> simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]
  case hx => exact H _

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