Registry · Theorem II.T13 established formalized

II.T13 — Torus Degeneration Theorem

Torus Degeneration Theorem

Book II Part 3 Ch. 17

Dependency Graph

Depends on (3)

II.D06 I.D18 I.T05

Depended on by (4)

II.D77 II.T14 II.T47 II.T49

Lean Formalization

Module: TauLib.BookII.Topology.TorusDegeneration

Symbol: pinch_surjective_check