𝕜 : Type u_2
E : Type u_1
F : Type ?u.53341
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ IsClosed ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v))
𝕜 : Type u_2
E : Type u_1
F : Type ?u.53341
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ IsClosed ↑Kᗮ
rw [orthogonal_eq_inter K]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.53341
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
this : ∀ (v : { x // x ∈ K }), IsClosed ↑(LinearMap.ker (↑(innerSL 𝕜) ↑v))
⊢ IsClosed ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v))
𝕜 : Type u_2
E : Type u_1
F : Type ?u.53341
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ IsClosed ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v))
have := fun v : K => ContinuousLinearMap.isClosed_ker (innerSL 𝕜 (v : E))
case h.e'_3
𝕜 : Type u_2
E : Type u_1
F : Type ?u.53341
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
this : ∀ (v : { x // x ∈ K }), IsClosed ↑(LinearMap.ker (↑(innerSL 𝕜) ↑v))
⊢ ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)) =
    ⋂ (i : { x // x ∈ K }), ↑(LinearMap.ker (↑(innerSL 𝕜) ↑i))
𝕜 : Type u_2
E : Type u_1
F : Type ?u.53341
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
this : ∀ (v : { x // x ∈ K }), IsClosed ↑(LinearMap.ker (↑(innerSL 𝕜) ↑v))
⊢ IsClosed ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v))
convert isClosed_iInter this
no goals
case h.e'_3
𝕜 : Type u_2
E : Type u_1
F : Type ?u.53341
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
this : ∀ (v : { x // x ∈ K }), IsClosed ↑(LinearMap.ker (↑(innerSL 𝕜) ↑v))
⊢ ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)) =
    ⋂ (i : { x // x ∈ K }), ↑(LinearMap.ker (↑(innerSL 𝕜) ↑i))
simp only [iInf_coe]