class PiBase.TorontoSpace (X : Type u_1) [TopologicalSpace X] : Prop

219. Toronto

• toronto ⦃Y : Set X⦄ : Cardinal.mk ↑Y = Cardinal.mk X → Nonempty (↑Y ≃ₜ X)