Vector3

Mathlib.Data.Vector3

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

English

Vector3 α n is defined as the type Fin2 n → α, i.e., a vector of length n is a function on Fin2 n.

Русский

Vector3 α n задаётся как тип Fin2 n → α, то есть вектор длины n — функция на Fin2 n.

LaTeX

$$$\mathrm{Vector3}(\alpha,n) = \mathrm{Fin2}(n) \to \alpha$$$

Lean4

/-- Alternate definition of `Vector` based on `Fin2`. -/
def Vector3 (α : Type u) (n : ℕ) : Type u :=
  Fin2 n → α

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

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

Разделы

Аффилиация

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