isEmpty_sum

Mathlib.Logic.IsEmpty

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

English

The sum type α ⊕ β is empty iff α is empty or β is empty.

Русский

Сумма типов α ⊕ β пустая тогда, когда либо α пустой, либо β пустой.

LaTeX

$$IsEmpty(\\Sum\\{\\alpha\\,\\beta\\}) \\leftrightarrow \\IsEmpty(\\alpha) \\lor \\ IsEmpty(\\beta)$$

Lean4

@[simp]
theorem isEmpty_sum {α β} : IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β := by
  simp only [← not_nonempty_iff, nonempty_sum, not_or]

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

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

Разделы

Аффилиация

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