Cardinality of second-countable spaces

A second-countable T₀ space has at most continuum many points, since a point is determined by the basic open sets containing it.

Main results

• TauCeti.mk_le_continuum_of_secondCountableTopology: a second-countable T₀ space has at most 𝔠 points; in particular so does every Polish space.

References

• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995, Corollary 6.3.

theorem TauCeti.mk_le_continuum_of_secondCountableTopology (X : Type u) [TopologicalSpace X] [SecondCountableTopology X] [T0Space X] : Cardinal.mk X ≤ Cardinal.continuum

A second-countable T₀ space has at most continuum many points. A point is determined by the members of a countable basis containing it. In particular a Polish space has at most 𝔠 points.