English
If a continuous linear map f has its range complemented by a subspace G (IsCompl(range f, G)) and G is closed, and ker f = {0}, then the range of f is a closed set in F.
Русский
Пусть f: E →L[𝕜] F — непрерывное линейное отображение. Пусть G ⊂ F таково, что F = range(f) ⊕ G (IsCompl(range f, G)) и G закрыто, а ker f = {0}. Тогда range(f) — замкнутое подмножество в F.
LaTeX
$$$\text{IsClosed}(G) \Rightarrow \text{IsClosed}(\operatorname{range} f : Set F) \quad \text{under } \ker f = \{0\} \text{ and } \operatorname{IsCompl}(\operatorname{range} f, G)$$$
Lean4
theorem closed_complemented_range_of_isCompl_of_ker_eq_bot {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
[CompleteSpace F] (f : E →L[𝕜] F) (G : Submodule 𝕜 F) (h : IsCompl (LinearMap.range f) G)
(hG : IsClosed (G : Set F)) (hker : ker f = ⊥) : IsClosed (LinearMap.range f : Set F) :=
by
haveI : CompleteSpace G := hG.completeSpace_coe
let g := coprodSubtypeLEquivOfIsCompl f h hker
rw [range_eq_map_coprodSubtypeLEquivOfIsCompl f h hker]
apply g.toHomeomorph.isClosed_image.2
exact isClosed_univ.prod isClosed_singleton
