English
Let s be an affine subspace of a real inner product space with nonempty and whose direction admits an orthogonal projection. Then the linear part of the projection map onto s equals the orthogonal projection onto the direction of s.
Русский
Пусть s — аффинное подпространство реального пространства с вещественным скалярным произведением, ненулевое по определению направления, совершающее ортогональную проекцию. Тогда линейная часть отображения ортогональной проекции на s равна ортогональной проекции на направление s.
LaTeX
$$$ (\operatorname{orthogonalProjection} s).linear = s.direction.orthogonalProjection $$$
Lean4
/-- The linear map corresponding to `orthogonalProjection`. -/
@[simp]
theorem orthogonalProjection_linear {s : AffineSubspace ℝ P} [Nonempty s] [s.direction.HasOrthogonalProjection] :
(orthogonalProjection s).linear = s.direction.orthogonalProjection :=
rfl
