Mathlib.SetTheory.Ordinal.Enum

Ordinal.enumOrd definition

(s : Set Ordinal.{u}) (o : Ordinal.{u}) : Ordinal.{u}

Full source

/-- Enumerator function for an unbounded set of ordinals. -/
noncomputable def enumOrd (s : Set OrdinalOrdinal.{u}) (o : OrdinalOrdinal.{u}) : OrdinalOrdinal.{u} :=
  sInf (s ∩ { b | ∀ c, c < o → enumOrd s c < b })
termination_by o

Ordinal enumeration function

Informal description

The function `enumOrd` enumerates an unbounded set of ordinals $s$ by an ordinal $o$, returning the smallest ordinal in $s$ that is greater than all previously enumerated ordinals (those indexed by ordinals less than $o$). More precisely, for a given set $s$ of ordinals and an ordinal $o$, `enumOrd s o` is defined as the infimum of the intersection of $s$ with the set of ordinals $b$ such that for all $c < o$, `enumOrd s c < b`.

Ordinal.enumOrd_le_of_forall_lt theorem

(ha : a ∈ s) (H : ∀ b < o, enumOrd s b < a) : enumOrd s o ≤ a

Full source

theorem enumOrd_le_of_forall_lt (ha : a ∈ s) (H : ∀ b < o, enumOrd s b < a) : enumOrd s o ≤ a := by
  rw [enumOrd]
  exact csInf_le' ⟨ha, H⟩

Upper Bound Property for Ordinal Enumeration

Informal description

For any ordinal $a$ in an unbounded set $s$ of ordinals and any ordinal $o$, if for all ordinals $b < o$ we have $\text{enumOrd}(s, b) < a$, then $\text{enumOrd}(s, o) \leq a$.

Ordinal.enumOrd_mem theorem

(hs : ¬BddAbove s) (o : Ordinal) : enumOrd s o ∈ s

Full source

theorem enumOrd_mem (hs : ¬ BddAbove s) (o : Ordinal) : enumOrdenumOrd s o ∈ s :=
  (enumOrd_mem_aux hs o).1

Membership Property of Ordinal Enumeration for Unbounded Sets

Informal description

For any unbounded set $s$ of ordinals (i.e., $s$ is not bounded above) and any ordinal $o$, the ordinal $\text{enumOrd}(s)(o)$ belongs to $s$.

Ordinal.enumOrd_strictMono theorem

(hs : ¬BddAbove s) : StrictMono (enumOrd s)

Full source

theorem enumOrd_strictMono (hs : ¬ BddAbove s) : StrictMono (enumOrd s) :=
  fun a b ↦ (enumOrd_mem_aux hs b).2 a

Strict Monotonicity of Ordinal Enumeration Function for Unbounded Sets

Informal description

For any unbounded set $s$ of ordinals (i.e., $\neg\text{BddAbove}(s)$), the enumeration function $\text{enumOrd}(s)$ is strictly monotonic. That is, for any ordinals $a$ and $b$, if $a < b$ then $\text{enumOrd}(s)(a) < \text{enumOrd}(s)(b)$.

Ordinal.enumOrd_injective theorem

(hs : ¬BddAbove s) : Function.Injective (enumOrd s)

Full source

theorem enumOrd_injective (hs : ¬ BddAbove s) : Function.Injective (enumOrd s) :=
  (enumOrd_strictMono hs).injective

Injectivity of Ordinal Enumeration for Unbounded Sets

Informal description

For any unbounded set $s$ of ordinals (i.e., $s$ is not bounded above), the enumeration function $\text{enumOrd}(s)$ is injective. That is, for any ordinals $a$ and $b$, if $\text{enumOrd}(s)(a) = \text{enumOrd}(s)(b)$, then $a = b$.

Ordinal.enumOrd_inj theorem

(hs : ¬BddAbove s) {a b : Ordinal} : enumOrd s a = enumOrd s b ↔ a = b

Full source

