isClosedEmbedding — Mathlib

English

If X,Y are topological spaces with X Hausdorff, and f,g satisfy a left-inverse relation with f,g continuous, then g is a closed embedding.

Русский

Пусть X,Y — топологические пространства, X — Хаусдорфово. Если существует левый обратный к f через g и оба отображения непрерывны, то g является замкнутым вложением.

LaTeX

$$$[T2Space X]\\; \\{f:X\\to Y\\}\\;\\{g:Y\\to X\\}\\; h:\\text{LeftInverse } f g \\rightarrow \\text{Continuous } f \\rightarrow \\text{Continuous } g\\rightarrow \\text{IsClosedEmbedding } g.$$$

Lean4

theorem isClosedEmbedding [T2Space X] {f : X → Y} {g : Y → X} (h : Function.LeftInverse f g) (hf : Continuous f)
    (hg : Continuous g) : IsClosedEmbedding g :=
  ⟨.of_leftInverse h hf hg, h.isClosed_range hf hg⟩

Похожие утверждения