mathlib documentation

set_theory.cofinality

Cofinality #

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

Main Definitions #

Main Statements #

Implementation Notes #

Tags #

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

source
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
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
def strict_order.cof {α : Type u_1} (r : α → α → Prop) [h : is_irrefl α r] :
cardinal
Equations
source
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, ¬(b > a). 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
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
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
@[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
@[simp]
theorem ordinal.cof_cof (o : ordinal) :
o.cof.ord.cof = o.cof
source
theorem ordinal.omega_le_cof {o : ordinal} :
cardinal.omega ≤ o.cof ↔ o.is_limit
source
@[simp]
theorem ordinal.cof_omega  :
ω.cof = cardinal.omega
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
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.cof_bsup_le_lift {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.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
@[simp]
theorem ordinal.cof_univ  :
ordinal.univ.cof = cardinal.univ
source
theorem ordinal.sup_lt_ord {ι : Type u} (f : ι → ordinal) {c : ordinal} (H1 : # ι < c.cof) (H2 : ∀ (i : ι), f i < c) :
ordinal.sup f < c
source
theorem ordinal.sup_lt {ι : Type u} (f : ι → cardinal) {c : cardinal} (H1 : # ι < c.ord.cof) (H2 : ∀ (i : ι), f i < c) :
cardinal.sup f < c
source
theorem ordinal.unbounded_of_unbounded_sUnion {α : Type u_1} (r : α → α → Prop) [wo : is_well_order α r] {s : set (set α)} (h₁ : unbounded r (⋃₀s)) (h₂ : # ↥s < strict_order.cof r) :
∃ (x : set α) (H : x ∈ s), 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₁ : unbounded r (⋃ (x : β), s x)) (h₂ : # β < strict_order.cof r) :
∃ (x : β), 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₁ : cardinal.omega ≤ # β) (h₂ : # α < (# β).ord.cof) :
∃ (a : α), # ↥(f ⁻¹' {a}) = # β

The infinite pigeonhole principle

source
theorem ordinal.infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : cardinal) (hθ : θ ≤ # β) (h₁ : cardinal.omega ≤ θ) (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₁ : cardinal.omega ≤ θ) (h₂ : # α < θ.ord.cof) :
∃ (a : α) (t : set β) (h : t ⊆ s), θ ≤ # ↥t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, _⟩ = a
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
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
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
source
theorem cardinal.cof_is_regular {o : ordinal} (h : o.is_limit) :
o.cof.is_regular
source
theorem cardinal.omega_is_regular  :
cardinal.omega.is_regular
source
theorem cardinal.succ_is_regular {c : cardinal} (h : cardinal.omega ≤ c) :
c.succ.is_regular
source
theorem cardinal.sup_lt_ord_of_is_regular {ι : Type u} (f : ι → ordinal) {c : cardinal} (hc : c.is_regular) (H1 : # ι < c) (H2 : ∀ (i : ι), f i < c.ord) :
ordinal.sup f < c.ord
source
theorem cardinal.sup_lt_of_is_regular {ι : Type u} (f : ι → cardinal) {c : cardinal} (hc : c.is_regular) (H1 : # ι < c) (H2 : ∀ (i : ι), f i < c) :
cardinal.sup f < c
source
theorem cardinal.sum_lt_of_is_regular {ι : Type u} (f : ι → cardinal) {c : cardinal} (hc : c.is_regular) (H1 : # ι < c) (H2 : ∀ (i : ι), f i < c) :
cardinal.sum f < c
source
def cardinal.is_inaccessible (c : cardinal) :
Prop

A cardinal is inaccessible if it is an uncountable regular strong limit cardinal.

Equations
source
theorem cardinal.is_inaccessible.mk {c : cardinal} (h₁ : cardinal.omega < c) (h₂ : c ≤ c.ord.cof) (h₃ : ∀ (x : cardinal), x < c → 2 ^ x < c) :
c.is_inaccessible
source
theorem cardinal.univ_inaccessible  :
cardinal.univ.is_inaccessible
source
theorem cardinal.lt_power_cof {c : cardinal} :
cardinal.omega ≤ c → c < c ^ c.ord.cof
source
theorem cardinal.lt_cof_power {a b : cardinal} (ha : cardinal.omega ≤ a) (b1 : 1 < b) :
a < (b ^ a).ord.cof