vsub_left_cancel

Mathlib.Algebra.AddTorsor.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

/-- If the same point subtracted from two points produces equal
results, those points are equal. -/
theorem vsub_left_cancel {p₁ p₂ p : P} (h : p₁ -ᵥ p = p₂ -ᵥ p) : p₁ = p₂ := by
  rwa [← sub_eq_zero, vsub_sub_vsub_cancel_right, vsub_eq_zero_iff_eq] at h

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

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

Разделы

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

Аффилиация

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