Registry · Proposition
I.P03
established
formalized
I.P03 — Pairwise Disjointness of Orbits
The five sets {omega}, O_alpha, O_pi, O_gamma, O_eta are pairwise disjoint.
Dependency Graph
Depends on (3)
Depended on by (3)
Lean Formalization
Module: TauLib.BookI.Orbit.Generation
Symbol: Tau.Orbit.orbit_disjoint