Registry · Axiom I.K1 established formalized

I.K1 — Strict Order (K1)

alpha < pi < gamma < eta < omega is a strict total order on the 5 generators.

Book I Part 1 Ch. 1

Dependency Graph

Depends on (1)

I.D01

Depended on by (10)

I.D04 I.D16a I.K3 I.P01 I.R01 I.T07 I.T08 V.T07 V.T103 V.T31

Lean Formalization

Module: TauLib.BookI.Kernel.Axioms

Symbol: Tau.Kernel.K1_strict_order