eq_nil

Mathlib.Data.Vector.Defs

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

← MathLib Explorer

English

A vector of length 0 is equal to nil: for v : Vector α 0, v = nil.

Русский

Вектор нулевой длины равен nil: для v : Vector α 0, v = nil.

LaTeX

$$$\\forall v:\\text{Vector}(\\alpha,0),\\ v=\\text{nil}$$$

Lean4

/-- A vector of length `0` is a `nil` vector. -/
protected theorem eq_nil (v : Vector α 0) : v = nil :=
  v.eq nil (List.eq_nil_of_length_eq_zero v.2)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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