signedDist_neg

Mathlib.Geometry.Euclidean.SignedDist

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

English

For any v ∈ V, signedDist (-v) p q = - signedDist v p q.

Русский

Для любого v ∈ V, signedDist (-v) p q = - signedDist v p q.

LaTeX

$$$signedDist(-v)\ p\ q = -\, signedDist(v)\ p\ q$$$

Lean4

@[simp]
theorem signedDist_neg : signedDist (-v) p q = -signedDist v p q := by simpa using signedDist_smul v p q (-1)

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

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

Разделы

Аффилиация

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