isClosedEmbedding_iff_continuous_injective_isClosedMap

English

IsClosedEmbedding f is equivalent to Continuous f ∧ Injective f ∧ IsClosedMap f.

Русский

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

LaTeX

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

Lean4

theorem isClosedEmbedding_iff_continuous_injective_isClosedMap {f : X → Y} :
    IsClosedEmbedding f ↔ Continuous f ∧ Injective f ∧ IsClosedMap f
    where
  mp h := ⟨h.continuous, h.injective, h.isClosedMap⟩
  mpr h := .of_continuous_injective_isClosedMap h.1 h.2.1 h.2.2

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