English
If f is strictly monotone and x < f x, then the iterates f^[n] x form a strictly increasing sequence.
Русский
Если f строго монотонна и x < f x, то итераты f^[n] x образуют строго возрастающую последовательность.
LaTeX
$$$\\forall {\\alpha} [\\mathrm{Preorder}\\,\\alpha],\\ {f: \\alpha \\to \\alpha},\\ {x: \\alpha},\\ \\mathrm{StrictMono}\\ f\\ \\to\\ x < f x\\ \\to\\mathrm{StrictMono}\\ (n \\mapsto \\operatorname{Nat.iterate} f n x).$$$
Lean4
/-- If `f` is a strictly monotone map and `x < f x` at some point `x`, then the iterates `f^[n] x`
form a strictly monotone sequence. -/
theorem strictMono_iterate_of_lt_map (hf : StrictMono f) (hx : x < f x) : StrictMono fun n => f^[n] x :=
strictMono_nat_of_lt_succ fun n => by
rw [iterate_succ_apply]
exact hf.iterate n hx