theorem enumOrd_inj (hs : ¬ BddAbove s) {a b : Ordinal} : enumOrdenumOrd s a = enumOrd s b ↔ a = b :=
  (enumOrd_injective hs).eq_iff

Bijective Correspondence of Ordinal Enumeration for Unbounded Sets

Informal description

For any unbounded set $s$ of ordinals (i.e., $s$ is not bounded above), and for any ordinals $a$ and $b$, the enumeration $\text{enumOrd}(s)(a)$ equals $\text{enumOrd}(s)(b)$ if and only if $a = b$.

Ordinal.enumOrd_le_enumOrd theorem

(hs : ¬BddAbove s) {a b : Ordinal} : enumOrd s a ≤ enumOrd s b ↔ a ≤ b

Full source

theorem enumOrd_le_enumOrd (hs : ¬ BddAbove s) {a b : Ordinal} :
    enumOrdenumOrd s a ≤ enumOrd s b ↔ a ≤ b :=
  (enumOrd_strictMono hs).le_iff_le

Order-Preserving Property of Ordinal Enumeration for Unbounded Sets

Informal description

For any unbounded set $s$ of ordinals (i.e., $s$ is not bounded above), and for any ordinals $a$ and $b$, the enumeration $\text{enumOrd}(s)(a)$ is less than or equal to $\text{enumOrd}(s)(b)$ if and only if $a \leq b$.

Ordinal.enumOrd_lt_enumOrd theorem

(hs : ¬BddAbove s) {a b : Ordinal} : enumOrd s a < enumOrd s b ↔ a < b

Full source

theorem enumOrd_lt_enumOrd (hs : ¬ BddAbove s) {a b : Ordinal} :
    enumOrdenumOrd s a < enumOrd s b ↔ a < b :=
  (enumOrd_strictMono hs).lt_iff_lt

Strict Order-Preserving Property of Ordinal Enumeration for Unbounded Sets

Informal description

For any unbounded set $s$ of ordinals (i.e., $s$ is not bounded above), the enumeration function $\text{enumOrd}(s)$ satisfies $\text{enumOrd}(s)(a) < \text{enumOrd}(s)(b)$ if and only if $a < b$ for any ordinals $a$ and $b$.

Ordinal.id_le_enumOrd theorem

(hs : ¬BddAbove s) : id ≤ enumOrd s

Full source

theorem id_le_enumOrd (hs : ¬ BddAbove s) : id ≤ enumOrd s :=
  (enumOrd_strictMono hs).id_le

Identity is Bounded by Ordinal Enumeration for Unbounded Sets

Informal description

For any unbounded set $s$ of ordinals (i.e., $s$ has no upper bound), the enumeration function $\text{enumOrd}(s)$ dominates the identity function. That is, for every ordinal $a$, we have $a \leq \text{enumOrd}(s)(a)$.

Ordinal.le_enumOrd_self theorem

(hs : ¬BddAbove s) {a} : a ≤ enumOrd s a

Full source

theorem le_enumOrd_self (hs : ¬ BddAbove s) {a} : a ≤ enumOrd s a :=
  (enumOrd_strictMono hs).le_apply

Ordinal enumeration function dominates identity on unbounded sets

Informal description

For any unbounded set $s$ of ordinals (i.e., $s$ is not bounded above) and any ordinal $a$, we have $a \leq \text{enumOrd}(s)(a)$, where $\text{enumOrd}(s)$ is the ordinal enumeration function for $s$.

Ordinal.enumOrd_succ_le theorem

(hs : ¬BddAbove s) (ha : a ∈ s) (hb : enumOrd s b < a) : enumOrd s (succ b) ≤ a

Full source

theorem enumOrd_succ_le (hs : ¬ BddAbove s) (ha : a ∈ s) (hb : enumOrd s b < a) :
    enumOrd s (succ b) ≤ a := by
  apply enumOrd_le_of_forall_lt ha
  intro c hc
  rw [lt_succ_iff] at hc
  exact ((enumOrd_strictMono hs).monotone hc).trans_lt hb

Successor Enumeration Bound for Unbounded Ordinal Sets

