Toronto spaces

A Toronto space is a topological space which is homeomorphic to all of its subspaces of same cardinality.

It is conjectured that every T2, Toronto space is discrete. W.R. Brian proved that this holds under GCH.

References:

• Wikipedia
• The Toronto problem by W.R. Brian

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

A Toronto space is a topological space which is homeomorphic to all of its subspaces of same cardinality.

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

instance Toronto.Finite.torontoSpace (X : Type u_1) [TopologicalSpace X] [Finite X] : TorontoSpace X

Every finite space is Toronto, since the only subspace with same cardinality is the space itself.

Equations

• Toronto.Finite.torontoSpace X = { toronto := fun ⦃Y : Set X⦄ (hY : Cardinal.mk ↑Y = Cardinal.mk X) => have eq := ⋯; ⋯.mpr (Homeomorph.Set.univ X) }

theorem Toronto.DiscreteTopology.of_t2_of_torontoSpace (X : Type u_1) [TopologicalSpace X] [T2Space X] [TorontoSpace X] : DiscreteTopology X

Any T2, Toronto space is discrete.