English
There exist distinct ordinals a and b below the successor of the domain's cardinality such that a ≠ b and the GFP approximations at a and b are equal.
Русский
Существуют различные ординалы a и b, меньшие чем succ#α, такие что a ≠ b и аппроксимации GFP в a и в b равны.
LaTeX
$$$ \\exists a,b < \\operatorname{succ}(\\lvert \\alpha \\rvert) , a \\neq b \\wedge \\mathrm{gfpApprox} f x a = \\mathrm{gfpApprox} f x b $$$
Lean4
/-- The approximations of the least fixed point stabilize at a fixed point of `f` -/
theorem lfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : x ≤ f x) (h_ab : a ≤ b)
(h : lfpApprox f x a ∈ fixedPoints f) : lfpApprox f x b = lfpApprox f x a :=
by
rw [mem_fixedPoints_iff] at h
induction b using Ordinal.induction with
| h b IH =>
apply le_antisymm
· conv => left; rw [lfpApprox]
apply sSup_le
simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, forall_eq_or_imp,
forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
apply And.intro (le_lfpApprox f x)
intro a' ha'b
by_cases haa : a' < a
· rw [← lfpApprox_add_one f x h_init]
apply lfpApprox_monotone
simp only [Ordinal.add_one_eq_succ, succ_le_iff]
exact haa
· rw [IH a' ha'b (le_of_not_gt haa), h]
· exact lfpApprox_monotone f x h_ab
