Theorems · Definition · logic and foundations

Ordinal.enum

{α : Type u} → (r : α → α → Prop) → [inst : IsWellOrder α r] → (fun x1 x2 => x1 < x2) ≃r r

A well order r is order-isomorphic to the set of ordinals smaller than type r. enum r ⟨o, h⟩ is the o-th element of α ordered by r. That is, enum maps an initial segment of the ordinals, those less than the order type of r, to the elements of α.

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

39 results in Mathlib

Foundations

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

Assumes

IsWellOrder