Documentation

Mathlib.SetTheory.Cardinal.Cofinality

Cofinality #

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

Main Definitions #

Main Statements #

Implementation Notes #

Cofinality of orders #

source
noncomputable def Order.cof (α : Type u) [Preorder α] :
Cardinal.{u}

The cofinality of a preorder is the smallest cardinality of a cofinal subset.

Equations
Instances For
    source
    theorem Order.cof_le {α : Type u} [Preorder α] {s : Set α} (h : IsCofinal s) :
    cof α ≤ Cardinal.mk ↑s
    source
    theorem Order.le_lift_cof_iff {α : Type u} [Preorder α] {c : Cardinal.{max u v}} :
    c ≤ Cardinal.lift.{v, u} (cof α) ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑s)
    source
    theorem Order.le_cof_iff {α : Type u} [Preorder α] {c : Cardinal.{u}} :
    c ≤ cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.mk ↑s
    source
    @[deprecated Order.le_cof_iff (since := "2026-02-18")]
    theorem Order.le_cof {α : Type u} [Preorder α] {c : Cardinal.{u}} :
    c ≤ cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.mk ↑s

    Alias of Order.le_cof_iff.

    source
    theorem Order.cof_eq (α : Type u) [Preorder α] :
    ∃ (s : Set α), IsCofinal s ∧ Cardinal.mk ↑s = cof α
    source
    theorem Order.cof_le_cardinalMk (α : Type u) [Preorder α] :
    cof α ≤ Cardinal.mk α
    source
    theorem Order.cof_eq_zero_iff {α : Type u} [Preorder α] :
    cof α = 0 ↔ IsEmpty α
    source
    @[simp]
    theorem Order.cof_eq_zero {α : Type u} [Preorder α] [h : IsEmpty α] :
    cof α = 0
    source
    theorem Order.cof_ne_zero_iff {α : Type u} [Preorder α] :
    cof α ≠ 0 ↔ Nonempty α
    source
    @[simp]
    theorem Order.cof_ne_zero {α : Type u} [Preorder α] [h : Nonempty α] :
    cof α ≠ 0
    source
    theorem Order.cof_eq_one_iff {α : Type u} [Preorder α] :
    cof α = 1 ↔ ∃ (x : α), IsTop x
    source
    @[simp]
    theorem Order.cof_eq_one {α : Type u} [Preorder α] [OrderTop α] :
    cof α = 1
    source
    theorem Order.cof_ne_one_iff {α : Type u} [Preorder α] :
    cof α ≠ 1 ↔ NoTopOrder α
    source
    @[simp]
    theorem Order.cof_ne_one {α : Type u} [Preorder α] [h : NoTopOrder α] :
    cof α ≠ 1
    source
    theorem Order.cof_le_one_iff {α : Type u} [Preorder α] [Nonempty α] :
    cof α ≤ 1 ↔ ∃ (x : α), IsTop x
    source
    theorem Order.one_lt_cof_iff {α : Type u} [Preorder α] [Nonempty α] :
    1 < cof α ↔ NoTopOrder α
    source
    @[simp]
    theorem Order.one_lt_cof {α : Type u} [Preorder α] [Nonempty α] [h : NoTopOrder α] :
    1 < cof α
    source
    theorem Order.lift_cof_congr_of_strictMono {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : StrictMono f) (hf' : IsCofinal (Set.range f)) :
    Cardinal.lift.{v, u} (cof α) = Cardinal.lift.{u, v} (cof β)
    source
    theorem Order.cof_congr_of_strictMono {α γ : Type u} [LinearOrder α] [LinearOrder γ] {f : α → γ} (hf : StrictMono f) (hf' : IsCofinal (Set.range f)) :
    cof α = cof γ
    source
    @[simp]
    theorem Order.cof_lt_aleph0_iff {α : Type u} [LinearOrder α] :
    cof α < Cardinal.aleph0 ↔ cof α ≤ 1
    source
    @[simp]
    theorem Order.aleph0_le_cof_iff {α : Type u} [LinearOrder α] :
    Cardinal.aleph0 ≤ cof α ↔ 1 < cof α
    source
    @[simp]
    theorem Order.cof_eq_aleph0 {α : Type u} [LinearOrder α] [NoMaxOrder α] [Nonempty α] [Countable α] :
    cof α = Cardinal.aleph0
    source
    theorem Order.cof_nat :
    cof ℕ = Cardinal.aleph0
    source
    theorem Order.cof_int :
    cof ℤ = Cardinal.aleph0
    source
    theorem GaloisConnection.cof_le_lift {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) :
    Cardinal.lift.{u, v} (Order.cof β) ≤ Cardinal.lift.{v, u} (Order.cof α)
    source
    theorem GaloisConnection.cof_le {α γ : Type u} [Preorder α] [Preorder γ] {f : γ → α} {g : α → γ} (h : GaloisConnection f g) :
    Order.cof γ ≤ Order.cof α
    source
    theorem OrderIso.lift_cof_congr {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α ≃o β) :
    Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, v} (Order.cof β)
    source
    @[deprecated OrderIso.lift_cof_congr (since := "2026-03-20")]
    theorem OrderIso.lift_cof_eq {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α ≃o β) :
    Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, v} (Order.cof β)

    Alias of OrderIso.lift_cof_congr.

    source
    theorem OrderIso.cof_congr {α γ : Type u} [Preorder α] [Preorder γ] (f : α ≃o γ) :
    Order.cof α = Order.cof γ
    source
    @[deprecated OrderIso.cof_congr (since := "2026-03-20")]
    theorem OrderIso.cof_eq {α γ : Type u} [Preorder α] [Preorder γ] (f : α ≃o γ) :
    Order.cof α = Order.cof γ

    Alias of OrderIso.cof_congr.

    source
    @[deprecated OrderIso.lift_cof_congr (since := "2026-02-18")]
    theorem RelIso.cof_eq_lift {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α ≃o β) :
    Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, v} (Order.cof β)

    Alias of OrderIso.lift_cof_congr.

    source
    @[deprecated OrderIso.cof_congr (since := "2026-02-18")]
    theorem RelIso.cof_eq {α γ : Type u} [Preorder α] [Preorder γ] (f : α ≃o γ) :
    Order.cof α = Order.cof γ

    Alias of OrderIso.cof_congr.

    source
    theorem isCofinal_of_isCofinal_sUnion {α : Type u_1} [LinearOrder α] {s : Set (Set α)} (h₁ : IsCofinal (⋃₀ s)) (h₂ : Cardinal.mk ↑s < Order.cof α) :
    ∃ x ∈ s, IsCofinal x

    If the union of s is cofinal and s is smaller than the cofinality, then s has a cofinal member.

    source
    theorem isCofinal_of_isCofinal_iUnion {α ι : Type u_1} [LinearOrder α] {s : ι → Set α} (h₁ : IsCofinal (⋃ (i : ι), s i)) (h₂ : Cardinal.mk ι < Order.cof α) :
    ∃ (i : ι), IsCofinal (s i)

    If the union of the ι-indexed family s is cofinal and ι is smaller than the cofinality, then s has a cofinal member.

    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

      Cofinality of suprema and least strict upper bounds #

      source
      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
      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
      theorem Ordinal.exists_lsub_cof (o : Ordinal.{u}) :
      ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ Cardinal.mk ι = o.cof
      source
      theorem Ordinal.cof_lsub_le {ι : Type u} (f : ι → Ordinal.{u}) :
      (lsub f).cof ≤ Cardinal.mk ι
      source
      theorem Ordinal.cof_lsub_le_lift {ι : Type u} (f : ι → Ordinal.{max u v}) :
      (lsub f).cof ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)
      source
      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
      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
      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
      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
      theorem Ordinal.cof_iSup_le {ι : Type u_1} {f : ι → Ordinal.{u_1}} (H : ∀ (i : ι), f i < iSup f) :
      (iSup f).cof ≤ Cardinal.mk ι
      source
      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
      theorem Ordinal.iSup_lt_ord {ι : Type u_1} {f : ι → Ordinal.{u_1}} {c : Ordinal.{u_1}} (hι : Cardinal.mk ι < c.cof) :
      (∀ (i : ι), f i < c) → iSup f < c
      source
      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
      theorem Ordinal.iSup_lt {ι : Type u_1} {f : ι → Cardinal.{u_1}} {c : Cardinal.{u_1}} (hι : Cardinal.mk ι < c.ord.cof) :
      (∀ (i : ι), f i < c) → iSup f < c
      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
      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
      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
      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
      theorem Ordinal.cof_blsub_le {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}) :
      (o.blsub f).cof ≤ o.card
      source
      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
      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
      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
      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
      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
      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
      source
      @[simp]
      theorem Ordinal.cof_add (a b : Ordinal.{u_1}) :
      b ≠ 0 → (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.

      If the union of s is cofinal and s is smaller than the cofinality, then s has a cofinal member.

      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.

      If the union of the ι-indexed family s is cofinal and ι is smaller than the cofinality, then s has a cofinal member.

      Consequences of König's lemma #

      source
      theorem Cardinal.lt_power_cof {c : Cardinal.{u}} :
      aleph0 ≤ c → c < c ^ c.ord.cof
      source
      theorem Cardinal.lt_cof_power {a b : Cardinal.{u_1}} (ha : aleph0 ≤ a) (b1 : 1 < b) :
      a < (b ^ a).ord.cof