iterate_pos_lt_of_map_lt — Mathlib

English

If f and g commute and f is strictly monotone while g is monotone, then f^{[n]} x < g^{[n]} x for x with f x < g x and n > 0.

Русский

Если f и g коммутируют, f строго монотонна, g монотонна, и f x < g x, то f^{[n]} x < g^{[n]} x для n > 0.

LaTeX

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

Lean4

theorem iterate_pos_lt_of_map_lt (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x} (hx : f x < g x) {n}
    (hn : 0 < n) : f^[n] x < g^[n] x := by
  apply hf.seq_pos_lt_seq_of_le_of_lt hn
  · rfl
  · intros; rw [iterate_succ_apply']
  · simp [h.iterate_right _ _, hg.iterate _ hx]

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