English
If f is monotone on a preorder and x ≤ f x, then the sequence n ↦ f^[n] x is monotone in n.
Русский
Если f монотонно отображает множество и выполнено x ≤ f x, то последовательность n ↦ f^[n] x монотонна по n.
LaTeX
$$$\\forall {\\alpha} [\\mathrm{Preorder}\\,\\alpha],\\ {f: \\alpha \\to \\alpha},\\ {x: \\alpha},\\ \\mathrm{Monotone}\\ f\\ \\to\\ x \\le f x\\ \\to\\mathrm{Monotone}\\ (n \\mapsto \\operatorname{Nat.iterate} f n x).$$$
Lean4
/-- If `f` is a monotone map and `x ≤ f x` at some point `x`, then the iterates `f^[n] x` form
a monotone sequence. -/
theorem monotone_iterate_of_le_map (hf : Monotone f) (hx : x ≤ f x) : Monotone fun n => f^[n] x :=
monotone_nat_of_le_succ fun n => by
rw [iterate_succ_apply]
exact hf.iterate n hx
