arrowPUnitOfIsEmpty — Mathlib

English

If α is empty, then maps α → β are equivalent to PUnit.

Русский

Если α пусто, то отображения α → β эквивалентны PUnit.

LaTeX

$$$ (\alpha \to \beta) \simeq PUnit \quad [\mathrm{IsEmpty}(\alpha)] $$$

Lean4

/-- The sort of maps from a type that `IsEmpty` is equivalent to `PUnit`. -/
def arrowPUnitOfIsEmpty (α β : Sort*) [IsEmpty α] : (α → β) ≃ PUnit.{u}
    where
  toFun _ := PUnit.unit
  invFun _ := isEmptyElim
  left_inv _ := funext isEmptyElim

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