eq_vadd_iff_vsub_eq — Mathlib

English

The equation p1 = g +ᵥ p2 is equivalent to p1 -ᵥ p2 = g.

Русский

Уравнение p1 = g +ᵥ p2 эквивалентно p1 -ᵥ p2 = g.

LaTeX

$$$p_1 = g +ᵥ p_2 \iff p_1 -ᵥ p_2 = g$$$

Lean4

/-- Convert between an equality with adding a group element to a point
and an equality of a subtraction of two points with a group
element. -/
theorem eq_vadd_iff_vsub_eq (p₁ : P) (g : G) (p₂ : P) : p₁ = g +ᵥ p₂ ↔ p₁ -ᵥ p₂ = g :=
  ⟨fun h => h.symm ▸ vadd_vsub _ _, fun h => h ▸ (vsub_vadd _ _).symm⟩

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