English
Given a finset l and a predicate p with a unique a ∈ l and p a, the value choose p l hp returns that unique a in the ambient type.
Русский
Пусть дан финсет l и предикат p с существованием единственного элемента a ∈ l, удовлетворяющего p; тогда choose p l hp возвращает этот элемент в исходном типе.
LaTeX
$$$ (hp : \\\\exists! a, a \\\\in l \\\land p a) \\\\Rightarrow \\\\mathrm{choose}(p,l,hp) \\\\in l \\\land p(\\\\mathrm{choose}(p,l,hp)) \\\\land \\\\forall b \\\\in l, p(b) \\\\Rightarrow b = \\\\mathrm{choose}(p,l,hp)$$$
Lean4
/-- Given a finset `l` and a predicate `p`, associate to a proof that there is a unique element of
`l` satisfying `p` this unique element, as an element of the ambient type. -/
def choose (hp : ∃! a, a ∈ l ∧ p a) : α :=
chooseX p l hp
