isHomeomorph_iff_continuous_isClosedMap_bijective

English

A map is a homeomorphism iff it is continuous, bijective, and closed (under appropriate hypotheses).

Русский

Отображение является гомеоморфизмом тогда и только тогда, когда оно непрерывно и биективно (и замкнутое при соответствующих гипотезах).

LaTeX

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

Lean4

/-- A map is a homeomorphism iff it is continuous, closed and bijective. -/
theorem isHomeomorph_iff_continuous_isClosedMap_bijective :
    IsHomeomorph f ↔ Continuous f ∧ IsClosedMap f ∧ Function.Bijective f :=
  ⟨fun hf => ⟨hf.continuous, hf.isClosedMap, hf.bijective⟩, fun ⟨hf, hf', hf''⟩ =>
    ⟨hf, fun _ hu => isClosed_compl_iff.1 (image_compl_eq hf'' ▸ hf' _ hu.isClosed_compl), hf''⟩⟩

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