toList_singleton — Mathlib

English

A vector of length 1 corresponds to the single-element list with its head.

Русский

Вектор длины 1 соответствует односоставному списку, содержащему его голову.

LaTeX

$$$\forall v:\mathrm{Vector}\,\alpha\,1,\ v.toList = [v.head]$$$

Lean4

/-- The list that makes up a `Vector` made up of a single element,
retrieved via `toList`, is equal to the list of that single element. -/
@[simp]
theorem toList_singleton (v : Vector α 1) : v.toList = [v.head] :=
  by
  rw [← v.cons_head_tail]
  simp only [toList_cons, toList_nil, head_cons, singleton_tail]

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