tail

Mathlib.Data.Vector3

URI: https://scilib.ai/kg/mathlib#Vector3.tail

English

For v ∈ Vector3 α (n+1), tail(v) is the vector of length n with tail(v)(i) = v(fs(i)).

Русский

Для v ∈ Vector3 α (n+1) хвостом является вектор длины n с tail(v)(i) = v(fs(i)).

LaTeX

$$$ \mathrm{tail}(v)(i) = v(\mathrm{fs}(i)). $$$

Lean4

/-- Get the tail of a nonempty vector. -/
def tail (v : Vector3 α (n + 1)) : Vector3 α n := fun i => v (fs i)

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

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

Разделы

Аффилиация

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