strictAnti_iterate_of_map_lt — Mathlib

English

If f is strictly increasing and f x < x, then the iterates f^[n] x form a strictly decreasing sequence.

Русский

Если f строго возрастает и f x < x, то итераты f^[n] x образуют строго убывающую последовательность.

LaTeX

$$$\\forall {\\alpha} [\\mathrm{Preorder}\\,\\alpha],\\ {f: \\alpha \\to \\alpha},\\ {x: \\alpha},\\ \\mathrm{StrictMono}\\ f\\ \\to\\ f x < x\\ \\to\\mathrm{StrictAnti}\\ (n \\mapsto \\operatorname{Nat.iterate} f n x).$$$

Lean4

/-- If `f` is a strictly antitone map and `f x < x` at some point `x`, then the iterates `f^[n] x`
form a strictly antitone sequence. -/
theorem strictAnti_iterate_of_map_lt (hf : StrictMono f) (hx : f x < x) : StrictAnti fun n => f^[n] x :=
  hf.dual.strictMono_iterate_of_lt_map hx

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