choose_spec

Mathlib.Logic.Encodable.Basic

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

English

If ∃ x, p x, then p (choose h).

Русский

Если существует x с p x, то выбраный элемент удовлетворяет p.

LaTeX

$$$ p(\mathrm{choose}(h)) $$$

Lean4

theorem choose_spec (h : ∃ x, p x) : p (choose h) :=
  (chooseX h).2

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

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

Разделы

Аффилиация

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