drop_append1'

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.drop_append1'

English

The equation drop (append1 α β) = α holds universally, i.e., equality of TypeVecs.

Русский

Уравнение drop (append1 α β) = α справедливо вообще, т.е. равенство TypeVec.

LaTeX

$$drop (append1 α β) = α$$

Lean4

theorem drop_append1' {α : TypeVec n} {β : Type*} : drop (append1 α β) = α :=
  funext fun _ => drop_append1

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

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

Разделы

Аффилиация

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