choose_spec

Mathlib.Data.Fintype.Inv

URI: https://scilib.ai/kg/mathlib#Fintype.choose_spec

English

If hp := exists unique, then p (choose p hp) holds.

Русский

Если hp задано как существование единственного элемента, то p(choose p hp) истинно.

LaTeX

$$$\\forall p\\, (\\exists! a, p(a))\\Rightarrow p(\\text{choose } p \\! hp)$$$

Lean4

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

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

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

Разделы

Аффилиация

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