FormalConjectures.Wikipedia.Toronto

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

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


namespace Toronto


open Cardinal


variable (X : Type*) [TopologicalSpace X]

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

class TorontoSpace where
  toronto : ∀ ⦃Y : Set X⦄, #Y = #X → Y ≃ₜ X

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

@[category test, AMS 54]
instance Finite.torontoSpace [Finite X] : TorontoSpace X where
  toronto := byX:Type u_1inst✝¹:TopologicalSpace Xinst✝:Finite X⊢ ⦃Y : Set X⦄ → #↑Y = #X → ↑Y ≃ₜ X
    intro Y hYX:Type u_1inst✝¹:TopologicalSpace Xinst✝:Finite XY:Set XhY:#↑Y = #X⊢ ↑Y ≃ₜ X
    have eq : Y = Set.univ := byX:Type u_1inst✝¹:TopologicalSpace Xinst✝:Finite X⊢ ⦃Y : Set X⦄ → #↑Y = #X → ↑Y ≃ₜ X
      refine (Set.eq_univ_iff_ncard Y).mpr ?_X:Type u_1inst✝¹:TopologicalSpace Xinst✝:Finite XY:Set XhY:#↑Y = #X⊢ Y.ncard = Nat.card X
      have : Y.ncard = (#↑Y).toNat := byX:Type u_1inst✝¹:TopologicalSpace Xinst✝:Finite X⊢ ⦃Y : Set X⦄ → #↑Y = #X → ↑Y ≃ₜ X
        exact rflAll goals completed! 🐙
      rw [this, hY]X:Type u_1inst✝¹:TopologicalSpace Xinst✝:Finite XY:Set XhY:#↑Y = #Xthis:Y.ncard = Cardinal.toNat #↑Y := rfl⊢ Cardinal.toNat #X = Nat.card X
      exact rflAll goals completed! 🐙
    rw [eq]X:Type u_1inst✝¹:TopologicalSpace Xinst✝:Finite XY:Set XhY:#↑Y = #Xeq:Y = Set.univ := 
  (Set.eq_univ_iff_ncard Y).mpr
    (have this := rfl;
    Eq.mpr (id (congrArg (fun _a => _a = Nat.card X) this))
      (Eq.mpr (id (congrArg (fun _a => Cardinal.toNat _a = Nat.card X) hY)) rfl))⊢ ↑Set.univ ≃ₜ X
    exact Homeomorph.Set.univ XAll goals completed! 🐙

Any T2, Toronto space is discrete.

@[category research open, AMS 54]
theorem declaration uses 'sorry'DiscreteTopology.of_t2_of_torontoSpace [T2Space X] [TorontoSpace X] :
    DiscreteTopology X := byX:Type u_1inst✝²:TopologicalSpace Xinst✝¹:T2Space Xinst✝:TorontoSpace X⊢ DiscreteTopology X
  sorryAll goals completed! 🐙


-- TODO: Add implication that this holds under the GCH

end Toronto