English
The GFP approximation sequence converges at the successor of the domain's cardinality to the least fixed point when starting from bottom.
Русский
Аппроксимационная последовательность GFP сходится к наименьшей фиксированной точке при индексе succ Cardinal.mk α, начиная с нуля.
LaTeX
$$$ \\mathrm{lfpApprox}\\ f\\ x\\ (\\operatorname{ord}(\\operatorname{succ}(\\lvert \\alpha \\rvert)).\\ord) = \\mathrm{lfp}(f) $$$
Lean4
/-- The approximation sequence converges at the successor of the domain's cardinality
to the least fixed point if starting from `⊥` -/
theorem lfpApprox_ord_eq_lfp : lfpApprox f ⊥ (ord <| succ #α) = f.lfp :=
by
apply le_antisymm
· have h_lfp : ∃ y : fixedPoints f, f.lfp = y := by use ⊥; exact rfl
let ⟨y, h_y⟩ := h_lfp; rw [h_y]
exact lfpApprox_le_of_mem_fixedPoints f ⊥ y.2 bot_le (ord <| succ #α)
· have h_fix : ∃ y : fixedPoints f, lfpApprox f ⊥ (ord <| succ #α) = y := by
simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
lfpApprox_ord_mem_fixedPoint f ⊥ bot_le
let ⟨x, h_x⟩ := h_fix; rw [h_x]
exact lfp_le_fixed f x.prop
