isProperMap_of_isClosedMap_of_inj

English

An injective continuous closed map is proper.

Русский

Инъективное непрерывное замыкание отображение проперно.

LaTeX

$$$\text{IsProperMap}(f) \iff \text{IsClosedMap}(f) \land f\text{ is injective}$$$

Lean4

/-- A injective continuous and closed map is proper. -/
theorem isProperMap_of_isClosedMap_of_inj (f_cont : Continuous f) (f_inj : f.Injective) (f_closed : IsClosedMap f) :
    IsProperMap f :=
  (isProperMap_iff_isClosedMap_of_inj f_cont f_inj).2 f_closed

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