isIso_iff_isHomeomorph — Mathlib

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_iff_isHomeomorph {X Y : TopCat.{u}} (f : X ⟶ Y) : IsIso f ↔ IsHomeomorph f :=
  ⟨fun _ ↦ (homeoOfIso (asIso f)).isHomeomorph, fun H ↦ isIso_of_bijective_of_isOpenMap _ H.bijective H.isOpenMap⟩

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