prodEmpty — Mathlib

English

The Empty type acts as a right absorbing element for type products: α × Empty ≃ Empty.

Русский

Тип Empty служит правым абсорбирующим элементом для декартова произведения: α × Empty ≃ Empty.

LaTeX

$$$$ \\alpha \\times \\mathrm{Empty} \\simeq \\mathrm{Empty}. $$$$

Lean4

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

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