choose_spec — Mathlib

English

If there exists a unique element a of the multiset l such that a ∈ l and p a, then the chosen element and its property hold: the chosen element belongs to l and satisfies p.

Русский

Если существует единственный элемент a мультимножества l such that a ∈ l и p a, то выбранный элемент удовлетворяет условию: он принадлежит l и имеет свойство p.

LaTeX

$$$\\exists! a, a \\in l \\land p(a) \\implies p(\\operatorname{choose} p l (hp))$$$

Lean4

theorem choose_spec (hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp) :=
  (chooseX p l hp).property

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