Topological space structure on Shrink X

@[implicit_reducible]

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

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

equivShrink as a homeomorphism.

@[simp]

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