antitone_iterate_of_map_le — Mathlib

English

If f is monotone and f x ≤ x, then the sequence n ↦ f^[n] x is antitone (decreasing).

Русский

Если f монотонна и f x ≤ x, то последовательность n ↦ f^[n] x убывающая.

LaTeX

$$$\\forall {\\alpha} [\\mathrm{Preorder}\\,\\alpha],\\ {f: \\alpha \\to \\alpha},\\ {x: \\alpha},\\ \\mathrm{Monotone}\\ f\\ \\to\\ f x \\le x\\ \\to\\mathrm{Antitone}\\ (n \\mapsto \\operatorname{Nat.iterate} f n x).$$$

Lean4

/-- If `f` is a monotone map and `f x ≤ x` at some point `x`, then the iterates `f^[n] x` form
an antitone sequence. -/
theorem antitone_iterate_of_map_le (hf : Monotone f) (hx : f x ≤ x) : Antitone fun n => f^[n] x :=
  hf.dual.monotone_iterate_of_le_map hx

Похожие утверждения