Continuous_Bijection_from_Compact_to_Hausdorff_is_Homeomorphism

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

compact-spacescontinuous-mappingshausdorff-spaceshomeomorphismsproofwiki

Let $T_1$ be a compact space. Let $T_2$ be a Hausdorff space. Let $f: T_1 \to T_2$ be a continuous bijection. Then $f$ is a homeomorphism.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Continuous_Bijection_from_Compact_to_Hausdorff_is_Homeomorphism {α : Type _} {β : Type _} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] (f : α → β) (hf : Continuous f) (hbij : Function.Bijective f) : IsOpenMap f := by sorry

Source

https://proofwiki.org/wiki/Continuous_Bijection_from_Compact_to_Hausdorff_is_Homeomorphism

View graph