isClosedEmbedding — Mathlib

English

A continuous injective map from a compact space to a Hausdorff space is a closed embedding.

Русский

Непрерывное инъективное отображение из компактного пространства в Хаусдорфовоe пространство является замкнутым вложением.

LaTeX

$$$[CompactSpace X][T2Space Y]\\; f\\text{ continuous},\\;\\text{Injective } f \\Rightarrow IsClosedEmbedding f.$$$

Lean4

/-- A continuous injective map from a compact space to a Hausdorff space is a closed embedding. -/
theorem isClosedEmbedding [CompactSpace X] [T2Space Y] {f : X → Y} (h : Continuous f) (hf : Function.Injective f) :
    IsClosedEmbedding f :=
  .of_continuous_injective_isClosedMap h hf h.isClosedMap

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