vsub_right_cancel

Mathlib.Algebra.AddTorsor.Basic

URI: https://scilib.ai/kg/mathlib#vsub_right_cancel

← MathLib Explorer

English

If p −ᵥ p1 = p −ᵥ p2, then p1 = p2.

Русский

Если p −ᵥ p1 = p −ᵥ p2, то p1 = p2.

LaTeX

$$$ p -ᵥ p_1 = p -ᵥ p_2 \Rightarrow p_1 = p_2 $$$

Lean4

/-- If subtracting two points from the same point produces equal
results, those points are equal. -/
theorem vsub_right_cancel {p₁ p₂ p : P} (h : p -ᵥ p₁ = p -ᵥ p₂) : p₁ = p₂ :=
  by
  refine vadd_left_cancel (p -ᵥ p₂) ?_
  rw [vsub_vadd, ← h, vsub_vadd]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru