isIso_of_bijective_of_isClosedMap

English

If f is bijective and IsOpenMap, then f is an isomorphism in TopCat.

Русский

Если f биективно и открыто отображение, то оно является изоморфизмом в TopCat.

LaTeX

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

Lean4

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

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