dist_orthogonalProjection_ne_zero_of_notMem

English

The nonnegative distance to the projection equals the infimum distance in the nonnegative real sense.

Русский

Неотрицательное расстояние до проекции равно infNndist.

LaTeX

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

Lean4

/-- The distance between a point and its orthogonal projection is
nonzero if it does not lie in the subspace. -/
theorem dist_orthogonalProjection_ne_zero_of_notMem {s : AffineSubspace ℝ P} [Nonempty s]
    [s.direction.HasOrthogonalProjection] {p : P} (hp : p ∉ s) : dist p (orthogonalProjection s p) ≠ 0 :=
  mt dist_orthogonalProjection_eq_zero_iff.mp hp

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