signedDist_vadd_vadd

Mathlib.Geometry.Euclidean.SignedDist

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

English

For all v,w,p,q, signedDist v (w + p) (w + q) = signedDist v p q.

Русский

Для всех v,w,p,q выполняется: signedDist v (w + p) (w + q) = signedDist v p q.

LaTeX

$$signedDist v (w+ p) (w+ q) = signedDist v p q$$

Lean4

theorem signedDist_vadd_vadd : signedDist v (w +ᵥ p) (w +ᵥ q) = signedDist v p q := by
  rw [signedDist_vadd_left_swap, neg_vadd_vadd]

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

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

Разделы

Аффилиация

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