gfpApprox_ord_eq_gfp — Mathlib

English

The GFP approximation along the ordinal indices converges to the GFP itself when starting from the top element, i.e., the GFP is reached at the limit of the ordinal sequence.

Русский

Аппроксимация GFP по порядковым индексам сходится к GFP сама по себе, если начинать от начала сверху, то есть GFP достигается на пределе последовательности ординалов.

LaTeX

$$$ \\mathrm{gfpApprox}(f,\\top,i) \\to f\\mathrm{gfp} \\text{ as } i \\to \\omega $$$

Lean4

/-- The approximation sequence converges at the successor of the domain's cardinality
to the greatest fixed point if starting from `⊥` -/
theorem gfpApprox_ord_eq_gfp : gfpApprox f ⊤ (ord <| succ #α) = f.gfp :=
  lfpApprox_ord_eq_lfp f.dual

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