English
Let p1, p2 be points in a normed affine space and c be a scalar from 𝕜. The distance from p2 to the point on the line through p1 and p2 given by the lineMap p1 p2 c equals the distance between p1 and p2 scaled by |1 − c|, i.e., nndist(p2, lineMap(p1, p2, c)) = |1 − c|_+ · nndist(p1, p2).
Русский
Пусть p1, p2 — точки в нормированном аффинном пространстве, и c — скаляр из 𝕜. Расстояние от p2 до точки на прямой через p1 и p2, заданной lineMap p1 p2 c, равно расстоянию между p1 и p2, умноженному на |1 − c|_+.
LaTeX
$$$nndist\,p_2\; (\text{lineMap}\; p_1\; p_2\; c) = ‖1 - c‖_+ \cdot nndist\,p_1\, p_2$$$
Lean4
@[simp]
theorem nndist_right_lineMap (p₁ p₂ : P) (c : 𝕜) : nndist p₂ (lineMap p₁ p₂ c) = ‖1 - c‖₊ * nndist p₁ p₂ :=
NNReal.eq <| dist_right_lineMap _ _ _
