Registry · Theorem II.T10 established formalized

II.T10 — Topology Uniqueness

The profinite topology on tau^3 is the unique topology satisfying CRT continuity, Hausdorff separation, and compactness.

Book II Part 3 Ch. 14

Dependency Graph

Depends on (3)

II.T04 II.T07 II.T08

Depended on by (1)

II.R06

Lean Formalization

Module: TauLib.BookII.Topology.Invariant

Symbol: topology_unique_check