instIsEmptyPSum

Mathlib.Logic.IsEmpty

URI: https://scilib.ai/kg/mathlib#instIsEmptyPSum

English

The PSum of empty types is empty if each component is empty.

Русский

PSum пустых типов пуст, если каждый компонент пуст.

LaTeX

$$$ \forall {\alpha}, {\beta} [IsEmpty(\alpha)] [IsEmpty(\beta)] : IsEmpty(PSum(\alpha, \beta)) $$$

Lean4

instance [IsEmpty α] [IsEmpty β] : IsEmpty (α ⊕' β) :=
  ⟨fun x ↦ PSum.rec IsEmpty.false IsEmpty.false x⟩

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

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

Разделы

Аффилиация

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