homeoOfEquivCompactToT2 — Mathlib

English

Continuous equivalences from a compact space to a T2 space are homeomorphisms.

Русский

Непрерывные эквивалентности между компактным пространством и пространством Т2 являются гомеоморфизмами.

LaTeX

$$$\exists h : X \simeq_{\mathrm{Top}} Y, h = f$$$

Lean4

/-- Continuous equivalences from a compact space to a T2 space are homeomorphisms.

This is not true when T2 is weakened to T1
(see `Continuous.homeoOfEquivCompactToT2.t1_counterexample`). -/
@[simps toEquiv]
def homeoOfEquivCompactToT2 [CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous f) : X ≃ₜ Y :=
  { f with
    continuous_toFun := hf
    continuous_invFun := hf.continuous_symm_of_equiv_compact_to_t2 }

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