𝕜 : Type u_2
E : Type u_1
F : Type ?u.890931
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
x y : E
inst✝ : CompleteSpace E
hK✝ : Dense ↑K
hK : Kᗮ = ⊥
h : x - y ∈ Kᗮ
⊢ x = y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.890931
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
x y : E
inst✝ : CompleteSpace E
hK : Dense ↑K
h : x - y ∈ Kᗮ
⊢ x = y
rw [dense_iff_topologicalClosure_eq_top, topologicalClosure_eq_top_iff] at hK
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.890931
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
x y : E
inst✝ : CompleteSpace E
hK✝ : Dense ↑K
hK : Kᗮ = ⊥
h : x - y ∈ Kᗮ
⊢ x = y
rwa [hK, Submodule.mem_bot, sub_eq_zero] at h