arrowPUnitEquivPUnit — Mathlib

English

If α has a unique element, then the space of dependent functions (∀ i, β i) is equivalent to β at the unique element.

Русский

Если у α есть единственный элемент, то пространство зависимых функций (∀ i, β i) эквивалентно β на этом уникальном элементе.

LaTeX

$$$ (\forall i:\alpha, \beta(i)) \simeq \beta(\ast) \quad [\text{Unique } \alpha] $$$

Lean4

/-- The sort of maps to `PUnit.{v}` is equivalent to `PUnit.{w}`. -/
def arrowPUnitEquivPUnit (α : Sort*) : (α → PUnit.{v}) ≃ PUnit.{w}
    where
  toFun _ := .unit
  invFun _ _ := .unit

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