mathlib3 documentation

set_theory.cardinal.cofinality

Cofinality #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main Definitions #

Main Statements #

Implementation Notes #

Tags #

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

Cofinality of orders #

source
noncomputable def order.cof {α : Type u_1} (r : α → α → Prop) :
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_nonempty {α : Type u_1} (r : α → α → Prop) [is_refl α r] :
{c : cardinal | ∃ (S : set α), (∀ (a : α), ∃ (b : α) (H : b ∈ S), r a b) ∧ cardinal.mk ↥S = c}.nonempty

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

source
theorem order.cof_le {α : Type u_1} (r : α → α → Prop) {S : set α} (h : ∀ (a : α), ∃ (b : α) (H : b ∈ S), r a b) :
order.cof r ≤ cardinal.mk ↥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 ≤ cardinal.mk ↥S
source
theorem rel_iso.cof_le_lift {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_refl β s] (f : r ≃r s) :
(order.cof r).lift ≤ (order.cof s).lift
source
theorem rel_iso.cof_eq_lift {α : 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_le {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [is_refl β s] (f : r ≃r s) :
order.cof r ≤ order.cof s
source
theorem rel_iso.cof_eq {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [is_refl α r] [is_refl β s] (f : r ≃r s) :
order.cof r = order.cof s
source
noncomputable def strict_order.cof {α : Type u_1} (r : α → α → Prop) :
cardinal

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

Equations
source
theorem strict_order.cof_nonempty {α : Type u_1} (r : α → α → Prop) [is_irrefl α r] :
{c : cardinal | ∃ (S : set α), set.unbounded r S ∧ cardinal.mk ↥S = c}.nonempty

The set in the definition of order.strict_order.cof is nonempty.

Cofinality of ordinals #

source
noncomputable 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, 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
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 α), set.unbounded r S → c ≤ cardinal.mk ↥S
source
theorem ordinal.cof_type_le {α : Type u_1} {r : α → α → Prop} [is_well_order α r] {S : set α} (h : set.unbounded r S) :
(ordinal.type r).cof ≤ cardinal.mk ↥S
source
theorem ordinal.lt_cof_type {α : Type u_1} {r : α → α → Prop} [is_well_order α r] {S : set α} :
cardinal.mk ↥S < (ordinal.type r).cof → set.bounded r S
source
theorem ordinal.cof_eq {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
∃ (S : set α), set.unbounded r S ∧ cardinal.mk ↥S = (ordinal.type r).cof
source
theorem ordinal.ord_cof_eq {α : Type u_1} (r : α → α → Prop) [is_well_order α 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 #

source
theorem ordinal.cof_lsub_def_nonempty (o : ordinal) :
{a : cardinal | ∃ {ι : Type u} (f : ι → ordinal), ordinal.lsub f = o ∧ cardinal.mk ι = a}.nonempty

The set in the lsub characterization of cof is nonempty.

source
theorem ordinal.cof_eq_Inf_lsub (o : ordinal) :
o.cof = has_Inf.Inf {a : cardinal | ∃ {ι : Type u} (f : ι → ordinal), ordinal.lsub f = o ∧ cardinal.mk ι = a}
source
@[simp]
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
theorem ordinal.ord_cof_le (o : ordinal) :
o.cof.ord ≤ o
source
theorem ordinal.exists_lsub_cof (o : ordinal) :
∃ {ι : Type u} (f : ι → ordinal), ordinal.lsub f = o ∧ cardinal.mk ι = o.cof
source
theorem ordinal.cof_lsub_le {ι : Type u} (f : ι → ordinal) :
(ordinal.lsub f).cof ≤ cardinal.mk ι
source
theorem ordinal.cof_lsub_le_lift {ι : Type u} (f : ι → ordinal) :
(ordinal.lsub f).cof ≤ (cardinal.mk ι).lift
source
theorem ordinal.le_cof_iff_lsub {o : ordinal} {a : cardinal} :
a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → ordinal), ordinal.lsub f = o → a ≤ cardinal.mk ι
source
theorem ordinal.lsub_lt_ord_lift {ι : Type u} {f : ι → ordinal} {c : ordinal} (hι : (cardinal.mk ι).lift < c.cof) (hf : ∀ (i : ι), f i < c) :
ordinal.lsub f < c
source
theorem ordinal.lsub_lt_ord {ι : Type u} {f : ι → ordinal} {c : ordinal} (hι : cardinal.mk ι < c.cof) :
(∀ (i : ι), f i < c) → ordinal.lsub f < c
source
theorem ordinal.cof_sup_le_lift {ι : Type u_1} {f : ι → ordinal} (H : ∀ (i : ι), f i < ordinal.sup f) :
(ordinal.sup f).cof ≤ (cardinal.mk ι).lift
source
theorem ordinal.cof_sup_le {ι : Type u} {f : ι → ordinal} (H : ∀ (i : ι), f i < ordinal.sup f) :
(ordinal.sup f).cof ≤ cardinal.mk ι
source
theorem ordinal.sup_lt_ord_lift {ι : Type u} {f : ι → ordinal} {c : ordinal} (hι : (cardinal.mk ι).lift < c.cof) (hf : ∀ (i : ι), f i < c) :
ordinal.sup f < c
source
theorem ordinal.sup_lt_ord {ι : Type u} {f : ι → ordinal} {c : ordinal} (hι : cardinal.mk ι < c.cof) :
(∀ (i : ι), f i < c) → ordinal.sup f < c
source
theorem ordinal.supr_lt_lift {ι : Type u_1} {f : ι → cardinal} {c : cardinal} (hι : (cardinal.mk ι).lift < c.ord.cof) (hf : ∀ (i : ι), f i < c) :
supr f < c
source
theorem ordinal.supr_lt {ι : Type u_1} {f : ι → cardinal} {c : cardinal} (hι : cardinal.mk ι < c.ord.cof) :
(∀ (i : ι), f i < c) → supr f < c
source
theorem ordinal.nfp_family_lt_ord_lift {ι : Type u} {f : ι → ordinal → ordinal} {c : ordinal} (hc : cardinal.aleph_0 < c.cof) (hc' : (cardinal.mk ι).lift < c.cof) (hf : ∀ (i : ι) (b : ordinal), b < c → f i b < c) {a : ordinal} (ha : a < c) :
ordinal.nfp_family f a < c
source
theorem ordinal.nfp_family_lt_ord {ι : Type u} {f : ι → ordinal → ordinal} {c : ordinal} (hc : cardinal.aleph_0 < c.cof) (hc' : cardinal.mk ι < c.cof) (hf : ∀ (i : ι) (b : ordinal), b < c → f i b < c) {a : ordinal} :
a < c → ordinal.nfp_family f a < c
source
theorem ordinal.nfp_bfamily_lt_ord_lift {o : ordinal} {f : Π (a : ordinal), a < o → ordinal → ordinal} {c : ordinal} (hc : cardinal.aleph_0 < c.cof) (hc' : o.card.lift < c.cof) (hf : ∀ (i : ordinal) (hi : i < o) (b : ordinal), b < c → f i hi b < c) {a : ordinal} :
a < c → o.nfp_bfamily f a < c
source
theorem ordinal.nfp_bfamily_lt_ord {o : ordinal} {f : Π (a : ordinal), a < o → ordinal → ordinal} {c : ordinal} (hc : cardinal.aleph_0 < c.cof) (hc' : o.card < c.cof) (hf : ∀ (i : ordinal) (hi : i < o) (b : ordinal), b < c → f i hi b < c) {a : ordinal} :
a < c → o.nfp_bfamily f a < c
source
theorem ordinal.nfp_lt_ord {f : ordinal → ordinal} {c : ordinal} (hc : cardinal.aleph_0 < c.cof) (hf : ∀ (i : ordinal), i < c → f i < c) {a : ordinal} :
a < c → ordinal.nfp f a < c
source
theorem ordinal.exists_blsub_cof (o : ordinal) :
∃ (f : Π (a : ordinal), a < o.cof.ord → ordinal), o.cof.ord.blsub f = o
source
theorem ordinal.le_cof_iff_blsub {b : ordinal} {a : cardinal} :
a ≤ b.cof ↔ ∀ {o : ordinal} (f : Π (a : ordinal), a < o → ordinal), o.blsub f = b → a ≤ o.card
source
theorem ordinal.cof_blsub_le_lift {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
(o.blsub f).cof ≤ o.card.lift
source
theorem ordinal.cof_blsub_le {o : ordinal} (f : Π (a : ordinal), a < o → ordinal) :
(o.blsub f).cof ≤ o.card
source
theorem ordinal.blsub_lt_ord_lift {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : ordinal} (ho : o.card.lift < c.cof) (hf : ∀ (i : ordinal) (hi : i < o), f i hi < c) :
o.blsub f < c
source
theorem ordinal.blsub_lt_ord {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : ordinal} (ho : o.card < c.cof) (hf : ∀ (i : ordinal) (hi : i < o), f i hi < c) :
o.blsub f < c
source
theorem ordinal.cof_bsup_le_lift {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} (H : ∀ (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
theorem ordinal.bsup_lt_ord_lift {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : ordinal} (ho : o.card.lift < c.cof) (hf : ∀ (i : ordinal) (hi : i < o), f i hi < c) :
o.bsup f < c
source
theorem ordinal.bsup_lt_ord {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : ordinal} (ho : o.card < c.cof) :
(∀ (i : ordinal) (hi : i < o), f i hi < c) → o.bsup f < c

Basic results #

source
@[simp]
theorem ordinal.cof_zero  :
0.cof = 0
source
@[simp]
theorem ordinal.cof_eq_zero {o : ordinal} :
o.cof = 0 ↔ o = 0
source
theorem ordinal.cof_ne_zero {o : ordinal} :
o.cof ≠ 0 ↔ o ≠ 0
source
@[simp]
theorem ordinal.cof_succ (o : ordinal) :
(order.succ o).cof = 1
source
@[simp]
theorem ordinal.cof_eq_one_iff_is_succ {o : ordinal} :
o.cof = 1 ↔ ∃ (a : ordinal), o = order.succ a
source
def ordinal.is_fundamental_sequence (a o : ordinal) (f : Π (b : ordinal), b < o → ordinal) :
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
source
@[protected]
theorem ordinal.is_fundamental_sequence.cof_eq {a o : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) :
a.cof.ord = o
source
@[protected]
theorem ordinal.is_fundamental_sequence.strict_mono {a o : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) {i j : ordinal} (hi : i < o) (hj : j < o) :
i < j → f i hi < f j hj
source
theorem ordinal.is_fundamental_sequence.blsub_eq {a o : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) :
o.blsub f = a
source
theorem ordinal.is_fundamental_sequence.ord_cof {a o : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) :
a.is_fundamental_sequence a.cof.ord (λ (i : ordinal) (hi : i < a.cof.ord), f i _)
source
theorem ordinal.is_fundamental_sequence.id_of_le_cof {o : ordinal} (h : o ≤ o.cof.ord) :
o.is_fundamental_sequence o (λ (a : ordinal) (_x : a < o), a)
source
@[protected]
theorem ordinal.is_fundamental_sequence.zero {f : Π (b : ordinal), b < 0 → ordinal} :
0.is_fundamental_sequence 0 f
source
@[protected]
theorem ordinal.is_fundamental_sequence.succ {o : ordinal} :
(order.succ o).is_fundamental_sequence 1 (λ (_x : ordinal) (_x : _x < 1), o)
source
@[protected]
theorem ordinal.is_fundamental_sequence.monotone {a o : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) {i j : ordinal} (hi : i < o) (hj : j < o) (hij : i ≤ j) :
f i hi ≤ f j hj
source
theorem ordinal.is_fundamental_sequence.trans {a o o' : ordinal} {f : Π (b : ordinal), b < o → ordinal} (hf : a.is_fundamental_sequence o f) {g : Π (b : ordinal), b < o' → ordinal} (hg : o.is_fundamental_sequence o' g) :
a.is_fundamental_sequence o' (λ (i : ordinal) (hi : i < o'), f (g i hi) _)
source
theorem ordinal.exists_fundamental_sequence (a : ordinal) :
∃ (f : Π (b : ordinal), b < a.cof.ord → ordinal), a.is_fundamental_sequence a.cof.ord f

Every ordinal has a fundamental sequence.

source
@[simp]
theorem ordinal.cof_cof (a : ordinal) :
a.cof.ord.cof = a.cof
source
@[protected]
theorem ordinal.is_normal.is_fundamental_sequence {f : ordinal → ordinal} (hf : ordinal.is_normal f) {a o : ordinal} (ha : a.is_limit) {g : Π (b : ordinal), b < o → ordinal} (hg : a.is_fundamental_sequence o g) :
(f a).is_fundamental_sequence o (λ (b : ordinal) (hb : b < o), f (g b hb))
source
theorem ordinal.is_normal.cof_eq {f : ordinal → ordinal} (hf : ordinal.is_normal f) {a : ordinal} (ha : a.is_limit) :
(f a).cof = a.cof
source
theorem ordinal.is_normal.cof_le {f : ordinal → ordinal} (hf : ordinal.is_normal f) (a : ordinal) :
a.cof ≤ (f a).cof
source
@[simp]
theorem ordinal.cof_add (a b : ordinal) :
b ≠ 0 → (a + b).cof = b.cof
source
theorem ordinal.aleph_0_le_cof {o : ordinal} :
cardinal.aleph_0 ≤ o.cof ↔ o.is_limit
source
@[simp]
theorem ordinal.aleph'_cof {o : ordinal} (ho : o.is_limit) :
(cardinal.aleph' o).ord.cof = o.cof
source
@[simp]
theorem ordinal.aleph_cof {o : ordinal} (ho : o.is_limit) :
(cardinal.aleph o).ord.cof = o.cof
source
@[simp]
theorem ordinal.cof_omega  :
ordinal.omega.cof = cardinal.aleph_0
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) ∧ cardinal.mk ↥S = (ordinal.type r).cof
source
@[simp]
theorem ordinal.cof_univ  :
ordinal.univ.cof = cardinal.univ

Infinite pigeonhole principle #

source
theorem ordinal.unbounded_of_unbounded_sUnion {α : Type u_1} (r : α → α → Prop) [wo : is_well_order α r] {s : set (set α)} (h₁ : set.unbounded r (⋃₀ s)) (h₂ : cardinal.mk ↥s < strict_order.cof r) :
∃ (x : set α) (H : 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

source
theorem ordinal.unbounded_of_unbounded_Union {α β : Type u} (r : α → α → Prop) [wo : is_well_order α r] (s : β → set α) (h₁ : set.unbounded r (⋃ (x : β), s x)) (h₂ : cardinal.mk β < strict_order.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

source
theorem ordinal.infinite_pigeonhole {β α : Type u} (f : β → α) (h₁ : cardinal.aleph_0 ≤ cardinal.mk β) (h₂ : cardinal.mk α < (cardinal.mk β).ord.cof) :
∃ (a : α), cardinal.mk ↥(f ⁻¹' {a}) = cardinal.mk β

The infinite pigeonhole principle

source
theorem ordinal.infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : cardinal) (hθ : θ ≤ cardinal.mk β) (h₁ : cardinal.aleph_0 ≤ θ) (h₂ : cardinal.mk α < θ.ord.cof) :
∃ (a : α), θ ≤ cardinal.mk ↥(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θ : θ ≤ cardinal.mk ↥s) (h₁ : cardinal.aleph_0 ≤ θ) (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 #

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.ne_zero {c : cardinal} (h : c.is_strong_limit) :
c ≠ 0
source
theorem cardinal.is_strong_limit.two_power_lt {x c : cardinal} (h : c.is_strong_limit) :
x < c → 2 ^ x < c
source
theorem cardinal.is_strong_limit_aleph_0  :
cardinal.aleph_0.is_strong_limit
source
@[protected]
theorem cardinal.is_strong_limit.is_succ_limit {c : cardinal} (H : c.is_strong_limit) :
order.is_succ_limit c
source
theorem cardinal.is_strong_limit.is_limit {c : cardinal} (H : c.is_strong_limit) :
c.is_limit
source
theorem cardinal.is_strong_limit_beth {o : ordinal} (H : order.is_succ_limit o) :
(cardinal.beth o).is_strong_limit
source
theorem cardinal.mk_bounded_subset {α : Type u} (h : ∀ (x : cardinal), x < cardinal.mk α → 2 ^ x < cardinal.mk α) {r : α → α → Prop} [is_well_order α r] (hr : (cardinal.mk α).ord = ordinal.type r) :
cardinal.mk {s // set.bounded r s} = cardinal.mk α
source
theorem cardinal.mk_subset_mk_lt_cof {α : Type u} (h : ∀ (x : cardinal), x < cardinal.mk α → 2 ^ x < cardinal.mk α) :
cardinal.mk {s // cardinal.mk ↥s < (cardinal.mk α).ord.cof} = cardinal.mk α
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.is_regular.aleph_0_le {c : cardinal} (H : c.is_regular) :
cardinal.aleph_0 ≤ c
source
theorem cardinal.is_regular.cof_eq {c : cardinal} (H : c.is_regular) :
c.ord.cof = c
source
theorem cardinal.is_regular.pos {c : cardinal} (H : c.is_regular) :
0 < c
source
theorem cardinal.is_regular.ord_pos {c : cardinal} (H : c.is_regular) :
0 < c.ord
source
theorem cardinal.is_regular_cof {o : ordinal} (h : o.is_limit) :
o.cof.is_regular
source
theorem cardinal.is_regular_aleph_0  :
cardinal.aleph_0.is_regular
source
theorem cardinal.is_regular_succ {c : cardinal} (h : cardinal.aleph_0 ≤ c) :
(order.succ c).is_regular
source
theorem cardinal.is_regular_aleph_one  :
(cardinal.aleph 1).is_regular
source
theorem cardinal.is_regular_aleph'_succ {o : ordinal} (h : ordinal.omega ≤ o) :
(cardinal.aleph' (order.succ o)).is_regular
source
theorem cardinal.is_regular_aleph_succ (o : ordinal) :
(cardinal.aleph (order.succ o)).is_regular
source
theorem cardinal.infinite_pigeonhole_card_lt {β α : Type u} (f : β → α) (w : cardinal.mk α < cardinal.mk β) (w' : cardinal.aleph_0 ≤ 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.

source
theorem cardinal.exists_infinite_fiber {β α : Type u_1} (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.

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

source
theorem cardinal.lsub_lt_ord_lift_of_is_regular {ι : Type u_1} {f : ι → ordinal} {c : cardinal} (hc : c.is_regular) (hι : (cardinal.mk ι).lift < c) :
(∀ (i : ι), f i < c.ord) → ordinal.lsub f < c.ord
source
theorem cardinal.lsub_lt_ord_of_is_regular {ι : Type (max u_1 u_2)} {f : ι → ordinal} {c : cardinal} (hc : c.is_regular) (hι : cardinal.mk ι < c) :
(∀ (i : ι), f i < c.ord) → ordinal.lsub f < c.ord
source
theorem cardinal.sup_lt_ord_lift_of_is_regular {ι : Type u_1} {f : ι → ordinal} {c : cardinal} (hc : c.is_regular) (hι : (cardinal.mk ι).lift < c) :
(∀ (i : ι), f i < c.ord) → ordinal.sup f < c.ord
source
theorem cardinal.sup_lt_ord_of_is_regular {ι : Type (max u_1 u_2)} {f : ι → ordinal} {c : cardinal} (hc : c.is_regular) (hι : cardinal.mk ι < c) :
(∀ (i : ι), f i < c.ord) → ordinal.sup f < c.ord
source
theorem cardinal.blsub_lt_ord_lift_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : cardinal} (hc : c.is_regular) (ho : o.card.lift < c) :
(∀ (i : ordinal) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord
source
theorem cardinal.blsub_lt_ord_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : cardinal} (hc : c.is_regular) (ho : o.card < c) :
(∀ (i : ordinal) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord
source
theorem cardinal.bsup_lt_ord_lift_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : cardinal} (hc : c.is_regular) (hι : o.card.lift < c) :
(∀ (i : ordinal) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord
source
theorem cardinal.bsup_lt_ord_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o → ordinal} {c : cardinal} (hc : c.is_regular) (hι : o.card < c) :
(∀ (i : ordinal) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord
source
theorem cardinal.supr_lt_lift_of_is_regular {ι : Type u_1} {f : ι → cardinal} {c : cardinal} (hc : c.is_regular) (hι : (cardinal.mk ι).lift < c) :
(∀ (i : ι), f i < c) → supr f < c
source
theorem cardinal.supr_lt_of_is_regular {ι : Type u_1} {f : ι → cardinal} {c : cardinal} (hc : c.is_regular) (hι : cardinal.mk ι < c) :
(∀ (i : ι), f i < c) → supr f < c
source
theorem cardinal.sum_lt_lift_of_is_regular {ι : Type u} {f : ι → cardinal} {c : cardinal} (hc : c.is_regular) (hι : (cardinal.mk ι).lift < c) (hf : ∀ (i : ι), f i < c) :
cardinal.sum f < c
source
theorem cardinal.sum_lt_of_is_regular {ι : Type u} {f : ι → cardinal} {c : cardinal} (hc : c.is_regular) (hι : cardinal.mk ι < c) :
(∀ (i : ι), f i < c) → cardinal.sum f < c
source
theorem cardinal.nfp_family_lt_ord_lift_of_is_regular {ι : Type u} {f : ι → ordinal → ordinal} {c : cardinal} (hc : c.is_regular) (hι : (cardinal.mk ι).lift < c) (hc' : c ≠ cardinal.aleph_0) (hf : ∀ (i : ι) (b : ordinal), b < c.ord → f i b < c.ord) {a : ordinal} (ha : a < c.ord) :
ordinal.nfp_family f a < c.ord
source
theorem cardinal.nfp_family_lt_ord_of_is_regular {ι : Type u} {f : ι → ordinal → ordinal} {c : cardinal} (hc : c.is_regular) (hι : cardinal.mk ι < c) (hc' : c ≠ cardinal.aleph_0) {a : ordinal} (hf : ∀ (i : ι) (b : ordinal), b < c.ord → f i b < c.ord) :
a < c.ord → ordinal.nfp_family f a < c.ord
source
theorem cardinal.nfp_bfamily_lt_ord_lift_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o → ordinal → ordinal} {c : cardinal} (hc : c.is_regular) (ho : o.card.lift < c) (hc' : c ≠ cardinal.aleph_0) (hf : ∀ (i : ordinal) (hi : i < o) (b : ordinal), b < c.ord → f i hi b < c.ord) {a : ordinal} :
a < c.ord → o.nfp_bfamily f a < c.ord
source
theorem cardinal.nfp_bfamily_lt_ord_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o → ordinal → ordinal} {c : cardinal} (hc : c.is_regular) (ho : o.card < c) (hc' : c ≠ cardinal.aleph_0) (hf : ∀ (i : ordinal) (hi : i < o) (b : ordinal), b < c.ord → f i hi b < c.ord) {a : ordinal} :
a < c.ord → o.nfp_bfamily f a < c.ord
source
theorem cardinal.nfp_lt_ord_of_is_regular {f : ordinal → ordinal} {c : cardinal} (hc : c.is_regular) (hc' : c ≠ cardinal.aleph_0) (hf : ∀ (i : ordinal), i < c.ord → f i < c.ord) {a : ordinal} :
a < c.ord → ordinal.nfp f a < c.ord
source
theorem cardinal.deriv_family_lt_ord_lift {ι : Type u} {f : ι → ordinal → ordinal} {c : cardinal} (hc : c.is_regular) (hι : (cardinal.mk ι).lift < c) (hc' : c ≠ cardinal.aleph_0) (hf : ∀ (i : ι) (b : ordinal), b < c.ord → f i b < c.ord) {a : ordinal} :
a < c.ord → ordinal.deriv_family f a < c.ord
source
theorem cardinal.deriv_family_lt_ord {ι : Type u} {f : ι → ordinal → ordinal} {c : cardinal} (hc : c.is_regular) (hι : cardinal.mk ι < c) (hc' : c ≠ cardinal.aleph_0) (hf : ∀ (i : ι) (b : ordinal), b < c.ord → f i b < c.ord) {a : ordinal} :
a < c.ord → ordinal.deriv_family f a < c.ord
source
theorem cardinal.deriv_bfamily_lt_ord_lift {o : ordinal} {f : Π (a : ordinal), a < o → ordinal → ordinal} {c : cardinal} (hc : c.is_regular) (hι : o.card.lift < c) (hc' : c ≠ cardinal.aleph_0) (hf : ∀ (i : ordinal) (hi : i < o) (b : ordinal), b < c.ord → f i hi b < c.ord) {a : ordinal} :
a < c.ord → o.deriv_bfamily f a < c.ord
source
theorem cardinal.deriv_bfamily_lt_ord {o : ordinal} {f : Π (a : ordinal), a < o → ordinal → ordinal} {c : cardinal} (hc : c.is_regular) (hι : o.card < c) (hc' : c ≠ cardinal.aleph_0) (hf : ∀ (i : ordinal) (hi : i < o) (b : ordinal), b < c.ord → f i hi b < c.ord) {a : ordinal} :
a < c.ord → o.deriv_bfamily f a < c.ord
source
theorem cardinal.deriv_lt_ord {f : ordinal → ordinal} {c : cardinal} (hc : c.is_regular) (hc' : c ≠ cardinal.aleph_0) (hf : ∀ (i : ordinal), i < c.ord → f i < c.ord) {a : ordinal} :
a < c.ord → ordinal.deriv f a < c.ord
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.aleph_0 < 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.aleph_0 ≤ c → c < c ^ c.ord.cof
source
theorem cardinal.lt_cof_power {a b : cardinal} (ha : cardinal.aleph_0 ≤ a) (b1 : 1 < b) :
a < (b ^ a).ord.cof