English
For an affine subspace s with an orthogonal projection, the signed infimum distance from a point p to s is the signed distance from p − v to any fixed point in s, where v is the projection of p onto s.
Русский
Для аффинного подпространства s с ортогональной проекцией расстояние signedInfDist(p) до s равно signedDist(p −ᵥ Proj_s(p), q) для любого фиксированного q ∈ s, где q задаётся как представитель s.
LaTeX
$$$s.signedInfDist(p) = \operatorname{signedDist}(p -\!\vec{\mathrm{Proj}}_s(p), \uparrow(\mathrm{Classical.ofNonempty}: s))$$$
Lean4
theorem signedInfDist_def :
s.signedInfDist p = signedDist (p -ᵥ orthogonalProjection s p) ↑(Classical.ofNonempty : s) :=
rfl