Alexandrov–Urysohn characterization of Baire space

DefinitionZero-dimensional space#✓fully proved

A topological space \(X\) is zero-dimensional if for every point \(x \in X\) and every open set \(U \subseteq X\) containing \(x\) there is a clopen set \(V\) with \(x \in V \subseteq U\).

def IsZeroDimensionalSpace (X : Type*) [TopologicalSpace X] : Prop :=
  ∀ (x : X) (U : Set X), IsOpen U → x ∈ U → ∃ V : Set X, IsClopen V ∧ x ∈ V ∧ V ⊆ U

Used by 1

Used byAlexandrov–Urysohn theorem on Baire space

TheoremAlexandrov–Urysohn theorem on Baire space#✓fully proved

Let \(X\) be a nonempty Polish space that is zero-dimensional (for every point \(x\) and every open set \(U\) containing \(x\) there is a clopen set \(V\) with \(x \in V \subseteq U\)) and in which every compact subset has empty interior. Then \(X\) is homeomorphic to the Baire space \(\mathbb{N}^{\mathbb{N}}\) of all sequences of natural numbers, with the product of the discrete topologies.

theorem baire_space_characterization
    {X : Type*} [TopologicalSpace X] [PolishSpace X] [Nonempty X]
    (hZero : IsZeroDimensionalSpace X)
    (hCompact : ∀ (K : Set X), IsCompact K → interior K = ∅) :
    Nonempty (X ≃ₜ (ℕ → ℕ))

Sources

• Alexandrov–Urysohn characterization; A. S. Kechris, Classical Descriptive Set Theory (1995), Theorem 7.7.

Uses 1

Statement usesZero-dimensional space

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.