cons_fs

Mathlib.Data.Vector3

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

English

For any a ∈ α and v ∈ Vector3 α n, the tail of cons(a,v) at index fs(i) is v(i); i.e., (a :: v)(fs(i)) = v(i).

Русский

Для любого a ∈ α и v ∈ Vector3 α n хвост cons(a,v) в позиции fs(i) равен v(i); то есть (a :: v)(fs(i)) = v(i).

LaTeX

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

Lean4

@[simp]
theorem cons_fs (a : α) (v : Vector3 α n) (i) : (a :: v) (fs i) = v i :=
  rfl

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

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

Разделы

Аффилиация

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