English
A map is a homeomorphism iff it is continuous and bijective (under compact domain and T2 codomain).
Русский
Отображение — гомеоморфизм тогда и только тогда, когда оно непрерывно и биективно (при компактном домене и пространстве Т2).
LaTeX
$$$\IsHomeomorph f \iff \mathrm{Continuous}(f) \wedge \mathrm{Bijective}(f)$$$
Lean4
/-- A map is a homeomorphism iff it is continuous and has a continuous inverse. -/
theorem isHomeomorph_iff_exists_inverse :
IsHomeomorph f ↔ Continuous f ∧ ∃ g : Y → X, LeftInverse g f ∧ RightInverse g f ∧ Continuous g :=
by
refine ⟨fun hf ↦ ⟨hf.continuous, ?_⟩, fun ⟨hf, g, hg⟩ ↦ ?_⟩
· let h := hf.homeomorph f
exact ⟨h.symm, h.left_inv, h.right_inv, h.continuous_invFun⟩
· exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph
