efixedPoint_isFixedPt

Mathlib.Topology.MetricSpace.Contracting

URI: https://scilib.ai/kg/mathlib#ContractingWith.efixedPoint_isFixedPt

← MathLib Explorer

English

efixedPoint is a fixed point of f.

Русский

efixedPoint является фиксированной точкой f.

LaTeX

$$$ IsFixedPt\, f\, (efixedPoint\, f\, hf\, x\, hx) $$$

Lean4

theorem efixedPoint_isFixedPt (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ∞) :
    IsFixedPt f (efixedPoint f hf x hx) :=
  (Classical.choose_spec <| hf.exists_fixedPoint x hx).1

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru