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_1} (r : α → α → Prop) : Cardinal.{u_1}

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 | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ Cardinal.mk ↑S = c}

theorem Order.cof_nonempty {α : Type u_1} (r : α → α → Prop) [IsRefl α r] : Set.Nonempty {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ Cardinal.mk ↑S = c}

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

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

theorem Order.le_cof {α : Type u_1} {r : α → α → Prop} [IsRefl α r] (c : Cardinal.{u_1}) : c ≤ Order.cof r ↔ ∀ {S : Set α}, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) → c ≤ Cardinal.mk ↑S

theorem RelIso.cof_le_lift {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsRefl β s] (f : r ≃r s) : Cardinal.lift.{max u v, u} (Order.cof r) ≤ Cardinal.lift.{max u v, v} (Order.cof s)

theorem RelIso.cof_eq_lift {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsRefl α r] [IsRefl β s] (f : r ≃r s) : Cardinal.lift.{max u v, u} (Order.cof r) = Cardinal.lift.{max u v, v} (Order.cof s)

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

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

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

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ᶜ)

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

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. 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

• Ordinal.cof o = Quotient.liftOn o (fun a => StrictOrder.cof a.r) Ordinal.cof.proof_1

theorem Ordinal.cof_type {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r] : Ordinal.cof (Ordinal.type r) = StrictOrder.cof r

theorem Ordinal.le_cof_type {α : Type u_1} {r : α → α → Prop} [IsWellOrder α r] {c : Cardinal.{u_1}} : c ≤ Ordinal.cof (Ordinal.type r) ↔ ∀ (S : Set α), Set.Unbounded r S → c ≤ Cardinal.mk ↑S

theorem Ordinal.cof_type_le {α : Type u_1} {r : α → α → Prop} [IsWellOrder α r] {S : Set α} (h : Set.Unbounded r S) : Ordinal.cof (Ordinal.type r) ≤ Cardinal.mk ↑S

theorem Ordinal.lt_cof_type {α : Type u_1} {r : α → α → Prop} [IsWellOrder α r] {S : Set α} : Cardinal.mk ↑S < Ordinal.cof (Ordinal.type r) → Set.Bounded r S

theorem Ordinal.cof_eq {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r] : ∃ S, Set.Unbounded r S ∧ Cardinal.mk ↑S = Ordinal.cof (Ordinal.type r)

theorem Ordinal.ord_cof_eq {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r] : ∃ S, Set.Unbounded r S ∧ Ordinal.type (Subrel r S) = Cardinal.ord (Ordinal.cof (Ordinal.type r))

Cofinality of suprema and least strict upper bounds

theorem Ordinal.cof_lsub_def_nonempty (o : Ordinal.{u}) : Set.Nonempty {a | ∃ ι f, Ordinal.lsub f = o ∧ Cardinal.mk ι = a}

The set in the lsub characterization of cof is nonempty.

theorem Ordinal.cof_eq_sInf_lsub (o : Ordinal.{u}) : Ordinal.cof o = sInf {a | ∃ ι f, Ordinal.lsub f = o ∧ Cardinal.mk ι = a}

@[simp]

theorem Ordinal.lift_cof (o : Ordinal.{v}) : Cardinal.lift.{u, v} (Ordinal.cof o) = Ordinal.cof (Ordinal.lift.{u, v} o)

theorem Ordinal.cof_le_card (o : Ordinal.{u_2}) : Ordinal.cof o ≤ Ordinal.card o

theorem Ordinal.cof_ord_le (c : Cardinal.{u_2}) : Ordinal.cof (Cardinal.ord c) ≤ c

theorem Ordinal.ord_cof_le (o : Ordinal.{u}) : Cardinal.ord (Ordinal.cof o) ≤ o

theorem Ordinal.exists_lsub_cof (o : Ordinal.{u}) : ∃ ι f, Ordinal.lsub f = o ∧ Cardinal.mk ι = Ordinal.cof o

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

theorem Ordinal.cof_lsub_le_lift {ι : Type u} (f : ι → Ordinal.{max u v} ) : Ordinal.cof (Ordinal.lsub f) ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)

theorem Ordinal.le_cof_iff_lsub {o : Ordinal.{u}} {a : Cardinal.{u}} : a ≤ Ordinal.cof o ↔ ∀ {ι : 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 ι) < Ordinal.cof c) (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 ι < Ordinal.cof c) : (∀ (i : ι), f i < c) → Ordinal.lsub f < c

theorem Ordinal.cof_sup_le_lift {ι : Type u} {f : ι → Ordinal.{max u v} } (H : ∀ (i : ι), f i < Ordinal.sup f) : Ordinal.cof (Ordinal.sup f) ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)

theorem Ordinal.cof_sup_le {ι : Type u} {f : ι → Ordinal.{u}} (H : ∀ (i : ι), f i < Ordinal.sup f) : Ordinal.cof (Ordinal.sup f) ≤ Cardinal.mk ι

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 ι) < Ordinal.cof c) (hf : ∀ (i : ι), f i < c) : Ordinal.sup f < c

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

theorem Ordinal.iSup_lt {ι : Type u_2} {f : ι → Cardinal.{u_2}} {c : Cardinal.{u_2}} (hι : Cardinal.mk ι < Ordinal.cof (Cardinal.ord c)) : (∀ (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 < Ordinal.cof c) (hc' : Cardinal.lift.{v, u} (Cardinal.mk ι) < Ordinal.cof c) (hf : ∀ (i : ι) (b : Ordinal.{max u v} ), 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 < Ordinal.cof c) (hc' : Cardinal.mk ι < Ordinal.cof c) (hf : ∀ (i : ι) (b : Ordinal.{u}), b < c → f i b < c) {a : Ordinal.{u}} : a < c → Ordinal.nfpFamily f a < c

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

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

theorem Ordinal.nfp_lt_ord {f : Ordinal.{u_2} → Ordinal.{u_2}} {c : Ordinal.{u_2}} (hc : Cardinal.aleph0 < Ordinal.cof c) (hf : ∀ (i : Ordinal.{u_2}), i < c → f i < c) {a : Ordinal.{u_2}} : a < c → Ordinal.nfp f a < c

theorem Ordinal.exists_blsub_cof (o : Ordinal.{u}) : ∃ f, Ordinal.blsub (Cardinal.ord (Ordinal.cof o)) f = o

theorem Ordinal.le_cof_iff_blsub {b : Ordinal.{u}} {a : Cardinal.{u}} : a ≤ Ordinal.cof b ↔ ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), Ordinal.blsub o f = b → a ≤ Ordinal.card o

theorem Ordinal.cof_blsub_le_lift {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} ) : Ordinal.cof (Ordinal.blsub o f) ≤ Cardinal.lift.{v, u} (Ordinal.card o)

theorem Ordinal.cof_blsub_le {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}) : Ordinal.cof (Ordinal.blsub o f) ≤ Ordinal.card o

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} (Ordinal.card o) < Ordinal.cof c) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) : Ordinal.blsub o f < c

theorem Ordinal.blsub_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u}} {c : Ordinal.{u}} (ho : Ordinal.card o < Ordinal.cof c) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) : Ordinal.blsub o 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 < Ordinal.bsup o f) : Ordinal.cof (Ordinal.bsup o f) ≤ Cardinal.lift.{v, u} (Ordinal.card o)

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 < Ordinal.bsup o f) → Ordinal.cof (Ordinal.bsup o f) ≤ Ordinal.card o

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} (Ordinal.card o) < Ordinal.cof c) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) : Ordinal.bsup o f < c

theorem Ordinal.bsup_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u}} {c : Ordinal.{u}} (ho : Ordinal.card o < Ordinal.cof c) : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) → Ordinal.bsup o f < c

Basic results

@[simp]

theorem Ordinal.cof_zero : Ordinal.cof 0 = 0

@[simp]

theorem Ordinal.cof_eq_zero {o : Ordinal.{u_2}} : Ordinal.cof o = 0 ↔ o = 0

theorem Ordinal.cof_ne_zero {o : Ordinal.{u_2}} : Ordinal.cof o ≠ 0 ↔ o ≠ 0

@[simp]

theorem Ordinal.cof_succ (o : Ordinal.{u_2}) : Ordinal.cof (Order.succ o) = 1

@[simp]

theorem Ordinal.cof_eq_one_iff_is_succ {o : Ordinal.{u}} : Ordinal.cof o = 1 ↔ ∃ a, o = Order.succ a

def Ordinal.IsFundamentalSequence (a : Ordinal.{u}) (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

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

theorem Ordinal.IsFundamentalSequence.cof_eq {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : Ordinal.IsFundamentalSequence a o f) : Cardinal.ord (Ordinal.cof a) = o

theorem Ordinal.IsFundamentalSequence.strict_mono {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : Ordinal.IsFundamentalSequence a o f) {i : Ordinal.{u}} {j : Ordinal.{u}} (hi : i < o) (hj : j < o) : i < j → f i hi < f j hj

theorem Ordinal.IsFundamentalSequence.blsub_eq {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : Ordinal.IsFundamentalSequence a o f) : Ordinal.blsub o f = a

theorem Ordinal.IsFundamentalSequence.ord_cof {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : Ordinal.IsFundamentalSequence a o f) : Ordinal.IsFundamentalSequence a (Cardinal.ord (Ordinal.cof a)) fun i hi => f i (_ : i < o)

theorem Ordinal.IsFundamentalSequence.id_of_le_cof {o : Ordinal.{u}} (h : o ≤ Cardinal.ord (Ordinal.cof o)) : Ordinal.IsFundamentalSequence o o fun a x => a

theorem Ordinal.IsFundamentalSequence.zero {f : (b : Ordinal.{u_2}) → b < 0 → Ordinal.{u_2}} : Ordinal.IsFundamentalSequence 0 0 f

theorem Ordinal.IsFundamentalSequence.succ {o : Ordinal.{u}} : Ordinal.IsFundamentalSequence (Order.succ o) 1 fun x x => o

theorem Ordinal.IsFundamentalSequence.monotone {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : Ordinal.IsFundamentalSequence a o f) {i : Ordinal.{u}} {j : Ordinal.{u}} (hi : i < o) (hj : j < o) (hij : i ≤ j) : f i hi ≤ f j hj

theorem Ordinal.IsFundamentalSequence.trans {a : Ordinal.{u}} {o : Ordinal.{u}} {o' : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : Ordinal.IsFundamentalSequence a o f) {g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}} (hg : Ordinal.IsFundamentalSequence o o' g) : Ordinal.IsFundamentalSequence a o' fun i hi => f (g i hi) (_ : g i hi < o)

theorem Ordinal.exists_fundamental_sequence (a : Ordinal.{u}) : ∃ f, Ordinal.IsFundamentalSequence a (Cardinal.ord (Ordinal.cof a)) f

Every ordinal has a fundamental sequence.

@[simp]

theorem Ordinal.cof_cof (a : Ordinal.{u}) : Ordinal.cof (Cardinal.ord (Ordinal.cof a)) = Ordinal.cof a

theorem Ordinal.IsNormal.isFundamentalSequence {f : Ordinal.{u} → Ordinal.{u}} (hf : Ordinal.IsNormal f) {a : Ordinal.{u}} {o : Ordinal.{u}} (ha : Ordinal.IsLimit a) {g : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hg : Ordinal.IsFundamentalSequence a o g) : Ordinal.IsFundamentalSequence (f a) o fun b hb => f (g b hb)

theorem Ordinal.IsNormal.cof_eq {f : Ordinal.{u_2} → Ordinal.{u_2}} (hf : Ordinal.IsNormal f) {a : Ordinal.{u_2}} (ha : Ordinal.IsLimit a) : Ordinal.cof (f a) = Ordinal.cof a

theorem Ordinal.IsNormal.cof_le {f : Ordinal.{u_2} → Ordinal.{u_2}} (hf : Ordinal.IsNormal f) (a : Ordinal.{u_2}) : Ordinal.cof a ≤ Ordinal.cof (f a)

@[simp]

theorem Ordinal.cof_add (a : Ordinal.{u_2}) (b : Ordinal.{u_2}) : b ≠ 0 → Ordinal.cof (a + b) = Ordinal.cof b

theorem Ordinal.aleph0_le_cof {o : Ordinal.{u_2}} : Cardinal.aleph0 ≤ Ordinal.cof o ↔ Ordinal.IsLimit o

@[simp]

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

@[simp]

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

@[simp]

theorem Ordinal.cof_omega : Ordinal.cof Ordinal.omega = Cardinal.aleph0

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

@[simp]

theorem Ordinal.cof_univ : Ordinal.cof Ordinal.univ = Cardinal.univ

Infinite pigeonhole principle

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

theorem Ordinal.infinite_pigeonhole {β : Type u} {α : Type u} (f : β → α) (h₁ : Cardinal.aleph0 ≤ Cardinal.mk β) (h₂ : Cardinal.mk α < Ordinal.cof (Cardinal.ord (Cardinal.mk β))) : ∃ a, Cardinal.mk ↑(f ⁻¹' {a}) = Cardinal.mk β

The infinite pigeonhole principle

theorem Ordinal.infinite_pigeonhole_card {β : Type u} {α : Type u} (f : β → α) (θ : Cardinal.{u}) (hθ : θ ≤ Cardinal.mk β) (h₁ : Cardinal.aleph0 ≤ θ) (h₂ : Cardinal.mk α < Ordinal.cof (Cardinal.ord θ)) : ∃ a, θ ≤ Cardinal.mk ↑(f ⁻¹' {a})

Pigeonhole principle for a cardinality below the cardinality of the domain

theorem Ordinal.infinite_pigeonhole_set {β : Type u} {α : Type u} {s : Set β} (f : ↑s → α) (θ : Cardinal.{u}) (hθ : θ ≤ Cardinal.mk ↑s) (h₁ : Cardinal.aleph0 ≤ θ) (h₂ : Cardinal.mk α < Ordinal.cof (Cardinal.ord θ)) : ∃ a t h, θ ≤ Cardinal.mk ↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f { val := x, property := (_ : x ∈ s) } = a

Regular and inaccessible cardinals

def Cardinal.IsStrongLimit (c : Cardinal.{u_2}) : 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

• Cardinal.IsStrongLimit c = (c ≠ 0 ∧ ∀ (x : Cardinal.{u_2}), x < c → 2 ^ x < c)

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

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

theorem Cardinal.isStrongLimit_aleph0 : Cardinal.IsStrongLimit Cardinal.aleph0

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

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

theorem Cardinal.isStrongLimit_beth {o : Ordinal.{u_2}} (H : Order.IsSuccLimit o) : Cardinal.IsStrongLimit (Cardinal.beth o)

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

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

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

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

Equations

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

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

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

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

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

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

theorem Cardinal.isRegular_aleph0 : Cardinal.IsRegular Cardinal.aleph0

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

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

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

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

theorem Cardinal.infinite_pigeonhole_card_lt {β : Type u} {α : 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_2} {α : Type u_2} (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_2} {β : Type u_3} [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 : Cardinal.IsRegular c) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) : (∀ (i : ι), f i < Cardinal.ord c) → Ordinal.lsub f < Cardinal.ord c

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

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

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

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 : Cardinal.IsRegular c) (ho : Cardinal.lift.{v, u} (Ordinal.card o) < c) : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < Cardinal.ord c) → Ordinal.blsub o f < Cardinal.ord c

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

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 : Cardinal.IsRegular c) (hι : Cardinal.lift.{v, u} (Ordinal.card o) < c) : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < Cardinal.ord c) → Ordinal.bsup o f < Cardinal.ord c

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

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

theorem Cardinal.iSup_lt_of_isRegular {ι : Type u_2} {f : ι → Cardinal.{u_2}} {c : Cardinal.{u_2}} (hc : Cardinal.IsRegular c) (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 : Cardinal.IsRegular c) (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 : Cardinal.IsRegular c) (hι : Cardinal.mk ι < c) : (∀ (i : ι), f i < c) → Cardinal.sum f < 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 : Cardinal.IsRegular c) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ (i : ι) (b : Ordinal.{max u v} ), b < Cardinal.ord c → f i b < Cardinal.ord c) {a : Ordinal.{max u v} } (ha : a < Cardinal.ord c) : Ordinal.nfpFamily f a < Cardinal.ord c

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

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 : Cardinal.IsRegular c) (ho : Cardinal.lift.{v, u} (Ordinal.card o) < c) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ (i : Ordinal.{u}) (hi : i < o) (b : Ordinal.{max u v} ), b < Cardinal.ord c → f i hi b < Cardinal.ord c) {a : Ordinal.{max u v} } : a < Cardinal.ord c → Ordinal.nfpBFamily o f a < Cardinal.ord c

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

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

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

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

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 : Cardinal.IsRegular c) (hι : Cardinal.lift.{v, u} (Ordinal.card o) < c) (hc' : c ≠ Cardinal.aleph0) (hf : ∀ (i : Ordinal.{u}) (hi : i < o) (b : Ordinal.{max u v} ), b < Cardinal.ord c → f i hi b < Cardinal.ord c) {a : Ordinal.{max u v} } : a < Cardinal.ord c → Ordinal.derivBFamily o f a < Cardinal.ord c

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

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

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

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

Equations

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

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

theorem Cardinal.univ_inaccessible : Cardinal.IsInaccessible Cardinal.univ

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

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

theorem Ordinal.sup_sequence_lt_omega1 {α : Type u_2} [Countable α] (o : α → Ordinal.{max u_3 u_2} ) (ho : ∀ (n : α), o n < Cardinal.ord (Cardinal.aleph 1)) : Ordinal.sup o < Cardinal.ord (Cardinal.aleph 1)