iterateChain — Mathlib

English

The iterateChain construction yields a chain from the iterates of f starting at x, provided x ≤ f x.

Русский

Конструкция iterateChain порождает цепь из итератов f, начиная с x, при условии x ≤ f x.

LaTeX

$$$\text{iterateChain}(f,x,h) :\text{Chain}\;\alpha\quad\text{with } h:x\le f x$$$

Lean4

/-- Iteration of a function on an initial element interpreted as a chain. -/
def iterateChain (f : α →o α) (x : α) (h : x ≤ f x) : Chain α :=
  ⟨fun n => f^[n] x, f.monotone.monotone_iterate_of_le_map h⟩

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