𝕜 : Type u_2
E : Type u_1
F : Type ?u.883149
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ topologicalClosure Kᗮ = Kᗮ
𝕜 : Type u_2
E : Type u_1
F : Type ?u.883149
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮᗮ = Kᗮ
rw [Kᗮ.orthogonal_orthogonal_eq_closure]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.883149
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ topologicalClosure Kᗮ = Kᗮ
exact K.isClosed_orthogonal.submodule_topologicalClosure_eq