signedInfDist_apply_self — Mathlib

English

The signedInfDist of p to itself equals the distance from p to its projection onto s.

Русский

СsignedInfDist(p) при аргументе p совпадает с расстоянием от p до проекции p на s.

LaTeX

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

Lean4

@[simp]
theorem signedInfDist_apply_self : s.signedInfDist p p = ‖p -ᵥ orthogonalProjection s p‖ := by
  rw [signedInfDist_eq_signedDist_orthogonalProjection, signedDist_vsub_self, dist_eq_norm_vsub']

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