fromTypes_zero_equiv

Mathlib.Logic.Function.FromTypes

URI: https://scilib.ai/kg/mathlib#Function.fromTypes_zero_equiv

← MathLib Explorer

English

FromTypes p τ is equivalent to τ when p is empty.

Русский

FromTypes p τ эквивалентно τ, если p пусто.

LaTeX

$$$FromTypes p\tau \simeq \tau$$$

Lean4

/-- The definitional equality between `0`-ary heterogeneous functions into `τ` and `τ`. -/
@[simps!]
def fromTypes_zero_equiv (p : Fin 0 → Type u) (τ : Type u) : FromTypes p τ ≃ τ :=
  Equiv.refl _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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