iterate — Mathlib

English

Let f: α → α and x ∈ α. If x is a fixed point of f (i.e., f(x) = x), then x is a fixed point of every iterate f^n, for all n ∈ ℕ.

Русский

Пусть f: α → α и x ∈ α. Если x является фиксированной точкой f (то есть f(x) = x), то x является фиксированной точкой каждой итерации f^n для всех n ∈ ℕ.

LaTeX

$$$IsFixedPt\, f\, x \rightarrow \forall n:\mathbb{N},\ IsFixedPt\, (f^n)\, x$$$

Lean4

/-- If `x` is a fixed point of `f`, then it is a fixed point of `f^[n]`. -/
protected theorem iterate (hf : IsFixedPt f x) (n : ℕ) : IsFixedPt f^[n] x :=
  iterate_fixed hf n

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