nth

Mathlib.Data.Vector3

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

English

Let i ∈ Fin2 n and v ∈ Vector3 α n. The i-th element of v is given by nth(i,v) = v(i).

Русский

Пусть i ∈ Fin2 n и v ∈ Vector3 α n. i-й элемент v задаётся как nth(i,v) = v(i).

LaTeX

$$$ \mathrm{nth}(i,v) = v(i). $$$

Lean4

/-- Get the `i`th element of a vector -/
abbrev nth (i : Fin2 n) (v : Vector3 α n) : α :=
  v i

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

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

Разделы

Аффилиация

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