Descriptive set theory

The topology of Polish spaces and their definable subsets: classical characterizations of Cantor space, Baire space and the rationals, Borel complexity, Bernstein sets and topological games.

• Alexandrov–Urysohn characterization of Baire space
• Banach–Mazur game
• Borel complexity of differentiable functions

TheoremBrouwer's characterization of the Cantor space#✓fully proved

Every nonempty compact metrizable perfect totally disconnected space is homeomorphic to the Cantor space.

theorem brouwer_cantor_space_characterization
    {X : Type*} [TopologicalSpace X] [CompactSpace X]
    [TopologicalSpace.MetrizableSpace X] [PerfectSpace X]
    [TotallyDisconnectedSpace X] [Nonempty X] :
    Nonempty (X ≃ₜ (ℕ → Bool))

Sources

• L. E. J. Brouwer, Proc. Kon. Ned. Akad. Wet. 12 (1910), 785-794.

TheoremExistence of a Bernstein set#✓fully proved

There is a set \(B \subseteq \mathbb{R}\) such that every closed, uncountable set \(F \subseteq \mathbb{R}\) meets both \(B\) and its complement \(\mathbb{R} \setminus B\).

theorem bernstein_set_exists :
    ∃ (B : Set ℝ), ∀ (F : Set ℝ), IsClosed F → ¬F.Countable →
      (B ∩ F).Nonempty ∧ (Set.compl B ∩ F).Nonempty

Sources

• F. Bernstein (construction); J. C. Oxtoby, Measure and Category, 2nd ed. (1980); A. S. Kechris, Classical Descriptive Set Theory, Thm 8.24 (1995).

TheoremSierpinski's characterization of the rationals#✓fully proved

Every nonempty countable metrizable space with no isolated points is homeomorphic to Q.

theorem sierpinski_rationals_characterization
    {X : Type*} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X]
    [PerfectSpace X] [Countable X] [Nonempty X] :
    Nonempty (X ≃ₜ ℚ)

Sources

• W. Sierpinski, Sur une propriete topologique, Fund. Math. 1 (1920), 11-16, DOI 10.4064/FM-1-1-11-16.

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.