fixedPoint_unique — Mathlib

English

For a contraction f on a complete space, the fixed point given by fixedPoint f hf is the unique fixed point of f.

Русский

Для сжатия на полном пространстве фиксированная точка fixedPoint f hf является единственной фиксированной точкой f.

LaTeX

$$$\\text{IsFixedPt}(f, \\mathrm{fixedPoint}(f,hf))$ and any fixed point is equal to this one.$$

Lean4

theorem fixedPoint_unique {x} (hx : IsFixedPt f x) : x = fixedPoint f hf :=
  hf.fixedPoint_unique' hx hf.fixedPoint_isFixedPt

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