Mathlib Map

Theorems · Definition · logic and foundations

Ordinal.enumOrd

Set Ordinal.{u} → Ordinal.{u} → Ordinal.{u}

Enumerator function for an unbounded set of ordinals. The definition is an implementation detail; this function is entirely characterized by being an order isomorphism. See enumOrdOrderIso.

Defined in
Mathlib.SetTheory.Ordinal.Enum
Cited by
23 results in Mathlib
Foundations
Depth 40 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Ordinal.preOmega · cited by 31Ordinal.preOmegaOrdinal.enumOrd_strictMono · cited by 10Ordinal.enumOrd_strictMonoOrdinal.enumOrd_le_of_forall_lt · cited by 5Ordinal.enumOrd_le_of_for…Ordinal.range_enumOrd · cited by 4Ordinal.range_enumOrdOrdinal.enumOrd_mem · cited by 4Ordinal.enumOrd_memOrdinal.veblenWith_add_one · cited by 3Ordinal.veblenWith_add_oneOrdinal.derivFamily_eq_enumOrd · cited by 2Ordinal.derivFamily_eq_en…Ordinal.eq_enumOrd · cited by 2Ordinal.eq_enumOrdOrdinal.enumOrdOrderIso · cited by 1Ordinal.enumOrdOrderIsoOrdinal.enumOrd_injective · cited by 1Ordinal.enumOrd_injectiveOrdinal.enumOrd_range · cited by 1Ordinal.enumOrd_rangeOrdinal.enumOrd_succ_le · cited by 1Ordinal.enumOrd_succ_leOrdinal.enumOrd_zero · cited by 1Ordinal.enumOrd_zeroOrdinal.coe_preOmega · cited by 1Ordinal.coe_preOmegaOrdinal.deriv_eq_enumOrd · cited by 1Ordinal.deriv_eq_enumOrdSet · cited by 53352SetSet.ofPred · cited by 6101Set.ofPredOrdinal · cited by 1688OrdinalInfSet.sInf · cited by 935InfSet.sInfOrdinal.enumOrdCITED BYCITES

Cites4

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

Cited by25

Results whose statement or proof uses this declaration.