orthogonalProjection_contLinear — Mathlib

English

Let s be as above. The continuous linear map underlying the projection onto s coincides with the linear orthogonal projection onto the direction of s.

Русский

Пусть s — указанное выше аффинное подпространство. Непрерывная линейная часть отображения проекции совпадает с линейной ортогональной проекцией на направление s.

LaTeX

$$$ (\operatorname{orthogonalProjection} s).contLinear = s.direction.orthogonalProjection $$$

Lean4

/-- The continuous linear map corresponding to `orthogonalProjection`. -/
@[simp]
theorem orthogonalProjection_contLinear {s : AffineSubspace ℝ P} [Nonempty s] [s.direction.HasOrthogonalProjection] :
    (orthogonalProjection s).contLinear = s.direction.orthogonalProjection :=
  rfl

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