𝕜 : Type u_2
E : Type u_1
F : Type ?u.37226
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ K ⊓ Kᗮ ≤ ⊥
𝕜 : Type u_2
E : Type u_1
F : Type ?u.37226
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ K ⊓ Kᗮ = ⊥
rw [eq_bot_iff]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.37226
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ⊓ Kᗮ → x ∈ ⊥
𝕜 : Type u_2
E : Type u_1
F : Type ?u.37226
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ K ⊓ Kᗮ ≤ ⊥
intro x
𝕜 : Type u_2
E : Type u_1
F : Type ?u.37226
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ∧ x ∈ Kᗮ → x ∈ ⊥
𝕜 : Type u_2
E : Type u_1
F : Type ?u.37226
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ⊓ Kᗮ → x ∈ ⊥
rw [mem_inf]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.37226
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ∧ x ∈ Kᗮ → x ∈ ⊥
exact fun ⟨hx, ho⟩ => inner_self_eq_zero.1 (ho x hx)