isHomeomorph_iff_isEmbedding_surjective

English

A map is a homeomorphism iff it is an embedding and surjective.

Русский

Отображение является гомеоморфизмом тогда и только тогда, когда оно вложение и сюръективно.

LaTeX

$$$\IsHomeomorph f \iff \IsEmbedding f \wedge \mathrm{Surjective}(f)$$$

Lean4

/-- A map is a homeomorphism iff it is a surjective embedding. -/
theorem isHomeomorph_iff_isEmbedding_surjective : IsHomeomorph f ↔ IsEmbedding f ∧ Surjective f
    where
  mp hf := ⟨hf.isEmbedding, hf.surjective⟩
  mpr h := ⟨h.1.continuous, ((isOpenEmbedding_iff f).2 ⟨h.1, h.2.range_eq ▸ isOpen_univ⟩).isOpenMap, h.1.injective, h.2⟩

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