exists_gfpApprox_eq_gfpApprox — Mathlib

English

There exist two distinct ordinals a,b below succ #α with a ≠ b such that gfpApprox at a equals gfpApprox at b.

Русский

Существуют два различных ординала a,b ниже succ #α, такие что gfpApprox в a равно gfpApprox в b.

LaTeX

$$$ \\exists a < \\operatorname{succ}(\\lvert \\alpha \\rvert), \\exists 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_gfpApprox_eq_gfpApprox :
    ∃ a < ord <| succ #α, ∃ b < ord <| succ #α, a ≠ b ∧ gfpApprox f x a = gfpApprox f x b :=
  exists_lfpApprox_eq_lfpApprox f.dual x

Похожие утверждения