English
Given a finset l and a predicate p with a unique element of l satisfying p, this unique element is produced as an element of the corresponding subtype.
Русский
Дано финсет l и предикат p, задано единственное в l элемент, удовлетворяющий p; этот элемент получается как элемент соответствующего подтипа.
LaTeX
$$$ (hp : \\\\exists! a, a \\\\in l \\\land p a) \\\\Rightarrow \\\\mathrm{chooseX}(p,l,hp) \\\\in \\\\{ a \\\\mid a \\\\in l \\\land p a \}$$$
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 corresponding subtype. -/
def chooseX (hp : ∃! a, a ∈ l ∧ p a) : { a // a ∈ l ∧ p a } :=
Multiset.chooseX p l.val hp
