signedInfDist_eq_signedDist_orthogonalProjection

English

For any x, the signed infimum distance from p to x equals the signed distance between p − Proj_s(p) and Proj_s(x) evaluated at x.

Русский

Для любого x: s.signedInfDist(p, x) = signedDist(p − Proj_s(p), Proj_s(x)) в точке x.

LaTeX

$$$s.signedInfDist(p,x) = \operatorname{signedDist}(p -\!\mathrm{orthogonalProjection}_s(p), \uparrow(\mathrm{orthogonalProjection}_s(x))) x$$$

Lean4

theorem signedInfDist_eq_signedDist_orthogonalProjection {x : P} :
    s.signedInfDist p x = signedDist (p -ᵥ orthogonalProjection s p) (↑(orthogonalProjection s x)) x := by
  rw [signedInfDist_eq_signedDist_of_mem (orthogonalProjection_mem x)]

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