append_left — Mathlib

English

Reiterates that head and tail reconstruct the vector: head(v) :: tail(v) = v.

Русский

Повторяет, что голова и хвост восстанавливают вектор: head(v) :: tail(v) = v.

LaTeX

$$$ \mathrm{Vector3.cons}( \mathrm{head}(v), \mathrm{tail}(v) ) = v. $$$

Lean4

@[simp]
theorem append_left : ∀ {m} (i : Fin2 m) (v : Vector3 α m) {n} (w : Vector3 α n), (v +-+ w) (left n i) = v i
  | _, @fz m, v, _, _ => v.consElim fun a _t => by simp [*, left]
  | _, @fs m i, v, n, w => v.consElim fun _a t => by simp [append_left, left]

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