constVAdd_add — Mathlib

English

For vectors v and w in the modeling space, translating by v+w is the same as translating by w then by v.

Русский

Для векторов v и w в линейном пространстве, перенос на v+w равен по сути переносу на w затем на v.

LaTeX

$$$T_{v+w} = T_w \circ T_v$, where $T_v$ denotes translation by $v$.$$

Lean4

@[simp]
theorem constVAdd_add (v w : V₁) : constVAdd k P₁ (v + w) = (constVAdd k P₁ w).trans (constVAdd k P₁ v) :=
  ext <| add_vadd _ _

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