exists_eq_cons — Mathlib

English

Every nonempty vector v of length n+1 can be written as a head a followed by a vector as of length n.

Русский

Каждый не пустой вектор v длины n+1 можно записать как голова a и вектор as длины n: v = a ::ᵥ as.

LaTeX

$$$\\exists a : \\alpha, \\exists as : Vector(\\alpha, n),\\ v = a ::ᵥ as$$$

Lean4

theorem exists_eq_cons (v : Vector α n.succ) : ∃ (a : α) (as : Vector α n), v = a ::ᵥ as :=
  ⟨v.head, v.tail, (eq_cons_iff v.head v v.tail).2 ⟨rfl, rfl⟩⟩

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