choose_property

Mathlib.Data.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.choose_property

English

If hp asserts uniqueness, then p holds for the chosen element.

Русский

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

LaTeX

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

Lean4

theorem choose_property (hp : ∃! a, a ∈ l ∧ p a) : p (choose p l hp) :=
  (choose_spec _ _ _).2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru