𝕜 : Type u_1
E : Type u_2
F : Type ?u.275809
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
this : IsPositive (comp (orthogonalProjection U) (comp T (↑adjoint (orthogonalProjection U))))
⊢ IsPositive (comp (orthogonalProjection U) (comp T (Submodule.subtypeL U)))
𝕜 : Type u_1
E : Type u_2
F : Type ?u.275809
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ IsPositive (comp (orthogonalProjection U) (comp T (Submodule.subtypeL U)))
have := hT.conj_adjoint (orthogonalProjection U : E →L[𝕜] U)
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.275809
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
this : IsPositive (comp (orthogonalProjection U) (comp T (↑adjoint (orthogonalProjection U))))
⊢ IsPositive (comp (orthogonalProjection U) (comp T (Submodule.subtypeL U)))
rwa [U.adjoint_orthogonalProjection] at this