Registry · Theorem II.T09 established formalized

II.T09 — Total Disconnectedness

Total Disconnectedness

Book II Part 3 Ch. 13

Dependency Graph

Depends on (2)

II.D11 II.T04

Depended on by (1)

II.D14

Lean Formalization

Module: TauLib.BookII.Topology.StoneSpace

Symbol: totally_disconnected_check