vadd_eq_vadd_iff_sub_eq_vsub — Mathlib

English

Let v1, v2 ∈ G and p1, p2 ∈ P. Then v1 +ᵥ p1 = v2 +ᵥ p2 if and only if v2 − v1 = p1 −ᵥ p2.

Русский

Пусть v1, v2 ∈ G и p1, p2 ∈ P. Тогда v1 +ᵥ p1 = v2 +ᵥ p2 тогда и только тогда, когда v2 − v1 = p1 −ᵥ p2.

LaTeX

$$$ (v_1 +_{\!v} p_1) = (v_2 +_{\!v} p_2) \\iff v_2 - v_1 = p_1 -_{\!v} p_2 $$$

Lean4

theorem vadd_eq_vadd_iff_sub_eq_vsub {v₁ v₂ : G} {p₁ p₂ : P} : v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂ := by
  rw [vadd_eq_vadd_iff_neg_add_eq_vsub, neg_add_eq_sub]

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