signedDist_smul_of_neg

Mathlib.Geometry.Euclidean.SignedDist

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

English

If r < 0, then signedDist (r • v) p q = - signedDist v p q.

Русский

Если r < 0, то signedDist (r • v) p q = - signedDist v p q.

LaTeX

$$$r<0 \Rightarrow signedDist(r\cdot v)\ p\ q = -\, signedDist(v)\ p\ q$$$

Lean4

theorem signedDist_smul_of_neg {r : ℝ} (h : r < 0) : signedDist (r • v) p q = -signedDist v p q := by
  simp [signedDist_smul, h]

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

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

Разделы

Аффилиация

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