Documentation

Mathlib.SetTheory.Ordinal.Enum

Enumerating sets of ordinals by ordinals #

The ordinals have the peculiar property that every subset bounded above is a small type, while themselves not being small. As a consequence of this, every unbounded subset of Ordinal is order isomorphic to Ordinal.

We define this correspondence as enumOrd, and use it to then define an order isomorphism enumOrdOrderIso.

This can be thought of as an ordinal analog of Nat.nth.

source
@[irreducible]
noncomputable def Ordinal.enumOrd (s : Set Ordinal.{u}) (o : Ordinal.{u}) :
Ordinal.{u}

Enumerator function for an unbounded set of ordinals.

Equations
Instances For
    source
    @[deprecated "No deprecation message was provided." (since := "2024-09-20")]
    theorem Ordinal.enumOrd_def {s : Set Ordinal.{u}} (o : Ordinal.{u}) :
    enumOrd s o = sInf (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b})
    source
    theorem Ordinal.enumOrd_le_of_forall_lt {o a : Ordinal.{u}} {s : Set Ordinal.{u}} (ha : a ∈ s) (H : ∀ b < o, enumOrd s b < a) :
    enumOrd s o ≤ a
    source
    theorem Ordinal.enumOrd_mem {s : Set Ordinal.{u}} (hs : ¬BddAbove s) (o : Ordinal.{u}) :
    enumOrd s o ∈ s
    source
    theorem Ordinal.enumOrd_strictMono {s : Set Ordinal.{u}} (hs : ¬BddAbove s) :
    StrictMono (enumOrd s)
    source
    theorem Ordinal.enumOrd_injective {s : Set Ordinal.{u}} (hs : ¬BddAbove s) :
    Function.Injective (enumOrd s)
    source
    theorem Ordinal.enumOrd_inj {s : Set Ordinal.{u}} (hs : ¬BddAbove s) {a b : Ordinal.{u}} :
    enumOrd s a = enumOrd s b ↔ a = b
    source
    theorem Ordinal.enumOrd_le_enumOrd {s : Set Ordinal.{u}} (hs : ¬BddAbove s) {a b : Ordinal.{u}} :
    enumOrd s a ≤ enumOrd s b ↔ a ≤ b
    source
    theorem Ordinal.enumOrd_lt_enumOrd {s : Set Ordinal.{u}} (hs : ¬BddAbove s) {a b : Ordinal.{u}} :
    enumOrd s a < enumOrd s b ↔ a < b
    source
    theorem Ordinal.id_le_enumOrd {s : Set Ordinal.{u}} (hs : ¬BddAbove s) :
    id ≤ enumOrd s
    source
    theorem Ordinal.le_enumOrd_self {s : Set Ordinal.{u}} (hs : ¬BddAbove s) {a : Ordinal.{u}} :
    a ≤ enumOrd s a
    source
    theorem Ordinal.enumOrd_succ_le {a b : Ordinal.{u}} {s : Set Ordinal.{u}} (hs : ¬BddAbove s) (ha : a ∈ s) (hb : enumOrd s b < a) :
    enumOrd s (Order.succ b) ≤ a
    source
    theorem Ordinal.range_enumOrd {s : Set Ordinal.{u}} (hs : ¬BddAbove s) :
    Set.range (enumOrd s) = s
    source
    theorem Ordinal.enumOrd_surjective {s : Set Ordinal.{u}} (hs : ¬BddAbove s) {b : Ordinal.{u}} (hb : b ∈ s) :
    ∃ (a : Ordinal.{u}), enumOrd s a = b
    source
    @[irreducible]
    theorem Ordinal.enumOrd_le_of_subset {s t : Set Ordinal.{u}} (hs : ¬BddAbove s) (hst : s ⊆ t) :
    enumOrd t ≤ enumOrd s
    source
    theorem Ordinal.eq_enumOrd {s : Set Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{u}) (hs : ¬BddAbove s) :
    enumOrd s = f ↔ StrictMono f ∧ Set.range f = s

    A characterization of enumOrd: it is the unique strict monotonic function with range s.

    source
    theorem Ordinal.enumOrd_range {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : StrictMono f) :
    enumOrd (Set.range f) = f
    source
    @[simp]
    theorem Ordinal.enumOrd_univ :
    enumOrd Set.univ = id
    source
    @[simp]
    theorem Ordinal.enumOrd_zero {s : Set Ordinal.{u}} :
    enumOrd s 0 = sInf s
    source
    noncomputable def Ordinal.enumOrdOrderIso (s : Set Ordinal.{u_1}) (hs : ¬BddAbove s) :
    Ordinal.{u_1} ≃o ↑s

    An order isomorphism between an unbounded set of ordinals and the ordinals.

    Equations
    Instances For