punitArrowEquiv

Mathlib.Logic.Equiv.Defs

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

English

There is a natural equivalence between maps from PUnit to α and α itself:

Русский

Существует естественная эквивалентность между отображениями PUnit → α и α.

LaTeX

$$$ (\mathrm{PUnit} \to \alpha) \simeq \alpha $$$

Lean4

/-- The sort of maps from `PUnit` is equivalent to the codomain. -/
def punitArrowEquiv (α : Sort*) : (PUnit.{u} → α) ≃ α :=
  funUnique PUnit.{u} α

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

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

Разделы

Аффилиация

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