Registry · Proposition I.P04 established formalized

I.P04 — Orbit Countability

Each orbit ray O_g is countably infinite (isomorphic to N as a totally ordered set).

Book I Part 2 Ch. 7

Dependency Graph

Depends on (2)

I.D05 I.P02

Lean Formalization

Module: TauLib.BookI.Orbit.Countability

Symbol: Tau.Orbit.orbit_countable