Theorems · Theorem · logic and foundations

ONote.cmp.eq_def

∀ (x x_1 : ONote),
  x.cmp x_1 =
    match x, x_1 with
    | ONote.zero, ONote.zero => Ordering.eq
    | x, ONote.zero => Ordering.gt
    | ONote.zero, x => Ordering.lt
    | _o₁@h:(e₁.oadd n₁ a₁), _o₂@h_1:(e₂.oadd n₂ a₂) => (e₁.cmp e₂).then ((cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))

Defined in

Mathlib.SetTheory.Ordinal.Notation

Cited by

0 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext