isHomeomorph_iff_continuous_bijective

English

A map from a compact space to a T2 space is a homeomorphism iff it is continuous and bijective.

Русский

Отображение между компактным пространством и пространством Т2 является гомеоморфизмом тогда и только тогда, когда оно непрерывно и биективно.

LaTeX

$$$\IsHomeomorph f \iff \mathrm{Continuous}(f) \wedge \mathrm{Bijective}(f)$$$

Lean4

/-- A map from a compact space to a T2 space is a homeomorphism iff it is continuous and
  bijective. -/
theorem isHomeomorph_iff_continuous_bijective [CompactSpace X] [T2Space Y] :
    IsHomeomorph f ↔ Continuous f ∧ Bijective f :=
  by
  rw [isHomeomorph_iff_continuous_isClosedMap_bijective]
  refine and_congr_right fun hf ↦ ?_
  rw [eq_true hf.isClosedMap, true_and]

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