mk_toList — Mathlib

English

Converting a vector to a list and back with a suitable witness recovers the original vector.

Русский

Преобразование вектора в список и обратно с корректной записью восстанавливают исходный вектор.

LaTeX

$$$\\forall v : Vector(\\alpha,n),\\forall h,\\langle \\mathrm{toList}(v), h \\rangle = v$$$

Lean4

@[simp]
theorem mk_toList : ∀ (v : Vector α n) (h), (⟨toList v, h⟩ : Vector α n) = v
  | ⟨_, _⟩, _ => rfl

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