isoEquivHomeo — Mathlib

English

There is a natural equivalence between isomorphisms in Sequential and homeomorphisms of the underlying topological spaces.

Русский

Существует естественное эквиваленство между изоморфизмами в Sequential и гомеоморфизмами принадлежащих базовым топологическим пространствам.

LaTeX

$$$(X \cong Y) \simeq (X \simeq_{t} Y)$$$

Lean4

/-- The equivalence between isomorphisms in `Sequential` and homeomorphisms
of topological spaces. -/
@[simps]
def isoEquivHomeo {X Y : Sequential.{u}} : (X ≅ Y) ≃ (X ≃ₜ Y)
    where
  toFun := homeoOfIso
  invFun := isoOfHomeo

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