# mathlibdocumentation

set_theory.cofinality

# Cofinality on ordinals, regular cardinals

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

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

Equations
• = (λ (S : {S // ∀ (a : α), ∃ (b : α) (H : b S), r a b}), # S)
theorem order.cof_le {α : Type u_1} (r : α → α → Prop) [ r] {S : set α} :
(∀ (a : α), ∃ (b : α) (H : b S), r a b) # S

theorem order.le_cof {α : Type u_1} {r : α → α → Prop} [ r] (c : cardinal) :
c ∀ {S : set α}, (∀ (a : α), ∃ (b : α) (H : b S), r a b)c # S

theorem rel_iso.cof.aux {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] :

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

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

Equations
def ordinal.cof  :

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
• o.cof = (λ (_x : Well_order), ordinal.cof._match_1 _x) ordinal.cof._proof_1
• ordinal.cof._match_1 {α := α, r := r, wo := _x} =
theorem ordinal.cof_type {α : Type u_1} (r : α → α → Prop) [ r] :

theorem ordinal.le_cof_type {α : Type u_1} {r : α → α → Prop} [ r] {c : cardinal} :
c (ordinal.type r).cof ∀ (S : set α), (∀ (a : α), ∃ (b : α) (H : b S), ¬r b a)c # S

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

theorem ordinal.lt_cof_type {α : Type u_1} {r : α → α → Prop} [ r] (S : set α) :
# S < (ordinal.type r).cof(∃ (a : α), ∀ (b : α), b Sr b a)

theorem ordinal.cof_eq {α : Type u_1} (r : α → α → Prop) [ r] :
∃ (S : set α), (∀ (a : α), ∃ (b : α) (H : b S), ¬r b a) # S = (ordinal.type r).cof

theorem ordinal.ord_cof_eq {α : Type u_1} (r : α → α → Prop) [ r] :
∃ (S : set α), (∀ (a : α), ∃ (b : α) (H : b S), ¬r b a) ordinal.type (subrel r S) = (ordinal.type r).cof.ord

theorem ordinal.lift_cof (o : ordinal) :

theorem ordinal.cof_le_card (o : ordinal) :

theorem ordinal.cof_ord_le (c : cardinal) :
c.ord.cof c

@[simp]
theorem ordinal.cof_zero  :
0.cof = 0

@[simp]
theorem ordinal.cof_eq_zero {o : ordinal} :
o.cof = 0 o = 0

@[simp]
theorem ordinal.cof_succ (o : ordinal) :
o.succ.cof = 1

@[simp]
theorem ordinal.cof_eq_one_iff_is_succ {o : ordinal} :
o.cof = 1 ∃ (a : ordinal), o = a.succ

@[simp]
theorem ordinal.cof_add (a b : ordinal) :
b 0(a + b).cof = b.cof

@[simp]
theorem ordinal.cof_cof (o : ordinal) :

@[simp]
theorem ordinal.cof_omega  :

theorem ordinal.cof_eq' {α : Type u_1} (r : α → α → Prop) [ r] :
(ordinal.type r).is_limit(∃ (S : set α), (∀ (a : α), ∃ (b : α) (H : b S), r a b) # S = (ordinal.type r).cof)

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

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

theorem ordinal.cof_bsup_le_lift {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
(∀ (i : ordinal) (h : i < o), f i h < o.bsup f)(o.bsup f).cof o.card.lift

theorem ordinal.cof_bsup_le {o : ordinal} (f : Π (a : ordinal), a < oordinal) :
(∀ (i : ordinal) (h : i < o), f i h < o.bsup f)(o.bsup f).cof o.card

@[simp]

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

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

theorem ordinal.unbounded_of_unbounded_sUnion {α : Type u_1} (r : α → α → Prop) [wo : r] {s : set (set α)} :
(⋃₀s)(∃ (x : set α) (H : x s), x)

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

theorem ordinal.unbounded_of_unbounded_Union {α β : Type u} (r : α → α → Prop) [wo : r] (s : β → set α) :
(⋃ (x : β), s x)(∃ (x : β), (s x))

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

theorem ordinal.infinite_pigeonhole {β α : Type u} (f : β → α) :
# α < (# β).ord.cof(∃ (a : α), # (f ⁻¹' {a}) = # β)

The infinite pigeonhole principle

theorem ordinal.infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : cardinal) :
θ # β# α < θ.ord.cof(∃ (a : α), θ # (f ⁻¹' {a}))

pigeonhole principle for a cardinality below the cardinality of the domain

theorem ordinal.infinite_pigeonhole_set {β α : Type u} {s : set β} (f : s → α) (θ : cardinal) :
θ # s# α < θ.ord.cof(∃ (a : α) (t : set β) (h : t s), θ # t ∀ ⦃x : β⦄ (hx : x t), f x, _⟩ = a)

def cardinal.is_limit  :
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

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
def cardinal.is_regular  :
cardinal → Prop

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

Equations
theorem cardinal.sup_lt_ord_of_is_regular {ι : Type u} (f : ι → ordinal) {c : cardinal} :
c.is_regular# ι < c(∀ (i : ι), f i < c.ord) < c.ord

theorem cardinal.sup_lt_of_is_regular {ι : Type u} (f : ι → cardinal) {c : cardinal} :
c.is_regular# ι < c(∀ (i : ι), f i < c)

theorem cardinal.sum_lt_of_is_regular {ι : Type u} (f : ι → cardinal) {c : cardinal} :
c.is_regular# ι < c(∀ (i : ι), f i < c)

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

Equations
theorem cardinal.is_inaccessible.mk {c : cardinal} :
c c.ord.cof(∀ (x : cardinal), x < c2 ^ x < c) → c.is_inaccessible

theorem cardinal.lt_power_cof {c : cardinal} :
c < c ^ c.ord.cof

theorem cardinal.lt_cof_power {a b : cardinal} :
1 < ba < (b ^ a).ord.cof