trueArrowEquiv

Mathlib.Logic.Equiv.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

/-- The sort of maps from `True` is equivalent to the codomain. -/
def trueArrowEquiv (α : Sort*) : (True → α) ≃ α :=
  funUnique _ _

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

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

Разделы

Аффилиация

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