English
Let f and g commute, f monotone, g strictly monotone. For x and n>0, f^{[n]} x < g^{[n]} x if and only if 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) \\land \\text{Monotone}(f) \\land \\text{StrictMono}(g) \\land (0 < n) \\,\\Rightarrow \\, (f^{[n]} x < g^{[n]} x \\iff f x < g x).$$$
Lean4
theorem iterate_pos_lt_iff_map_lt (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
rcases lt_trichotomy (f x) (g x) with (H | H | H)
· simp only [*, iterate_pos_lt_of_map_lt]
· simp only [*, h.iterate_eq_of_map_eq, lt_irrefl]
· simp only [lt_asymm H, lt_asymm (h.symm.iterate_pos_lt_of_map_lt' hg hf H hn)]
