nil

Mathlib.Data.Vector.Defs

URI: https://scilib.ai/kg/mathlib#List.Vector.nil

English

The empty vector of length 0 is the pair consisting of the empty list and a proof that its length is 0.

Русский

Пустой вектор длины 0 равен паре пустого списка и доказательства длины 0.

LaTeX

$$$\\text{nil} : \\text{Vector } α 0 = \\langle [] , \\mathrm{rfl} \\rangle$$$

Lean4

/-- The empty vector with elements of type `α` -/
@[match_pattern]
def nil : Vector α 0 :=
  ⟨[], rfl⟩

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

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

Разделы

Аффилиация

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