Registry · Definition II.D15 established formalized

II.D15 — Tau-Dimension

The minimal number of independent refinement rays whose joint cylinders separate all points of tau^3. Replaces classical covering dimension (which yields zero for profinite spaces).

Book II Part 3 Ch. 15

Dependency Graph

Depends on (2)

II.D10 I.P08

Depended on by (6)

II.D25 II.D30 II.D76 II.R06a II.T11 II.T20

Lean Formalization

Module: TauLib.BookII.Topology.DimensionFour

Symbol: tau_dim