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.IsStrongLimit c means that c is a strong limit cardinal: c ≠ 0 ∧ ∀ x < c, 2 ^ x < c.
• Cardinal.IsRegular c means that c is a regular cardinal: ℵ₀ ≤ c ∧ c.ord.cof = c.
• Cardinal.IsInaccessible c means that c is strongly inaccessible: ℵ₀ < c ∧ IsRegular c ∧ IsStrongLimit 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

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.

Equations

• Order.cof r = sInf {c : Cardinal.{?u.6} | ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ Cardinal.mk ↑S = c}

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

theorem Order.le_cof {α : Type u} {r : α → α → Prop} [IsRefl α r] (c : Cardinal.{u}) : c ≤ Order.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

@[deprecated RelIso.cof_eq]

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

@[deprecated Order.cof]

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

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

Equations

• StrictOrder.cof r = Order.cof (Function.swap rᶜ)

@[deprecated]

theorem StrictOrder.cof_nonempty {α : Type u} (r : α → α → Prop) [IsIrrefl α r] : {c : Cardinal.{u} | ∃ (S : Set α), Set.Unbounded r S ∧ Cardinal.mk ↑S = c}.Nonempty

The set in the definition of Order.StrictOrder.cof is nonempty.

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.

Equations

• o.cof = Quotient.liftOn o (fun (a : WellOrder) => Order.cof (Function.swap a.rᶜ)) Ordinal.cof.proof_1

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

theorem Ordinal.cof_type_lt {α : Type u} [LinearOrder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] : (Ordinal.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 ≤ (Ordinal.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) : (Ordinal.type r).cof ≤ Cardinal.mk ↑S

theorem Ordinal.lt_cof_type {α : Type u} {r : α → α → Prop} [IsWellOrder α r] {S : Set α} : Cardinal.mk ↑S < (Ordinal.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 = (Ordinal.type r).cof

theorem Ordinal.ord_cof_eq {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : ∃ (S : Set α), Set.Unbounded r S ∧ Ordinal.type (Subrel r S) = (Ordinal.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}), Ordinal.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}), Ordinal.lsub f = o ∧ Cardinal.mk ι = a}

@[simp]

theorem Ordinal.lift_cof (o : Ordinal.{v}) : Cardinal.lift.{u, v} o.cof = (Ordinal.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}), Ordinal.lsub f = o ∧ Cardinal.mk ι = o.cof

theorem Ordinal.cof_lsub_le {ι : Type u} (f : ι → Ordinal.{u}) : (Ordinal.lsub f).cof ≤ Cardinal.mk ι

theorem Ordinal.cof_lsub_le_lift {ι : Type u} (f : ι → Ordinal.{max u v} ) : (Ordinal.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}), Ordinal.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) : Ordinal.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) → Ordinal.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 ι)

@[deprecated Ordinal.cof_iSup_le_lift]

theorem Ordinal.cof_sup_le_lift {ι : Type u} {f : ι → Ordinal.{max u v} } (H : ∀ (i : ι), f i < Ordinal.sup f) : (Ordinal.sup 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 ι

@[deprecated Ordinal.cof_iSup_le]

theorem Ordinal.cof_sup_le {ι : Type u} {f : ι → Ordinal.{u}} (H : ∀ (i : ι), f i < Ordinal.sup f) : (Ordinal.sup 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

@[deprecated Ordinal.iSup_lt_ord_lift]

theorem Ordinal.sup_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) : Ordinal.sup 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

@[deprecated Ordinal.iSup_lt_ord]

theorem Ordinal.sup_lt_ord {ι : Type u} {f : ι → Ordinal.{u}} {c : Ordinal.{u}} (hι : Cardinal.mk ι < c.cof) : (∀ (i : ι), f i < c) → Ordinal.sup 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) : Ordinal.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 → Ordinal.nfpFamily f a < c

@[deprecated Ordinal.nfpFamily_lt_ord_lift]

theorem Ordinal.nfpBFamily_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v} } {c : Ordinal.{max u v} } (hc : Cardinal.aleph0 < c.cof) (hc' : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c, f i hi b < c) {a : Ordinal.{max u v} } : a < c → o.nfpBFamily f a < c

@[deprecated Ordinal.nfpFamily_lt_ord]

theorem Ordinal.nfpBFamily_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}} {c : Ordinal.{u}} (hc : Cardinal.aleph0 < c.cof) (hc' : o.card < c.cof) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c, f i hi b < c) {a : Ordinal.{u}} : a < c → o.nfpBFamily 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 → Ordinal.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 : Ordinal.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

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.

Equations

• a.IsFundamentalSequence o f = (o ≤ a.cof.ord ∧ (∀ {i j : Ordinal.{?u.38}} (hi : i < o) (hj : j < o), i < j → f i hi < f j hj) ∧ o.blsub f = a)

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}} : Ordinal.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 : Ordinal.IsNormal f) {a o : Ordinal.{u}} (ha : a.IsLimit) {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 : Ordinal.IsNormal f) {a : Ordinal.{u_1}} (ha : a.IsLimit) : (f a).cof = a.cof

theorem Ordinal.IsNormal.cof_le {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : Ordinal.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 ↔ o.IsLimit

@[simp]

theorem Ordinal.cof_preOmega {o : Ordinal.{u_1}} (ho : o.IsLimit) : (Ordinal.preOmega o).cof = o.cof

@[simp]

theorem Ordinal.cof_omega {o : Ordinal.{u_1}} (ho : o.IsLimit) : (Ordinal.omega o).cof = o.cof

@[deprecated Ordinal.cof_preOmega]

theorem Ordinal.preAleph_cof {o : Ordinal.{u_1}} (ho : o.IsLimit) : (Cardinal.preAleph o).ord.cof = o.cof

@[deprecated Ordinal.cof_preOmega]

theorem Ordinal.aleph'_cof {o : Ordinal.{u_1}} (ho : o.IsLimit) : (Cardinal.aleph' o).ord.cof = o.cof

@[deprecated Ordinal.cof_omega]

theorem Ordinal.aleph_cof {o : Ordinal.{u_1}} (ho : o.IsLimit) : (Cardinal.aleph o).ord.cof = o.cof

@[simp]

theorem Ordinal.cof_omega0 : Ordinal.omega0.cof = Cardinal.aleph0

theorem Ordinal.cof_eq' {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (h : (Ordinal.type r).IsLimit) : ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ Cardinal.mk ↑S = (Ordinal.type r).cof

@[simp]

theorem Ordinal.cof_univ : Ordinal.univ.{u, v} .cof = Cardinal.univ.{u, v}

Infinite pigeonhole principle

theorem Ordinal.unbounded_of_unbounded_sUnion {α : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] {s : Set (Set α)} (h₁ : Set.Unbounded r (⋃₀ s)) (h₂ : Cardinal.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 Ordinal.unbounded_of_unbounded_iUnion {α β : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] (s : β → Set α) (h₁ : Set.Unbounded r (⋃ (x : β), s x)) (h₂ : Cardinal.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

theorem Ordinal.infinite_pigeonhole {β α : Type u} (f : β → α) (h₁ : Cardinal.aleph0 ≤ Cardinal.mk β) (h₂ : 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.{u}) (hθ : θ ≤ Cardinal.mk β) (h₁ : Cardinal.aleph0 ≤ θ) (h₂ : 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.{u}) (hθ : θ ≤ Cardinal.mk ↑s) (h₁ : Cardinal.aleph0 ≤ θ) (h₂ : Cardinal.mk α < θ.ord.cof) : ∃ (a : α) (t : Set β) (h : t ⊆ s), θ ≤ Cardinal.mk ↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a

Regular and inaccessible cardinals

def Cardinal.IsStrongLimit (c : Cardinal.{u_1}) : 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.IsStrongLimit = (c ≠ 0 ∧ ∀ x < c, 2 ^ x < c)

theorem Cardinal.IsStrongLimit.ne_zero {c : Cardinal.{u_1}} (h : c.IsStrongLimit) : c ≠ 0

theorem Cardinal.IsStrongLimit.two_power_lt {x c : Cardinal.{u_1}} (h : c.IsStrongLimit) : x < c → 2 ^ x < c

theorem Cardinal.isStrongLimit_aleph0 : Cardinal.aleph0.IsStrongLimit

theorem Cardinal.IsStrongLimit.isSuccLimit {c : Cardinal.{u_1}} (H : c.IsStrongLimit) : Order.IsSuccLimit c

theorem Cardinal.IsStrongLimit.isSuccPrelimit {c : Cardinal.{u_1}} (H : c.IsStrongLimit) : Order.IsSuccPrelimit c

theorem Cardinal.IsStrongLimit.aleph0_le {c : Cardinal.{u_1}} (H : c.IsStrongLimit) : Cardinal.aleph0 ≤ c

@[deprecated Cardinal.IsStrongLimit.isSuccLimit]

theorem Cardinal.IsStrongLimit.isLimit {c : Cardinal.{u_1}} (H : c.IsStrongLimit) : c.IsLimit

theorem Cardinal.isStrongLimit_beth {o : Ordinal.{u_1}} (H : Order.IsSuccPrelimit o) : (Cardinal.beth o).IsStrongLimit

theorem Cardinal.mk_bounded_subset {α : Type u_1} (h : ∀ x < Cardinal.mk α, 2 ^ x < Cardinal.mk α) {r : α → α → Prop} [IsWellOrder α r] (hr : (Cardinal.mk α).ord = Ordinal.type r) : Cardinal.mk { s : Set α // Set.Bounded r s } = Cardinal.mk α

theorem Cardinal.mk_subset_mk_lt_cof {α : Type u_1} (h : ∀ x < Cardinal.mk α, 2 ^ x < Cardinal.mk α) : Cardinal.mk { s : Set α // Cardinal.mk ↑s < (Cardinal.mk α).ord.cof } = Cardinal.mk α

def Cardinal.IsRegular (c : Cardinal.{u_1}) : Prop

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

Equations

• c.IsRegular = (Cardinal.aleph0 ≤ c ∧ c ≤ c.ord.cof)

theorem Cardinal.IsRegular.aleph0_le {c : Cardinal.{u_1}} (H : c.IsRegular) : Cardinal.aleph0 ≤ c

theorem Cardinal.IsRegular.cof_eq {c : Cardinal.{u_1}} (H : c.IsRegular) : c.ord.cof = c

theorem Cardinal.IsRegular.cof_omega_eq {o : Ordinal.{u_1}} (H : (Cardinal.aleph o).IsRegular) : (Ordinal.omega o).cof = Cardinal.aleph o

theorem Cardinal.IsRegular.pos {c : Cardinal.{u_1}} (H : c.IsRegular) : 0 < c

theorem Cardinal.IsRegular.nat_lt {c : Cardinal.{u_1}} (H : c.IsRegular) (n : ℕ) : ↑n < c

theorem Cardinal.IsRegular.ord_pos {c : Cardinal.{u_1}} (H : c.IsRegular) : 0 < c.ord

theorem Cardinal.isRegular_cof {o : Ordinal.{u_1}} (h : o.IsLimit) : o.cof.IsRegular

theorem Cardinal.isRegular_aleph0 : Cardinal.aleph0.IsRegular

theorem Cardinal.isRegular_succ {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) : (Order.succ c).IsRegular

theorem Cardinal.isRegular_aleph_one : (Cardinal.aleph 1).IsRegular

theorem Cardinal.isRegular_preAleph_succ {o : Ordinal.{u_1}} (h : Ordinal.omega0 ≤ o) : (Cardinal.preAleph (Order.succ o)).IsRegular

@[deprecated Cardinal.isRegular_preAleph_succ]

theorem Cardinal.isRegular_aleph'_succ {o : Ordinal.{u_1}} (h : Ordinal.omega0 ≤ o) : (Cardinal.aleph' (Order.succ o)).IsRegular

theorem Cardinal.isRegular_aleph_succ (o : Ordinal.{u_1}) : (Cardinal.aleph (Order.succ o)).IsRegular

theorem Cardinal.infinite_pigeonhole_card_lt {β α : Type u} (f : β → α) (w : Cardinal.mk α < Cardinal.mk β) (w' : Cardinal.aleph0 ≤ Cardinal.mk α) : ∃ (a : α), Cardinal.mk α < Cardinal.mk ↑(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.

theorem Cardinal.exists_infinite_fiber {β α : Type u} (f : β → α) (w : Cardinal.mk α < Cardinal.mk β) (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.

theorem Cardinal.le_range_of_union_finset_eq_top {α : Type u_1} {β : Type u_2} [Infinite β] (f : α → Finset β) (w : ⋃ (a : α), ↑(f a) = ⊤) : Cardinal.mk β ≤ Cardinal.mk ↑(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 β.

theorem Cardinal.lsub_lt_ord_lift_of_isRegular {ι : Type u} {f : ι → Ordinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) : (∀ (i : ι), f i < c.ord) → Ordinal.lsub f < c.ord

theorem Cardinal.lsub_lt_ord_of_isRegular {ι : Type (max u_1 u_2)} {f : ι → Ordinal.{max u_1 u_2} } {c : Cardinal.{max u_1 u_2} } (hc : c.IsRegular) (hι : Cardinal.mk ι < c) : (∀ (i : ι), f i < c.ord) → Ordinal.lsub f < c.ord

theorem Cardinal.iSup_lt_ord_lift_of_isRegular {ι : Type u} {f : ι → Ordinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) : (∀ (i : ι), f i < c.ord) → iSup f < c.ord

@[deprecated Cardinal.iSup_lt_ord_lift_of_isRegular]

theorem Cardinal.sup_lt_ord_lift_of_isRegular {ι : Type u} {f : ι → Ordinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) : (∀ (i : ι), f i < c.ord) → Ordinal.sup f < c.ord

theorem Cardinal.iSup_lt_ord_of_isRegular {ι : Type u_1} {f : ι → Ordinal.{u_1}} {c : Cardinal.{u_1}} (hc : c.IsRegular) (hι : Cardinal.mk ι < c) : (∀ (i : ι), f i < c.ord) → iSup f < c.ord

@[deprecated Cardinal.iSup_lt_ord_of_isRegular]

theorem Cardinal.sup_lt_ord_of_isRegular {ι : Type (max u_1 u_2)} {f : ι → Ordinal.{max u_1 u_2} } {c : Cardinal.{max u_1 u_2} } (hc : c.IsRegular) (hι : Cardinal.mk ι < c) : (∀ (i : ι), f i < c.ord) → Ordinal.sup f < c.ord

theorem Cardinal.blsub_lt_ord_lift_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (ho : Cardinal.lift.{v, u} o.card < c) : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord

theorem Cardinal.blsub_lt_ord_of_isRegular {o : Ordinal.{max u_1 u_2} } {f : (a : Ordinal.{max u_1 u_2} ) → a < o → Ordinal.{max u_1 u_2} } {c : Cardinal.{max u_1 u_2} } (hc : c.IsRegular) (ho : o.card < c) : (∀ (i : Ordinal.{max u_1 u_2} ) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord

theorem Cardinal.bsup_lt_ord_lift_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} o.card < c) : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord

theorem Cardinal.bsup_lt_ord_of_isRegular {o : Ordinal.{max u_1 u_2} } {f : (a : Ordinal.{max u_1 u_2} ) → a < o → Ordinal.{max u_1 u_2} } {c : Cardinal.{max u_1 u_2} } (hc : c.IsRegular) (hι : o.card < c) : (∀ (i : Ordinal.{max u_1 u_2} ) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord

theorem Cardinal.iSup_lt_lift_of_isRegular {ι : Type u} {f : ι → Cardinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) : (∀ (i : ι), f i < c) → iSup f < c

theorem Cardinal.iSup_lt_of_isRegular {ι : Type u_1} {f : ι → Cardinal.{u_1}} {c : Cardinal.{u_1}} (hc : c.IsRegular) (hι : Cardinal.mk ι < c) : (∀ (i : ι), f i < c) → iSup f < c

theorem Cardinal.sum_lt_lift_of_isRegular {ι : Type u} {f : ι → Cardinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) (hf : ∀ (i : ι), f i < c) : Cardinal.sum f < c

theorem Cardinal.sum_lt_of_isRegular {ι : Type u} {f : ι → Cardinal.{u}} {c : Cardinal.{u}} (hc : c.IsRegular) (hι : Cardinal.mk ι < c) : (∀ (i : ι), f i < c) → Cardinal.sum f < c

@[simp]

theorem Cardinal.card_lt_of_card_iUnion_lt {ι α : Type u} {t : ι → Set α} {c : Cardinal.{u}} (h : Cardinal.mk ↑(⋃ (i : ι), t i) < c) (i : ι) : Cardinal.mk ↑(t i) < c

@[simp]

theorem Cardinal.card_iUnion_lt_iff_forall_of_isRegular {ι α : Type u} {t : ι → Set α} {c : Cardinal.{u}} (hc : c.IsRegular) (hι : Cardinal.mk ι < c) : Cardinal.mk ↑(⋃ (i : ι), t i) < c ↔ ∀ (i : ι), Cardinal.mk ↑(t i) < c

theorem Cardinal.card_lt_of_card_biUnion_lt {α β : Type u} {s : Set α} {t : (a : α) → a ∈ s → Set β} {c : Cardinal.{u}} (h : Cardinal.mk ↑(⋃ (a : α), ⋃ (h : a ∈ s), t a h) < c) (a : α) (ha : a ∈ s) : Cardinal.mk ↑(t a ha) < c

theorem Cardinal.card_biUnion_lt_iff_forall_of_isRegular {α β : Type u} {s : Set α} {t : (a : α) → a ∈ s → Set β} {c : Cardinal.{u}} (hc : c.IsRegular) (hs : Cardinal.mk ↑s < c) : Cardinal.mk ↑(⋃ (a : α), ⋃ (h : a ∈ s), t a h) < c ↔ ∀ (a : α) (ha : a ∈ s), Cardinal.mk ↑(t a ha) < c

theorem Cardinal.nfpFamily_lt_ord_lift_of_isRegular {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord) {a : Ordinal.{max u v} } (ha : a < c.ord) : Ordinal.nfpFamily f a < c.ord

theorem Cardinal.nfpFamily_lt_ord_of_isRegular {ι : Type u} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}} (hc : c.IsRegular) (hι : Cardinal.mk ι < c) (hc' : c ≠ Cardinal.aleph0) {a : Ordinal.{u}} (hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord) : a < c.ord → Ordinal.nfpFamily f a < c.ord

@[deprecated Cardinal.nfpFamily_lt_ord_lift_of_isRegular]

theorem Cardinal.nfpBFamily_lt_ord_lift_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (ho : Cardinal.lift.{v, u} o.card < c) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord) {a : Ordinal.{max u v} } : a < c.ord → o.nfpBFamily f a < c.ord

@[deprecated Cardinal.nfpFamily_lt_ord_of_isRegular]

theorem Cardinal.nfpBFamily_lt_ord_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}} (hc : c.IsRegular) (ho : o.card < c) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord) {a : Ordinal.{u}} : a < c.ord → o.nfpBFamily f a < c.ord

theorem Cardinal.nfp_lt_ord_of_isRegular {f : Ordinal.{u_1} → Ordinal.{u_1}} {c : Cardinal.{u_1}} (hc : c.IsRegular) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ i < c.ord, f i < c.ord) {a : Ordinal.{u_1}} : a < c.ord → Ordinal.nfp f a < c.ord

theorem Cardinal.derivFamily_lt_ord_lift {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord) {a : Ordinal.{max u v} } : a < c.ord → Ordinal.derivFamily f a < c.ord

theorem Cardinal.derivFamily_lt_ord {ι : Type u} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}} (hc : c.IsRegular) (hι : Cardinal.mk ι < c) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord) {a : Ordinal.{u}} : a < c.ord → Ordinal.derivFamily f a < c.ord

@[deprecated Cardinal.derivFamily_lt_ord_lift]

theorem Cardinal.derivBFamily_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} o.card < c) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord) {a : Ordinal.{max u v} } : a < c.ord → o.derivBFamily f a < c.ord

@[deprecated Cardinal.derivFamily_lt_ord]

theorem Cardinal.derivBFamily_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}} (hc : c.IsRegular) (hι : o.card < c) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord) {a : Ordinal.{u}} : a < c.ord → o.derivBFamily f a < c.ord

theorem Cardinal.deriv_lt_ord {f : Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}} (hc : c.IsRegular) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ i < c.ord, f i < c.ord) {a : Ordinal.{u}} : a < c.ord → Ordinal.deriv f a < c.ord

def Cardinal.IsInaccessible (c : Cardinal.{u_1}) : Prop

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

Equations

• c.IsInaccessible = (Cardinal.aleph0 < c ∧ c.IsRegular ∧ c.IsStrongLimit)

theorem Cardinal.IsInaccessible.mk {c : Cardinal.{u_1}} (h₁ : Cardinal.aleph0 < c) (h₂ : c ≤ c.ord.cof) (h₃ : ∀ x < c, 2 ^ x < c) : c.IsInaccessible

theorem Cardinal.univ_inaccessible : Cardinal.univ.{u, v} .IsInaccessible

theorem Cardinal.lt_power_cof {c : Cardinal.{u}} : Cardinal.aleph0 ≤ c → c < c ^ c.ord.cof

theorem Cardinal.lt_cof_power {a b : Cardinal.{u_1}} (ha : Cardinal.aleph0 ≤ a) (b1 : 1 < b) : a < (b ^ a).ord.cof

theorem Ordinal.iSup_sequence_lt_omega1 {α : Type u} [Countable α] (o : α → Ordinal.{max u v} ) (ho : ∀ (n : α), o n < (Cardinal.aleph 1).ord) : iSup o < (Cardinal.aleph 1).ord