signedDist_triangle

Mathlib.Geometry.Euclidean.SignedDist

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

← MathLib Explorer

English

If ⟪v, q −ᵥ p⟫ = 0 then signedDist v p q = 0.

Русский

Если ⟪v, q −ᵥ p⟫ = 0, то signedDist v p q = 0.

LaTeX

$$$\langle v, q -ᵥ p \rangle = 0 \Rightarrow signedDist(v)\ p q = 0$$$

Lean4

@[simp]
theorem signedDist_triangle : signedDist v p q + signedDist v q r = signedDist v p r :=
  by
  simp only [signedDist_apply_apply]
  rw [add_comm, ← inner_add_right, vsub_add_vsub_cancel]

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

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

Разделы

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

Аффилиация

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