𝕜 : Type u_2
E : Type u_1
F : Type ?u.794030
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace ↑↑K
⊢ Kᗮ = ⊥ → K = ⊤
𝕜 : Type u_2
E : Type u_1
F : Type ?u.794030
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace ↑↑K
⊢ Kᗮ = ⊥ ↔ K = ⊤
refine' ⟨_, fun h => by rw [h, Submodule.top_orthogonal_eq_bot]⟩
𝕜 : Type u_2
E : Type u_1
F : Type ?u.794030
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace ↑↑K
h : Kᗮ = ⊥
⊢ K = ⊤
𝕜 : Type u_2
E : Type u_1
F : Type ?u.794030
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace ↑↑K
⊢ Kᗮ = ⊥ → K = ⊤
intro h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.794030
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace ↑↑K
h : Kᗮ = ⊥
this : K ⊔ Kᗮ = ⊤
⊢ K = ⊤
𝕜 : Type u_2
E : Type u_1
F : Type ?u.794030
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace ↑↑K
h : Kᗮ = ⊥
⊢ K = ⊤
have : K ⊔ Kᗮ = ⊤ := Submodule.sup_orthogonal_of_completeSpace
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.794030
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace ↑↑K
h : Kᗮ = ⊥
this : K ⊔ Kᗮ = ⊤
⊢ K = ⊤
rwa [h, sup_comm, bot_sup_eq] at this
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.794030
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace ↑↑K
h : K = ⊤
⊢ Kᗮ = ⊥
rw [h, Submodule.top_orthogonal_eq_bot]