gfpApprox

Mathlib.SetTheory.Ordinal.FixedPointApproximants

URI: https://scilib.ai/kg/mathlib#OrdinalApprox.gfpApprox

Lean4

/-- The ordinal-indexed sequence approximating the greatest fixed point greater than
an initial value `x`. It is defined in such a way that we have `gfpApprox 0 x = x` and
`gfpApprox a x = ⨅ b < a, f (lfpApprox b x)`. -/
def gfpApprox (a : Ordinal.{u}) : α :=
  sInf ({f (gfpApprox b) | (b : Ordinal) (h : b < a)} ∪ { x })
termination_by a
decreasing_by exact h

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

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

Разделы

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

Аффилиация

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