signedDist_vadd_right_swap

Mathlib.Geometry.Euclidean.SignedDist

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

English

Similarly, signedDist v p (w +ᵥ q) = signedDist v (−w +ᵥ p) q.

Русский

Аналогично: signedDist v p (w +ᵥ q) = signedDist v (−w +ᵥ p) q.

LaTeX

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

Lean4

theorem signedDist_vadd_right_swap : signedDist v p (w +ᵥ q) = signedDist v (-w +ᵥ p) q := by
  rw [signedDist_vadd_left_swap, neg_neg]

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

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

Разделы

Аффилиация

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