iterate_le_of_map_le — Mathlib

English

If f and g commute and f ≤ g with f strictly below g at x, then f^[n] x < g^[n] x for any n > 0, assuming monotone f and strictly monotone g.

Русский

Если f и g коммутируют и f ниже g в точке x, тогда f^[n] x < g^[n] x для любого n > 0 при условии монотонности f и строгой монотонности g.

LaTeX

$$$\\text{Function.Commute}(f,g) \\land \\text{Monotone}(f) \\land \\text{StrictMono}(g) \\Rightarrow \\forall x, \\forall n>0, f^{[n]}(x) < g^{[n]}(x).$$$

Lean4

theorem iterate_le_of_map_le (h : Commute f g) (hf : Monotone f) (hg : Monotone g) {x} (hx : f x ≤ g x) (n : ℕ) :
    f^[n] x ≤ g^[n] x := by
  apply hf.seq_le_seq n
  · rfl
  · intros; rw [iterate_succ_apply']
  · simp [h.iterate_right _ _, hg.iterate _ hx]

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