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 = TopologicalSpace.coinduced (⇑(equivShrink X)) inferInstance

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 = { toEquiv := equivShrink X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

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