appendFun_aux

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.appendFun_aux

Lean4

theorem appendFun_aux {α α' : TypeVec n} {β β' : Type*} (f : (α ::: β) ⟹ (α' ::: β')) : (dropFun f ::: lastFun f) = f :=
  eq_of_drop_last_eq rfl rfl

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

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

Разделы

Аффилиация

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