isIso_of_bijective_of_isOpenMap — Mathlib

English

If f: X ⟶ Y is bijective and IsClosedMap, then f is an isomorphism in TopCat (i.e., a homeomorphism).

Русский

Если f: X ⟶ Y биективно и является замкнутым отображением, то f является изоморфизмом в TopCat (то есть гомеоморфизм).

LaTeX

$$$\\forall f: X \\to Y,\\ (Bijective(f) \\land IsClosedMap(f)) \\Rightarrow IsIso(f)$$$

Lean4

theorem isIso_of_bijective_of_isOpenMap {X Y : TopCat.{u}} (f : X ⟶ Y) (hfbij : Function.Bijective f)
    (hfcl : IsOpenMap f) : IsIso f :=
  let e : X ≃ₜ Y := (Equiv.ofBijective f hfbij).toHomeomorphOfContinuousOpen f.hom.continuous hfcl
  inferInstanceAs <| IsIso (TopCat.isoOfHomeo e).hom

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