choose_spec — Mathlib

English

If hp asserts uniqueness, then the chosen element lies in the set and satisfies p.

Русский

Пусть hp утверждает единственность; тогда выбранный элемент принадлежит множеству и удовлетворяет p.

LaTeX

$$$ (hp : \\\\exists! a, a \\\\in l \\\land p a) : \\\\mathrm{choose} p l hp \\\\in l \\\land p(\\\\mathrm{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

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