Registry · Proposition I.P07 established formalized

I.P07 — Well-Ordering of Obj(tau)

(Obj(tau), <_tau) is a well-ordering of order type omega*4+1: four copies of omega (one per orbit ray) followed by the beacon omega.

Book I Part 3 Ch. 15

Dependency Graph

Depends on (2)

I.D16a I.T01

Depended on by (2)

I.L03 I.L04

Lean Formalization

Module: TauLib.BookI.Denotation.Order

Symbol: Tau.Denotation.well_ordering