English
If a and b are indices with a < b and lfpApprox at a equals lfpApprox at b, then all later indices c ≥ b satisfy lfpApprox at c = lfpApprox at b, i.e., stabilization occurs at that value.
Русский
Если a < b и lfpApprox(f,x,a) = lfpApprox(f,x,b), то для всех c ≥ b выполняется lfpApprox(f,x,c) = lfpApprox(f,x,b), то есть наступает стабилизация в этом значении.
LaTeX
$$$ a < b \\wedge \\mathrm{lfpApprox}(f,x,a) = \\mathrm{lfpApprox}(f,x,b) \\Rightarrow \\forall c (b \\le c), \\mathrm{lfpApprox}(f,x,c) = \\mathrm{lfpApprox}(f,x,b) $$$
Lean4
/-- If the sequence of ordinal-indexed approximations takes a value twice,
then it actually stabilised at that value. -/
theorem lfpApprox_mem_fixedPoints_of_eq {a b c : Ordinal} (h_init : x ≤ f x) (h_ab : a < b) (h_ac : a ≤ c)
(h_fab : lfpApprox f x a = lfpApprox f x b) : lfpApprox f x c ∈ fixedPoints f :=
by
have lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints f :=
by
rw [mem_fixedPoints_iff, ← lfpApprox_add_one f x h_init]
exact Monotone.eq_of_ge_of_le (lfpApprox_monotone f x) h_fab (SuccOrder.le_succ a) (SuccOrder.succ_le_of_lt h_ab)
rw [lfpApprox_eq_of_mem_fixedPoints f x h_init]
· exact lfpApprox_mem_fixedPoint
· exact h_ac
· exact lfpApprox_mem_fixedPoint
