dist_orthogonalProjection_eq_zero_iff

English

The distance from a point to its orthogonal projection equals the distance to the subspace as given by InfDist.

Русский

Расстояние от точки до её ортогональной проекции равно расстоянию до подпроекта, заданному InfDist.

LaTeX

$$$ \operatorname{dist} p (\operatorname{orthogonalProjection} s p) = \operatorname{infDist} p s $$$

Lean4

/-- The distance to a point's orthogonal projection is 0 iff it lies in the subspace. -/
theorem dist_orthogonalProjection_eq_zero_iff {s : AffineSubspace ℝ P} [Nonempty s]
    [s.direction.HasOrthogonalProjection] {p : P} : dist p (orthogonalProjection s p) = 0 ↔ p ∈ s := by
  rw [dist_comm, dist_eq_zero, orthogonalProjection_eq_self_iff]

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