eq — Mathlib · SciLib

English

A vector is determined by its underlying list: if toList a1 = toList a2, then a1 = a2.

Русский

Вектор определяется по базовому списку: если toList a1 = toList a2, то a1 = a2.

LaTeX

$$$\\forall a_1,a_2:\\text{Vector }\\alpha n,\\ (toList\\ a_1 = toList\\ a_2)\\rightarrow a_1 = a_2$$$

Lean4

/-- Vector is determined by the underlying list. -/
protected theorem eq {n : ℕ} : ∀ a1 a2 : Vector α n, toList a1 = toList a2 → a1 = a2
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

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