Informal description

For any unbounded set $s$ of ordinals (i.e., $s$ is not bounded above), if $a \in s$ and $\text{enumOrd}(s, b) < a$ for some ordinal $b$, then $\text{enumOrd}(s, \text{succ}(b)) \leq a$.

Ordinal.range_enumOrd theorem

(hs : ¬BddAbove s) : range (enumOrd s) = s

Full source

theorem range_enumOrd (hs : ¬ BddAbove s) : range (enumOrd s) = s := by
  ext a
  let t := { b | a ≤ enumOrd s b }
  constructor
  · rintro ⟨b, rfl⟩
    exact enumOrd_mem hs b
  · intro ha
    refine ⟨sInf t, (enumOrd_le_of_forall_lt ha ?_).antisymm ?_⟩
    · intro b hb
      by_contra! hb'
      exact hb.not_le (csInf_le' hb')
    · exact csInf_mem (s := t) ⟨a, (enumOrd_strictMono hs).id_le a⟩

Range of Ordinal Enumeration Equals Unbounded Set

Informal description

For any unbounded set $s$ of ordinals (i.e., $s$ has no upper bound), the range of the enumeration function $\text{enumOrd}(s)$ is equal to $s$ itself. In other words, every ordinal in $s$ is enumerated by $\text{enumOrd}(s)$ at some ordinal index.

Ordinal.enumOrd_surjective theorem

(hs : ¬BddAbove s) {b : Ordinal} (hb : b ∈ s) : ∃ a, enumOrd s a = b

Full source

theorem enumOrd_surjective (hs : ¬ BddAbove s) {b : Ordinal} (hb : b ∈ s) :
    ∃ a, enumOrd s a = b := by
  rwa [← range_enumOrd hs] at hb

Surjectivity of Ordinal Enumeration for Unbounded Sets

Informal description

For any unbounded set $s$ of ordinals (i.e., $s$ is not bounded above) and any ordinal $b \in s$, there exists an ordinal $a$ such that $\text{enumOrd}(s, a) = b$. In other words, the enumeration function $\text{enumOrd}(s, \cdot)$ is surjective onto $s$ when $s$ is unbounded.

Ordinal.enumOrd_le_of_subset theorem

{t : Set Ordinal} (hs : ¬BddAbove s) (hst : s ⊆ t) : enumOrd t ≤ enumOrd s

Full source

theorem enumOrd_le_of_subset {t : Set Ordinal} (hs : ¬ BddAbove s) (hst : s ⊆ t) :
    enumOrd t ≤ enumOrd s := by
  intro a
  rw [enumOrd, enumOrd]
  apply csInf_le_csInf' (enumOrd_nonempty hs a) (inter_subset_inter hst _)
  intro b hb c hc
  exact (enumOrd_le_of_subset hs hst c).trans_lt <| hb c hc
termination_by a => a

Monotonicity of Ordinal Enumeration under Superset Inclusion

Informal description

For any unbounded set $s$ of ordinals and any superset $t$ of $s$ (i.e., $s \subseteq t$), the enumeration function satisfies $\text{enumOrd}_t \leq \text{enumOrd}_s$ pointwise. Here $\text{enumOrd}_s$ denotes the enumeration function for the set $s$.

Ordinal.enumOrd_range theorem

{f : Ordinal → Ordinal} (hf : StrictMono f) : enumOrd (range f) = f

Full source

theorem enumOrd_range {f : Ordinal → Ordinal} (hf : StrictMono f) : enumOrd (range f) = f :=
  (eq_enumOrd _ hf.not_bddAbove_range_of_wellFoundedLT).2 ⟨hf, rfl⟩

Enumeration of Range of Strictly Monotone Ordinal Function

Informal description

For any strictly monotone function $f \colon \mathrm{Ordinal} \to \mathrm{Ordinal}$, the enumeration function of its range equals $f$, i.e., $\mathrm{enumOrd}(\mathrm{range}(f)) = f$.

Ordinal.isNormal_enumOrd theorem

