Cofinality #

This file contains the definition of cofinality of an ordinal number and regular cardinals

Main Definitions #

ordinal.cof o is the cofinality of the ordinal o. If o is the order type of the relation < on α, then o.cof is the smallest cardinality of a subset s of α that is cofinal in α, i.e. ∀ x : α, ∃ y ∈ s, ¬ y < x.
cardinal.is_limit c means that c is a (weak) limit cardinal: c ≠ 0 ∧ ∀ x < c, succ x < c.
cardinal.is_strong_limit c means that c is a strong limit cardinal: c ≠ 0 ∧ ∀ x < c, 2 ^ x < c.
cardinal.is_regular c means that c is a regular cardinal: ω ≤ c ∧ c.ord.cof = c.
cardinal.is_inaccessible c means that c is strongly inaccessible: ω < c ∧ is_regular c ∧ is_strong_limit c.

Main Statements #

ordinal.infinite_pigeonhole_card: the infinite pigeonhole principle
cardinal.lt_power_cof: A consequence of König's theorem stating that c < c ^ c.ord.cof for c ≥ ω
cardinal.univ_inaccessible: The type of ordinals in Type u form an inaccessible cardinal (in Type v with v > u). This shows (externally) that in Type u there are at least u inaccessible cardinals.

Implementation Notes #

The cofinality is defined for ordinals. If c is a cardinal number, its cofinality is c.ord.cof.

Tags #

cofinality, regular cardinals, limits cardinals, inaccessible cardinals, infinite pigeonhole principle

Cofinality of orders #

source

noncomputable def order.cof {α : Type u_1} (r : α → α → Prop) [is_refl α r] :

cardinal

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

Equations

