English
Let f,g commute, with f monotone and 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
$$$\\forall {\\alpha} [\\mathrm{LinearOrder}\\,\\alpha] \\{f,g : \\alpha \\to \\alpha\\},\\ \\mathrm{Commute}\\ f\\ g\\ \\to\\ \\mathrm{Monotone}\\ f\\ \\to\\ \\mathrm{StrictMono}\\ g\\ \\to\\forall {x} {n}, 0 < n \\to f^{[n]} x = g^{[n]} x \\iff f x = g x.$$$
Lean4
theorem iterate_pos_eq_iff_map_eq (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
simp only [le_antisymm_iff, h.iterate_pos_le_iff_map_le hf hg hn, h.symm.iterate_pos_le_iff_map_le' hg hf hn]
