case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.803050
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
hv : v ∈ Kᗮ
⊢ ↑(↑(orthogonalProjection K) v) = ↑0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.803050
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
hv : v ∈ Kᗮ
⊢ ↑(orthogonalProjection K) v = 0
ext
no goals
case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.803050
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
hv : v ∈ Kᗮ
⊢ ↑(↑(orthogonalProjection K) v) = ↑0
convert eq_orthogonalProjection_of_mem_orthogonal (K := K) _ _ <;> simp [hv]