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.

The definition is an implementation detail; this function is entirely characterized by being an order isomorphism. See enumOrdOrderIso.

Equations
Instances For
    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
    theorem Ordinal.isNormal_enumOrd {s : Set Ordinal.{u}} (H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s) (hs : ¬BddAbove s) :
    Order.IsNormal (enumOrd s)

    If s is closed under nonempty suprema, then its enumerator function is normal. See also enumOrd_isNormal_iff_isClosed.

    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