doc-next-gen

Mathlib.SetTheory.Cardinal.Cofinality

Module docstring

{"# Cofinality

This file contains the definition of cofinality of an order and an ordinal number.

Main Definitions

  • Order.cof r is the cofinality of a reflexive order. This is the smallest cardinality of a subset s that is cofinal, i.e. ∀ x, ∃ y ∈ s, r x y.
  • Ordinal.cof o is the cofinality of the ordinal o when viewed as a linear order.

Main Statements

  • Cardinal.lt_power_cof: A consequence of König's theorem stating that c < c ^ c.ord.cof for c ≥ ℵ₀.

Implementation Notes

  • The cofinality is defined for ordinals. If c is a cardinal number, its cofinality is c.ord.cof. ","### Cofinality of orders ","### Cofinality of ordinals ","### Cofinality of suprema and least strict upper bounds ","### Basic results ","### Fundamental sequences ","### Results on sets ","### Consequences of König's lemma "}
Order.cof definition
(r : α → α → Prop) : Cardinal
Full source 
/-- Cofinality of a reflexive order `≼`. This is the smallest cardinality
  of a subset `S : Set α` such that `∀ a, ∃ b ∈ S, a ≼ b`. -/
def cof (r : α → α → Prop) : Cardinal :=
  sInf { c | ∃ S : Set α, (∀ a, ∃ b ∈ S, r a b) ∧ #S = c }
Cofinality of an order
Informal description
The cofinality of a reflexive order $\preceq$ on a type $\alpha$ is the smallest cardinality of a subset $S \subseteq \alpha$ such that for every element $a \in \alpha$, there exists an element $b \in S$ with $a \preceq b$. Formally, it is defined as the infimum of the set of cardinals $\{ c \mid \exists S \subseteq \alpha, (\forall a \in \alpha, \exists b \in S, a \preceq b) \land \#S = c \}$.
Order.cof_le theorem
(r : α → α → Prop) {S : Set α} (h : ∀ a, ∃ b ∈ S, r a b) : cof r ≤ #S
Full source 
theorem cof_le (r : α → α → Prop) {S : Set α} (h : ∀ a, ∃ b ∈ S, r a b) : cof r ≤ #S :=
  csInf_le' ⟨S, h, rfl⟩
Cofinality is Bounded by Cardinality of Cofinal Subset
Informal description
For any reflexive order $\preceq$ on a type $\alpha$ and any subset $S \subseteq \alpha$ that is cofinal (i.e., for every $a \in \alpha$, there exists $b \in S$ such that $a \preceq b$), the cofinality of $\preceq$ is less than or equal to the cardinality of $S$. In symbols, $\mathrm{cof}(\preceq) \leq \#S$.
Order.le_cof theorem
[IsRefl α r] (c : Cardinal) : c ≤ cof r ↔ ∀ {S : Set α}, (∀ a, ∃ b ∈ S, r a b) → c ≤ #S
Full source 
theorem le_cof [IsRefl α r] (c : Cardinal) :
    c ≤ cof r ↔ ∀ {S : Set α}, (∀ a, ∃ b ∈ S, r a b) → c ≤ #S := by
  rw [cof, le_csInf_iff'' (cof_nonempty r)]
  use fun H S h => H _ ⟨S, h, rfl⟩
  rintro H d ⟨S, h, rfl⟩
  exact H h
Characterization of Cofinality via Cofinal Subsets
Informal description
Let $\preceq$ be a reflexive order on a type $\alpha$. A cardinal $c$ satisfies $c \leq \mathrm{cof}(\preceq)$ if and only if for every subset $S \subseteq \alpha$ that is cofinal in $\alpha$ (i.e., for every $a \in \alpha$ there exists $b \in S$ with $a \preceq b$), the cardinality of $S$ is at least $c$.
RelIso.cof_eq_lift theorem
[IsRefl β s] (f : r ≃r s) : Cardinal.lift.{v} (Order.cof r) = Cardinal.lift.{u} (Order.cof s)
Full source 
theorem cof_eq_lift [IsRefl β s] (f : r ≃r s) :
    Cardinal.lift.{v} (Order.cof r) = Cardinal.lift.{u} (Order.cof s) :=
  have := f.toRelEmbedding.isRefl
  (f.cof_le_lift).antisymm (f.symm.cof_le_lift)
Cofinality Preservation under Relation Isomorphism with Universe Lifting
Informal description
Let $r$ be a reflexive relation on a type $\alpha$ and $s$ a reflexive relation on a type $\beta$. Given a relation isomorphism $f : r \simeq s$, the cofinality of $r$ (lifted to universe $\max(u,v)$) equals the cofinality of $s$ (lifted to universe $\max(u,v)$). In other words, $\text{lift}(\text{cof}(r)) = \text{lift}(\text{cof}(s))$.
RelIso.cof_eq theorem
{α β : Type u} {r : α → α → Prop} {s} [IsRefl β s] (f : r ≃r s) : Order.cof r = Order.cof s
Full source 
theorem cof_eq {α β : Type u} {r : α → α → Prop} {s} [IsRefl β s] (f : r ≃r s) :
    Order.cof r = Order.cof s :=
  lift_inj.1 (f.cof_eq_lift)
Cofinality Preservation under Relation Isomorphism
Informal description
Let $\alpha$ and $\beta$ be types in the same universe, equipped with reflexive relations $r$ and $s$ respectively. Given a relation isomorphism $f : r \simeq s$ between these relations, the cofinality of $r$ equals the cofinality of $s$.
Ordinal.cof definition
(o : Ordinal.{u}) : Cardinal.{u}
Full source 
/-- Cofinality of an ordinal. This is the smallest cardinal of a subset `S` of the ordinal which is
unbounded, in the sense `∀ a, ∃ b ∈ S, a ≤ b`.

In particular, `cof 0 = 0` and `cof (succ o) = 1`. -/
def cof (o : OrdinalOrdinal.{u}) : CardinalCardinal.{u} :=
  o.liftOn (fun a ↦ Order.cof (swap a.rᶜ)) fun _ _ ⟨f⟩ ↦ f.compl.swap.cof_eq
Cofinality of an ordinal
Informal description
The cofinality of an ordinal $o$ is the smallest cardinality of a subset $S \subseteq o$ that is unbounded in $o$, meaning for every $a \in o$, there exists $b \in S$ with $a \leq b$. Specifically: - The cofinality of $0$ is $0$ - The cofinality of any successor ordinal $\operatorname{succ}(o)$ is $1$
Ordinal.cof_type theorem
(r : α → α → Prop) [IsWellOrder α r] : (type r).cof = Order.cof (swap rᶜ)
Full source 
theorem cof_type (r : α → α → Prop) [IsWellOrder α r] : (type r).cof = Order.cof (swap rᶜ) :=
  rfl
Cofinality of Ordinal Type Equals Cofinality of Complemented Swapped Relation
Informal description
For any well-order relation $r$ on a type $\alpha$, the cofinality of the ordinal type of $r$ is equal to the cofinality of the complement of the swapped relation $r^{\complement}$ (where $r^{\complement}$ denotes the complement of $r$).
Ordinal.cof_type_lt theorem
[LinearOrder α] [IsWellOrder α (· < ·)] : (@type α (· < ·) _).cof = @Order.cof α (· ≤ ·)
Full source 
theorem cof_type_lt [LinearOrder α] [IsWellOrder α (· < ·)] :
    (@type α (· < ·) _).cof = @Order.cof α (· ≤ ·) := by
  rw [cof_type, compl_lt, swap_ge]
Cofinality of Ordinal Type for Strict Order Equals Cofinality of Non-Strict Order
Informal description
For any linearly ordered type $\alpha$ where the strict less-than relation $<$ is a well-order, the cofinality of the ordinal type of $(\alpha, <)$ is equal to the cofinality of the non-strict order $(\alpha, \leq)$.
Ordinal.cof_eq_cof_toType theorem
(o : Ordinal) : o.cof = @Order.cof o.toType (· ≤ ·)
Full source 
theorem cof_eq_cof_toType (o : Ordinal) : o.cof = @Order.cof o.toType (· ≤ ·) := by
  conv_lhs => rw [← type_toType o, cof_type_lt]
Cofinality of Ordinal Equals Cofinality of Underlying Order
Informal description
For any ordinal number $o$, the cofinality of $o$ is equal to the cofinality of the order $(\alpha, \leq)$, where $\alpha$ is the underlying type of $o$ (i.e., $o.\mathrm{toType}$).
Ordinal.le_cof_type theorem
[IsWellOrder α r] {c} : c ≤ cof (type r) ↔ ∀ S, Unbounded r S → c ≤ #S
Full source 
theorem le_cof_type [IsWellOrder α r] {c} : c ≤ cof (type r) ↔ ∀ S, Unbounded r S → c ≤ #S :=
  (le_csInf_iff'' (Order.cof_nonempty _)).trans
    ⟨fun H S h => H _ ⟨S, h, rfl⟩, by
      rintro H d ⟨S, h, rfl⟩
      exact H _ h⟩
Characterization of Cofinality via Unbounded Subsets in Well-Orders
Informal description
Let $\alpha$ be a type equipped with a well-order relation $r$. For any cardinal number $c$, the inequality $c \leq \mathrm{cof}(\mathrm{type}\, r)$ holds if and only if for every subset $S \subseteq \alpha$ that is unbounded with respect to $r$, the cardinality of $S$ satisfies $c \leq \#S$.
Ordinal.cof_type_le theorem
[IsWellOrder α r] {S : Set α} (h : Unbounded r S) : cof (type r) ≤ #S
Full source 
theorem cof_type_le [IsWellOrder α r] {S : Set α} (h : Unbounded r S) : cof (type r) ≤ #S :=
  le_cof_type.1 le_rfl S h
Cofinality Bound via Unbounded Subsets in Well-Orders
Informal description
Let $\alpha$ be a type equipped with a well-order relation $r$. For any subset $S \subseteq \alpha$ that is unbounded with respect to $r$, the cofinality of the order type of $r$ is less than or equal to the cardinality of $S$, i.e., $\mathrm{cof}(\mathrm{type}\, r) \leq \#S$.
Ordinal.lt_cof_type theorem
[IsWellOrder α r] {S : Set α} : #S < cof (type r) → Bounded r S
Full source 
theorem lt_cof_type [IsWellOrder α r] {S : Set α} : #S < cof (type r) → Bounded r S := by
  simpa using not_imp_not.2 cof_type_le
Boundedness of Subsets with Cardinality Below Cofinality in Well-Orders
Informal description
Let $\alpha$ be a type equipped with a well-order relation $r$. For any subset $S \subseteq \alpha$, if the cardinality of $S$ is strictly less than the cofinality of the order type of $r$, then $S$ is bounded with respect to $r$.
Ordinal.cof_eq theorem
(r : α → α → Prop) [IsWellOrder α r] : ∃ S, Unbounded r S ∧ #S = cof (type r)
Full source 
theorem cof_eq (r : α → α → Prop) [IsWellOrder α r] : ∃ S, Unbounded r S ∧ #S = cof (type r) :=
  csInf_mem (Order.cof_nonempty (swap rᶜ))
Existence of Unbounded Subset with Cofinality Cardinality in Well-Orders
Informal description
For any well-order relation $r$ on a type $\alpha$, there exists a subset $S \subseteq \alpha$ that is unbounded with respect to $r$ and has cardinality equal to the cofinality of the order type of $r$. That is, $\exists S \subseteq \alpha, \text{Unbounded}(r, S) \land \#S = \mathrm{cof}(\mathrm{type}\, r)$.
Ordinal.ord_cof_eq theorem
(r : α → α → Prop) [IsWellOrder α r] : ∃ S, Unbounded r S ∧ type (Subrel r (· ∈ S)) = (cof (type r)).ord
Full source 
theorem ord_cof_eq (r : α → α → Prop) [IsWellOrder α r] :
    ∃ S, Unbounded r S ∧ type (Subrel r (· ∈ S)) = (cof (type r)).ord := by
  let ⟨S, hS, e⟩ := cof_eq r
  let ⟨s, _, e'⟩ := Cardinal.ord_eq S
  let T : Set α := { a | ∃ aS : a ∈ S, ∀ b : S, s b ⟨_, aS⟩ → r b a }
  suffices Unbounded r T by
    refine ⟨T, this, le_antisymm ?_ (Cardinal.ord_le.2 <| cof_type_le this)⟩
    rw [← e, e']
    refine
      (RelEmbedding.ofMonotone
          (fun a : T =>
            (⟨a,
                let ⟨aS, _⟩ := a.2
                aS⟩ :
              S))
          fun a b h => ?_).ordinal_type_le
    rcases a with ⟨a, aS, ha⟩
    rcases b with ⟨b, bS, hb⟩
    change s ⟨a, _⟩ ⟨b, _⟩
    refine ((trichotomous_of s _ _).resolve_left fun hn => ?_).resolve_left ?_
    · exact asymm h (ha _ hn)
    · intro e
      injection e with e
      subst b
      exact irrefl _ h
  intro a
  have : { b : S | ¬r b a }.Nonempty :=
    let ⟨b, bS, ba⟩ := hS a
    ⟨⟨b, bS⟩, ba⟩
  let b := (IsWellFounded.wf : WellFounded s).min _ this
  have ba : ¬r b a := IsWellFounded.wf.min_mem _ this
  refine ⟨b, ⟨b.2, fun c => not_imp_not.1 fun h => ?_⟩, ba⟩
  rw [show ∀ b : S, (⟨b, b.2⟩ : S) = b by intro b; cases b; rfl]
  exact IsWellFounded.wf.not_lt_min _ this (IsOrderConnected.neg_trans h ba)
Existence of Unbounded Subset with Cofinality Order Type in Well-Orders
Informal description
For any well-order relation $r$ on a type $\alpha$, there exists an unbounded subset $S \subseteq \alpha$ such that the order type of the restriction of $r$ to $S$ equals the ordinal corresponding to the cofinality of the order type of $r$.
Ordinal.cof_lsub_def_nonempty theorem
(o) : {a : Cardinal | ∃ (ι : _) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a}.Nonempty
Full source 
/-- The set in the `lsub` characterization of `cof` is nonempty. -/
theorem cof_lsub_def_nonempty (o) :
    { a : Cardinal | ∃ (ι : _) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a }.Nonempty :=
  ⟨_, card_mem_cof⟩
Nonemptiness of Cofinality Characterization via Least Strict Upper Bounds
Informal description
For any ordinal $o$, the set of cardinal numbers $a$ for which there exists a type $\iota$ and a function $f \colon \iota \to \text{Ordinal}$ such that the least strict upper bound (lsub) of $f$ is $o$ and the cardinality of $\iota$ is $a$, is nonempty.
Ordinal.cof_eq_sInf_lsub theorem
(o : Ordinal.{u}) : cof o = sInf {a : Cardinal | ∃ (ι : Type u) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a}
Full source 
theorem cof_eq_sInf_lsub (o : OrdinalOrdinal.{u}) : cof o =
    sInf { a : Cardinal | ∃ (ι : Type u) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a } := by
  refine le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)
  · rintro a ⟨ι, f, hf, rfl⟩
    rw [← type_toType o]
    refine
      (cof_type_le fun a => ?_).trans
        (@mk_le_of_injective _ _
          (fun s : typeintypein ((· < ·) : o.toType → o.toType → Prop) ⁻¹' Set.range f =>
            Classical.choose s.prop)
          fun s t hst => by
          let H := congr_arg f hst
          rwa [Classical.choose_spec s.prop, Classical.choose_spec t.prop, typein_inj,
            Subtype.coe_inj] at H)
    have := typein_lt_self a
    simp_rw [← hf, lt_lsub_iff] at this
    obtain ⟨i, hi⟩ := this
    refine ⟨enum (α := o.toType) (· < ·) ⟨f i, ?_⟩, ?_, ?_⟩
    · rw [type_toType, ← hf]
      apply lt_lsub
    · rw [mem_preimage, typein_enum]
      exact mem_range_self i
    · rwa [← typein_le_typein, typein_enum]
  · rcases cof_eq (α := o.toType) (· < ·) with ⟨S, hS, hS'⟩
    let f : S → Ordinal := fun s => typein LT.lt s.val
    refine ⟨S, f, le_antisymm (lsub_le fun i => typein_lt_self (o := o) i)
      (le_of_forall_lt fun a ha => ?_), by rwa [type_toType o] at hS'⟩
    rw [← type_toType o] at ha
    rcases hS (enum (· < ·) ⟨a, ha⟩) with ⟨b, hb, hb'⟩
    rw [← typein_le_typein, typein_enum] at hb'
    exact hb'.trans_lt (lt_lsub.{u, u} f ⟨b, hb⟩)
Cofinality as Infimum of Cardinalities for Least Strict Upper Bound Representations
Informal description
For any ordinal $o$, the cofinality $\mathrm{cof}(o)$ is equal to the infimum of the set of cardinal numbers $a$ for which there exists a type $\iota$ and a function $f \colon \iota \to \mathrm{Ordinal}$ such that the least strict upper bound of $f$ is $o$ and the cardinality of $\iota$ is $a$. In symbols: \[ \mathrm{cof}(o) = \inf \{a \mid \exists (\iota : \mathrm{Type}) (f : \iota \to \mathrm{Ordinal}), \mathrm{lsub}(f) = o \land \#\iota = a\} \]
Ordinal.lift_cof theorem
(o) : Cardinal.lift.{u, v} (cof o) = cof (Ordinal.lift.{u, v} o)
Full source 
@[simp]
theorem lift_cof (o) : Cardinal.lift.{u, v} (cof o) = cof (Ordinal.lift.{u, v} o) := by
  refine inductionOn o fun α r _ ↦ ?_
  rw [← type_uLift, cof_type, cof_type, ← Cardinal.lift_id'.{v, u} (Order.cof _),
    ← Cardinal.lift_umax]
  apply RelIso.cof_eq_lift ⟨Equiv.ulift.symm, _⟩
  simp [swap]
Cofinality Preservation under Ordinal Lifting: $\text{lift}(\text{cof}(o)) = \text{cof}(\text{lift}(o))$
Informal description
For any ordinal $o$, the cofinality of the lifted ordinal $\text{lift}_{u,v}(o)$ is equal to the lift of the cofinality of $o$, i.e., $\text{lift}_{u,v}(\text{cof}(o)) = \text{cof}(\text{lift}_{u,v}(o))$.
Ordinal.cof_le_card theorem
(o) : cof o ≤ card o
Full source 
theorem cof_le_card (o) : cof o ≤ card o := by
  rw [cof_eq_sInf_lsub]
  exact csInf_le' card_mem_cof
Cofinality Bound by Cardinality: $\mathrm{cof}(o) \leq \mathrm{card}(o)$
Informal description
For any ordinal $o$, the cofinality of $o$ is less than or equal to its cardinality, i.e., $\mathrm{cof}(o) \leq \mathrm{card}(o)$.
Ordinal.cof_ord_le theorem
(c : Cardinal) : c.ord.cof ≤ c
Full source 
theorem cof_ord_le (c : Cardinal) : c.ord.cof ≤ c := by simpa using cof_le_card c.ord
Cofinality Bound for Ordinal Associated to a Cardinal: $\mathrm{cof}(c.\mathrm{ord}) \leq c$
Informal description
For any cardinal number $c$, the cofinality of the ordinal associated to $c$ is less than or equal to $c$ itself, i.e., $\mathrm{cof}(c.\mathrm{ord}) \leq c$.
Ordinal.ord_cof_le theorem
(o : Ordinal.{u}) : o.cof.ord ≤ o
Full source 
theorem ord_cof_le (o : OrdinalOrdinal.{u}) : o.cof.ord ≤ o :=
  (ord_le_ord.2 (cof_le_card o)).trans (ord_card_le o)
Ordinal Bound for Cofinality: $\mathrm{ord}(\mathrm{cof}(o)) \leq o$
Informal description
For any ordinal $o$, the ordinal corresponding to the cofinality of $o$ is less than or equal to $o$ itself, i.e., $\mathrm{ord}(\mathrm{cof}(o)) \leq o$.
Ordinal.exists_lsub_cof theorem
(o : Ordinal) : ∃ (ι : _) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = cof o
Full source 
theorem exists_lsub_cof (o : Ordinal) :
    ∃ (ι : _) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = cof o := by
  rw [cof_eq_sInf_lsub]
  exact csInf_mem (cof_lsub_def_nonempty o)
Existence of Cofinal Sequence with Minimal Cardinality for Ordinals
Informal description
For every ordinal $o$, there exists a type $\iota$ and a function $f \colon \iota \to \text{Ordinal}$ such that the least strict upper bound of $f$ is $o$ and the cardinality of $\iota$ equals the cofinality of $o$. In symbols: \[ \forall o \in \text{Ordinal}, \exists (\iota : \text{Type}) (f : \iota \to \text{Ordinal}), \mathrm{lsub}(f) = o \land \#\iota = \mathrm{cof}(o) \]
Ordinal.cof_lsub_le theorem
{ι} (f : ι → Ordinal) : cof (lsub.{u, u} f) ≤ #ι
Full source 
theorem cof_lsub_le {ι} (f : ι → Ordinal) : cof (lsub.{u, u} f) ≤ #ι := by
  rw [cof_eq_sInf_lsub]
  exact csInf_le' ⟨ι, f, rfl, rfl⟩
Cofinality Bound for Least Strict Upper Bound of Ordinals
Informal description
For any family of ordinals $f : \iota \to \text{Ordinal}$ indexed by a type $\iota$, the cofinality of the least strict upper bound $\text{lsub}(f)$ is bounded above by the cardinality of $\iota$, i.e., $\text{cof}(\text{lsub}(f)) \leq \#\iota$.
Ordinal.cof_lsub_le_lift theorem
{ι} (f : ι → Ordinal) : cof (lsub.{u, v} f) ≤ Cardinal.lift.{v, u} #ι
Full source 
theorem cof_lsub_le_lift {ι} (f : ι → Ordinal) :
    cof (lsub.{u, v} f) ≤ Cardinal.lift.{v, u} #ι := by
  rw [← mk_uLiftmk_uLift.{u, v}]
  convert cof_lsub_le.{max u v} fun i : ULift.{v, u} ι => f i.down
  exact
    lsub_eq_of_range_eq.{u, max u v, max u v}
      (Set.ext fun x => ⟨fun ⟨i, hi⟩ => ⟨ULift.up.{v, u} i, hi⟩, fun ⟨i, hi⟩ => ⟨_, hi⟩⟩)
Cofinality Bound for Lifted Least Strict Upper Bound of Ordinals
Informal description
For any family of ordinals $f : \iota \to \text{Ordinal}$ indexed by a type $\iota$, the cofinality of the least strict upper bound $\text{lsub}(f)$ is bounded above by the lift of the cardinality of $\iota$ to the appropriate universe, i.e., $\text{cof}(\text{lsub}(f)) \leq \text{lift}(\#\iota)$.
Ordinal.le_cof_iff_lsub theorem
{o : Ordinal} {a : Cardinal} : a ≤ cof o ↔ ∀ {ι} (f : ι → Ordinal), lsub.{u, u} f = o → a ≤ #ι
Full source 
theorem le_cof_iff_lsub {o : Ordinal} {a : Cardinal} :
    a ≤ cof o ↔ ∀ {ι} (f : ι → Ordinal), lsub.{u, u} f = o → a ≤ #ι := by
  rw [cof_eq_sInf_lsub]
  exact
    (le_csInf_iff'' (cof_lsub_def_nonempty o)).trans
      ⟨fun H ι f hf => H _ ⟨ι, f, hf, rfl⟩, fun H b ⟨ι, f, hf, hb⟩ => by
        rw [← hb]
        exact H _ hf⟩
Characterization of Cofinality via Least Strict Upper Bounds
Informal description
For an ordinal $o$ and a cardinal number $a$, we have $a \leq \mathrm{cof}(o)$ if and only if for every type $\iota$ and every function $f \colon \iota \to \mathrm{Ordinal}$ such that the least strict upper bound of $f$ is $o$, the cardinality of $\iota$ is at least $a$. In symbols: \[ a \leq \mathrm{cof}(o) \iff \forall (\iota : \mathrm{Type}) (f : \iota \to \mathrm{Ordinal}), \mathrm{lsub}(f) = o \to a \leq \#\iota \]
Ordinal.lsub_lt_ord_lift theorem
{ι} {f : ι → Ordinal} {c : Ordinal} (hι : Cardinal.lift.{v, u} #ι < c.cof) (hf : ∀ i, f i < c) : lsub.{u, v} f < c
Full source 
theorem lsub_lt_ord_lift {ι} {f : ι → Ordinal} {c : Ordinal}
    (hι : Cardinal.lift.{v, u} #ι < c.cof)
    (hf : ∀ i, f i < c) : lsub.{u, v} f < c :=
  lt_of_le_of_ne (lsub_le hf) fun h => by
    subst h
    exact (cof_lsub_le_lift.{u, v} f).not_lt hι
Least Strict Upper Bound is Bounded by Cofinality Condition
Informal description
For any family of ordinals $f : \iota \to \text{Ordinal}$ indexed by a type $\iota$ and any ordinal $c$, if the lift of the cardinality of $\iota$ is less than the cofinality of $c$ (i.e., $\text{lift}(\#\iota) < \text{cof}(c)$) and each $f(i) < c$, then the least strict upper bound $\text{lsub}(f)$ is also less than $c$.
Ordinal.lsub_lt_ord theorem
{ι} {f : ι → Ordinal} {c : Ordinal} (hι : #ι < c.cof) : (∀ i, f i < c) → lsub.{u, u} f < c
Full source 
theorem lsub_lt_ord {ι} {f : ι → Ordinal} {c : Ordinal} (hι : #ι < c.cof) :
    (∀ i, f i < c) → lsub.{u, u} f < c :=
  lsub_lt_ord_lift (by rwa [(#ι).lift_id])
Least Strict Upper Bound Condition for Cofinality: $\text{lsub}(f) < c$ when $\#\iota < \text{cof}(c)$ and $f_i < c$ for all $i$
Informal description
For any family of ordinals $\{f_i\}_{i \in \iota}$ indexed by a type $\iota$ and any ordinal $c$, if the cardinality of $\iota$ is less than the cofinality of $c$ (i.e., $\#\iota < \text{cof}(c)$) and each $f_i < c$, then the least strict upper bound $\text{lsub}(f)$ is also less than $c$.
Ordinal.cof_iSup_le_lift theorem
{ι} {f : ι → Ordinal} (H : ∀ i, f i < iSup f) : cof (iSup f) ≤ Cardinal.lift.{v, u} #ι
Full source 
theorem cof_iSup_le_lift {ι} {f : ι → Ordinal} (H : ∀ i, f i < iSup f) :
    cof (iSup f) ≤ Cardinal.lift.{v, u} #ι := by
  rw [← Ordinal.sup] at *
  rw [← sup_eq_lsub_iff_lt_sup.{u, v}] at H
  rw [H]
  exact cof_lsub_le_lift f
Cofinality Bound for Supremum of Ordinals: $\text{cof}(\bigsqcup_i f_i) \leq \text{lift}(\#\iota)$
Informal description
For any family of ordinals $\{f_i\}_{i \in \iota}$ indexed by a type $\iota$, if each $f_i$ is strictly less than the supremum $\bigsqcup_{i \in \iota} f_i$, then the cofinality of $\bigsqcup_{i \in \iota} f_i$ is bounded above by the lift of the cardinality of $\iota$ to the appropriate universe, i.e., \[ \text{cof}\left(\bigsqcup_{i \in \iota} f_i\right) \leq \text{lift}(\#\iota). \]
Ordinal.cof_iSup_le theorem
{ι} {f : ι → Ordinal} (H : ∀ i, f i < iSup f) : cof (iSup f) ≤ #ι
Full source 
theorem cof_iSup_le {ι} {f : ι → Ordinal} (H : ∀ i, f i < iSup f) :
    cof (iSup f) ≤ #ι := by
  rw [← (#ι).lift_id]
  exact cof_iSup_le_lift H
Cofinality Bound for Supremum of Ordinals: $\text{cof}(\bigsqcup_i f_i) \leq \#\iota$
Informal description
For any family of ordinals $\{f_i\}_{i \in \iota}$ indexed by a type $\iota$, if each $f_i$ is strictly less than the supremum $\bigsqcup_{i \in \iota} f_i$, then the cofinality of $\bigsqcup_{i \in \iota} f_i$ is bounded above by the cardinality of $\iota$, i.e., \[ \text{cof}\left(\bigsqcup_{i \in \iota} f_i\right) \leq \#\iota. \]
Ordinal.iSup_lt_ord_lift theorem
{ι} {f : ι → Ordinal} {c : Ordinal} (hι : Cardinal.lift.{v, u} #ι < c.cof) (hf : ∀ i, f i < c) : iSup f < c
Full source 
theorem iSup_lt_ord_lift {ι} {f : ι → Ordinal} {c : Ordinal} (hι : Cardinal.lift.{v, u} #ι < c.cof)
    (hf : ∀ i, f i < c) : iSup f < c :=
  (sup_le_lsub.{u, v} f).trans_lt (lsub_lt_ord_lift hι hf)
Supremum Bounded by Cofinality Condition (Lifted Universe Version)
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of ordinals indexed by a type $\iota$, and let $c$ be an ordinal. If the lift of the cardinality of $\iota$ is less than the cofinality of $c$ (i.e., $\text{lift}(\#\iota) < \text{cof}(c)$) and each $f_i < c$, then the supremum $\bigsqcup_{i \in \iota} f_i$ is also less than $c$.
Ordinal.iSup_lt_ord theorem
{ι} {f : ι → Ordinal} {c : Ordinal} (hι : #ι < c.cof) : (∀ i, f i < c) → iSup f < c
Full source 
theorem iSup_lt_ord {ι} {f : ι → Ordinal} {c : Ordinal} (hι : #ι < c.cof) :
    (∀ i, f i < c) → iSup f < c :=
  iSup_lt_ord_lift (by rwa [(#ι).lift_id])
Supremum Bounded by Cofinality Condition
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of ordinals indexed by a type $\iota$, and let $c$ be an ordinal. If the cardinality of $\iota$ is less than the cofinality of $c$ (i.e., $\#\iota < \text{cof}(c)$) and each $f_i < c$, then the supremum $\bigsqcup_{i \in \iota} f_i$ is also less than $c$.
Ordinal.iSup_lt_lift theorem
{ι} {f : ι → Cardinal} {c : Cardinal} (hι : Cardinal.lift.{v, u} #ι < c.ord.cof) (hf : ∀ i, f i < c) : iSup f < c
Full source 
theorem iSup_lt_lift {ι} {f : ι → Cardinal} {c : Cardinal}
    (hι : Cardinal.lift.{v, u} #ι < c.ord.cof)
    (hf : ∀ i, f i < c) : iSup f < c := by
  rw [← ord_lt_ord, iSup_ord (Cardinal.bddAbove_range _)]
  refine iSup_lt_ord_lift hι fun i => ?_
  rw [ord_lt_ord]
  apply hf
Supremum of Cardinals Bounded by Cofinality (Lifted Universe Version)
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of cardinal numbers indexed by a type $\iota$, and let $c$ be a cardinal number. If the lift of the cardinality of $\iota$ is less than the cofinality of the ordinal associated with $c$ (i.e., $\text{lift}(\#\iota) < \text{cof}(c.\text{ord})$) and each $f_i < c$, then the supremum $\bigsqcup_{i \in \iota} f_i$ is also less than $c$.
Ordinal.iSup_lt theorem
{ι} {f : ι → Cardinal} {c : Cardinal} (hι : #ι < c.ord.cof) : (∀ i, f i < c) → iSup f < c
Full source 
theorem iSup_lt {ι} {f : ι → Cardinal} {c : Cardinal} (hι : #ι < c.ord.cof) :
    (∀ i, f i < c) → iSup f < c :=
  iSup_lt_lift (by rwa [(#ι).lift_id])
Supremum of Cardinals Bounded by Cofinality Condition
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of cardinal numbers indexed by a type $\iota$, and let $c$ be a cardinal number. If the cardinality of $\iota$ is less than the cofinality of the ordinal associated with $c$ (i.e., $\#\iota < \text{cof}(c.\text{ord})$) and each $f_i < c$, then the supremum $\bigsqcup_{i \in \iota} f_i$ is also less than $c$.
Ordinal.nfpFamily_lt_ord_lift theorem
{ι} {f : ι → Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hc' : Cardinal.lift.{v, u} #ι < cof c) (hf : ∀ (i), ∀ b < c, f i b < c) {a} (ha : a < c) : nfpFamily f a < c
Full source 
theorem nfpFamily_lt_ord_lift {ι} {f : ι → Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c)
    (hc' : Cardinal.lift.{v, u} #ι < cof c) (hf : ∀ (i), ∀ b < c, f i b < c) {a} (ha : a < c) :
    nfpFamily f a < c := by
  refine iSup_lt_ord_lift ((Cardinal.lift_le.2 (mk_list_le_max ι)).trans_lt ?_) fun l => ?_
  · rw [lift_max]
    apply max_lt _ hc'
    rwa [Cardinal.lift_aleph0]
  · induction' l with i l H
    · exact ha
    · exact hf _ _ H
Next Fixed Point of Family of Ordinal Functions is Bounded by Cofinality (Lifted Universe Version)
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of ordinal functions indexed by a type $\iota$, and let $c$ be an ordinal with cofinality greater than $\aleph_0$. If the lift of the cardinality of $\iota$ is less than the cofinality of $c$ (i.e., $\text{lift}(\#\iota) < \text{cof}(c)$) and for every $i \in \iota$ and every ordinal $b < c$, we have $f_i(b) < c$, then for any ordinal $a < c$, the next fixed point of the family $\text{nfpFamily}(f, a)$ is also less than $c$.
Ordinal.nfpFamily_lt_ord theorem
{ι} {f : ι → Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hc' : #ι < cof c) (hf : ∀ (i), ∀ b < c, f i b < c) {a} : a < c → nfpFamily.{u, u} f a < c
Full source 
theorem nfpFamily_lt_ord {ι} {f : ι → Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hc' : #ι < cof c)
    (hf : ∀ (i), ∀ b < c, f i b < c) {a} : a < c → nfpFamily.{u, u} f a < c :=
  nfpFamily_lt_ord_lift hc (by rwa [(#ι).lift_id]) hf
Next Fixed Point of Family of Ordinal Functions is Bounded by Cofinality
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of ordinal functions indexed by a type $\iota$, and let $c$ be an ordinal with cofinality greater than $\aleph_0$. If the cardinality of $\iota$ is less than the cofinality of $c$ (i.e., $\#\iota < \text{cof}(c)$) and for every $i \in \iota$ and every ordinal $b < c$, we have $f_i(b) < c$, then for any ordinal $a < c$, the next fixed point of the family $\text{nfpFamily}(f, a)$ is also less than $c$.
Ordinal.nfp_lt_ord theorem
{f : Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hf : ∀ i < c, f i < c) {a} : a < c → nfp f a < c
Full source 
theorem nfp_lt_ord {f : Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hf : ∀ i < c, f i < c) {a} :
    a < c → nfp f a < c :=
  nfpFamily_lt_ord_lift hc (by simpa using Cardinal.one_lt_aleph0.trans hc) fun _ => hf
Next Fixed Point of Ordinal Function is Bounded by Cofinality
Informal description
Let $f$ be a function from ordinals to ordinals, and let $c$ be an ordinal with cofinality greater than $\aleph_0$. If for every ordinal $i < c$, we have $f(i) < c$, then for any ordinal $a < c$, the next fixed point of $f$ starting from $a$ (denoted $\text{nfp}(f, a)$) is also less than $c$.
Ordinal.exists_blsub_cof theorem
(o : Ordinal) : ∃ f : ∀ a < (cof o).ord, Ordinal, blsub.{u, u} _ f = o
Full source 
theorem exists_blsub_cof (o : Ordinal) :
    ∃ f : ∀ a < (cof o).ord, Ordinal, blsub.{u, u} _ f = o := by
  rcases exists_lsub_cof o with ⟨ι, f, hf, hι⟩
  rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩
  rw [← @blsub_eq_lsub' ι r hr] at hf
  rw [← hι, hι']
  exact ⟨_, hf⟩
Existence of Cofinal Bounded Supremum Family for Ordinals
Informal description
For every ordinal $o$, there exists a family of ordinals indexed by the initial segment of the cofinality of $o$ (i.e., by all ordinals $a < (\mathrm{cof}\,o).\mathrm{ord}$) such that the bounded supremum of this family equals $o$. In symbols: \[ \forall o \in \mathrm{Ordinal}, \exists (f : \{a \mid a < (\mathrm{cof}\,o).\mathrm{ord}\} \to \mathrm{Ordinal}), \mathrm{blsub}\,f = o \]
Ordinal.le_cof_iff_blsub theorem
{b : Ordinal} {a : Cardinal} : a ≤ cof b ↔ ∀ {o} (f : ∀ a < o, Ordinal), blsub.{u, u} o f = b → a ≤ o.card
Full source 
theorem le_cof_iff_blsub {b : Ordinal} {a : Cardinal} :
    a ≤ cof b ↔ ∀ {o} (f : ∀ a < o, Ordinal), blsub.{u, u} o f = b → a ≤ o.card :=
  le_cof_iff_lsub.trans
    ⟨fun H o f hf => by simpa using H _ hf, fun H ι f hf => by
      rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩
      rw [← @blsub_eq_lsub' ι r hr] at hf
      simpa using H _ hf⟩
Characterization of Cofinality via Bounded Suprema
Informal description
For an ordinal $b$ and a cardinal $a$, the inequality $a \leq \mathrm{cof}(b)$ holds if and only if for every ordinal $o$ and every family of ordinals $f$ indexed by elements of $o$ (i.e., $f : \{a \mid a < o\} \to \mathrm{Ordinal}$), if the bounded supremum of $f$ equals $b$ (i.e., $\mathrm{blsub}(f) = b$), then the cardinality of $o$ is at least $a$ (i.e., $a \leq \mathrm{card}(o)$). In symbols: \[ a \leq \mathrm{cof}(b) \iff \forall o \in \mathrm{Ordinal}, \forall f \colon \{a \mid a < o\} \to \mathrm{Ordinal}, \mathrm{blsub}(f) = b \implies a \leq \mathrm{card}(o). \]
Ordinal.cof_blsub_le_lift theorem
{o} (f : ∀ a < o, Ordinal) : cof (blsub.{u, v} o f) ≤ Cardinal.lift.{v, u} o.card
Full source 
theorem cof_blsub_le_lift {o} (f : ∀ a < o, Ordinal) :
    cof (blsub.{u, v} o f) ≤ Cardinal.lift.{v, u} o.card := by
  rw [← mk_toType o]
  exact cof_lsub_le_lift _
Cofinality Bound for Bounded Supremum: $\mathrm{cof}(\mathrm{blsub}(f)) \leq \mathrm{lift}(\#o)$
Informal description
For any ordinal $o$ and any family of ordinals $f$ indexed by elements $a < o$, the cofinality of the bounded supremum $\mathrm{blsub}(f)$ is bounded above by the lift of the cardinality of $o$ to the appropriate universe level. In symbols: \[ \mathrm{cof}(\mathrm{blsub}(f)) \leq \mathrm{lift}(\#o) \] where $\#o$ denotes the cardinality of $o$.
Ordinal.cof_blsub_le theorem
{o} (f : ∀ a < o, Ordinal) : cof (blsub.{u, u} o f) ≤ o.card
Full source 
theorem cof_blsub_le {o} (f : ∀ a < o, Ordinal) : cof (blsub.{u, u} o f) ≤ o.card := by
  rw [← o.card.lift_id]
  exact cof_blsub_le_lift f
Cofinality Bound for Bounded Supremum: $\mathrm{cof}(\mathrm{blsub}(f)) \leq \#o$
Informal description
For any ordinal $o$ and any family of ordinals $f$ indexed by elements $a < o$, the cofinality of the bounded supremum $\mathrm{blsub}(f)$ is bounded above by the cardinality of $o$. In symbols: \[ \mathrm{cof}(\mathrm{blsub}(f)) \leq \#o \] where $\#o$ denotes the cardinality of $o$.
Ordinal.blsub_lt_ord_lift theorem
{o : Ordinal.{u}} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ i hi, f i hi < c) : blsub.{u, v} o f < c
Full source 
theorem blsub_lt_ord_lift {o : OrdinalOrdinal.{u}} {f : ∀ a < o, Ordinal} {c : Ordinal}
    (ho : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ i hi, f i hi < c) : blsub.{u, v} o f < c :=
  lt_of_le_of_ne (blsub_le hf) fun h =>
    ho.not_le (by simpa [← iSup_ord, hf, h] using cof_blsub_le_lift.{u, v} f)
Bounded Supremum Bound under Cofinality Condition: $\mathrm{blsub}(f) < c$ when $\mathrm{lift}(\#o) < \mathrm{cof}(c)$
Informal description
Let $o$ be an ordinal and $f$ a family of ordinals indexed by elements $a < o$. If the lift of the cardinality of $o$ is strictly less than the cofinality of an ordinal $c$ (i.e., $\mathrm{lift}(\#o) < \mathrm{cof}(c)$) and each $f(a) < c$ for all $a < o$, then the bounded supremum $\mathrm{blsub}(f)$ is strictly less than $c$.
Ordinal.blsub_lt_ord theorem
{o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : o.card < c.cof) (hf : ∀ i hi, f i hi < c) : blsub.{u, u} o f < c
Full source 
theorem blsub_lt_ord {o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : o.card < c.cof)
    (hf : ∀ i hi, f i hi < c) : blsub.{u, u} o f < c :=
  blsub_lt_ord_lift (by rwa [o.card.lift_id]) hf
Bounded Supremum Bound: $\mathrm{blsub}(f) < c$ when $\#o < \mathrm{cof}(c)$
Informal description
Let $o$ be an ordinal and $f$ a family of ordinals indexed by elements $a < o$. If the cardinality of $o$ is strictly less than the cofinality of an ordinal $c$ (i.e., $\#o < \mathrm{cof}(c)$) and each $f(a) < c$ for all $a < o$, then the bounded supremum $\mathrm{blsub}(f)$ is strictly less than $c$.
Ordinal.cof_bsup_le_lift theorem
{o : Ordinal} {f : ∀ a < o, Ordinal} (H : ∀ i h, f i h < bsup.{u, v} o f) : cof (bsup.{u, v} o f) ≤ Cardinal.lift.{v, u} o.card
Full source 
theorem cof_bsup_le_lift {o : Ordinal} {f : ∀ a < o, Ordinal} (H : ∀ i h, f i h < bsup.{u, v} o f) :
    cof (bsup.{u, v} o f) ≤ Cardinal.lift.{v, u} o.card := by
  rw [← bsup_eq_blsub_iff_lt_bsup.{u, v}] at H
  rw [H]
  exact cof_blsub_le_lift.{u, v} f
Cofinality Bound for Supremum: $\mathrm{cof}(\mathrm{bsup}(f)) \leq \mathrm{lift}(\#o)$
Informal description
For any ordinal $o$ and any family of ordinals $f$ indexed by elements $a < o$, if each $f(a) < \mathrm{bsup}(f)$ (where $\mathrm{bsup}(f)$ is the supremum of the family $f$), then the cofinality of $\mathrm{bsup}(f)$ is bounded above by the lift of the cardinality of $o$ to the appropriate universe level. In symbols: \[ \mathrm{cof}(\mathrm{bsup}(f)) \leq \mathrm{lift}(\#o) \] where $\#o$ denotes the cardinality of $o$.
Ordinal.cof_bsup_le theorem
{o : Ordinal} {f : ∀ a < o, Ordinal} : (∀ i h, f i h < bsup.{u, u} o f) → cof (bsup.{u, u} o f) ≤ o.card
Full source 
theorem cof_bsup_le {o : Ordinal} {f : ∀ a < o, Ordinal} :
    (∀ i h, f i h < bsup.{u, u} o f) → cof (bsup.{u, u} o f) ≤ o.card := by
  rw [← o.card.lift_id]
  exact cof_bsup_le_lift
Cofinality Bound for Supremum: $\mathrm{cof}(\mathrm{bsup}(f)) \leq \#o$
Informal description
For any ordinal $o$ and any family of ordinals $f$ indexed by elements $a < o$, if each $f(a) < \mathrm{bsup}(f)$ (where $\mathrm{bsup}(f)$ is the supremum of the family $f$), then the cofinality of $\mathrm{bsup}(f)$ is bounded above by the cardinality of $o$. In symbols: \[ \mathrm{cof}(\mathrm{bsup}(f)) \leq \#o \] where $\#o$ denotes the cardinality of $o$.
Ordinal.bsup_lt_ord_lift theorem
{o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ i hi, f i hi < c) : bsup.{u, v} o f < c
Full source 
theorem bsup_lt_ord_lift {o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal}
    (ho : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ i hi, f i hi < c) : bsup.{u, v} o f < c :=
  (bsup_le_blsub f).trans_lt (blsub_lt_ord_lift ho hf)
Bounded Supremum Bound under Cofinality Condition: $\mathrm{bsup}(f) < c$ when $\mathrm{lift}(\#o) < \mathrm{cof}(c)$
Informal description
Let $o$ be an ordinal and $f$ a family of ordinals indexed by elements $a < o$. If the lift of the cardinality of $o$ is strictly less than the cofinality of an ordinal $c$ (i.e., $\mathrm{lift}(\#o) < \mathrm{cof}(c)$) and each $f(a) < c$ for all $a < o$, then the bounded supremum $\mathrm{bsup}(f)$ is strictly less than $c$.
Ordinal.bsup_lt_ord theorem
{o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : o.card < c.cof) : (∀ i hi, f i hi < c) → bsup.{u, u} o f < c
Full source 
theorem bsup_lt_ord {o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : o.card < c.cof) :
    (∀ i hi, f i hi < c) → bsup.{u, u} o f < c :=
  bsup_lt_ord_lift (by rwa [o.card.lift_id])
Bounded Supremum Bound: $\mathrm{bsup}(f) < c$ when $\#o < \mathrm{cof}(c)$
Informal description
Let $o$ be an ordinal and $f$ a family of ordinals indexed by elements $a < o$. If the cardinality of $o$ is strictly less than the cofinality of an ordinal $c$ (i.e., $\#o < \mathrm{cof}(c)$) and each $f(a) < c$ for all $a < o$, then the bounded supremum $\mathrm{bsup}(f)$ is strictly less than $c$.
Ordinal.cof_eq_zero theorem
{o} : cof o = 0 ↔ o = 0
Full source 
@[simp]
theorem cof_eq_zero {o} : cofcof o = 0 ↔ o = 0 :=
  ⟨inductionOn o fun _ r _ z =>
      let ⟨_, hl, e⟩ := cof_eq r
      type_eq_zero_iff_isEmpty.2 <|
        ⟨fun a =>
          let ⟨_, h, _⟩ := hl a
          (mk_eq_zero_iff.1 (e.trans z)).elim' ⟨_, h⟩⟩,
    fun e => by simp [e]⟩
Characterization of Zero Cofinality: $\mathrm{cof}(o) = 0 \leftrightarrow o = 0$
Informal description
For any ordinal $o$, the cofinality of $o$ is zero if and only if $o$ is the zero ordinal. In other words, $\mathrm{cof}(o) = 0 \leftrightarrow o = 0$.
Ordinal.cof_ne_zero theorem
{o} : cof o ≠ 0 ↔ o ≠ 0
Full source 
theorem cof_ne_zero {o} : cofcof o ≠ 0cof o ≠ 0 ↔ o ≠ 0 :=
  cof_eq_zero.not
Nonzero Cofinality Characterization: $\mathrm{cof}(o) \neq 0 \leftrightarrow o \neq 0$
Informal description
For any ordinal $o$, the cofinality of $o$ is nonzero if and only if $o$ is not the zero ordinal. In other words, $\mathrm{cof}(o) \neq 0 \leftrightarrow o \neq 0$.
Ordinal.cof_succ theorem
(o) : cof (succ o) = 1
Full source 
@[simp]
theorem cof_succ (o) : cof (succ o) = 1 := by
  apply le_antisymm
  · refine inductionOn o fun α r _ => ?_
    change cof (type _) ≤ _
    rw [← (_ : #_ = 1)]
    · apply cof_type_le
      refine fun a => ⟨Sum.inr PUnit.unit, Set.mem_singleton _, ?_⟩
      rcases a with (a | ⟨⟨⟨⟩⟩⟩) <;> simp [EmptyRelation]
    · rw [Cardinal.mk_fintype, Set.card_singleton]
      simp
  · rw [← Cardinal.succ_zero, succ_le_iff]
    simpa [lt_iff_le_and_ne, Cardinal.zero_le] using fun h =>
      succ_ne_zero o (cof_eq_zero.1 (Eq.symm h))
Cofinality of Successor Ordinals: $\mathrm{cof}(\operatorname{succ}(o)) = 1$
Informal description
For any ordinal $o$, the cofinality of the successor ordinal $\operatorname{succ}(o)$ is equal to $1$.
Ordinal.cof_eq_one_iff_is_succ theorem
{o} : cof.{u} o = 1 ↔ ∃ a, o = succ a
Full source 
@[simp]
theorem cof_eq_one_iff_is_succ {o} : cofcof.{u} o = 1 ↔ ∃ a, o = succ a :=
  ⟨inductionOn o fun α r _ z => by
      rcases cof_eq r with ⟨S, hl, e⟩; rw [z] at e
      obtain ⟨a⟩ := mk_ne_zero_iff.1 (by rw [e]; exact one_ne_zero)
      refine
        ⟨typein r a,
          Eq.symm <|
            Quotient.sound
              ⟨RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ fun x y => ?_) fun x => ?_⟩⟩
      · apply Sum.rec <;> [exact Subtype.val; exact fun _ => a]
      · rcases x with (x | ⟨⟨⟨⟩⟩⟩) <;> rcases y with (y | ⟨⟨⟨⟩⟩⟩) <;>
          simp [Subrel, Order.Preimage, EmptyRelation]
        exact x.2
      · suffices r x a ∨ ∃ _ : PUnit.{u}, ↑a = x by
          convert this
          dsimp [RelEmbedding.ofMonotone]; simp
        rcases trichotomous_of r x a with (h | h | h)
        · exact Or.inl h
        · exact Or.inr ⟨PUnit.unit, h.symm⟩
        · rcases hl x with ⟨a', aS, hn⟩
          refine absurd h ?_
          convert hn
          change (a : α) = ↑(⟨a', aS⟩ : S)
          have := le_one_iff_subsingleton.1 (le_of_eq e)
          congr!,
    fun ⟨a, e⟩ => by simp [e]⟩
Cofinality-One Characterization: $\mathrm{cof}(o) = 1 \leftrightarrow o$ is a successor ordinal
Informal description
For any ordinal $o$, the cofinality of $o$ is equal to $1$ if and only if $o$ is a successor ordinal, i.e., there exists an ordinal $a$ such that $o = \operatorname{succ}(a)$.
Ordinal.IsFundamentalSequence definition
(a o : Ordinal.{u}) (f : ∀ b < o, Ordinal.{u}) : Prop
Full source 
/-- A fundamental sequence for `a` is an increasing sequence of length `o = cof a` that converges at
    `a`. We provide `o` explicitly in order to avoid type rewrites. -/
def IsFundamentalSequence (a o : OrdinalOrdinal.{u}) (f : ∀ b < o, OrdinalOrdinal.{u}) : Prop :=
  o ≤ a.cof.ord ∧ (∀ {i j} (hi hj), i < j → f i hi < f j hj) ∧ blsub.{u, u} o f = a
Fundamental sequence for an ordinal
Informal description
A family of ordinals $(f_i)_{i < o}$ indexed by ordinals $i < o$ is called a *fundamental sequence* for an ordinal $a$ if: 1. The length $o$ is at most the cofinality of $a$ (as an ordinal). 2. The sequence is strictly increasing: for any $i < j < o$, we have $f_i < f_j$. 3. The sequence converges to $a$: the least strict upper bound of $\{f_i \mid i < o\}$ is $a$.
Ordinal.IsFundamentalSequence.cof_eq theorem
(hf : IsFundamentalSequence a o f) : a.cof.ord = o
Full source 
protected theorem cof_eq (hf : IsFundamentalSequence a o f) : a.cof.ord = o :=
  hf.1.antisymm' <| by
    rw [← hf.2.2]
    exact (ord_le_ord.2 (cof_blsub_le f)).trans (ord_card_le o)
Cofinality of an Ordinal Equals Length of its Fundamental Sequence
Informal description
If $(f_i)_{i < o}$ is a fundamental sequence for an ordinal $a$, then the cofinality of $a$ is equal to the order type of $o$ (i.e., $\mathrm{cof}(a) = o$ as cardinals).
Ordinal.IsFundamentalSequence.strict_mono theorem
(hf : IsFundamentalSequence a o f) {i j} : ∀ hi hj, i < j → f i hi < f j hj
Full source 
protected theorem strict_mono (hf : IsFundamentalSequence a o f) {i j} :
    ∀ hi hj, i < j → f i hi < f j hj :=
  hf.2.1
Fundamental sequences are strictly increasing
Informal description
For any fundamental sequence $(f_i)_{i < o}$ of an ordinal $a$, the sequence is strictly increasing: for any indices $i < j < o$, we have $f_i < f_j$.
Ordinal.IsFundamentalSequence.blsub_eq theorem
(hf : IsFundamentalSequence a o f) : blsub.{u, u} o f = a
Full source 
theorem blsub_eq (hf : IsFundamentalSequence a o f) : blsub.{u, u} o f = a :=
  hf.2.2
Fundamental Sequence Least Upper Bound Property
Informal description
Given a fundamental sequence $(f_i)_{i < o}$ for an ordinal $a$, the least strict upper bound of the set $\{f_i \mid i < o\}$ is equal to $a$.
Ordinal.IsFundamentalSequence.ord_cof theorem
(hf : IsFundamentalSequence a o f) : IsFundamentalSequence a a.cof.ord fun i hi => f i (hi.trans_le (by rw [hf.cof_eq]))
Full source 
theorem ord_cof (hf : IsFundamentalSequence a o f) :
    IsFundamentalSequence a a.cof.ord fun i hi => f i (hi.trans_le (by rw [hf.cof_eq])) := by
  have H := hf.cof_eq
  subst H
  exact hf
Restriction of Fundamental Sequence to Cofinality Length
Informal description
Given a fundamental sequence $(f_i)_{i < o}$ for an ordinal $a$, the function $f$ restricted to indices $i < \mathrm{cof}(a).\mathrm{ord}$ (where $\mathrm{cof}(a).\mathrm{ord} = o$ by `hf.cof_eq`) also forms a fundamental sequence for $a$.
Ordinal.IsFundamentalSequence.id_of_le_cof theorem
(h : o ≤ o.cof.ord) : IsFundamentalSequence o o fun a _ => a
Full source 
theorem id_of_le_cof (h : o ≤ o.cof.ord) : IsFundamentalSequence o o fun a _ => a :=
  ⟨h, @fun _ _ _ _ => id, blsub_id o⟩
Identity Function as Fundamental Sequence for Ordinals Below Cofinality
Informal description
For any ordinal $o$ such that $o \leq \operatorname{cof}(o).\mathrm{ord}$, the identity function $f(a) = a$ indexed by $a < o$ forms a fundamental sequence for $o$.
Ordinal.IsFundamentalSequence.succ theorem
: IsFundamentalSequence (succ o) 1 fun _ _ => o
Full source 
protected theorem succ : IsFundamentalSequence (succ o) 1 fun _ _ => o := by
  refine ⟨?_, @fun i j hi hj h => ?_, blsub_const Ordinal.one_ne_zero o⟩
  · rw [cof_succ, ord_one]
  · rw [lt_one_iff_zero] at hi hj
    rw [hi, hj] at h
    exact h.false.elim
Fundamental Sequence for Successor Ordinals: $(f_i)_{i<1} = o$ for $\operatorname{succ}(o)$
Informal description
For any ordinal $o$, the constant sequence $(f_i)_{i < 1}$ where $f_i = o$ for all $i < 1$ forms a fundamental sequence for the successor ordinal $\operatorname{succ}(o)$.
Ordinal.IsFundamentalSequence.monotone theorem
(hf : IsFundamentalSequence a o f) {i j : Ordinal} (hi : i < o) (hj : j < o) (hij : i ≤ j) : f i hi ≤ f j hj
Full source 
protected theorem monotone (hf : IsFundamentalSequence a o f) {i j : Ordinal} (hi : i < o)
    (hj : j < o) (hij : i ≤ j) : f i hi ≤ f j hj := by
  rcases lt_or_eq_of_le hij with (hij | rfl)
  · exact (hf.2.1 hi hj hij).le
  · rfl
Monotonicity of Fundamental Sequences
Informal description
Let $(f_i)_{i < o}$ be a fundamental sequence for an ordinal $a$. For any indices $i, j < o$ with $i \leq j$, the corresponding terms satisfy $f_i \leq f_j$.
Ordinal.IsFundamentalSequence.trans theorem
{a o o' : Ordinal.{u}} {f : ∀ b < o, Ordinal.{u}} (hf : IsFundamentalSequence a o f) {g : ∀ b < o', Ordinal.{u}} (hg : IsFundamentalSequence o o' g) : IsFundamentalSequence a o' fun i hi => f (g i hi) (by rw [← hg.2.2]; apply lt_blsub)
Full source 
theorem trans {a o o' : OrdinalOrdinal.{u}} {f : ∀ b < o, OrdinalOrdinal.{u}} (hf : IsFundamentalSequence a o f)
    {g : ∀ b < o', OrdinalOrdinal.{u}} (hg : IsFundamentalSequence o o' g) :
    IsFundamentalSequence a o' fun i hi =>
      f (g i hi) (by rw [← hg.2.2]; apply lt_blsub) := by
  refine ⟨?_, @fun i j _ _ h => hf.2.1 _ _ (hg.2.1 _ _ h), ?_⟩
  · rw [hf.cof_eq]
    exact hg.1.trans (ord_cof_le o)
  · rw [@blsub_comp.{u, u, u} o _ f (@IsFundamentalSequence.monotone _ _ f hf)]
    · exact hf.2.2
    · exact hg.2.2
Transitivity of Fundamental Sequences: Composition of Fundamental Sequences is Fundamental
Informal description
Let $a$ be an ordinal with a fundamental sequence $(f_i)_{i < o}$ indexed by ordinals $i < o$, and let $o$ itself have a fundamental sequence $(g_j)_{j < o'}$ indexed by ordinals $j < o'$. Then the composition $(f_{g_j})_{j < o'}$ forms a fundamental sequence for $a$ indexed by $j < o'$.
Ordinal.IsFundamentalSequence.lt theorem
{a o : Ordinal} {s : Π p < o, Ordinal} (h : IsFundamentalSequence a o s) {p : Ordinal} (hp : p < o) : s p hp < a
Full source 
protected theorem lt {a o : Ordinal} {s : Π p < o, Ordinal}
    (h : IsFundamentalSequence a o s) {p : Ordinal} (hp : p < o) : s p hp < a :=
  h.blsub_eq ▸ lt_blsub s p hp
Fundamental Sequence Terms are Bounded by the Ordinal
Informal description
Let $(s_i)_{i < o}$ be a fundamental sequence for an ordinal $a$. Then for any ordinal $p < o$, the corresponding term $s_p$ satisfies $s_p < a$.
Ordinal.exists_fundamental_sequence theorem
(a : Ordinal.{u}) : ∃ f, IsFundamentalSequence a a.cof.ord f
Full source 
/-- Every ordinal has a fundamental sequence. -/
theorem exists_fundamental_sequence (a : OrdinalOrdinal.{u}) :
    ∃ f, IsFundamentalSequence a a.cof.ord f := by
  suffices h : ∃ o f, IsFundamentalSequence a o f by
    rcases h with ⟨o, f, hf⟩
    exact ⟨_, hf.ord_cof⟩
  rcases exists_lsub_cof a with ⟨ι, f, hf, hι⟩
  rcases ord_eq ι with ⟨r, wo, hr⟩
  haveI := wo
  let r' := Subrel r fun i ↦ ∀ j, r j i → f j < f i
  let hrr' : r' ↪r r := Subrel.relEmbedding _ _
  haveI := hrr'.isWellOrder
  refine
    ⟨_, _, hrr'.ordinal_type_le.trans ?_, @fun i j _ h _ => (enum r' ⟨j, h⟩).prop _ ?_,
      le_antisymm (blsub_le fun i hi => lsub_le_iff.1 hf.le _) ?_⟩
  · rw [← hι, hr]
  · change r (hrr'.1 _) (hrr'.1 _)
    rwa [hrr'.2, @enum_lt_enum _ r']
  · rw [← hf, lsub_le_iff]
    intro i
    suffices h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f i) i' hi' by
      rcases h with ⟨i', hi', hfg⟩
      exact hfg.trans_lt (lt_blsub _ _ _)
    by_cases h : ∀ j, r j i → f j < f i
    · refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩
      rw [bfamilyOfFamily'_typein]
    · push_neg at h
      obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h
      refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩
      · by_contra! H
        exact (wo.wf.not_lt_min _ h ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj
      · rwa [bfamilyOfFamily'_typein]
Existence of Fundamental Sequences for Ordinals
Informal description
For every ordinal $a$, there exists a fundamental sequence $(f_i)_{i < \mathrm{cof}(a)}$ for $a$, where $\mathrm{cof}(a)$ is the cofinality of $a$.
Ordinal.cof_cof theorem
(a : Ordinal.{u}) : cof (cof a).ord = cof a
Full source 
@[simp]
theorem cof_cof (a : OrdinalOrdinal.{u}) : cof (cof a).ord = cof a := by
  obtain ⟨f, hf⟩ := exists_fundamental_sequence a
  obtain ⟨g, hg⟩ := exists_fundamental_sequence a.cof.ord
  exact ord_injective (hf.trans hg).cof_eq.symm
Cofinality of Cofinality Ordinal: $\mathrm{cof}(\mathrm{cof}(a).\mathrm{ord}) = \mathrm{cof}(a)$
Informal description
For any ordinal $a$, the cofinality of the ordinal associated with the cofinality of $a$ is equal to the cofinality of $a$ itself. In symbols, $\mathrm{cof}(\mathrm{cof}(a).\mathrm{ord}) = \mathrm{cof}(a)$.
Ordinal.IsNormal.isFundamentalSequence theorem
{f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) {a o} (ha : IsLimit a) {g} (hg : IsFundamentalSequence a o g) : IsFundamentalSequence (f a) o fun b hb => f (g b hb)
Full source 
protected theorem IsNormal.isFundamentalSequence {f : OrdinalOrdinal.{u} → OrdinalOrdinal.{u}} (hf : IsNormal f)
    {a o} (ha : IsLimit a) {g} (hg : IsFundamentalSequence a o g) :
    IsFundamentalSequence (f a) o fun b hb => f (g b hb) := by
  refine ⟨?_, @fun i j _ _ h => hf.strictMono (hg.2.1 _ _ h), ?_⟩
  · rcases exists_lsub_cof (f a) with ⟨ι, f', hf', hι⟩
    rw [← hg.cof_eq, ord_le_ord, ← hι]
    suffices (lsub.{u, u} fun i => sInf { b : Ordinal | f' i ≤ f b }) = a by
      rw [← this]
      apply cof_lsub_le
    have H : ∀ i, ∃ b < a, f' i ≤ f b := fun i => by
      have := lt_lsub.{u, u} f' i
      rw [hf', ← IsNormal.blsub_eq.{u, u} hf ha, lt_blsub_iff] at this
      simpa using this
    refine (lsub_le fun i => ?_).antisymm (le_of_forall_lt fun b hb => ?_)
    · rcases H i with ⟨b, hb, hb'⟩
      exact lt_of_le_of_lt (csInf_le' hb') hb
    · have := hf.strictMono hb
      rw [← hf', lt_lsub_iff] at this
      obtain ⟨i, hi⟩ := this
      rcases H i with ⟨b, _, hb⟩
      exact
        ((le_csInf_iff'' ⟨b, by exact hb⟩).2 fun c hc =>
          hf.strictMono.le_iff_le.1 (hi.trans hc)).trans_lt (lt_lsub _ i)
  · rw [@blsub_comp.{u, u, u} a _ (fun b _ => f b) (@fun i j _ _ h => hf.strictMono.monotone h) g
        hg.2.2]
    exact IsNormal.blsub_eq.{u, u} hf ha
Fundamental Sequence Preservation under Normal Functions
Informal description
Let $f$ be a normal function on ordinals (i.e., strictly increasing and continuous). Given a limit ordinal $a$ and a fundamental sequence $(g_i)_{i < o}$ for $a$ of length $o$, the sequence $(f(g_i))_{i < o}$ forms a fundamental sequence for $f(a)$ of the same length $o$.
Ordinal.IsNormal.cof_eq theorem
{f} (hf : IsNormal f) {a} (ha : IsLimit a) : cof (f a) = cof a
Full source 
theorem IsNormal.cof_eq {f} (hf : IsNormal f) {a} (ha : IsLimit a) : cof (f a) = cof a :=
  let ⟨_, hg⟩ := exists_fundamental_sequence a
  ord_injective (hf.isFundamentalSequence ha hg).cof_eq
Cofinality Preservation under Normal Functions at Limit Ordinals
Informal description
Let $f$ be a normal function on ordinals (i.e., strictly increasing and continuous). For any limit ordinal $a$, the cofinality of $f(a)$ equals the cofinality of $a$, i.e., $\mathrm{cof}(f(a)) = \mathrm{cof}(a)$.
Ordinal.IsNormal.cof_le theorem
{f} (hf : IsNormal f) (a) : cof a ≤ cof (f a)
Full source 
theorem IsNormal.cof_le {f} (hf : IsNormal f) (a) : cof a ≤ cof (f a) := by
  rcases zero_or_succ_or_limit a with (rfl | ⟨b, rfl⟩ | ha)
  · rw [cof_zero]
    exact zero_le _
  · rw [cof_succ, Cardinal.one_le_iff_ne_zero, cof_ne_zero, ← Ordinal.pos_iff_ne_zero]
    exact (Ordinal.zero_le (f b)).trans_lt (hf.1 b)
  · rw [hf.cof_eq ha]
Cofinality Monotonicity for Normal Functions: $\mathrm{cof}(a) \leq \mathrm{cof}(f(a))$
Informal description
Let $f$ be a normal function on ordinals (i.e., strictly increasing and continuous). For any ordinal $a$, the cofinality of $a$ is less than or equal to the cofinality of $f(a)$, i.e., $\mathrm{cof}(a) \leq \mathrm{cof}(f(a))$.
Ordinal.cof_add theorem
(a b : Ordinal) : b ≠ 0 → cof (a + b) = cof b
Full source 
@[simp]
theorem cof_add (a b : Ordinal) : b ≠ 0 → cof (a + b) = cof b := fun h => by
  rcases zero_or_succ_or_limit b with (rfl | ⟨c, rfl⟩ | hb)
  · contradiction
  · rw [add_succ, cof_succ, cof_succ]
  · exact (isNormal_add_right a).cof_eq hb
Cofinality of Ordinal Addition: $\mathrm{cof}(a + b) = \mathrm{cof}(b)$ for $b \neq 0$
Informal description
For any ordinals $a$ and $b$ with $b \neq 0$, the cofinality of the ordinal sum $a + b$ is equal to the cofinality of $b$, i.e., $\mathrm{cof}(a + b) = \mathrm{cof}(b)$.
Ordinal.aleph0_le_cof theorem
{o} : ℵ₀ ≤ cof o ↔ IsLimit o
Full source 
theorem aleph0_le_cof {o} : ℵ₀ℵ₀ ≤ cof o ↔ IsLimit o := by
  rcases zero_or_succ_or_limit o with (rfl | ⟨o, rfl⟩ | l)
  · simp [not_zero_isLimit, Cardinal.aleph0_ne_zero]
  · simp [not_succ_isLimit, Cardinal.one_lt_aleph0]
  · simp only [l, iff_true]
    refine le_of_not_lt fun h => ?_
    obtain ⟨n, e⟩ := Cardinal.lt_aleph0.1 h
    have := cof_cof o
    rw [e, ord_nat] at this
    cases n
    · simp at e
      simp [e, not_zero_isLimit] at l
    · rw [natCast_succ, cof_succ] at this
      rw [← this, cof_eq_one_iff_is_succ] at e
      rcases e with ⟨a, rfl⟩
      exact not_succ_isLimit _ l
Cofinality of Limit Ordinals: $\aleph_0 \leq \mathrm{cof}(o) \leftrightarrow o$ is a limit ordinal
Informal description
For any ordinal $o$, the cofinality of $o$ is at least $\aleph_0$ if and only if $o$ is a limit ordinal.
Ordinal.cof_preOmega theorem
{o : Ordinal} (ho : IsSuccPrelimit o) : (preOmega o).cof = o.cof
Full source 
@[simp]
theorem cof_preOmega {o : Ordinal} (ho : IsSuccPrelimit o) : (preOmega o).cof = o.cof := by
  by_cases h : IsMin o
  · simp [h.eq_bot]
  · exact isNormal_preOmega.cof_eq ⟨h, ho⟩
Cofinality of Predecessor of Successor Pre-Limit Ordinal: $\mathrm{cof}(\mathrm{preOmega}(o)) = \mathrm{cof}(o)$
Informal description
For any ordinal $o$ that is a successor pre-limit (i.e., there is no element covered by $o$), the cofinality of the predecessor of $o$ is equal to the cofinality of $o$ itself, i.e., $\mathrm{cof}(\mathrm{preOmega}(o)) = \mathrm{cof}(o)$.
Ordinal.cof_omega theorem
{o : Ordinal} (ho : o.IsLimit) : (ω_ o).cof = o.cof
Full source 
@[simp]
theorem cof_omega {o : Ordinal} (ho : o.IsLimit) : (ω_ o).cof = o.cof :=
  isNormal_omega.cof_eq ho
Cofinality of $\omega$-sequence at limit ordinals: $\mathrm{cof}(\omega_o) = \mathrm{cof}(o)$
Informal description
For any limit ordinal $o$, the cofinality of the $\omega$-sequence $\omega_o$ is equal to the cofinality of $o$, i.e., $\mathrm{cof}(\omega_o) = \mathrm{cof}(o)$.
Ordinal.cof_eq' theorem
(r : α → α → Prop) [IsWellOrder α r] (h : IsLimit (type r)) : ∃ S : Set α, (∀ a, ∃ b ∈ S, r a b) ∧ #S = cof (type r)
Full source 
theorem cof_eq' (r : α → α → Prop) [IsWellOrder α r] (h : IsLimit (type r)) :
    ∃ S : Set α, (∀ a, ∃ b ∈ S, r a b) ∧ #S = cof (type r) :=
  let ⟨S, H, e⟩ := cof_eq r
  ⟨S, fun a =>
    let a' := enum r ⟨_, h.succ_lt (typein_lt_type r a)⟩
    let ⟨b, h, ab⟩ := H a'
    ⟨b, h,
      (IsOrderConnected.conn a b a' <|
            (typein_lt_typein r).1
              (by
                rw [typein_enum]
                exact lt_succ (typein _ _))).resolve_right
        ab⟩,
    e⟩
Existence of Cofinal Subset with Cofinality Cardinality for Limit Ordinals
Informal description
Let $\alpha$ be a type equipped with a well-order relation $r$, and suppose the order type of $r$ is a limit ordinal. Then there exists a subset $S \subseteq \alpha$ such that: 1. $S$ is cofinal in $\alpha$ (i.e., for every $a \in \alpha$, there exists $b \in S$ with $a < b$ under $r$) 2. The cardinality of $S$ equals the cofinality of the order type of $r$.
Ordinal.cof_univ theorem
: cof univ.{u, v} = Cardinal.univ.{u, v}
Full source 
@[simp]
theorem cof_univ : cof univuniv.{u, v} = Cardinal.univCardinal.univ.{u, v} :=
  le_antisymm (cof_le_card _)
    (by
      refine le_of_forall_lt fun c h => ?_
      rcases lt_univ'.1 h with ⟨c, rfl⟩
      rcases @cof_eq OrdinalOrdinal.{u} (· < ·) _ with ⟨S, H, Se⟩
      rw [univ, ← lift_cof, ← Cardinal.lift_liftCardinal.lift_lift.{u+1, v, u}, Cardinal.lift_lt, ← Se]
      refine lt_of_not_ge fun h => ?_
      obtain ⟨a, e⟩ := Cardinal.mem_range_lift_of_le h
      refine Quotient.inductionOn a (fun α e => ?_) e
      obtain ⟨f⟩ := Quotient.exact e
      have f := Equiv.ulift.symm.trans f
      let g a := (f a).1
      let o := succ (iSup g)
      rcases H o with ⟨b, h, l⟩
      refine l (lt_succ_iff.2 ?_)
      rw [← show g (f.symm ⟨b, h⟩) = b by simp [g]]
      apply Ordinal.le_iSup)
Cofinality of the universal ordinal equals the universal cardinal: $\text{cof}(\text{univ}) = \text{univ}$
Informal description
The cofinality of the universal ordinal `univ.{u, v}` (which represents the order type of all ordinals in the universe `Type u` lifted to `Type (max u v)`) is equal to the universal cardinal `Cardinal.univ.{u, v}` (which represents the cardinality of the universe `Type (max u v)`).
Cardinal.mk_bounded_subset theorem
{α : Type*} (h : ∀ x < #α, 2 ^ x < #α) {r : α → α → Prop} [IsWellOrder α r] (hr : (#α).ord = type r) : #{ s : Set α // Bounded r s } = #α
Full source 
theorem mk_bounded_subset {α : Type*} (h : ∀ x < #α, 2 ^ x < #α) {r : α → α → Prop}
    [IsWellOrder α r] (hr : (#α).ord = type r) : #{ s : Set α // Bounded r s } = #α := by
  rcases eq_or_ne #α 0 with (ha | ha)
  · rw [ha]
    haveI := mk_eq_zero_iff.1 ha
    rw [mk_eq_zero_iff]
    constructor
    rintro ⟨s, hs⟩
    exact (not_unbounded_iff s).2 hs (unbounded_of_isEmpty s)
  have h' : IsStrongLimit #α := ⟨ha, @h⟩
  have ha := h'.aleph0_le
  apply le_antisymm
  · have : { s : Set α | Bounded r s } = ⋃ i, 𝒫{ j | r j i } := setOf_exists _
    rw [← coe_setOf, this]
    refine mk_iUnion_le_sum_mk.trans ((sum_le_iSup (fun i => #(𝒫{ j | r j i }))).trans
      ((mul_le_max_of_aleph0_le_left ha).trans ?_))
    rw [max_eq_left]
    apply ciSup_le' _
    intro i
    rw [mk_powerset]
    apply (h'.two_power_lt _).le
    rw [coe_setOf, card_typein, ← lt_ord, hr]
    apply typein_lt_type
  · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · apply bounded_singleton
      rw [← hr]
      apply isLimit_ord ha
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab
Cardinality of Bounded Subsets Equals Cardinality of Type under Large Cardinal Assumption
Informal description
Let $\alpha$ be a type with a well-order $r$ such that the ordinal associated to the cardinality of $\alpha$ equals the order type of $r$. Assume that for every cardinal $x$ less than the cardinality of $\alpha$, the power $2^x$ is also less than the cardinality of $\alpha$. Then the cardinality of the collection of all bounded subsets of $\alpha$ with respect to $r$ equals the cardinality of $\alpha$.
Cardinal.mk_subset_mk_lt_cof theorem
{α : Type*} (h : ∀ x < #α, 2 ^ x < #α) : #{ s : Set α // #s < cof (#α).ord } = #α
Full source 
theorem mk_subset_mk_lt_cof {α : Type*} (h : ∀ x < #α, 2 ^ x < #α) :
    #{ s : Set α // #s < cof (#α).ord } = #α := by
  rcases eq_or_ne #α 0 with (ha | ha)
  · simp [ha]
  have h' : IsStrongLimit #α := ⟨ha, @h⟩
  rcases ord_eq α with ⟨r, wo, hr⟩
  haveI := wo
  apply le_antisymm
  · conv_rhs => rw [← mk_bounded_subset h hr]
    apply mk_le_mk_of_subset
    intro s hs
    rw [hr] at hs
    exact lt_cof_type hs
  · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · rw [mk_singleton]
      exact one_lt_aleph0.trans_le (aleph0_le_cof.2 (isLimit_ord h'.aleph0_le))
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab
Cardinality of Small Subsets Equals Cardinality of Type under Large Cardinal Assumption
Informal description
Let $\alpha$ be a type such that for every cardinal $x$ less than the cardinality of $\alpha$, the power set $2^x$ is also less than the cardinality of $\alpha$. Then the cardinality of the collection of all subsets of $\alpha$ with cardinality strictly less than the cofinality of the ordinal associated to $\#\alpha$ is equal to the cardinality of $\alpha$.
Cardinal.unbounded_of_unbounded_sUnion theorem
(r : α → α → Prop) [wo : IsWellOrder α r] {s : Set (Set α)} (h₁ : Unbounded r <| ⋃₀ s) (h₂ : #s < Order.cof (swap rᶜ)) : ∃ x ∈ s, Unbounded r x
Full source 
/-- If the union of s is unbounded and s is smaller than the cofinality,
  then s has an unbounded member -/
theorem unbounded_of_unbounded_sUnion (r : α → α → Prop) [wo : IsWellOrder α r] {s : Set (Set α)}
    (h₁ : Unbounded r <| ⋃₀ s) (h₂ : #s < Order.cof (swap rᶜ)) : ∃ x ∈ s, Unbounded r x := by
  by_contra! h
  simp_rw [not_unbounded_iff] at h
  let f : s → α := fun x : s => wo.wf.sup x (h x.1 x.2)
  refine h₂.not_le (le_trans (csInf_le' ⟨range f, fun x => ?_, rfl⟩) mk_range_le)
  rcases h₁ x with ⟨y, ⟨c, hc, hy⟩, hxy⟩
  exact ⟨f ⟨c, hc⟩, mem_range_self _, fun hxz => hxy (Trans.trans (wo.wf.lt_sup _ hy) hxz)⟩
Existence of Unbounded Subset in Union with Small Index Set
Informal description
Let $\alpha$ be a type with a well-order $r$, and let $s$ be a family of subsets of $\alpha$. If the union $\bigcup s$ is unbounded with respect to $r$ and the cardinality of $s$ is less than the cofinality of the complement of the reverse relation $r$, then there exists a subset $x \in s$ that is unbounded with respect to $r$.
Cardinal.unbounded_of_unbounded_iUnion theorem
{α β : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] (s : β → Set α) (h₁ : Unbounded r <| ⋃ x, s x) (h₂ : #β < Order.cof (swap rᶜ)) : ∃ x : β, Unbounded r (s x)
Full source 
/-- If the union of s is unbounded and s is smaller than the cofinality,
  then s has an unbounded member -/
theorem unbounded_of_unbounded_iUnion {α β : Type u} (r : α → α → Prop) [wo : IsWellOrder α r]
    (s : β → Set α) (h₁ : Unbounded r <| ⋃ x, s x) (h₂ : #β < Order.cof (swap rᶜ)) :
    ∃ x : β, Unbounded r (s x) := by
  rw [← sUnion_range] at h₁
  rcases unbounded_of_unbounded_sUnion r h₁ (mk_range_le.trans_lt h₂) with ⟨_, ⟨x, rfl⟩, u⟩
  exact ⟨x, u⟩
Existence of Unbounded Subset in Indexed Union with Small Index Set
Informal description
Let $\alpha$ and $\beta$ be types, and let $r$ be a well-order on $\alpha$. Given a family of subsets $s : \beta \to \text{Set } \alpha$ such that the union $\bigcup_{x \in \beta} s(x)$ is unbounded with respect to $r$, and the cardinality of $\beta$ is less than the cofinality of the complement of the reverse relation $r$, then there exists an index $x \in \beta$ such that the subset $s(x)$ is unbounded with respect to $r$.
Cardinal.lt_power_cof theorem
{c : Cardinal.{u}} : ℵ₀ ≤ c → c < c ^ c.ord.cof
Full source 
theorem lt_power_cof {c : CardinalCardinal.{u}} : ℵ₀ ≤ c → c < c ^ c.ord.cof :=
  Cardinal.inductionOn c fun α h => by
    rcases ord_eq α with ⟨r, wo, re⟩
    have := isLimit_ord h
    rw [re] at this ⊢
    rcases cof_eq' r this with ⟨S, H, Se⟩
    have := sum_lt_prod (fun a : S => #{ x // r x a }) (fun _ => #α) fun i => ?_
    · simp only [Cardinal.prod_const, Cardinal.lift_id, ← Se, ← mk_sigma, power_def] at this ⊢
      refine lt_of_le_of_lt ?_ this
      refine ⟨Embedding.ofSurjective ?_ ?_⟩
      · exact fun x => x.2.1
      · exact fun a =>
          let ⟨b, h, ab⟩ := H a
          ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩
    · have := typein_lt_type r i
      rwa [← re, lt_ord] at this
König's Theorem: $c < c^{\mathrm{cof}(c)}$ for infinite cardinals
Informal description
For any infinite cardinal number $c$ (i.e., $\aleph_0 \leq c$), we have $c < c^{\mathrm{cof}(c)}$, where $\mathrm{cof}(c)$ denotes the cofinality of $c$ (defined as the cofinality of the initial ordinal corresponding to $c$).
Cardinal.lt_cof_power theorem
{a b : Cardinal} (ha : ℵ₀ ≤ a) (b1 : 1 < b) : a < (b ^ a).ord.cof
Full source 
theorem lt_cof_power {a b : Cardinal} (ha : ℵ₀ ≤ a) (b1 : 1 < b) : a < (b ^ a).ord.cof := by
  have b0 : b ≠ 0 := (zero_lt_one.trans b1).ne'
  apply lt_imp_lt_of_le_imp_le (power_le_power_left <| power_ne_zero a b0)
  rw [← power_mul, mul_eq_self ha]
  exact lt_power_cof (ha.trans <| (cantor' _ b1).le)
König's Theorem: $a < \mathrm{cof}(b^a)$ for infinite $a$ and $b > 1$
Informal description
For any infinite cardinal number $a$ (i.e., $\aleph_0 \leq a$) and any cardinal number $b$ with $1 < b$, we have $a < \mathrm{cof}(b^a)$, where $\mathrm{cof}(b^a)$ denotes the cofinality of the initial ordinal corresponding to the cardinal exponentiation $b^a$.