cons_head_tail — Mathlib

English

Prepending the head of a vector to its tail yields the original vector.

Русский

Префиксация головы вектора к его хвосту восстанавливает исходный вектор.

LaTeX

$$$\\mathrm{cons\\_head\\_tail} : \\forall v : \\text{Vector } α (\\text{succ } n), \\mathrm{cons}(\\mathrm{head}\,v, \\mathrm{tail}\,v) = v$$$

Lean4

/-- Prepending the head of a vector to its tail gives the vector. -/
@[simp]
theorem cons_head_tail : ∀ v : Vector α (succ n), cons (head v) (tail v) = v
  | ⟨[], h⟩ => by contradiction
  | ⟨_ :: _, _⟩ => rfl

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