Topological space structure on Shrink X

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.homeomorph_toEquiv (X : Type u) [TopologicalSpace X] [Small.{v, u} X] : (homeomorph X).toEquiv = equivShrink X