English
There exist indices a and b below the successor of the domain's cardinality such that a ≠ b and the fixed-point approximations gfpApprox at a and b are equal.
Русский
Существуют индексы a и b ниже succ#α, такие что a ≠ b и значения gfpApprox(f,x,a) и gfpApprox(f,x,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
/-- There are distinct indices smaller than the successor of the domain's cardinality
yielding the same value -/
theorem exists_lfpApprox_eq_lfpApprox :
∃ a < ord <| succ #α, ∃ b < ord <| succ #α, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b :=
by
have h_ninj := not_injective_limitation_set <| lfpApprox f x
rw [Set.injOn_iff_injective, Function.not_injective_iff] at h_ninj
let ⟨a, b, h_fab, h_nab⟩ := h_ninj
use a.val; apply And.intro a.prop
use b.val; apply And.intro b.prop
apply And.intro
· intro h_eq; rw [Subtype.coe_inj] at h_eq; exact h_nab h_eq
· exact h_fab
