English
Let X,Y,Z be topological spaces with X Hausdorff. If f:X→Y and g:Y→X satisfy that g is a left-inverse of f, and f,g are continuous, then the range of g is closed in X.
Русский
Пусть X, Y, Z — топологические пространства, X — Хаусдорфово. Если существуют отображения f:X→Y и g:Y→X такие, что g является левой обратной к f, и оба отображения непрерывны, то образ g закрыт в X.
LaTeX
$$$\\text{If } f:X\\to Y,\\ g:Y\\to X\\text{ with } g\\circ f = \\mathrm{id}_X\\text{ (LeftInverse), and } f,g\\text{ are continuous, then } \\operatorname{range}(g)\\text{ is closed in } X.$$$
Lean4
theorem isClosed_range [T2Space X] {f : X → Y} {g : Y → X} (h : Function.LeftInverse f g) (hf : Continuous f)
(hg : Continuous g) : IsClosed (range g) :=
have : EqOn (g ∘ f) id (closure <| range g) := h.rightInvOn_range.eqOn.closure (hg.comp hf) continuous_id
isClosed_of_closure_subset fun x hx => ⟨f x, this hx⟩
