Ordinal.type

{α : Type u} → (r : α → α → Prop) → [wo : IsWellOrder α r] → Ordinal.{u}

The order type of a well order is an ordinal.

Defined in: Mathlib.SetTheory.Ordinal.Basic
Cited by: 207 results in Mathlib
Foundations: Depth 27 from the axioms, rests on 97 definitions · uses propext, Quot.sound
Assumes: IsWellOrder

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Results whose statement or proof uses this declaration.

Cardinal.ordproof · cited by 266
Ordinal.omega0proof · cited by 197
Ordinal.liftproof · cited by 86
Ordinal.typeinproof · cited by 60
Ordinal.enumstatement · cited by 39
Ordinal.type_toTypestatement · cited by 28
Cardinal.card_ordproof · cited by 23
Profinite.NobelingProof.termstatement and proof · cited by 22
Ordinal.univproof · cited by 18
Profinite.NobelingProof.C'statement and proof · cited by 18
Profinite.NobelingProof.GoodProducts.MaxProductsstatement and proof · cited by 17
Cardinal.mul_eq_selfproof · cited by 13

Showing the 200 most cited of 234.