Stone Space

A topological space that is compact, Hausdorff, and totally disconnected; equivalently, a profinite space. tau^3 is a Stone space by II.T07-T09, with clopen basis from the cylinder topology.

Stone Space

Summary

A topological space that is compact, Hausdorff, and totally disconnected; equivalently, a profinite space. tau^3 is a Stone space by II.T07-T09, with clopen basis from the cylinder topology.

Statement

%
\label{def:stone-space}
A \textbf{Stone space} is a topological space that is
compact, Hausdorff, and totally disconnected.
Equivalently, a Stone space is a compact Hausdorff space
with a basis of clopen sets.
Equivalently, a Stone space is a profinite space:
an inverse limit of finite discrete spaces.

The space~$\tau^3$ is a Stone space:
\[
    \boxed{\tau^3 \;\text{is compact}
    \;\;\textup{(II.T07)},\quad
    \text{Hausdorff}
    \;\;\textup{(II.T08)},\quad
    \text{totally disconnected}
    \;\;\textup{(II.T09)}.}
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 30
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part03/ch13-stone-space.tex lines 420-439

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Topology.StoneSpace
• Name: StoneWitness

Dependencies

• Canonical: II.T07, II.T08, II.T09

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.