fromTypes_nil_equiv

Mathlib.Logic.Function.FromTypes

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

← MathLib Explorer

English

FromTypes vecEmpty τ ≃ τ.

Русский

FromTypes vecEmpty τ эквивалентно τ.

LaTeX

$$$FromTypes(\text{vecEmpty})\tau \simeq \tau$$$

Lean4

/-- The definitional equality between `![]`-ary heterogeneous functions into `τ` and `τ`. -/
@[simps!]
def fromTypes_nil_equiv (τ : Type u) : FromTypes ![] τ ≃ τ :=
  fromTypes_zero_equiv ![] τ

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

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

Разделы

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

Аффилиация

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