Registry · Definition II.D11 established formalized

II.D11 — 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.

Book II Part 2 Ch. 9

Dependency Graph

Depends on (1)

II.D10

Depended on by (2)

II.T04 II.T09

Lean Formalization

Module: TauLib.BookII.Domains.Cylinders

Symbol: cylinder_clopen