orthogonalProjection — Mathlib

Lean4

/-- The orthogonal projection of a point onto a nonempty affine
subspace, whose direction is complete. The corresponding linear map
(mapping a vector to the difference between the projections of two
points whose difference is that vector) is the `orthogonalProjection`
for real inner product spaces, onto the direction of the affine
subspace being projected onto. -/
nonrec def orthogonalProjection (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection] : P →ᴬ[ℝ] s
    where
  __ := orthogonalProjectionAux s
  cont := AffineMap.continuous_linear_iff.1 s.direction.orthogonalProjection.cont

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