append_cons

Mathlib.Data.Vector3

URI: https://scilib.ai/kg/mathlib#Vector3.append_cons

English

Appending a cons with w preserves the front element: (a :: v) +-+ w = a :: (v +-+ w).

Русский

При объединении cons с w сохраняется первый элемент: (a :: v) +-+ w = a :: (v +-+ w).

LaTeX

$$$ (a :: v) \,+-+ w = a :: (v \,+-+ w). $$$

Lean4

@[simp]
theorem append_cons (a : α) (v : Vector3 α m) (w : Vector3 α n) : (a :: v) +-+ w = a :: v +-+ w :=
  rfl

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

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

Разделы

Аффилиация

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