orthogonalProjection_mem — Mathlib

English

The orthogonal projection of any point p onto s lies in s.

Русский

Ортогональная проекция точки p на s принадлежит s.

LaTeX

$$$ \uparrow(\operatorname{orthogonalProjection} s p) \in s $$$

Lean4

/-- The `orthogonalProjection` lies in the given subspace. -/
theorem orthogonalProjection_mem {s : AffineSubspace ℝ P} [Nonempty s] [s.direction.HasOrthogonalProjection] (p : P) :
    ↑(orthogonalProjection s p) ∈ s :=
  (orthogonalProjection s p).2

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