vadd_vsub_vadd_comm — Mathlib

English

The amount of difference when adding different vectors to two points decomposes as the difference of vectors plus the difference of points: (v1 +ᵥ p1) −ᵥ (v2 +ᵥ p2) = (v1 − v2) + (p1 −ᵥ p2).

Русский

Разность двух точек, полученная после добавления разных векторов, равна сумме разности векторов и разности самих точек: (v1 +ᵥ p1) −ᵥ (v2 +ᵥ p2) = (v1 − v2) + (p1 −ᵥ p2).

LaTeX

$$$ (v_1 +ᵥ p_1) -ᵥ (v_2 +ᵥ p_2) = (v_1 - v_2) + (p_1 -ᵥ p_2) $$$

Lean4

theorem vadd_vsub_vadd_comm (v₁ v₂ : G) (p₁ p₂ : P) : (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂) = (v₁ - v₂) + (p₁ -ᵥ p₂) := by
  rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_assoc, ← add_comm_sub]

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