tail_nil

Mathlib.Data.Vector.Basic

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

English

The tail of the empty vector is empty.

Русский

Хвост пустого вектора равен пустому.

LaTeX

$$$\forall\alpha,\; \mathrm{tail}({\mathrm{nil}}) = {\mathrm{nil}}$$$

Lean4

/-- The `tail` of a `nil` vector is `nil`. -/
@[simp]
theorem tail_nil : (@nil α).tail = nil :=
  rfl

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

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

Разделы

Аффилиация

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