Theorems · Theorem · logic and foundations

Ordinal.enum_lt_enum

∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r] {o₁ o₂ : ↑(Set.Iio (Ordinal.type r))},
  r ((Ordinal.enum r) o₁) ((Ordinal.enum r) o₂) ↔ o₁ < o₂

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

4 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

IsWellOrder