starProjection_coe_eq_isCompl_projection

English

For a subspace K with the orthogonal decomposition E = K ⊕ K⊥, the projection onto K along K⊥ agrees with the adjoint-projection coming from the perpendicular decomposition.

Русский

Для подпространства K с ортогональным разложением E = K ⊕ K⊥ проекция на K вдоль K⊥ совпадает с проекцией, полученной из ортогонального разложения.

LaTeX

$$$K.starProjection^{\\}\\toLinearMap = K.isCompl_orthogonal_of_hasOrthogonalProjection.projection$.$$

Lean4

theorem starProjection_coe_eq_isCompl_projection [K.HasOrthogonalProjection] :
    K.starProjection.toLinearMap = K.isCompl_orthogonal_of_hasOrthogonalProjection.projection := by
  simp [starProjection, orthogonalProjection_coe_eq_linearProjOfIsCompl, IsCompl.projection]

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