signedDist_smul_of_pos

Mathlib.Geometry.Euclidean.SignedDist

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

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

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

Lean4

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

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

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

Разделы

Аффилиация

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