iterate_pos_le_iff_map_le — Mathlib

English

Let f and g commute, f monotone, g strictly monotone. For x and n>0, f^{[n]} x ≤ g^{[n]} x iff f x ≤ g x.

Русский

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

LaTeX

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

Lean4

theorem iterate_pos_le_iff_map_le (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n} (hn : 0 < n) :
    f^[n] x ≤ g^[n] x ↔ f x ≤ g x := by simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt' hg hf hn)

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