choice_eq_none

Mathlib.Data.Option.Basic

URI: https://scilib.ai/kg/mathlib#Option.choice_eq_none

English

If α is an empty type, then the canonical choice value for α is none.

Русский

Пусть α пустого типа. Тогда элемент выбора α равен none.

LaTeX

$$$ [IsEmpty \alpha] \Rightarrow \mathrm{choice}(\alpha) = \mathrm{none}$$$

Lean4

theorem choice_eq_none (α : Type*) [IsEmpty α] : choice α = none :=
  dif_neg (not_nonempty_iff_imp_false.mpr isEmptyElim)

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

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

Разделы

Аффилиация

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