adjoint_orthogonalProjection — Mathlib

English

The adjoint of the orthogonal projection onto a subspace U is the inclusion map U → E.

Русский

Сопряжённый ортогональной проекции на U является включением U в E.

LaTeX

$$$(U.orthogonalProjection)^{\dagger} = U.subtypeL$$$

Lean4

theorem _root_.Submodule.adjoint_orthogonalProjection (U : Submodule 𝕜 E) [CompleteSpace U] :
    (U.orthogonalProjection : E →L[𝕜] U)† = U.subtypeL := by rw [← U.adjoint_subtypeL, adjoint_adjoint]

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