toHomeomorphOfContinuousClosed — Mathlib

English

If a bijection is continuous and closed, it is a homeomorphism.

Русский

Если биекция непрерывна и отображает замкнутые множества в замкнутые, она является гомеоморфизмом.

LaTeX

$$$ \\text{toHomeomorphOfContinuousClosed}(e,h_1,h_2) : X \\simeq_t Y $$$

Lean4

/-- If a bijective map `e : X ≃ Y` is continuous and open, then it is a homeomorphism. -/
@[simps! toEquiv]
def toHomeomorphOfContinuousClosed (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsClosedMap e) : X ≃ₜ Y :=
  e.toHomeomorphOfIsInducing <| IsClosedEmbedding.of_continuous_injective_isClosedMap h₁ e.injective h₂ |>.toIsInducing

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