English
The lfpApprox at the successor of the domain's cardinality is a fixed point of f; i.e., it belongs to fixedPoints f.
Русский
Аппроксимация lfp в индексе succ(Card α) является точкой фиксированности функции f.
LaTeX
$$$ \\mathrm{lfpApprox} f x (\\operatorname{ord}(\\operatorname{succ}(\\lvert \\alpha \\rvert))) \\in \\mathrm{fixedPoints}\, f $$$
Lean4
/-- The approximation at the index of the successor of the domain's cardinality is a fixed point -/
theorem lfpApprox_ord_mem_fixedPoint (h_init : x ≤ f x) : lfpApprox f x (ord <| succ #α) ∈ fixedPoints f :=
by
let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := exists_lfpApprox_eq_lfpApprox f x
cases le_total a b with
| inl h_ab => exact lfpApprox_mem_fixedPoints_of_eq f x h_init (h_nab.lt_of_le h_ab) (le_of_lt h_a) h_fab
| inr h_ba => exact lfpApprox_mem_fixedPoints_of_eq f x h_init (h_nab.symm.lt_of_le h_ba) (le_of_lt h_b) (h_fab.symm)
