of_isEmbedding_isClosedMap — Mathlib

English

If f is an embedding and a closed map, then f is a closed embedding.

Русский

Если f — вложение и замкнутое отображение, то f — замкнутое вложение.

LaTeX

$$$\mathrm{IsEmbedding}(f) \rightarrow \mathrm{IsClosedMap}(f) \rightarrow \mathrm{IsClosedEmbedding}(f)$$$

Lean4

theorem of_isEmbedding_isClosedMap (h₁ : IsEmbedding f) (h₂ : IsClosedMap f) : IsClosedEmbedding f :=
  ⟨h₁, image_univ (f := f) ▸ h₂ univ isClosed_univ⟩

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