Theorems · Definition · logic and foundations

Ordinal.ToType

Ordinal.{u} → Type u

A "canonical" type order-isomorphic to the ordinal o, living in the same universe. This is defined through the axiom of choice; in particular, it has no useful def-eqs, and it is not exposed. Use this over Iio o only when it is paramount to have a Type u rather than a Type (u + 1), and convert using `` Ordinal.ToType.mk : Iio o → o.ToType Ordinal.ToType.toOrd : o.ToType → Iio o ``

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

143 results in Mathlib

Foundations

Depth 27 from the axioms, rests on 105 definitions · uses propext, Classical.choice, Quot.sound