nil

Mathlib.Data.Vector3

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

English

nil is the empty vector in Vector3 α 0, defined as the empty function.

Русский

nil является пустым вектором в Vector3 α 0 и задаётся как пустая функция.

LaTeX

$$$\text{nil} : \mathrm{Vector3}(\alpha,0)\quad\text{is the empty function}$$$

Lean4

/-- The empty vector -/
@[match_pattern]
def nil : Vector3 α 0 :=
  nofun

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

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

Разделы

Аффилиация

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