mathlib documentation

set_theory.cardinal.cofinality

Cofinality #

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 #

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

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

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

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

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

Equations
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 #

noncomputable def ordinal.cof (o : ordinal) :

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
theorem ordinal.cof_type {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
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 Sc cardinal.mk S
theorem ordinal.cof_type_le {α : Type u_1} {r : α → α → Prop} [is_well_order α r] {S : set α} (h : set.unbounded r S) :
theorem ordinal.lt_cof_type {α : Type u_1} {r : α → α → Prop} [is_well_order α r] {S : set α} :
theorem ordinal.cof_eq {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
theorem ordinal.ord_cof_eq {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

Cofinality of suprema and least strict upper bounds #

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.

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

Basic results #

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

Every ordinal has a fundamental sequence.

@[simp]
theorem ordinal.cof_cof (a : ordinal) :
@[protected]
theorem ordinal.is_normal.is_fundamental_sequence {f : ordinalordinal} (hf : ordinal.is_normal f) {a o : ordinal} (ha : a.is_limit) {g : Π (b : ordinal), b < oordinal} (hg : a.is_fundamental_sequence o g) :
(f a).is_fundamental_sequence o (λ (b : ordinal) (hb : b < o), f (g b hb))
theorem ordinal.is_normal.cof_eq {f : ordinalordinal} (hf : ordinal.is_normal f) {a : ordinal} (ha : a.is_limit) :
(f a).cof = a.cof
theorem ordinal.is_normal.cof_le {f : ordinalordinal} (hf : ordinal.is_normal f) (a : ordinal) :
a.cof (f a).cof
@[simp]
theorem ordinal.cof_add (a b : ordinal) :
b 0(a + b).cof = b.cof
@[simp]
theorem ordinal.aleph'_cof {o : ordinal} (ho : o.is_limit) :
@[simp]
theorem ordinal.aleph_cof {o : ordinal} (ho : o.is_limit) :
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

Infinite pigeonhole principle #

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

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

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

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

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 #

def cardinal.is_limit (c : 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
theorem cardinal.is_limit.ne_zero {c : cardinal} (h : c.is_limit) :
c 0
theorem cardinal.is_limit.succ_lt {x c : cardinal} (h : c.is_limit) :
x < corder.succ x < c

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
theorem cardinal.is_strong_limit.two_power_lt {x c : cardinal} (h : c.is_strong_limit) :
x < c2 ^ x < c
theorem cardinal.is_strong_limit_beth {o : ordinal} (H : ∀ (a : ordinal), a < oorder.succ a < o) :
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) :
theorem cardinal.mk_subset_mk_lt_cof {α : Type u} (h : ∀ (x : cardinal), x < cardinal.mk α2 ^ x < cardinal.mk α) :
def cardinal.is_regular (c : cardinal) :
Prop

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

Equations
theorem cardinal.is_regular.pos {c : cardinal} (H : c.is_regular) :
0 < c
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.

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.

theorem cardinal.le_range_of_union_finset_eq_top {α : Type u_1} {β : Type u_2} [infinite β] (f : α → finset β) (w : (⋃ (a : α), (f a)) = ) :

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_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
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
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
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
theorem cardinal.blsub_lt_ord_lift_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < oordinal} {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
theorem cardinal.blsub_lt_ord_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < oordinal} {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
theorem cardinal.bsup_lt_ord_lift_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < oordinal} {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
theorem cardinal.bsup_lt_ord_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < oordinal} {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
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
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
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) :
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
theorem cardinal.nfp_family_lt_ord_lift_of_is_regular {ι : Type u} {f : ι → ordinalordinal} {c : cardinal} (hc : c.is_regular) (hι : (cardinal.mk ι).lift < c) (hc' : c cardinal.aleph_0) (hf : ∀ (i : ι) (b : ordinal), b < c.ordf i b < c.ord) {a : ordinal} (ha : a < c.ord) :
theorem cardinal.nfp_family_lt_ord_of_is_regular {ι : Type u} {f : ι → ordinalordinal} {c : cardinal} (hc : c.is_regular) (hι : cardinal.mk ι < c) (hc' : c cardinal.aleph_0) {a : ordinal} (hf : ∀ (i : ι) (b : ordinal), b < c.ordf i b < c.ord) :
a < c.ordordinal.nfp_family f a < c.ord
theorem cardinal.nfp_bfamily_lt_ord_lift_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < oordinalordinal} {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.ordf i hi b < c.ord) {a : ordinal} :
a < c.ordo.nfp_bfamily f a < c.ord
theorem cardinal.nfp_bfamily_lt_ord_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < oordinalordinal} {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.ordf i hi b < c.ord) {a : ordinal} :
a < c.ordo.nfp_bfamily f a < c.ord
theorem cardinal.nfp_lt_ord_of_is_regular {f : ordinalordinal} {c : cardinal} (hc : c.is_regular) (hc' : c cardinal.aleph_0) (hf : ∀ (i : ordinal), i < c.ordf i < c.ord) {a : ordinal} :
a < c.ordordinal.nfp f a < c.ord
theorem cardinal.deriv_family_lt_ord_lift {ι : Type u} {f : ι → ordinalordinal} {c : cardinal} (hc : c.is_regular) (hι : (cardinal.mk ι).lift < c) (hc' : c cardinal.aleph_0) (hf : ∀ (i : ι) (b : ordinal), b < c.ordf i b < c.ord) {a : ordinal} :
theorem cardinal.deriv_family_lt_ord {ι : Type u} {f : ι → ordinalordinal} {c : cardinal} (hc : c.is_regular) (hι : cardinal.mk ι < c) (hc' : c cardinal.aleph_0) (hf : ∀ (i : ι) (b : ordinal), b < c.ordf i b < c.ord) {a : ordinal} :
theorem cardinal.deriv_bfamily_lt_ord_lift {o : ordinal} {f : Π (a : ordinal), a < oordinalordinal} {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.ordf i hi b < c.ord) {a : ordinal} :
a < c.ordo.deriv_bfamily f a < c.ord
theorem cardinal.deriv_bfamily_lt_ord {o : ordinal} {f : Π (a : ordinal), a < oordinalordinal} {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.ordf i hi b < c.ord) {a : ordinal} :
a < c.ordo.deriv_bfamily f a < c.ord
theorem cardinal.deriv_lt_ord {f : ordinalordinal} {c : cardinal} (hc : c.is_regular) (hc' : c cardinal.aleph_0) (hf : ∀ (i : ordinal), i < c.ordf i < c.ord) {a : ordinal} :
a < c.ordordinal.deriv f a < c.ord

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

Equations
theorem cardinal.is_inaccessible.mk {c : cardinal} (h₁ : cardinal.aleph_0 < c) (h₂ : c c.ord.cof) (h₃ : ∀ (x : cardinal), x < c2 ^ x < c) :
theorem cardinal.lt_cof_power {a b : cardinal} (ha : cardinal.aleph_0 a) (b1 : 1 < b) :
a < (b ^ a).ord.cof