toHomeomorphOfContinuousOpen — Mathlib

English

If a bijection e: X ≃ Y is continuous and an open map, then it is a homeomorphism.

Русский

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

LaTeX

$$$ \\text{toHomeomorphOfContinuousOpen}(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 toHomeomorphOfContinuousOpen (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) : X ≃ₜ Y :=
  e.toHomeomorphOfIsInducing <| IsOpenEmbedding.of_continuous_injective_isOpenMap h₁ e.injective h₂ |>.toIsInducing

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