(H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s) (hs : ¬BddAbove s) : IsNormal (enumOrd s)

Full source

/-- If `s` is closed under nonempty suprema, then its enumerator function is normal.
See also `enumOrd_isNormal_iff_isClosed`. -/
theorem isNormal_enumOrd (H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s) (hs : ¬ BddAbove s) :
    IsNormal (enumOrd s) := by
  refine (isNormal_iff_strictMono_limit _).2 ⟨enumOrd_strictMono hs, fun o ho a ha ↦ ?_⟩
  trans ⨆ b : Iio o, enumOrd s b
  · refine enumOrd_le_of_forall_lt ?_ (fun b hb ↦ (enumOrd_strictMono hs (lt_succ b)).trans_le ?_)
    · have : Nonempty (Iio o) := ⟨0, ho.pos⟩
      apply H _ _ (range_nonempty _) (bddAbove_of_small _)
      rintro _ ⟨c, rfl⟩
      exact enumOrd_mem hs c
    · exact Ordinal.le_iSup _ (⟨_, ho.succ_lt hb⟩ : Iio o)
  · exact Ordinal.iSup_le fun x ↦ ha _ x.2

Normality of the Ordinal Enumeration Function for Closed Unbounded Sets

Informal description

Let $s$ be an unbounded set of ordinals (i.e., $\neg\text{BddAbove}(s)$) that is closed under nonempty suprema (i.e., for every nonempty subset $t \subseteq s$ that is bounded above, $\sup t \in s$). Then the enumeration function $\text{enumOrd}(s)$ is a normal function. Here, a normal function is a strictly increasing and continuous (i.e., preserves suprema of nonempty bounded sets) function on ordinals.

Ordinal.enumOrd_univ theorem

: enumOrd Set.univ = id

Full source

@[simp]
theorem enumOrd_univ : enumOrd Set.univ = id := by
  rw [← range_id]
  exact enumOrd_range strictMono_id

Enumeration of Universal Set of Ordinals is Identity

Informal description

The enumeration function for the universal set of ordinals is equal to the identity function, i.e., $\mathrm{enumOrd}(\mathrm{univ}) = \mathrm{id}$.

Ordinal.enumOrd_zero theorem

: enumOrd s 0 = sInf s

Full source

@[simp]
theorem enumOrd_zero : enumOrd s 0 = sInf s := by
  rw [enumOrd]
  simp [Ordinal.not_lt_zero]

Initial Enumeration of Ordinals: $\text{enumOrd}(s, 0) = \inf s$

Informal description

For any set $s$ of ordinals, the enumeration function evaluated at $0$ is equal to the infimum of $s$, i.e., $\text{enumOrd}(s, 0) = \inf s$.

Ordinal.enumOrdOrderIso definition

(s : Set Ordinal) (hs : ¬BddAbove s) : Ordinal ≃o s

Full source

/-- An order isomorphism between an unbounded set of ordinals and the ordinals. -/
noncomputable def enumOrdOrderIso (s : Set Ordinal) (hs : ¬ BddAbove s) : OrdinalOrdinal ≃o s :=
  StrictMono.orderIsoOfSurjective (fun o => ⟨_, enumOrd_mem hs o⟩) (enumOrd_strictMono hs) fun s =>
    let ⟨a, ha⟩ := enumOrd_surjective hs s.prop
    ⟨a, Subtype.eq ha⟩

Order isomorphism between ordinals and an unbounded set of ordinals

Informal description

Given an unbounded set $ s $ of ordinals (i.e., $ s $ is not bounded above), the function `enumOrdOrderIso` constructs an order isomorphism between the class of all ordinals and the set $ s $. More precisely, `enumOrdOrderIso s hs` is an order-preserving bijection $ f : \text{Ordinal} \to s $ such that for any ordinals $ a $ and $ b $, $ a \leq b $ if and only if $ f(a) \leq f(b) $. This isomorphism is constructed using the enumeration function `enumOrd`, which ensures that $ f $ is strictly monotonic and surjective onto $ s $.