Documentation

Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Cofinality of an ordinal #

This file contains the definition of the cofinality Ordinal.cof o of an ordinal. This is the cofinality of the ordinal o when viewed as a linear order.

Main statements #

Implementation notes #

source
theorem Order.cof_int :
cof ℤ = Cardinal.aleph0

Cofinality of ordinals #

source
noncomputable def Ordinal.cof (o : Ordinal.{u}) :
Cardinal.{u}

The cofinality on an ordinal is the Order.cof of any isomorphic linear order.

In particular, cof 0 = 0 and cof (succ o) = 1.

Equations
Instances For
    source
    @[simp]
    theorem Ordinal.cof_type (α : Type u_1) [LinearOrder α] [WellFoundedLT α] :
    (type fun (x1 x2 : α) => x1 < x2).cof = Order.cof α
    source
    @[deprecated Ordinal.cof_type (since := "2026-02-18")]
    theorem Ordinal.cof_type_lt (α : Type u_1) [LinearOrder α] [WellFoundedLT α] :
    (type fun (x1 x2 : α) => x1 < x2).cof = Order.cof α

    Alias of Ordinal.cof_type.

    source
    @[simp]
    theorem Ordinal.cof_toType (o : Ordinal.{u_1}) :
    Order.cof o.ToType = o.cof
    source
    @[deprecated Ordinal.cof_toType (since := "2026-02-18")]
    theorem Ordinal.cof_eq_cof_toType (o : Ordinal.{u_1}) :
    Order.cof o.ToType = o.cof

    Alias of Ordinal.cof_toType.

    source
    @[deprecated Order.le_cof_iff (since := "2026-02-18")]
    theorem Ordinal.le_cof_type {α : Type u} [Preorder α] {c : Cardinal.{u}} :
    c ≤ Order.cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.mk ↑s

    Alias of Order.le_cof_iff.

    source
    @[deprecated Order.cof_le (since := "2026-02-18")]
    theorem Ordinal.cof_type_le {α : Type u} [Preorder α] {s : Set α} (h : IsCofinal s) :
    Order.cof α ≤ Cardinal.mk ↑s

    Alias of Order.cof_le.

    source
    @[deprecated Order.cof_le (since := "2026-02-18")]
    theorem Ordinal.lt_cof_type {α : Type u} [Preorder α] {s : Set α} (h : IsCofinal s) :
    Order.cof α ≤ Cardinal.mk ↑s

    Alias of Order.cof_le.

    source
    @[deprecated Order.cof_eq (since := "2026-02-18")]
    theorem Ordinal.cof_eq (α : Type u) [Preorder α] :
    ∃ (s : Set α), IsCofinal s ∧ Cardinal.mk ↑s = Order.cof α

    Alias of Order.cof_eq.

    source
    @[simp]
    theorem Ordinal.lift_cof (o : Ordinal.{u}) :
    Cardinal.lift.{v, u} o.cof = (lift.{v, u} o).cof
    source
    theorem Order.cof_Iio {α : Type u} [LinearOrder α] [WellFoundedLT α] (x : α) :
    cof ↑(Set.Iio x) = ((Ordinal.typein fun (x1 x2 : α) => x1 < x2).toRelEmbedding x).cof
    source
    @[simp]
    theorem Ordinal.cof_Iio (o : Ordinal.{u}) :
    Order.cof ↑(Set.Iio o) = (lift.{u + 1, u} o).cof
    source
    theorem Ordinal.cof_le_card (o : Ordinal.{u_1}) :
    o.cof ≤ o.card
    source
    theorem Ordinal.cof_ord_le (c : Cardinal.{u_1}) :
    c.ord.cof ≤ c
    source
    theorem Ordinal.ord_cof_le (o : Ordinal.{u_1}) :
    o.cof.ord ≤ o
    source
    @[simp]
    theorem Ordinal.cof_eq_zero {o : Ordinal.{u_1}} :
    o.cof = 0 ↔ o = 0
    source
    @[deprecated Ordinal.cof_eq_zero (since := "2026-02-18")]
    theorem Ordinal.cof_ne_zero {o : Ordinal.{u_1}} :
    o.cof ≠ 0 ↔ o ≠ 0
    source
    @[simp]
    theorem Ordinal.cof_pos {o : Ordinal.{u_1}} :
    0 < o.cof ↔ 0 < o
    source
    @[simp]
    theorem Ordinal.cof_zero :
    cof 0 = 0
    source
    theorem Ordinal.cof_eq_one_iff {o : Ordinal.{u_1}} :
    o.cof = 1 ↔ o ∈ Set.range Order.succ
    source
    theorem Ordinal.cof_add_one (o : Ordinal.{u_1}) :
    (o + 1).cof = 1
    source
    @[simp]
    theorem Ordinal.cof_one :
    cof 1 = 1
    source
    theorem Ordinal.cof_succ (o : Ordinal.{u_1}) :
    (Order.succ o).cof = 1
    source
    theorem Ordinal.one_lt_cof_iff {o : Ordinal.{u_1}} :
    1 < o.cof ↔ Order.IsSuccLimit o
    source
    @[simp]
    theorem Ordinal.cof_lt_aleph0_iff {o : Ordinal.{u_1}} :
    o.cof < Cardinal.aleph0 ↔ o.cof ≤ 1
    source
    @[simp]
    theorem Ordinal.aleph0_le_cof_iff {o : Ordinal.{u_1}} :
    Cardinal.aleph0 ≤ o.cof ↔ 1 < o.cof
    source
    @[deprecated Ordinal.one_lt_cof_iff (since := "2026-03-22")]
    theorem Ordinal.aleph0_le_cof {o : Ordinal.{u_1}} :
    Cardinal.aleph0 ≤ o.cof ↔ Order.IsSuccLimit o
    source
    theorem Ordinal.cof_eq_aleph0_of_isSuccLimit {o : Ordinal.{u_1}} (ho : Order.IsSuccLimit o) (ho' : o < omega 1) :
    o.cof = Cardinal.aleph0

    A countable limit ordinal has cofinality ℵ₀.

    source
    @[simp]
    theorem Ordinal.cof_omega0 :
    omega0.cof = Cardinal.aleph0
    source
    @[deprecated Ordinal.cof_eq_one_iff (since := "2026-02-18")]
    theorem Ordinal.cof_eq_one_iff_is_succ {o : Ordinal.{u_1}} :
    o.cof = 1 ↔ o ∈ Set.range Order.succ

    Alias of Ordinal.cof_eq_one_iff.

    source
    theorem Ordinal.ord_cof_eq (α : Type u_1) [LinearOrder α] [WellFoundedLT α] :
    ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : ↑s) => x1 < x2) = (Order.cof α).ord
    source
    @[simp]
    theorem Order.cof_ord_cof (α : Type u_1) [LinearOrder α] [WellFoundedLT α] :
    (cof α).ord.cof = cof α
    source
    @[simp]
    theorem Ordinal.cof_ord_cof (o : Ordinal.{u_1}) :
    o.cof.ord.cof = o.cof
    source
    @[deprecated Ordinal.cof_ord_cof (since := "2026-03-21")]
    theorem Ordinal.cof_cof (o : Ordinal.{u_1}) :
    o.cof.ord.cof = o.cof

    Alias of Ordinal.cof_ord_cof.

    Cofinalities and suprema #

    source
    theorem Ordinal.lift_cof_iSup_add_one {β : Type v} [LinearOrder β] [Small.{u, v} β] {f : β → Ordinal.{u}} (hf : StrictMono f) :
    Cardinal.lift.{v, u} (⨆ (i : β), f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)
    source
    theorem Ordinal.cof_iSup_add_one {γ : Type u} [LinearOrder γ] {f : γ → Ordinal.{u}} (hf : StrictMono f) :
    (⨆ (i : γ), f i + 1).cof = Order.cof γ
    source
    theorem Ordinal.lift_cof_iSup {β : Type v} [LinearOrder β] [Small.{u, v} β] [NoMaxOrder β] {f : β → Ordinal.{u}} (hf : StrictMono f) :
    Cardinal.lift.{v, u} (⨆ (i : β), f i).cof = Cardinal.lift.{u, v} (Order.cof β)
    source
    theorem Ordinal.cof_iSup {γ : Type u} [LinearOrder γ] [NoMaxOrder γ] {f : γ → Ordinal.{u}} (hf : StrictMono f) :
    (⨆ (i : γ), f i).cof = Order.cof γ
    source
    theorem Ordinal.cof_iSup_Iio_add_one {a : Ordinal.{u_1}} {f : ↑(Set.Iio a) → Ordinal.{u_1}} (hf : StrictMono f) :
    (⨆ (i : ↑(Set.Iio a)), f i + 1).cof = a.cof
    source
    theorem Ordinal.cof_iSup_Iio {a : Ordinal.{u_1}} {f : ↑(Set.Iio a) → Ordinal.{u_1}} (hf : StrictMono f) (ha : Order.IsSuccPrelimit a) :
    (⨆ (i : ↑(Set.Iio a)), f i).cof = a.cof
    source
    theorem Ordinal.cof_map_of_isNormal {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : Order.IsNormal f) {a : Ordinal.{u_1}} (ha : Order.IsSuccLimit a) :
    (f a).cof = a.cof
    source
    @[deprecated Ordinal.cof_map_of_isNormal (since := "2026-03-19")]
    theorem Ordinal.cof_eq_of_isNormal {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : Order.IsNormal f) {a : Ordinal.{u_1}} (ha : Order.IsSuccLimit a) :
    (f a).cof = a.cof

    Alias of Ordinal.cof_map_of_isNormal.

    source
    @[deprecated Ordinal.cof_eq_of_isNormal (since := "2025-12-25")]
    theorem Ordinal.IsNormal.cof_eq {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : Order.IsNormal f) {a : Ordinal.{u_1}} (ha : Order.IsSuccLimit a) :
    (f a).cof = a.cof

    Alias of Ordinal.cof_map_of_isNormal.

    Alias of Ordinal.cof_map_of_isNormal.

    source
    theorem Ordinal.le_cof_map_of_isNormal {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : Order.IsNormal f) (a : Ordinal.{u_1}) :
    a.cof ≤ (f a).cof
    source
    @[deprecated Ordinal.le_cof_map_of_isNormal (since := "2026-03-19")]
    theorem Ordinal.cof_le_of_isNormal {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : Order.IsNormal f) (a : Ordinal.{u_1}) :
    a.cof ≤ (f a).cof

    Alias of Ordinal.le_cof_map_of_isNormal.

    source
    @[deprecated Ordinal.le_cof_map_of_isNormal (since := "2025-12-25")]
    theorem Ordinal.IsNormal.cof_le {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : Order.IsNormal f) (a : Ordinal.{u_1}) :
    a.cof ≤ (f a).cof

    Alias of Ordinal.le_cof_map_of_isNormal.

    source
    theorem Ordinal.sSup_add_one_lt_of_lt_cof {s : Set Ordinal.{u}} {a : Ordinal.{u}} (ha : Cardinal.mk ↑s < (lift.{u + 1, u} a).cof) (hs : ∀ i ∈ s, i < a) :
    sSup ((fun (x : Ordinal.{u}) => x + 1) '' s) < a
    source
    theorem Ordinal.sSup_lt_of_lt_cof {s : Set Ordinal.{u}} {a : Ordinal.{u}} (ha : Cardinal.mk ↑s < (lift.{u + 1, u} a).cof) (hs : ∀ i ∈ s, i < a) :
    sSup s < a
    source
    theorem Ordinal.lift_iSup_add_one_lt_of_lt_cof {β : Type v} {f : β → Ordinal.{u}} {a : Ordinal.{u}} (ha : Cardinal.lift.{u, v} (Cardinal.mk β) < (lift.{v, u} a).cof) (hf : ∀ (i : β), f i < a) :
    ⨆ (i : β), f i + 1 < a
    source
    theorem Ordinal.iSup_add_one_lt_of_lt_cof {α : Type u} {f : α → Ordinal.{u}} {a : Ordinal.{u}} (ha : Cardinal.mk α < a.cof) (hf : ∀ (i : α), f i < a) :
    ⨆ (i : α), f i + 1 < a
    source
    theorem Ordinal.lift_iSup_lt_of_lt_cof {β : Type v} {f : β → Ordinal.{u}} {a : Ordinal.{u}} (ha : Cardinal.lift.{u, v} (Cardinal.mk β) < (lift.{v, u} a).cof) (hf : ∀ (i : β), f i < a) :
    ⨆ (i : β), f i < a
    source
    theorem Ordinal.iSup_lt_of_lt_cof {α : Type u} {f : α → Ordinal.{u}} {a : Ordinal.{u}} (ha : Cardinal.mk α < a.cof) (hf : ∀ (i : α), f i < a) :
    ⨆ (i : α), f i < a
    source
    theorem Ordinal.cof_lift_iSup_add_one_le {β : Type v} [Small.{u, v} β] (f : β → Ordinal.{u}) :
    (lift.{v, u} (⨆ (i : β), f i + 1)).cof ≤ Cardinal.lift.{u, v} (Cardinal.mk β)
    source
    theorem Ordinal.cof_iSup_add_one_le {α : Type u} (f : α → Ordinal.{u}) :
    (⨆ (i : α), f i + 1).cof ≤ Cardinal.mk α
    source
    theorem Cardinal.sSup_lt_of_lt_cof_ord {s : Set Cardinal.{u}} {a : Cardinal.{u}} (ha : mk ↑s < (lift.{u + 1, u} a).ord.cof) (hs : ∀ i ∈ s, i < a) :
    sSup s < a
    source
    theorem Cardinal.lift_iSup_lt_of_lt_cof_ord {β : Type v} {f : β → Cardinal.{u}} {a : Cardinal.{u}} (ha : lift.{u, v} (mk β) < (lift.{v, u} a).ord.cof) (hf : ∀ (i : β), f i < a) :
    ⨆ (i : β), f i < a
    source
    theorem Cardinal.iSup_lt_of_lt_cof_ord {α : Type u} {f : α → Cardinal.{u}} {a : Cardinal.{u}} (ha : mk α < a.ord.cof) (hf : ∀ (i : α), f i < a) :
    ⨆ (i : α), f i < a
    source
    @[deprecated "to build an increasing function with limit o, use the fundamental sequence API." (since := "2026-03-27")]
    theorem Ordinal.cof_lsub_def_nonempty (o : Ordinal.{u}) :
    {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ Cardinal.mk ι = a}.Nonempty

    The set in the lsub characterization of cof is nonempty.

    source
    @[deprecated "to build an increasing function with limit o, use the fundamental sequence API." (since := "2026-03-27")]
    theorem Ordinal.cof_eq_sInf_lsub (o : Ordinal.{u}) :
    o.cof = sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ Cardinal.mk ι = a}
    source
    @[deprecated "to build an increasing function with limit o, use the fundamental sequence API." (since := "2026-03-27")]
    theorem Ordinal.exists_lsub_cof (o : Ordinal.{u}) :
    ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ Cardinal.mk ι = o.cof
    source
    @[deprecated Ordinal.cof_iSup_add_one_le (since := "2026-03-22")]
    theorem Ordinal.cof_lsub_le {ι : Type u} (f : ι → Ordinal.{u}) :
    (lsub f).cof ≤ Cardinal.mk ι
    source
    @[deprecated Ordinal.cof_lift_iSup_add_one_le (since := "2026-03-22")]
    theorem Ordinal.cof_lsub_le_lift {ι : Type u} (f : ι → Ordinal.{max u v}) :
    (lsub f).cof ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)
    source
    @[deprecated Order.le_cof_iff (since := "2026-03-21")]
    theorem Ordinal.le_cof_iff_lsub {o : Ordinal.{u}} {a : Cardinal.{u}} :
    a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ Cardinal.mk ι
    source
    @[deprecated Ordinal.lift_iSup_add_one_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.lsub_lt_ord_lift {ι : Type u} {f : ι → Ordinal.{max u v}} {c : Ordinal.{max u v}} (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c.cof) (hf : ∀ (i : ι), f i < c) :
    lsub f < c
    source
    @[deprecated Ordinal.iSup_add_one_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.lsub_lt_ord {ι : Type u} {f : ι → Ordinal.{u}} {c : Ordinal.{u}} (hι : Cardinal.mk ι < c.cof) :
    (∀ (i : ι), f i < c) → lsub f < c
    source
    @[deprecated Ordinal.lift_iSup_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.cof_iSup_le_lift {ι : Type u} {f : ι → Ordinal.{max u v}} (H : ∀ (i : ι), f i < iSup f) :
    (iSup f).cof ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)
    source
    @[deprecated Ordinal.iSup_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.cof_iSup_le {ι : Type u_1} {f : ι → Ordinal.{u_1}} (H : ∀ (i : ι), f i < iSup f) :
    (iSup f).cof ≤ Cardinal.mk ι
    source
    @[deprecated Ordinal.lift_iSup_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.iSup_lt_ord_lift {ι : Type u} {f : ι → Ordinal.{max u v}} {c : Ordinal.{max u v}} (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c.cof) (hf : ∀ (i : ι), f i < c) :
    iSup f < c
    source
    @[deprecated Ordinal.iSup_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.iSup_lt_ord {α : Type u} {f : α → Ordinal.{u}} {a : Ordinal.{u}} (ha : Cardinal.mk α < a.cof) (hf : ∀ (i : α), f i < a) :
    ⨆ (i : α), f i < a

    Alias of Ordinal.iSup_lt_of_lt_cof.

    source
    @[deprecated Ordinal.lift_iSup_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.iSup_lt_lift {ι : Type u} {f : ι → Cardinal.{max u v}} {c : Cardinal.{max u v}} (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c.ord.cof) (hf : ∀ (i : ι), f i < c) :
    iSup f < c
    source
    @[deprecated Cardinal.iSup_lt_of_lt_cof_ord (since := "2026-03-22")]
    theorem Ordinal.iSup_lt {α : Type u} {f : α → Cardinal.{u}} {a : Cardinal.{u}} (ha : Cardinal.mk α < a.ord.cof) (hf : ∀ (i : α), f i < a) :
    ⨆ (i : α), f i < a

    Alias of Cardinal.iSup_lt_of_lt_cof_ord.

    source
    theorem Ordinal.nfpFamily_lt_ord_lift {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {c : Ordinal.{max u v}} (hc : Cardinal.aleph0 < c.cof) (hc' : Cardinal.lift.{v, u} (Cardinal.mk ι) < c.cof) (hf : ∀ (i : ι), ∀ b < c, f i b < c) {a : Ordinal.{max u v}} (ha : a < c) :
    nfpFamily f a < c
    source
    theorem Ordinal.nfpFamily_lt_ord {ι : Type u} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Ordinal.{u}} (hc : Cardinal.aleph0 < c.cof) (hc' : Cardinal.mk ι < c.cof) (hf : ∀ (i : ι), ∀ b < c, f i b < c) {a : Ordinal.{u}} :
    a < c → nfpFamily f a < c
    source
    theorem Ordinal.nfp_lt_ord {f : Ordinal.{u_1} → Ordinal.{u_1}} {c : Ordinal.{u_1}} (hc : Cardinal.aleph0 < c.cof) (hf : ∀ i < c, f i < c) {a : Ordinal.{u_1}} :
    a < c → nfp f a < c
    source
    @[deprecated Ordinal.exists_lsub_cof (since := "2026-03-21")]
    theorem Ordinal.exists_blsub_cof (o : Ordinal.{u}) :
    ∃ (f : (a : Ordinal.{u}) → a < o.cof.ord → Ordinal.{u}), o.cof.ord.blsub f = o
    source
    @[deprecated Order.le_cof_iff (since := "2026-03-21")]
    theorem Ordinal.le_cof_iff_blsub {b : Ordinal.{u}} {a : Cardinal.{u}} :
    a ≤ b.cof ↔ ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
    source
    @[deprecated Ordinal.cof_lift_iSup_add_one_le (since := "2026-03-22")]
    theorem Ordinal.cof_blsub_le_lift {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) :
    (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card
    source
    @[deprecated Ordinal.cof_iSup_add_one_le (since := "2026-03-22")]
    theorem Ordinal.cof_blsub_le {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}) :
    (o.blsub f).cof ≤ o.card
    source
    @[deprecated Ordinal.lift_iSup_add_one_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.blsub_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {c : Ordinal.{max u v}} (ho : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) :
    o.blsub f < c
    source
    @[deprecated Ordinal.iSup_add_one_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.blsub_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u}} {c : Ordinal.{u}} (ho : o.card < c.cof) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) :
    o.blsub f < c
    source
    @[deprecated Ordinal.lift_iSup_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.cof_bsup_le_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} (H : ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) :
    (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card
    source
    @[deprecated Ordinal.iSup_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.cof_bsup_le {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u}} :
    (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ o.card
    source
    @[deprecated Ordinal.lift_iSup_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.bsup_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {c : Ordinal.{max u v}} (ho : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) :
    o.bsup f < c
    source
    @[deprecated Ordinal.iSup_lt_of_lt_cof (since := "2026-03-22")]
    theorem Ordinal.bsup_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u}} {c : Ordinal.{u}} (ho : o.card < c.cof) :
    (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) → o.bsup f < c

    Cofinality arithmetic #

    source
    @[simp]
    theorem Ordinal.cof_add (a : Ordinal.{u_1}) {b : Ordinal.{u_1}} (hb : b ≠ 0) :
    (a + b).cof = b.cof
    source
    @[simp]
    theorem Ordinal.cof_mul {a b : Ordinal.{u_1}} (ha : a ≠ 0) (hb : Order.IsSuccPrelimit b) :
    (a * b).cof = b.cof
    source
    @[simp]
    theorem Ordinal.cof_preOmega {o : Ordinal.{u_1}} (ho : Order.IsSuccPrelimit o) :
    (preOmega o).cof = o.cof
    source
    @[simp]
    theorem Ordinal.cof_omega {o : Ordinal.{u_1}} (ho : Order.IsSuccLimit o) :
    (omega o).cof = o.cof
    source
    theorem Ordinal.cof_eq' {α : Type u} (r : α → α → Prop) [H : IsWellOrder α r] (h : Order.IsSuccLimit (type r)) :
    ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ Cardinal.mk ↑S = (type r).cof
    source
    @[simp]
    theorem Ordinal.cof_univ :
    univ.{u, v}.cof = Cardinal.univ.{u, v}

    Results on sets #

    source
    theorem Cardinal.mk_bounded_subset {α : Type u_1} (h : ∀ x < mk α, 2 ^ x < mk α) {r : α → α → Prop} [IsWellOrder α r] (hr : (mk α).ord = Ordinal.type r) :
    mk { s : Set α // Set.Bounded r s } = mk α
    source
    theorem Cardinal.mk_subset_mk_lt_cof {α : Type u_1} (h : ∀ x < mk α, 2 ^ x < mk α) :
    mk { s : Set α // mk ↑s < (mk α).ord.cof } = mk α
    source
    @[deprecated isCofinal_of_isCofinal_sUnion (since := "2026-02-25")]
    theorem Cardinal.unbounded_of_unbounded_sUnion {α : Type u_1} [LinearOrder α] {s : Set (Set α)} (h₁ : IsCofinal (⋃₀ s)) (h₂ : mk ↑s < Order.cof α) :
    ∃ x ∈ s, IsCofinal x

    Alias of isCofinal_of_isCofinal_sUnion.

    source
    @[deprecated isCofinal_of_isCofinal_iUnion (since := "2026-02-25")]
    theorem Cardinal.unbounded_of_unbounded_iUnion {α ι : Type u_1} [LinearOrder α] {s : ι → Set α} (h₁ : IsCofinal (⋃ (i : ι), s i)) (h₂ : mk ι < Order.cof α) :
    ∃ (i : ι), IsCofinal (s i)

    Alias of isCofinal_of_isCofinal_iUnion.

    Consequences of König's lemma #

    source
    theorem Cardinal.lt_power_cof_ord {c : Cardinal.{u_1}} (hc : aleph0 ≤ c) :
    c < c ^ c.ord.cof
    source
    @[deprecated Cardinal.lt_power_cof_ord (since := "2026-03-30")]
    theorem Cardinal.lt_power_cof {c : Cardinal.{u_1}} (hc : aleph0 ≤ c) :
    c < c ^ c.ord.cof

    Alias of Cardinal.lt_power_cof_ord.

    source
    theorem Cardinal.lt_cof_ord_power {a b : Cardinal.{u_1}} (ha : aleph0 ≤ a) (hb : 1 < b) :
    a < (b ^ a).ord.cof
    source
    @[deprecated Cardinal.lt_cof_ord_power (since := "2026-03-30")]
    theorem Cardinal.lt_cof_power {a b : Cardinal.{u_1}} (ha : aleph0 ≤ a) (hb : 1 < b) :
    a < (b ^ a).ord.cof

    Alias of Cardinal.lt_cof_ord_power.