fixedPoint_isFixedPt — Mathlib

English

If a contraction f has a contracting iterate f^[n], then the fixed point of f^[n] is a fixed point of f.

Русский

Если сжимающее отображение f имеет сжатую последовательность итераций f^[n], то фиксированная точка f^[n] является фиксированной точкой f.

LaTeX

$$$\\text{IsFixedPt}(f, \\mathrm{fixedPoint}(f^{[n]}, hf))$ for some n; i.e., the fixed point of the iterate is fixed by f.$$

Lean4

/-- The point provided by `ContractingWith.fixedPoint` is actually a fixed point. -/
theorem fixedPoint_isFixedPt : IsFixedPt f (fixedPoint f hf) :=
  hf.efixedPoint_isFixedPt _

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