fromTypes_succ

Mathlib.Logic.Function.FromTypes

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

English

FromTypes for a successor index equals vecHead p → FromTypes (vecTail p) τ.

Русский

FromTypes для перехода к следующему индексу равняется vecHead p → FromTypes (vecTail p) τ.

LaTeX

$$$FromTypes p\tau = (\text{vecHead } p) \to FromTypes (\text{vecTail } p) \tau$$$

Lean4

theorem fromTypes_succ {n} (p : Fin (n + 1) → Type u) (τ : Type u) :
    FromTypes p τ = (vecHead p → FromTypes (vecTail p) τ) :=
  rfl

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

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

Разделы

Аффилиация

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