English
Let p and q be points in a Euclidean space. The signed distance determined by the displacement from q to p, evaluated at the pair (p, q), is the negative of the ordinary distance between p and q. In particular, reversing the orientation from q to p flips the sign of the distance.
Русский
Пусть p и q — точки в евклидовом пространстве. Подписанное расстояние, заданное вектором смещения p−q и в точках p, q, равно отрицательному расстоянию между p и q. Иначе говоря, ориентирование противоположно меняет знак расстояния.
LaTeX
$$$\operatorname{signedDist}(p - q)\, p\, q = -\operatorname{dist}(p,q)$$$
Lean4
@[simp]
theorem signedDist_vsub_self_rev : signedDist (p -ᵥ q) p q = -dist p q :=
by
rw [← neg_eq_iff_eq_neg, ← signedDist_neg, neg_vsub_eq_vsub_rev]
apply signedDist_vsub_self
