isEmpty_left

Mathlib.Logic.IsEmpty

URI: https://scilib.ai/kg/mathlib#Prod.isEmpty_left

English

If α is empty, then the product α × β is empty.

Русский

Если α пусто, то произведение α × β пусто.

LaTeX

$$$ [IsEmpty(\alpha)] \Rightarrow IsEmpty( \alpha \times \beta ) $$$

Lean4

instance isEmpty_left {α β} [IsEmpty α] : IsEmpty (α × β) :=
  Function.isEmpty Prod.fst

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

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

Разделы

Аффилиация

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