vsub_sub_vsub_cancel_left — Mathlib

English

Cancellation: p3 −ᵥ p2 − (p3 −ᵥ p1) = p1 −ᵥ p2 for all p1, p2, p3.

Русский

Умножение: для любых p1, p2, p3 выполняется p3 −ᵥ p2 − (p3 −ᵥ p1) = p1 −ᵥ p2.

LaTeX

$$$ p_3 -ᵥ p_2 - (p_3 -ᵥ p_1) = p_1 -ᵥ p_2 $$$

Lean4

/-- Cancellation subtracting the results of two subtractions. -/
@[simp]
theorem vsub_sub_vsub_cancel_left (p₁ p₂ p₃ : P) : p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂ := by
  rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]

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