lfpApprox

Mathlib.SetTheory.Ordinal.FixedPointApproximants

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

Lean4

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

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

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

Разделы

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

Аффилиация

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