signedInfDist_eq_signedDist_of_mem

English

If q lies in s, then the signed infimum distance from p to q equals the signed distance from p − Proj_s(p) to q.

Русский

Пусть q ∈ s. Тогда s.signedInfDist(p) = signedDist(p − Proj_s(p), q).

LaTeX

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

Lean4

theorem signedInfDist_eq_signedDist_of_mem (h : q ∈ s) :
    s.signedInfDist p = signedDist (p -ᵥ orthogonalProjection s p) q :=
  by
  apply signedDist_left_congr
  apply s.direction.inner_left_of_mem_orthogonal
  · exact vsub_mem_direction (SetLike.coe_mem _) h
  · exact vsub_orthogonalProjection_mem_direction_orthogonal s p

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