/-
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 FormalConjecturesUtilToronto 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:
The Toronto problem by W.R. Brian
namespace Torontoopen Cardinalvariable (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 ≃ₜ XEvery finite space is Toronto, since the only subspace with same cardinality is the space itself.
X:Type u_1inst✝¹:TopologicalSpace Xinst✝:Finite XY:Set XhY:#↑Y = #Xeq:Y = Set.univ⊢ ↑Set.univ ≃ₜ X
All goals completed! 🐙Any T2, Toronto space is discrete.
@[category research open, AMS 54]
theorem DiscreteTopology.of_t2_of_torontoSpace [T2Space X] [TorontoSpace X] :
DiscreteTopology X := X:Type u_1inst✝²:TopologicalSpace Xinst✝¹:T2Space Xinst✝:TorontoSpace X⊢ DiscreteTopology X
All goals completed! 🐙-- TODO: Add implication that this holds under the GCH
end Toronto