Cofinality

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

Main Definitions

• Order.cof α is the cofinality of a preorder. This is the smallest cardinality of a cofinal subset.
• 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

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

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

Equations

• Order.cof α = ⨅ (s : { s : Set α // IsCofinal s }), Cardinal.mk ↑↑s

theorem Order.cof_le {α : Type u} [Preorder α] {s : Set α} (h : IsCofinal s) : cof α ≤ Cardinal.mk ↑s

theorem Order.le_cof_iff {α : Type u} [Preorder α] {c : Cardinal.{u}} : c ≤ cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.mk ↑s

@[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.

theorem Order.cof_eq (α : Type u) [Preorder α] : ∃ (s : Set α), IsCofinal s ∧ Cardinal.mk ↑s = cof α

theorem Order.cof_le_cardinalMk (α : Type u) [Preorder α] : cof α ≤ Cardinal.mk α

theorem Order.cof_eq_zero_iff {α : Type u} [Preorder α] : cof α = 0 ↔ IsEmpty α

@[simp]

theorem Order.cof_eq_zero {α : Type u} [Preorder α] [h : IsEmpty α] : cof α = 0

theorem Order.cof_ne_zero_iff {α : Type u} [Preorder α] : cof α ≠ 0 ↔ Nonempty α

@[simp]

theorem Order.cof_ne_zero {α : Type u} [Preorder α] [h : Nonempty α] : cof α ≠ 0

theorem Order.cof_eq_one_iff {α : Type u} [Preorder α] : cof α = 1 ↔ ∃ (x : α), IsTop x

@[simp]

theorem Order.cof_eq_one {α : Type u} [Preorder α] [OrderTop α] : cof α = 1

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 α)

theorem GaloisConnection.cof_le {α γ : Type u} [Preorder α] [Preorder γ] {f : γ → α} {g : α → γ} (h : GaloisConnection f g) : Order.cof γ ≤ Order.cof α

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 β)

theorem OrderIso.cof_eq {α γ : Type u} [Preorder α] [Preorder γ] (f : α ≃o γ) : Order.cof α = Order.cof γ

@[deprecated OrderIso.lift_cof_eq (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_eq.

@[deprecated OrderIso.cof_eq (since := "2026-02-18")]

theorem RelIso.cof_eq {α γ : Type u} [Preorder α] [Preorder γ] (f : α ≃o γ) : Order.cof α = Order.cof γ

Alias of OrderIso.cof_eq.

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.

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

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

• o.cof = o.liftOnWellOrder (fun (α : Type ?u.10) (x : LinearOrder α) (x_1 : WellFoundedLT α) => Order.cof α) Ordinal.cof._proof_2✝

@[simp]

theorem Ordinal.cof_type (α : Type u_1) [LinearOrder α] [WellFoundedLT α] : (type fun (x1 x2 : α) => x1 < x2).cof = Order.cof α

@[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.

@[simp]

theorem Ordinal.cof_toType (o : Ordinal.{u_1}) : Order.cof o.ToType = o.cof

@[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.

@[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.

@[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.

@[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.

@[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.

@[simp]

theorem Ordinal.lift_cof (o : Ordinal.{u}) : Cardinal.lift.{v, u} o.cof = (lift.{v, u} o).cof

theorem Ordinal.cof_le_card (o : Ordinal.{u_1}) : o.cof ≤ o.card

theorem Ordinal.cof_ord_le (c : Cardinal.{u_1}) : c.ord.cof ≤ c

theorem Ordinal.ord_cof_le (o : Ordinal.{u_1}) : o.cof.ord ≤ o

@[simp]

theorem Ordinal.cof_eq_zero {o : Ordinal.{u_1}} : o.cof = 0 ↔ o = 0

@[deprecated Ordinal.cof_eq_zero (since := "2026-02-18")]

theorem Ordinal.cof_ne_zero {o : Ordinal.{u_1}} : o.cof ≠ 0 ↔ o ≠ 0

@[simp]

theorem Ordinal.cof_zero : cof 0 = 0

theorem Ordinal.cof_eq_one_iff {o : Ordinal.{u_1}} : o.cof = 1 ↔ o ∈ Set.range Order.succ

theorem Ordinal.cof_add_one (o : Ordinal.{u_1}) : (o + 1).cof = 1

@[simp]

theorem Ordinal.cof_one : cof 1 = 1

theorem Ordinal.cof_succ (o : Ordinal.{u_1}) : (Order.succ o).cof = 1

@[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.

theorem Ordinal.ord_cof_eq (α : Type u_1) [LinearOrder α] [WellFoundedLT α] : ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : ↑s) => x1 < x2) = (Order.cof α).ord

Cofinality of suprema and least strict upper bounds

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.

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}

theorem Ordinal.exists_lsub_cof (o : Ordinal.{u}) : ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ Cardinal.mk ι = o.cof

theorem Ordinal.cof_lsub_le {ι : Type u} (f : ι → Ordinal.{u}) : (lsub f).cof ≤ Cardinal.mk ι

theorem Ordinal.cof_lsub_le_lift {ι : Type u} (f : ι → Ordinal.{max u v}) : (lsub f).cof ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)

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 ι

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

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

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 ι)

theorem Ordinal.cof_iSup_le {ι : Type u_1} {f : ι → Ordinal.{u_1}} (H : ∀ (i : ι), f i < iSup f) : (iSup f).cof ≤ Cardinal.mk ι

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

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

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

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

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

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

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

theorem Ordinal.exists_blsub_cof (o : Ordinal.{u}) : ∃ (f : (a : Ordinal.{u}) → a < o.cof.ord → Ordinal.{u}), o.cof.ord.blsub f = o

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

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

theorem Ordinal.cof_blsub_le {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}) : (o.blsub f).cof ≤ o.card

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

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

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

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

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

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

Fundamental sequences

def Ordinal.IsFundamentalSequence (a o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}) : Prop

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.

Equations

• a.IsFundamentalSequence o f = (o ≤ a.cof.ord ∧ (∀ {i j : Ordinal.{?u.29}} (hi : i < o) (hj : j < o), i < j → f i hi < f j hj) ∧ o.blsub f = a)

theorem Ordinal.IsFundamentalSequence.cof_eq {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) : a.cof.ord = o

theorem Ordinal.IsFundamentalSequence.strict_mono {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) {i j : Ordinal.{u}} (hi : i < o) (hj : j < o) : i < j → f i hi < f j hj

theorem Ordinal.IsFundamentalSequence.blsub_eq {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) : o.blsub f = a

theorem Ordinal.IsFundamentalSequence.ord_cof {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) : a.IsFundamentalSequence a.cof.ord fun (i : Ordinal.{u}) (hi : i < a.cof.ord) => f i ⋯

theorem Ordinal.IsFundamentalSequence.id_of_le_cof {o : Ordinal.{u}} (h : o ≤ o.cof.ord) : o.IsFundamentalSequence o fun (a : Ordinal.{u}) (x : a < o) => a

theorem Ordinal.IsFundamentalSequence.zero {f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}} : IsFundamentalSequence 0 0 f

theorem Ordinal.IsFundamentalSequence.succ {o : Ordinal.{u}} : (Order.succ o).IsFundamentalSequence 1 fun (x : Ordinal.{u}) (x_1 : x < 1) => o

theorem Ordinal.IsFundamentalSequence.monotone {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) {i j : Ordinal.{u}} (hi : i < o) (hj : j < o) (hij : i ≤ j) : f i hi ≤ f j hj

theorem Ordinal.IsFundamentalSequence.trans {a o o' : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) {g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}} (hg : o.IsFundamentalSequence o' g) : a.IsFundamentalSequence o' fun (i : Ordinal.{u}) (hi : i < o') => f (g i hi) ⋯

theorem Ordinal.IsFundamentalSequence.lt {a o : Ordinal.{u_1}} {s : (p : Ordinal.{u_1}) → p < o → Ordinal.{u_1}} (h : a.IsFundamentalSequence o s) {p : Ordinal.{u_1}} (hp : p < o) : s p hp < a

theorem Ordinal.exists_fundamental_sequence (a : Ordinal.{u}) : ∃ (f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}), a.IsFundamentalSequence a.cof.ord f

