English
Let α be a linearly ordered set and f,g: α → α commute. Suppose f is strictly increasing and g is monotone. Then for every x ∈ α and every n ∈ ℕ with n > 0, the inequality f^[n] x ≤ g^[n] x holds if and only if f x ≤ g x.
Русский
Пусть α — линейно упорядоченное множество и f, g : α → α коммутируют. Предположим, что f строго возрастает, а g монотонна. Тогда для любого x ∈ α и любого n ∈ ℕ при n > 0 верно: f^[n] x ≤ g^[n] x тогда и только тогда, когда f x ≤ g x.
LaTeX
$$$\\forall {\\alpha} [\\mathrm{LinearOrder}\\,\\alpha] \\{f,g : \\alpha \\to \\alpha\\},\\ \\mathrm{Commute}\\ f\\ g\\ \\to\\ \\mathrm{StrictMono}\\ f\\ \\to\\ \\mathrm{Monotone}\\ g\\ \\to\\ \\forall {x : \\alpha} {n : \\mathbb{N}}, 0 < n \\to 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 : StrictMono f) (hg : Monotone 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)
