Registry · Definition II.D09 established formalized

II.D09 — Cylinder Domain

A subset of tau^3 expressible as a finite Boolean combination of stage-k cylinders. The cylinder domains form the Boolean algebra generated by {C_k(x)}.

Book II Part 2 Ch. 9

Dependency Graph

Depends on (2)

I.T18 II.D02

Depended on by (1)

II.D36

Lean Formalization

Module: TauLib.BookII.Domains.Cylinders

Symbol: cylinder_mem