Theorems · Definition · logic and foundations

Ordinal.typein

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

The order type of an element inside a well order. This is registered as a principal segment embedding into the ordinals, with top type r.

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

60 results in Mathlib

Foundations

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

Assumes

IsWellOrder