signedInfDist_def — Mathlib

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

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