ofVector_cons

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.ofVector_cons

English

The coercion of Vector.cons corresponds to Sym.cons on the underlying vector.

Русский

Приведение Vector.cons соответствует Sym.cons на базовом векторе.

LaTeX

$$$ \uparrow(\operatorname{Vector.cons}(a,v)) = \mathrm{Sym.cons}(a, \uparrow(v)) $$$

Lean4

@[simp]
theorem ofVector_cons (a : α) (v : List.Vector α n) : ↑(Vector.cons a v) = a ::ₛ (↑v : Sym α n) :=
  by
  cases v
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru