Cofinality on ordinals, regular cardinals
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}), cardinal.mk ↥S)
theorem
order.cof_le
{α : Type u_1}
(r : α → α → Prop)
[is_refl α r]
{S : set α} :
(∀ (a : α), ∃ (b : α) (H : b ∈ S), r a b) → order.cof r ≤ cardinal.mk ↥S
Equations
- strict_order.cof r = order.cof (λ (x y : α), ¬r y x)
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 = quot.lift_on o (λ (_x : Well_order), ordinal.cof._match_1 _x) ordinal.cof._proof_1
- ordinal.cof._match_1 {α := α, r := r, wo := _x} = strict_order.cof r
theorem
ordinal.cof_type
{α : Type u_1}
(r : α → α → Prop)
[is_well_order α r] :
(ordinal.type r).cof = strict_order.cof r
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 ≤ cardinal.mk ↥S
theorem
ordinal.cof_type_le
{α : Type u_1}
{r : α → α → Prop}
[is_well_order α r]
(S : set α) :
(∀ (a : α), ∃ (b : α) (H : b ∈ S), ¬r b a) → (ordinal.type r).cof ≤ cardinal.mk ↥S
theorem
ordinal.lt_cof_type
{α : Type u_1}
{r : α → α → Prop}
[is_well_order α r]
(S : set α) :
cardinal.mk ↥S < (ordinal.type r).cof → (∃ (a : α), ∀ (b : α), b ∈ S → r b a)
theorem
ordinal.cof_eq
{α : Type u_1}
(r : α → α → Prop)
[is_well_order α r] :
∃ (S : set α), (∀ (a : α), ∃ (b : α) (H : b ∈ S), ¬r b a) ∧ cardinal.mk ↥S = (ordinal.type r).cof
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
theorem
ordinal.cof_eq'
{α : Type u_1}
(r : α → α → Prop)
[is_well_order α r] :
(ordinal.type r).is_limit → (∃ (S : set α), (∀ (a : α), ∃ (b : α) (H : b ∈ S), r a b) ∧ cardinal.mk ↥S = (ordinal.type r).cof)
theorem
ordinal.cof_sup_le_lift
{ι : Type u_1}
(f : ι → ordinal) :
(∀ (i : ι), f i < ordinal.sup f) → (ordinal.sup f).cof ≤ (cardinal.mk ι).lift
theorem
ordinal.cof_sup_le
{ι : Type u}
(f : ι → ordinal) :
(∀ (i : ι), f i < ordinal.sup f) → (ordinal.sup f).cof ≤ cardinal.mk ι
theorem
ordinal.sup_lt_ord
{ι : Type u}
(f : ι → ordinal)
{c : ordinal} :
cardinal.mk ι < c.cof → (∀ (i : ι), f i < c) → ordinal.sup f < c
theorem
ordinal.sup_lt
{ι : Type u}
(f : ι → cardinal)
{c : cardinal} :
cardinal.mk ι < c.ord.cof → (∀ (i : ι), f i < c) → cardinal.sup f < c
theorem
ordinal.unbounded_of_unbounded_sUnion
{α : Type u_1}
(r : α → α → Prop)
[wo : is_well_order α r]
{s : set (set α)} :
unbounded r (⋃₀s) → cardinal.mk ↥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
theorem
ordinal.unbounded_of_unbounded_Union
{α β : Type u}
(r : α → α → Prop)
[wo : is_well_order α r]
(s : β → set α) :
unbounded r (⋃ (x : β), s x) → cardinal.mk β < 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
theorem
ordinal.infinite_pigeonhole
{β α : Type u}
(f : β → α) :
cardinal.omega ≤ cardinal.mk β → cardinal.mk α < (cardinal.mk β).ord.cof → (∃ (a : α), cardinal.mk ↥(f ⁻¹' {a}) = cardinal.mk β)
The infinite pigeonhole principle
theorem
ordinal.infinite_pigeonhole_card
{β α : Type u}
(f : β → α)
(θ : cardinal) :
θ ≤ cardinal.mk β → cardinal.omega ≤ θ → cardinal.mk α < θ.ord.cof → (∃ (a : α), θ ≤ cardinal.mk ↥(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) :
θ ≤ cardinal.mk ↥s → cardinal.omega ≤ θ → cardinal.mk α < θ.ord.cof → (∃ (a : α) (t : set β) (h : t ⊆ s), θ ≤ cardinal.mk ↥t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, _⟩ = a)
A cardinal is regular if it is infinite and it equals its own cofinality.
Equations
- c.is_regular = (cardinal.omega ≤ c ∧ c.ord.cof = c)
theorem
cardinal.sup_lt_ord_of_is_regular
{ι : Type u}
(f : ι → ordinal)
{c : cardinal} :
c.is_regular → cardinal.mk ι < c → (∀ (i : ι), f i < c.ord) → ordinal.sup f < c.ord
theorem
cardinal.sup_lt_of_is_regular
{ι : Type u}
(f : ι → cardinal)
{c : cardinal} :
c.is_regular → cardinal.mk ι < c → (∀ (i : ι), f i < c) → cardinal.sup f < c
theorem
cardinal.sum_lt_of_is_regular
{ι : Type u}
(f : ι → cardinal)
{c : cardinal} :
c.is_regular → cardinal.mk ι < c → (∀ (i : ι), f i < c) → cardinal.sum f < c
A cardinal is inaccessible if it is an uncountable regular strong limit cardinal.
Equations
- c.is_inaccessible = (cardinal.omega < c ∧ c.is_regular ∧ c.is_strong_limit)
theorem
cardinal.is_inaccessible.mk
{c : cardinal} :
cardinal.omega < c → c ≤ c.ord.cof → (∀ (x : cardinal), x < c → 2 ^ x < c) → c.is_inaccessible