Every ordinal has a fundamental sequence.

@[simp]

theorem Ordinal.cof_cof (a : Ordinal.{u}) : a.cof.ord.cof = a.cof

theorem Ordinal.IsFundamentalSequence.of_isNormal {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) {a o : Ordinal.{u}} (ha : Order.IsSuccLimit a) {g : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hg : a.IsFundamentalSequence o g) : (f a).IsFundamentalSequence o fun (b : Ordinal.{u}) (hb : b < o) => f (g b hb)

@[deprecated Ordinal.IsFundamentalSequence.of_isNormal (since := "2025-12-25")]

theorem Ordinal.IsNormal.isFundamentalSequence {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) {a o : Ordinal.{u}} (ha : Order.IsSuccLimit a) {g : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hg : a.IsFundamentalSequence o g) : (f a).IsFundamentalSequence o fun (b : Ordinal.{u}) (hb : b < o) => f (g b hb)

Alias of Ordinal.IsFundamentalSequence.of_isNormal.

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

@[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_eq_of_isNormal.

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

@[deprecated Ordinal.cof_le_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.cof_le_of_isNormal.

@[simp]

theorem Ordinal.cof_add (a b : Ordinal.{u_1}) : b ≠ 0 → (a + b).cof = b.cof

theorem Ordinal.aleph0_le_cof {o : Ordinal.{u_1}} : Cardinal.aleph0 ≤ o.cof ↔ Order.IsSuccLimit o

@[simp]

theorem Ordinal.cof_preOmega {o : Ordinal.{u_1}} (ho : Order.IsSuccPrelimit o) : (preOmega o).cof = o.cof

@[simp]

theorem Ordinal.cof_omega {o : Ordinal.{u_1}} (ho : Order.IsSuccLimit o) : (omega o).cof = o.cof

@[simp]

theorem Ordinal.cof_omega0 : omega0.cof = Cardinal.aleph0

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

@[simp]

theorem Ordinal.cof_univ : univ.{u, v}.cof = Cardinal.univ.{u, v}

Results on sets

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 α

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 α

@[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.

@[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

theorem Cardinal.lt_power_cof {c : Cardinal.{u}} : aleph0 ≤ c → c < c ^ c.ord.cof

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