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
    @[simp]
    theorem Ordinal.cof_toType (o : Ordinal.{u_1}) :
    Order.cof o.ToType = o.cof
    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
    @[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
    @[deprecated Ordinal.cof_add_one (since := "2026-05-25")]
    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
    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
    theorem Ordinal.exists_ord_cof_eq (α : Type u) [LinearOrder α] [WellFoundedLT α] :
    ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : ↑s) => x1 < x2) = (Order.cof α).ord

    Every well-order has a cofinal subset of order type (cof α).ord.

    source
    @[deprecated Ordinal.exists_ord_cof_eq (since := "2026-05-25")]
    theorem Ordinal.ord_cof_eq (α : Type u) [LinearOrder α] [WellFoundedLT α] :
    ∃ (s : Set α), IsCofinal s ∧ (type fun (x1 x2 : ↑s) => x1 < x2) = (Order.cof α).ord

    Alias of Ordinal.exists_ord_cof_eq.

    Every well-order has a cofinal subset of order type (cof α).ord.

    source
    theorem Ordinal.exists_ord_cof_eq_of_isCofinal {α : Type u} [LinearOrder α] [WellFoundedLT α] {s : Set α} (hs : IsCofinal s) :
    ∃ t ⊆ s, IsCofinal t ∧ (type fun (x1 x2 : ↑t) => x1 < x2) = (Order.cof α).ord

    Every cofinal set has a cofinal subset of order type (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

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

    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
    @[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 : (mk α).IsStrongPrelimit) {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 : (mk α).IsStrongPrelimit) :
    mk { s : Set α // mk ↑s < (mk α).ord.cof } = mk α

    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
    theorem Cardinal.lt_cof_ord_power {a b : Cardinal.{u_1}} (ha : aleph0 ≤ a) (hb : 1 < b) :
    a < (b ^ a).ord.cof