𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
⊢ IsClosed ↑(LinearMap.range f)
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
⊢ IsClosed ↑(LinearMap.range f)
haveI : CompleteSpace G := hG.completeSpace_coe
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
g : (E × { x // x ∈ G }) ≃L[𝕜] F := coprodSubtypeLEquivOfIsCompl f h hker
⊢ IsClosed ↑(LinearMap.range f)
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
⊢ IsClosed ↑(LinearMap.range f)
let g := coprodSubtypeLEquivOfIsCompl f h hker
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
g : (E × { x // x ∈ G }) ≃L[𝕜] F := coprodSubtypeLEquivOfIsCompl f h hker
⊢ IsClosed ↑(Submodule.map (↑↑(coprodSubtypeLEquivOfIsCompl f h hker)) (Submodule.prod ⊤ ⊥))
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
g : (E × { x // x ∈ G }) ≃L[𝕜] F := coprodSubtypeLEquivOfIsCompl f h hker
⊢ IsClosed ↑(LinearMap.range f)
rw [range_eq_map_coprodSubtypeLEquivOfIsCompl f h hker]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
g : (E × { x // x ∈ G }) ≃L[𝕜] F := coprodSubtypeLEquivOfIsCompl f h hker
⊢ IsClosed ↑(Submodule.prod ⊤ ⊥)
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
g : (E × { x // x ∈ G }) ≃L[𝕜] F := coprodSubtypeLEquivOfIsCompl f h hker
⊢ IsClosed ↑(Submodule.map (↑↑(coprodSubtypeLEquivOfIsCompl f h hker)) (Submodule.prod ⊤ ⊥))
apply g.toHomeomorph.isClosed_image.2
no goals
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
hG : IsClosed ↑G
hker : ker f = ⊥
this : CompleteSpace { x // x ∈ G }
g : (E × { x // x ∈ G }) ≃L[𝕜] F := coprodSubtypeLEquivOfIsCompl f h hker
⊢ IsClosed ↑(Submodule.prod ⊤ ⊥)
exact isClosed_univ.prod isClosed_singleton