singleton_tail

Mathlib.Data.Vector.Basic

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

← MathLib Explorer

English

The tail of a vector of length 1 is empty.

Русский

Хвост вектора длины 1 равен пустому.

LaTeX

$$$\forall v:\mathrm{Vector}\,\alpha\,1,\; v.tail = \mathrm{Vector}.nil$$$

Lean4

/-- The `tail` of a vector made up of one element is `nil`. -/
@[simp]
theorem singleton_tail : ∀ (v : Vector α 1), v.tail = Vector.nil
  | ⟨[_], _⟩ => rfl

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

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

Разделы

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

Аффилиация

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