case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ ≤ ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)

case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ (⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)) ≤ Kᗮ
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ = ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)
apply le_antisymm
case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ∀ (i : { x // x ∈ K }), Kᗮ ≤ LinearMap.ker (↑(innerSL 𝕜) ↑i)
case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ ≤ ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)
rw [le_iInf_iff]
case a.mk
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ w ∈ LinearMap.ker (↑(innerSL 𝕜) ↑{ val := v, property := hv })
case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ∀ (i : { x // x ∈ K }), Kᗮ ≤ LinearMap.ker (↑(innerSL 𝕜) ↑i)
rintro ⟨v, hv⟩ w hw
no goals
case a.mk
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ w ∈ LinearMap.ker (↑(innerSL 𝕜) ↑{ val := v, property := hv })
simpa using hw _ hv
case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v : E
hv : v ∈ ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)
w : E
hw : w ∈ K
⊢ inner w v = 0
case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ (⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)) ≤ Kᗮ
intro v hv w hw
case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v w : E
hw : w ∈ K
hv : ∀ (i : { x // x ∈ K }), v ∈ LinearMap.ker (↑(innerSL 𝕜) ↑i)
⊢ inner w v = 0
case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v : E
hv : v ∈ ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)
w : E
hw : w ∈ K
⊢ inner w v = 0
simp only [mem_iInf] at hv
no goals
case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.42949
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v w : E
hw : w ∈ K
hv : ∀ (i : { x // x ∈ K }), v ∈ LinearMap.ker (↑(innerSL 𝕜) ↑i)
⊢ inner w v = 0
exact hv ⟨w, hw⟩