instIsEmptySum

Mathlib.Logic.IsEmpty

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

English

The sum type α ⊕ β is empty if both α and β are empty.

Русский

Тип суммы α ⊕ β пуст, если оба α и β пусты.

LaTeX

$$$ [IsEmpty \alpha] [IsEmpty \beta] : IsEmpty (\alpha \oplus β) $$$

Lean4

instance instIsEmptySum {α β} [IsEmpty α] [IsEmpty β] : IsEmpty (α ⊕ β) :=
  ⟨fun x ↦ Sum.rec IsEmpty.false IsEmpty.false x⟩

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

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

Разделы

Аффилиация

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