Registry · Theorem II.T08 established formalized

II.T08 — Hausdorff Property

tau^3 is Hausdorff: any two distinct points are separated by disjoint cylinder neighborhoods at the first disagreement depth.

Book II Part 3 Ch. 13

Dependency Graph

Depends on (2)

II.D13 II.T05

Depended on by (2)

II.D14 II.T10

Lean Formalization

Module: TauLib.BookII.Topology.StoneSpace

Symbol: hausdorff_check