of_continuous_injective_isClosedMap

English

If f is continuous, injective, and a closed map, then f is a closed embedding.

Русский

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

LaTeX

$$$\mathrm{Continuous}(f) \land \mathrm{Injective}(f) \land \mathrm{IsClosedMap}(f) \Rightarrow \mathrm{IsClosedEmbedding}(f)$$$

Lean4

theorem of_continuous_injective_isClosedMap (h₁ : Continuous f) (h₂ : Injective f) (h₃ : IsClosedMap f) :
    IsClosedEmbedding f := by
  refine .of_isEmbedding_isClosedMap ⟨⟨?_⟩, h₂⟩ h₃
  refine h₁.le_induced.antisymm fun s hs => ?_
  refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩
  rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]

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