drop

Mathlib.Data.TypeVec

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

English

drop keeps only the first n coordinates of an (n+1)-tuple: (drop α)(i) = α(i.fs).

Русский

drop сохраняет только первые n координат (n+1)-кортежа: (drop α)(i) = α(i.fs).

LaTeX

$$ (TypeVec.drop α) i = α i.fs $$

Lean4

/-- retain only a `n-length` prefix of the argument -/
def drop (α : TypeVec.{u} (n + 1)) : TypeVec n := fun i => α i.fs

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

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

Разделы

Аффилиация

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