The space ω₁ #
The space ω₁ with the order topology, a source of many counterexamples in general topology.
We follow [Mun00], where this space is denoted S_Ω.
References #
Instances For
theorem
Counterexample.Omega1Space.not_normalSpace_Iio_prod_Iic_omega_one :
¬NormalSpace (↑(Set.Iio (Ordinal.omega 1)) × ↑(Set.Iic (Ordinal.omega 1)))
Main theorem: Iio ω₁ × Iic ω₁ is not normal.
With this result, the counterexamples below can be proven for topological spaces X and Y in Type (u+1). We use Shrink to build versions of Iio.{1} ω₁ and Iic.{1} ω₁ in every universe and make the results more general.
instance
Counterexample.Omega1Space.instNormalSpaceShrink_counterexamples
{X : Type u_1}
[TopologicalSpace X]
[Small.{v, u_1} X]
[NormalSpace X]
:
instance
Counterexample.Omega1Space.instT3SpaceShrink_counterexamples
{X : Type u_1}
[TopologicalSpace X]
[Small.{v, u_1} X]
[T3Space X]
:
instance
Counterexample.Omega1Space.instCompactSpaceShrink_counterexamples
{X : Type u_1}
[TopologicalSpace X]
[Small.{v, u_1} X]
[CompactSpace X]
:
theorem
Counterexample.Omega1Space.isEmbedding_shrink_prodMap_inc_id :
Topology.IsEmbedding
(⇑(Shrink.homeomorph (↑(Set.Iic (Ordinal.omega 1)) × ↑(Set.Iic (Ordinal.omega 1)))) ∘ Prod.map inc id ∘ ⇑(Shrink.homeomorph (↑(Set.Iio (Ordinal.omega 1)) × ↑(Set.Iic (Ordinal.omega 1)))).symm)
Iio ω₁ × Iic ω₁ embeds into the compact Hausdorff space Iic ω₁ × Iic ω₁, shrunk.
Counterexamples
theorem
Counterexample.Omega1Space.subspace_of_paracompact_not_paracompact :
¬∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
ParacompactSpace Y → Topology.IsEmbedding f → ParacompactSpace X
A subspace of a paracompact space need not be paracompact.
theorem
Counterexample.Omega1Space.product_of_normal_not_normal :
¬∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
NormalSpace X → NormalSpace Y → NormalSpace (X × Y)
The product of two normal spaces need not be normal.
theorem
Counterexample.Omega1Space.subspace_of_normal_not_normal :
¬∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
NormalSpace Y → Topology.IsEmbedding f → NormalSpace X
A subspace of a normal space need not be normal.
theorem
Counterexample.Omega1Space.regular_not_normal :
¬∀ (X : Type u) [inst : TopologicalSpace X], RegularSpace X → NormalSpace X
A regular space need not be normal.