signedDist_eq_zero_of_orthogonal

Mathlib.Geometry.Euclidean.SignedDist

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

English

If ⟪v, q −ᵥ p⟫ = 0 then signedDist v p q = 0.

Русский

Если ⟪v, q −ᵥ p⟫ = 0, то signedDist v p q = 0.

LaTeX

$$⟨v, q -ᵥ p⟫ = 0 ⇒ signedDist v p q = 0$$

Lean4

theorem signedDist_eq_zero_of_orthogonal (h : ⟪v, q -ᵥ p⟫ = 0) : signedDist v p q = 0 := by
  simpa using signedDist_right_congr p h

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

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

Разделы

Аффилиация

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