English
Given a finite type α and a predicate p with a unique element satisfying p, there exists a canonical element of the subtype {a ∈ α | p a} witnessing this uniqueness.
Русский
Для конечного типа α и предиката p, для которого существует ровно один элемент с p, существует канонический элемент подтипа {a ∈ α | p a}, доказывающий уникальность.
LaTeX
$$$\\exists! a: α, p(a) \\Rightarrow \\exists! (a, ha) : { a // p(a) }$$
Lean4
/-- Given a fintype `α` and a predicate `p`, associate to a proof that there is a unique element of
`α` satisfying `p` this unique element, as an element of the corresponding subtype. -/
def chooseX (hp : ∃! a : α, p a) : { a // p a } :=
⟨Finset.choose p univ (by simpa), Finset.choose_property _ _ _⟩
