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

def Order.cof {α : Type u} (r : α → α → Prop) : Cardinal.{u}

Cofinality of a reflexive order ≼. This is the smallest cardinality of a subset S : Set α such that ∀ a, ∃ b ∈ S, a ≼ b.

theorem Order.cof_le {α : Type u} (r : α → α → Prop) {S : Set α} (h : ∀ (a : α), ∃ b ∈ S, r a b) : cof r ≤ Cardinal.mk ↑S

theorem Order.le_cof {α : Type u} {r : α → α → Prop} [IsRefl α r] (c : Cardinal.{u}) : c ≤ cof r ↔ ∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ Cardinal.mk ↑S

theorem RelIso.cof_eq_lift {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsRefl β s] (f : r ≃r s) : Cardinal.lift.{v, u} (Order.cof r) = Cardinal.lift.{u, v} (Order.cof s)

theorem RelIso.cof_eq {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsRefl β s] (f : r ≃r s) : Order.cof r = Order.cof s

Cofinality of ordinals

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

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.

theorem Ordinal.cof_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : (type r).cof = Order.cof (Function.swap rᶜ)

theorem Ordinal.cof_type_lt {α : Type u} [LinearOrder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] : (type fun (x1 x2 : α) => x1 < x2).cof = Order.cof fun (x1 x2 : α) => x1 ≤ x2

theorem Ordinal.cof_eq_cof_toType (o : Ordinal.{u_1}) : o.cof = Order.cof fun (x1 x2 : o.toType) => x1 ≤ x2

theorem Ordinal.le_cof_type {α : Type u} {r : α → α → Prop} [IsWellOrder α r] {c : Cardinal.{u}} : c ≤ (type r).cof ↔ ∀ (S : Set α), Set.Unbounded r S → c ≤ Cardinal.mk ↑S

theorem Ordinal.cof_type_le {α : Type u} {r : α → α → Prop} [IsWellOrder α r] {S : Set α} (h : Set.Unbounded r S) : (type r).cof ≤ Cardinal.mk ↑S

theorem Ordinal.lt_cof_type {α : Type u} {r : α → α → Prop} [IsWellOrder α r] {S : Set α} : Cardinal.mk ↑S < (type r).cof → Set.Bounded r S

theorem Ordinal.cof_eq {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : ∃ (S : Set α), Set.Unbounded r S ∧ Cardinal.mk ↑S = (type r).cof

theorem Ordinal.ord_cof_eq {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : ∃ (S : Set α), Set.Unbounded r S ∧ type (Subrel r fun (x : α) => x ∈ S) = (type r).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}

@[simp]

theorem Ordinal.lift_cof (o : Ordinal.{v}) : Cardinal.lift.{u, v} o.cof = (lift.{u, v} 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}) : o.cof.ord ≤ o

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

Basic results

@[simp]

theorem Ordinal.cof_zero : cof 0 = 0

@[simp]

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

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

@[simp]

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

@[simp]

theorem Ordinal.cof_eq_one_iff_is_succ {o : Ordinal.{u}} : o.cof = 1 ↔ ∃ (a : Ordinal.{u}), o = Order.succ a

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.

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 : 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.IsNormal.isFundamentalSequence {f : Ordinal.{u} → Ordinal.{u}} (hf : 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)

theorem Ordinal.IsNormal.cof_eq {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : IsNormal f) {a : Ordinal.{u_1}} (ha : Order.IsSuccLimit a) : (f a).cof = a.cof

theorem Ordinal.IsNormal.cof_le {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : IsNormal f) (a : Ordinal.{u_1}) : a.cof ≤ (f a).cof

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

theorem Cardinal.unbounded_of_unbounded_sUnion {α : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] {s : Set (Set α)} (h₁ : Set.Unbounded r (⋃₀ s)) (h₂ : mk ↑s < Order.cof (Function.swap rᶜ)) : ∃ x ∈ s, Set.Unbounded r x

If the union of s is unbounded and s is smaller than the cofinality, then s has an unbounded member

theorem Cardinal.unbounded_of_unbounded_iUnion {α β : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] (s : β → Set α) (h₁ : Set.Unbounded r (⋃ (x : β), s x)) (h₂ : mk β < Order.cof (Function.swap rᶜ)) : ∃ (x : β), Set.Unbounded r (s x)

If the union of s is unbounded and s is smaller than the cofinality, then s has an unbounded 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