Registry · Proposition II.P05 established formalized

II.P05 — Lobes as Clopen Sets

Lobes as Clopen Sets

Book II Part 3 Ch. 16

Dependency Graph

Depends on (2)

II.T12 II.D17

Lean Formalization

Module: TauLib.BookII.Topology.BoundaryMinimality

Symbol: lobes_clopen_check