vsub_sub_vsub_comm — Mathlib

English

For all p1, p2, p3, p4 ∈ P, p1 −ᵥ p2 − (p3 −ᵥ p4) = p1 −ᵥ p3 − (p2 −ᵥ p4).

Русский

Для любых p1, p2, p3, p4 ∈ P выполняется p1 −ᵥ p2 − (p3 −ᵥ p4) = p1 −ᵥ p3 − (p2 −ᵥ p4).

LaTeX

$$$ p_1 -_{\!v} p_2 - (p_3 -_{\!v} p_4) = p_1 -_{\!v} p_3 - (p_2 -_{\!v} p_4) $$$

Lean4

theorem vsub_sub_vsub_comm (p₁ p₂ p₃ p₄ : P) : p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄) := by
  rw [← vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub]

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