orthogonalProjection_coe_eq_linearProjOfIsCompl

English

The orthogonal projection map (viewed as a linear map to K) is exactly the canonical linear projection arising from the orthogonal direct sum decomposition, i.e., the projection along K⊥ onto K.

Русский

Коэффициентная проекция ортогонального проектора: линейное отображение $E\\to K$ совпадает с канонической линейной проекцией, полученной из разложения $E=K\\oplus K^\\perp$.

LaTeX

$$$(K.orthogonalProjection) : E \\to[K] K \;=\\; K.linearProjOfIsCompl _ Submodule.isCompl_orthogonal_of_hasOrthogonalProjection$.$$

Lean4

theorem orthogonalProjection_coe_eq_linearProjOfIsCompl [K.HasOrthogonalProjection] :
    (K.orthogonalProjection : E →ₗ[𝕜] K) =
      K.linearProjOfIsCompl _ Submodule.isCompl_orthogonal_of_hasOrthogonalProjection :=
  LinearMap.ext <| orthogonalProjection_eq_linearProjOfIsCompl

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