emptyProd

Mathlib.Logic.Equiv.Prod

URI: https://scilib.ai/kg/mathlib#Equiv.emptyProd

English

Let α be any type. The product Empty × α is canonically equivalent to Empty.

Русский

Пусть α — произвольный тип. Произведение Empty × α эквивалентно Empty канонически.

LaTeX

$$$Empty \times \alpha \cong Empty$$$

Lean4

/-- `Empty` type is a left absorbing element for type product up to an equivalence. -/
def emptyProd (α) : Empty × α ≃ Empty :=
  equivEmpty _

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

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

Разделы

Аффилиация

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