Registry · Proposition I.P36 established formalized

I.P36 — No Free Cartesian Diagonal

No free Cartesian diagonal: the diagonal discipline (I.D03) prevents free contraction/reuse, blocking the Cartesian product diagonal map that Cantor's argument requires.

Book I Part 9 Ch. 37

Dependency Graph

Depends on (1)

I.T35

Lean Formalization

Module: TauLib.BookI.Sets.CantorRefutation

Symbol: Tau.Sets.no_free_cartesian