Clopen Basis

The collection B = {C_k(x)} of all stage-k cylinders. Every element is clopen: both C_k(x) and its complement are finite unions of basis elements.

Clopen Basis

Summary

The collection B = {C_k(x)} of all stage-k cylinders. Every element is clopen: both C_k(x) and its complement are finite unions of basis elements.

Statement

%
\label{def:clopen-basis}
The \textbf{clopen basis} for~$\tau^3$ is the collection
\[
    \boxed{\mathcal{B}
    \;:=\;
    \bigl\{\, C_k(x) \;:\;
    k \geq 1,\; x \in \tau^3 \,\bigr\}.}
\]
Every element of $\mathcal{B}$ is clopen
in the sense that both $C_k(x)$
and $\tau^3 \setminus C_k(x)$
are finite unions of elements of~$\mathcal{B}$
(Proposition~\ref{prop:ch09-complement}).

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 21
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part02/ch09-cylinder-domains.tex lines 433-448

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Domains.Cylinders
• Name: cylinder_clopen

Dependencies

• Canonical: II.D10

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.