Topological space structure on Shrink X

noncomputable instance Shrink.instTopologicalSpace (X : Type u) [TopologicalSpace X] [Small.{v, u} X] : TopologicalSpace (Shrink.{v, u} X)

Equations

• Shrink.instTopologicalSpace X = (equivShrink X).symm.topologicalSpace

noncomputable def Shrink.homeomorph (X : Type u) [TopologicalSpace X] [Small.{v, u} X] : X ≃ₜ Shrink.{v, u} X

equivShrink as a homeomorphism.

Equations

• Shrink.homeomorph X = (equivShrink X).symm.homeomorph.symm

@[simp]

theorem Shrink.toEquiv_homeomorph (X : Type u) [TopologicalSpace X] [Small.{v, u} X] : (homeomorph X).toEquiv = (equivShrink X).symm.homeomorph.symm