signedDist_anticomm

Mathlib.Geometry.Euclidean.SignedDist

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

English

The signed distance anticommutes with swapping arguments: -signedDist v p q = signedDist v q p.

Русский

SignedDist антикомутивно меняется при перестановке аргументов: -signedDist v p q = signedDist v q p.

LaTeX

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

Lean4

@[simp]
theorem signedDist_anticomm : -signedDist v p q = signedDist v q p := by
  simp [signedDist_apply_apply, ← inner_neg_right]

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

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

Разделы

Аффилиация

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