fromTypes_cons

Mathlib.Logic.Function.FromTypes

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

← MathLib Explorer

English

FromTypes(vecCons α p) τ equals α → FromTypes p τ.

Русский

FromTypes(vecCons α p) τ равно α → FromTypes p τ.

LaTeX

$$$FromTypes(\text{vecCons } α\ p)\; τ = α \to FromTypes p \tau$$$

Lean4

theorem fromTypes_cons {n} (α : Type u) (p : Fin n → Type u) (τ : Type u) :
    FromTypes (vecCons α p) τ = (α → FromTypes p τ) :=
  fromTypes_succ _ τ

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

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

Разделы

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

Аффилиация

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