order.cof r = cardinal.min _ (λ (S : {S // ∀ (a : α), ∃ (b : α) (H : b ∈ S), r a b}), # ↥S)

source

theorem order.cof_le {α : Type u_1} (r : α → α → Prop) [is_refl α r] {S : set α} (h : ∀ (a : α), ∃ (b : α) (H : b ∈ S), r a b) :

order.cof r ≤ # ↥S

source

theorem order.le_cof {α : Type u_1} {r : α → α → Prop} [is_refl α r] (c : cardinal) :

c ≤ order.cof r ↔ ∀ {S : set α}, (∀ (a : α), ∃ (b : α) (H : b ∈ S), r a b) → c ≤ # ↥S

source

theorem rel_iso.cof.aux {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_refl α r] [is_refl β s] (f : r ≃r s) :

(order.cof r).lift ≤ (order.cof s).lift

source

theorem rel_iso.cof {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_refl α r] [is_refl β s] (f : r ≃r s) :

(order.cof r).lift = (order.cof s).lift

source

noncomputable def strict_order.cof {α : Type u_1} (r : α → α → Prop) [h : is_irrefl α r] :

cardinal

Cofinality of a strict order ≺. This is the smallest cardinality of a set S : set α such that ∀ a, ∃ b ∈ S, ¬ b ≺ a.

Equations

strict_order.cof r = order.cof (λ (x y : α), ¬r y x)

Cofinality of ordinals #

source

noncomputable def ordinal.cof (o : ordinal) :

cardinal

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. It is defined for all ordinals, but cof 0 = 0 and cof (succ o) = 1, so it is only really interesting on limit ordinals (when it is an infinite cardinal).

Equations

o.cof = quot.lift_on o (λ (a : Well_order), strict_order.cof a.r) ordinal.cof._proof_2

source

theorem ordinal.cof_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

(ordinal.type r).cof = strict_order.cof r

source

theorem ordinal.le_cof_type {α : Type u_1} {r : α → α → Prop} [is_well_order α r] {c : cardinal} :

c ≤ (ordinal.type r).cof ↔ ∀ (S : set α), (∀ (a : α), ∃ (b : α) (H : b ∈ S), ¬r b a) → c ≤ # ↥S

source

theorem ordinal.cof_type_le {α : Type u_1} {r : α → α → Prop} [is_well_order α r] (S : set α) (h : ∀ (a : α), ∃ (b : α) (H : b ∈ S), ¬r b a) :

(ordinal.type r).cof ≤ # ↥S

source

theorem ordinal.lt_cof_type {α : Type u_1} {r : α → α → Prop} [is_well_order α r] (S : set α) (hl : # ↥S < (ordinal.type r).cof) :

∃ (a : α), ∀ (b : α), b ∈ S → r b a

source

theorem ordinal.cof_eq {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

∃ (S : set α), (∀ (a : α), ∃ (b : α) (H : b ∈ S), ¬r b a) ∧ # ↥S = (ordinal.type r).cof

source

theorem ordinal.ord_cof_eq {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

∃ (S : set α), (∀ (a : α), ∃ (b : α) (H : b ∈ S), ¬r b a) ∧ ordinal.type (subrel r S) = (ordinal.type r).cof.ord

Cofinality of suprema and least strict upper bounds #

source

theorem ordinal.cof_lsub_def_nonempty (o : ordinal) :

{a : cardinal | ∃ {ι : Type u} (f : ι → ordinal), ordinal.lsub f = o ∧ # ι = a}.nonempty

The set in the lsub characterization of cof is nonempty.

source

theorem ordinal.cof_eq_Inf_lsub (o : ordinal) :

o.cof = Inf {a : cardinal | ∃ {ι : Type u} (f : ι → ordinal), ordinal.lsub f = o ∧ # ι = a}

source

theorem ordinal.lift_cof (o : ordinal) :

o.cof.lift = o.lift.cof

source

theorem ordinal.cof_le_card (o : ordinal) :

o.cof ≤ o.card

source

theorem ordinal.cof_ord_le (c : cardinal) :

c.ord.cof ≤ c

source

theorem ordinal.ord_cof_le (o : ordinal) :

o.cof.ord ≤ o

source

theorem ordinal.exists_lsub_cof (o : ordinal) :

∃ {ι : Type u} (f : ι → ordinal), ordinal.lsub f = o ∧ # ι = o.cof

source

theorem ordinal.cof_lsub_le {ι : Type u} (f : ι → ordinal) :

(ordinal.lsub f).cof ≤ # ι

source

theorem ordinal.cof_lsub_le_lift {ι : Type u} (f : ι → ordinal) :

(ordinal.lsub f).cof ≤ (# ι).lift

source

theorem ordinal.le_cof_iff_lsub {o : ordinal} {a : cardinal} :

a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → ordinal), ordinal.lsub f = o → a ≤ # ι

source

theorem ordinal.lsub_lt_ord_lift {ι : Type u} {f : ι → ordinal} {c : ordinal} (hι : (# ι).lift < c.cof) (hf : ∀ (i : ι), f i < c) :

ordinal.lsub f < c

source

theorem ordinal.lsub_lt_ord {ι : Type u} {f : ι → ordinal} {c : ordinal} (hι : # ι < c.cof) :

(∀ (i : ι), f i < c) → ordinal.lsub f < c

source

theorem ordinal.cof_sup_le_lift {ι : Type u_1} {f : ι → ordinal} (H : ∀ (i : ι), f i < ordinal.sup f) :

(ordinal.sup f).cof ≤ (# ι).lift

source

theorem ordinal.cof_sup_le {ι : Type u} {f : ι → ordinal} (H : ∀ (i : ι), f i < ordinal.sup f) :

(ordinal.sup f).cof ≤ # ι

source

theorem ordinal.sup_lt_ord_lift {ι : Type u} {f : ι → ordinal} {c : ordinal} (hι : (# ι).lift < c.cof) (hf : ∀ (i : ι), f i < c) :

ordinal.sup f < c

source

theorem ordinal.sup_lt_ord {ι : Type u} {f : ι → ordinal} {c : ordinal} (hι : # ι < c.cof) :

(∀ (i : ι), f i < c) → ordinal.sup f < c

source

theorem ordinal.sup_lt_lift {ι : Type u} {f : ι → cardinal} {c : cardinal} (hι : (# ι).lift < c.ord.cof) (hf : ∀ (i : ι), f i < c) :

cardinal.sup f < c

source

theorem ordinal.sup_lt {ι : Type u} {f : ι → cardinal} {c : cardinal} (hι : # ι < c.ord.cof) :

(∀ (i : ι), f i < c) → cardinal.sup f < c

source

theorem ordinal.exists_blsub_cof (o : ordinal) :

∃ (f : Π (a : ordinal), a < o.cof.ord → ordinal), o.cof.ord.blsub f = o

source

theorem ordinal.le_cof_iff_blsub {b : ordinal} {a : cardinal} :

a ≤ b.cof ↔ ∀ {o : ordinal} (f : Π (a : ordinal), a < o → ordinal), o.blsub f = b → a ≤ o.card

source

theorem ordinal.cof_blsub_le_lift {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :

(o.blsub f).cof ≤ o.card.lift

source

theorem ordinal.cof_blsub_le {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :

(o.blsub f).cof ≤ o.card

source

theorem ordinal.blsub_lt_ord_lift {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : ordinal} (ho : o.card.lift < c.cof) (hf : ∀ (i : ordinal) (hi : i < o), f i hi < c) :

o.blsub f < c

source

theorem ordinal.blsub_lt_ord {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : ordinal} (ho : o.card < c.cof) (hf : ∀ (i : ordinal) (hi : i < o), f i hi < c) :

o.blsub f < c

source

theorem ordinal.cof_bsup_le_lift {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} (H : ∀ (i : ordinal) (h : i < o), f i h < o.bsup f) :

(o.bsup f).cof ≤ o.card.lift

source

theorem ordinal.cof_bsup_le {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} :

(∀ (i : ordinal) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ o.card

source

theorem ordinal.bsup_lt_ord_lift {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : ordinal} (ho : o.card.lift < c.cof) (hf : ∀ (i : ordinal) (hi : i < o), f i hi < c) :

o.bsup f < c

source

theorem ordinal.bsup_lt_ord {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : ordinal} (ho : o.card < c.cof) :

(∀ (i : ordinal) (hi : i < o), f i hi < c) → o.bsup f < c

Basic results #

source

@[simp]

theorem ordinal.cof_zero :

0.cof = 0

source

@[simp]

theorem ordinal.cof_eq_zero {o : ordinal} :

o.cof = 0 ↔ o = 0

source

@[simp]

theorem ordinal.cof_succ (o : ordinal) :

o.succ.cof = 1

source

@[simp]

theorem ordinal.cof_eq_one_iff_is_succ {o : ordinal} :

o.cof = 1 ↔ ∃ (a : ordinal), o = a.succ

source

@[simp]

theorem ordinal.cof_add (a b : ordinal) :

b ≠ 0 → (a + b).cof = b.cof

source

def ordinal.is_fundamental_sequence (a o : ordinal) (f : Π (b : ordinal), b < o → ordinal) :

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.is_fundamental_sequence o f = (o ≤ a.cof.ord ∧ (∀ {i j : ordinal} (hi : i < o) (hj : j < o), i < j → f i hi < f j hj) ∧ o.blsub f = a)

source

theorem ordinal.is_fundamental_sequence.cof_eq {a o : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) :

a.cof.ord = o

source

theorem ordinal.is_fundamental_sequence.strict_mono {a o : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) {i j : ordinal} (hi : i < o) (hj : j < o) :

i < j → f i hi < f j hj

source

theorem ordinal.is_fundamental_sequence.blsub_eq {a o : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) :

o.blsub f = a

source

theorem ordinal.is_fundamental_sequence_id_of_le_cof {o : ordinal} (h : o ≤ o.cof.ord) :

o.is_fundamental_sequence o (λ (a : ordinal) (_x : a < o), a)

source

theorem ordinal.is_fundamental_sequence_zero {f : Π (b : ordinal), b < 0 → ordinal} :

0.is_fundamental_sequence 0 f

source

theorem ordinal.is_fundamental_sequence_succ {o : ordinal} :

o.succ.is_fundamental_sequence 1 (λ (_x : ordinal) (_x : _x < 1), o)

source

theorem ordinal.is_fundamental_sequence.monotone {a o : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) {i j : ordinal} (hi : i < o) (hj : j < o) (hij : i ≤ j) :

f i hi ≤ f j hj

source

theorem ordinal.is_fundamental_sequence.trans {a o o' : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) {g : Π (b : ordinal), b < o' → ordinal} (hg : o.is_fundamental_sequence o' g) :

a.is_fundamental_sequence o' (λ (i : ordinal) (hi : i < o'), f (g i hi) _)

source

theorem ordinal.exists_fundamental_sequence (a : ordinal) :

∃ (f : Π (b : ordinal), b < a.cof.ord → ordinal), a.is_fundamental_sequence a.cof.ord f

Every ordinal has a fundamental sequence.

source

@[simp]

theorem ordinal.cof_cof (a : ordinal) :

a.cof.ord.cof = a.cof

source

theorem ordinal.omega_le_cof {o : ordinal} :

ω ≤ o.cof ↔ o.is_limit

source

@[simp]

theorem ordinal.cof_omega :

ω.cof = ω

source

theorem ordinal.cof_eq' {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (h : (ordinal.type r).is_limit) :

∃ (S : set α), (∀ (a : α), ∃ (b : α) (H : b ∈ S), r a b) ∧ # ↥S = (ordinal.type r).cof

source

@[simp]

theorem ordinal.cof_univ :

ordinal.univ.cof = cardinal.univ

Infinite pigeonhole principle #

source

theorem ordinal.unbounded_of_unbounded_sUnion {α : Type u_1} (r : α → α → Prop) [wo : is_well_order α r] {s : set (set α)} (h₁ : set.unbounded r (⋃₀s)) (h₂ : # ↥s < strict_order.cof r) :

∃ (x : set α) (H : 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

source

theorem ordinal.unbounded_of_unbounded_Union {α β : Type u} (r : α → α → Prop) [wo : is_well_order α r] (s : β → set α) (h₁ : set.unbounded r (⋃ (x : β), s x)) (h₂ : # β < strict_order.cof 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

source

theorem ordinal.infinite_pigeonhole {β α : Type u} (f : β → α) (h₁ : ω ≤ # β) (h₂ : # α < (# β).ord.cof) :

∃ (a : α), # ↥(f ⁻¹' {a}) = # β

The infinite pigeonhole principle

source

theorem ordinal.infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : cardinal) (hθ : θ ≤ # β) (h₁ : ω ≤ θ) (h₂ : # α < θ.ord.cof) :

∃ (a : α), θ ≤ # ↥(f ⁻¹' {a})

pigeonhole principle for a cardinality below the cardinality of the domain

source

theorem ordinal.infinite_pigeonhole_set {β α : Type u} {s : set β} (f : ↥s → α) (θ : cardinal) (hθ : θ ≤ # ↥s) (h₁ : ω ≤ θ) (h₂ : # α < θ.ord.cof) :

∃ (a : α) (t : set β) (h : t ⊆ s), θ ≤ # ↥t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, _⟩ = a

Regular and inaccessible cardinals #

source

def cardinal.is_limit (c : cardinal) :

Prop

A cardinal is a limit if it is not zero or a successor cardinal. Note that ω is a limit cardinal by this definition.

Equations

c.is_limit = (c ≠ 0 ∧ ∀ (x : cardinal), x < c → x.succ < c)

source

def cardinal.is_strong_limit (c : cardinal) :

Prop

A cardinal is a strong limit if it is not zero and it is closed under powersets. Note that ω is a strong limit by this definition.

Equations

c.is_strong_limit = (c ≠ 0 ∧ ∀ (x : cardinal), x < c → 2 ^ x < c)

source

theorem cardinal.is_strong_limit.is_limit {c : cardinal} (H : c.is_strong_limit) :

c.is_limit

source

def cardinal.is_regular (c : cardinal) :

Prop

A cardinal is regular if it is infinite and it equals its own cofinality.

Equations

c.is_regular = (ω ≤ c ∧ c.ord.cof = c)

source

theorem cardinal.is_regular.omega_le {c : cardinal} (H : c.is_regular) :

ω ≤ c

source

theorem cardinal.is_regular.cof_eq {c : cardinal} (H : c.is_regular) :

c.ord.cof = c

source

theorem cardinal.is_regular.pos {c : cardinal} (H : c.is_regular) :

0 < c

source

theorem cardinal.is_regular.ord_pos {c : cardinal} (H : c.is_regular) :

0 < c.ord

source

theorem cardinal.is_regular_cof {o : ordinal} (h : o.is_limit) :

o.cof.is_regular

source

theorem cardinal.is_regular_omega :

ω.is_regular

source

theorem cardinal.is_regular_succ {c : cardinal} (h : ω ≤ c) :

c.succ.is_regular

source

theorem cardinal.is_regular_aleph_one :

(cardinal.aleph 1).is_regular

source

theorem cardinal.is_regular_aleph'_succ {o : ordinal} (h : ω ≤ o) :

(cardinal.aleph' o.succ).is_regular

source

theorem cardinal.is_regular_aleph_succ (o : ordinal) :

(cardinal.aleph o.succ).is_regular

source

theorem cardinal.infinite_pigeonhole_card_lt {β α : Type u} (f : β → α) (w : # α < # β) (w' : ω ≤ # α) :

∃ (a : α), # α < # ↥(f ⁻¹' {a})

A function whose codomain's cardinality is infinite but strictly smaller than its domain's has a fiber with cardinality strictly great than the codomain.

source

theorem cardinal.exists_infinite_fiber {β α : Type u_1} (f : β → α) (w : # α < # β) (w' : infinite α) :

∃ (a : α), infinite ↥(f ⁻¹' {a})

A function whose codomain's cardinality is infinite but strictly smaller than its domain's has an infinite fiber.

source

theorem cardinal.le_range_of_union_finset_eq_top {α : Type u_1} {β : Type u_2} [infinite β] (f : α → finset β) (w : (⋃ (a : α), ↑(f a)) = ⊤) :

# β ≤ # ↥(set.range f)

If an infinite type β can be expressed as a union of finite sets, then the cardinality of the collection of those finite sets must be at least the cardinality of β.

source

theorem cardinal.lsub_lt_ord_lift_of_is_regular {ι : Type u_1} {f : ι → ordinal} {c : cardinal} (hc : c.is_regular) (hι : (# ι).lift < c) :

(∀ (i : ι), f i < c.ord) → ordinal.lsub f < c.ord

source

theorem cardinal.lsub_lt_ord_of_is_regular {ι : Type (max u_1 u_2)} {f : ι → ordinal} {c : cardinal} (hc : c.is_regular) (hι : # ι < c) :

(∀ (i : ι), f i < c.ord) → ordinal.lsub f < c.ord

source

theorem cardinal.sup_lt_ord_lift_of_is_regular {ι : Type u_1} {f : ι → ordinal} {c : cardinal} (hc : c.is_regular) (hι : (# ι).lift < c) :

(∀ (i : ι), f i < c.ord) → ordinal.sup f < c.ord

source

theorem cardinal.sup_lt_ord_of_is_regular {ι : Type (max u_1 u_2)} {f : ι → ordinal} {c : cardinal} (hc : c.is_regular) (hι : # ι < c) :

(∀ (i : ι), f i < c.ord) → ordinal.sup f < c.ord

source

theorem cardinal.blsub_lt_ord_lift_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : cardinal} (hc : c.is_regular) (ho : o.card.lift < c) :

(∀ (i : ordinal) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord

source

theorem cardinal.blsub_lt_ord_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : cardinal} (hc : c.is_regular) (ho : o.card < c) :

(∀ (i : ordinal) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord

source

theorem cardinal.bsup_lt_ord_lift_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : cardinal} (hc : c.is_regular) (hι : o.card.lift < c) :

(∀ (i : ordinal) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord

source

theorem cardinal.bsup_lt_ord_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : cardinal} (hc : c.is_regular) (hι : o.card < c) :

(∀ (i : ordinal) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord

source

theorem cardinal.sup_lt_lift_of_is_regular {ι : Type u} {f : ι → cardinal} {c : cardinal} (hc : c.is_regular) (hι : (# ι).lift < c) :

(∀ (i : ι), f i < c) → cardinal.sup f < c

source

theorem cardinal.sup_lt_of_is_regular {ι : Type u} {f : ι → cardinal} {c : cardinal} (hc : c.is_regular) (hι : # ι < c) :

(∀ (i : ι), f i < c) → cardinal.sup f < c

source

theorem cardinal.sum_lt_lift_of_is_regular {ι : Type u} {f : ι → cardinal} {c : cardinal} (hc : c.is_regular) (hι : (# ι).lift < c) (hf : ∀ (i : ι), f i < c) :

cardinal.sum f < c

source