# mathlib3documentation

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 #

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

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) [ r] :
{c : cardinal | (S : set α), ( (a : α), (b : α) (H : b S), r a b) = 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} [ r] (c : cardinal) :
c {S : set α}, ( (a : α), (b : α) (H : b S), r a b)
theorem rel_iso.cof_le_lift {α : Type u} {β : Type v} {r : α α Prop} {s : β β Prop} [ s] (f : r ≃r s) :
theorem rel_iso.cof_eq_lift {α : Type u} {β : Type v} {r : α α Prop} {s : β β Prop} [ r] [ s] (f : r ≃r s) :
theorem rel_iso.cof_le {α β : Type u} {r : α α Prop} {s : β β Prop} [ s] (f : r ≃r s) :
theorem rel_iso.cof_eq {α β : Type u} {r : α α Prop} {s : β β Prop} [ r] [ 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) [ r] :
{c : cardinal | (S : set α), = 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) [ r] :
theorem ordinal.le_cof_type {α : Type u_1} {r : α α Prop} [ r] {c : cardinal} :
c (ordinal.type r).cof (S : set α),
theorem ordinal.cof_type_le {α : Type u_1} {r : α α Prop} [ r] {S : set α} (h : S) :
theorem ordinal.lt_cof_type {α : Type u_1} {r : α α Prop} [ r] {S : set α} :
theorem ordinal.cof_eq {α : Type u_1} (r : α α Prop) [ r] :
(S : set α), = (ordinal.type r).cof
theorem ordinal.ord_cof_eq {α : Type u_1} (r : α α Prop) [ r] :

### Cofinality of suprema and least strict upper bounds #

theorem ordinal.cof_lsub_def_nonempty (o : ordinal) :
{a : cardinal | {ι : Type u} (f : ι ordinal), = 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), = 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), = o.cof
theorem ordinal.cof_lsub_le {ι : Type u} (f : ι ordinal) :
theorem ordinal.le_cof_iff_lsub {o : ordinal} {a : cardinal} :
a o.cof {ι : Type u} (f : ι ordinal), a
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ι : < c.cof) :
( (i : ι), f i < c)
theorem ordinal.cof_sup_le_lift {ι : Type u_1} {f : ι ordinal} (H : (i : ι), f i < ) :
theorem ordinal.cof_sup_le {ι : Type u} {f : ι ordinal} (H : (i : ι), f i < ) :
theorem ordinal.sup_lt_ord_lift {ι : Type u} {f : ι ordinal} {c : ordinal} (hι : (cardinal.mk ι).lift < c.cof) (hf : (i : ι), f i < c) :
< c
theorem ordinal.sup_lt_ord {ι : Type u} {f : ι ordinal} {c : ordinal} (hι : < c.cof) :
( (i : ι), f i < c) < 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ι : < c.ord.cof) :
( (i : ι), f i < c) supr f < c
theorem ordinal.nfp_family_lt_ord_lift {ι : Type u} {f : ι } {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) :
< c
theorem ordinal.nfp_family_lt_ord {ι : Type u} {f : ι } {c : ordinal} (hc : cardinal.aleph_0 < c.cof) (hc' : < c.cof) (hf : (i : ι) (b : ordinal), b < c f i b < c) {a : ordinal} :
a < c < c
theorem ordinal.nfp_bfamily_lt_ord_lift {o : ordinal} {f : Π (a : ordinal), a < o } {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
theorem ordinal.nfp_bfamily_lt_ord {o : ordinal} {f : Π (a : ordinal), a < o } {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
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 a < c
theorem ordinal.exists_blsub_cof (o : ordinal) :
(f : Π (a : ordinal), a < o.cof.ord ordinal), 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 < o ordinal), o.blsub f = b a o.card
theorem ordinal.cof_blsub_le_lift {o : ordinal} (f : Π (a : ordinal), a < o ordinal) :
theorem ordinal.cof_blsub_le {o : ordinal} (f : Π (a : ordinal), a < o ordinal) :
(o.blsub f).cof o.card
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
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
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
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
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
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 #

@[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 =
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
@[protected]
theorem ordinal.is_fundamental_sequence.cof_eq {a o : ordinal} {f : Π (b : ordinal), b < o ordinal} (hf : f) :
a.cof.ord = o
@[protected]
theorem ordinal.is_fundamental_sequence.strict_mono {a o : ordinal} {f : Π (b : ordinal), b < o ordinal} (hf : f) {i j : ordinal} (hi : i < o) (hj : j < o) :
i < j f i hi < f j hj
theorem ordinal.is_fundamental_sequence.blsub_eq {a o : ordinal} {f : Π (b : ordinal), b < o ordinal} (hf : f) :
o.blsub f = a
theorem ordinal.is_fundamental_sequence.ord_cof {a o : ordinal} {f : Π (b : ordinal), b < o ordinal} (hf : f) :
(λ (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) :
(λ (a : ordinal) (_x : a < o), a)
@[protected]
@[protected]
theorem ordinal.is_fundamental_sequence.succ {o : ordinal} :
(λ (_x : ordinal) (_x : _x < 1), o)
@[protected]
theorem ordinal.is_fundamental_sequence.monotone {a o : ordinal} {f : Π (b : ordinal), b < o ordinal} (hf : 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 < o ordinal} (hf : f) {g : Π (b : ordinal), b < o' ordinal} (hg : g) :
(λ (i : ordinal) (hi : i < o'), f (g i hi) _)

Every ordinal has a fundamental sequence.

@[simp]
theorem ordinal.cof_cof (a : ordinal) :
@[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 : g) :
(f a).is_fundamental_sequence o (λ (b : ordinal) (hb : b < o), f (g b hb))
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
@[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) :
@[simp]
theorem ordinal.cof_eq' {α : Type u_1} (r : α α Prop) [ r] (h : (ordinal.type r).is_limit) :
(S : set α), ( (a : α), (b : α) (H : b S), r a b) = (ordinal.type r).cof
@[simp]

### Infinite pigeonhole principle #

theorem ordinal.unbounded_of_unbounded_sUnion {α : Type u_1} (r : α α Prop) [wo : r] {s : set (set α)} (h₁ : (⋃₀ s)) (h₂ : < ) :
(x : set α) (H : x s),

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 : r] (s : β set α) (h₁ : ( (x : β), s x)) (h₂ : < ) :
(x : β), (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 ) (h₂ : < (cardinal.mk β).ord.cof) :
(a : α), cardinal.mk (f ⁻¹' {a}) =

The infinite pigeonhole principle

theorem ordinal.infinite_pigeonhole_card {β α : Type u} (f : β α) (θ : cardinal) (hθ : θ ) (h₁ : cardinal.aleph_0 θ) (h₂ : < θ.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θ : θ ) (h₁ : cardinal.aleph_0 θ) (h₂ : < θ.ord.cof) :
(a : α) (t : set β) (h : t s), ⦃x : β⦄ (hx : x t), f x, _⟩ = a

### Regular and inaccessible cardinals #

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.mk_bounded_subset {α : Type u} (h : (x : cardinal), x < 2 ^ x < ) {r : α α Prop} [ r] (hr : (cardinal.mk α).ord = ) :
cardinal.mk {s // s} =
theorem cardinal.mk_subset_mk_lt_cof {α : Type u} (h : (x : cardinal), x < 2 ^ x < ) :
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.is_regular_cof {o : ordinal} (h : o.is_limit) :
theorem cardinal.infinite_pigeonhole_card_lt {β α : Type u} (f : β α) (w : < ) (w' : cardinal.aleph_0 ) :
(a : α), < 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 : < ) (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 : α ) (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) < 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ι : < c) :
( (i : ι), f i < c.ord) < 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) < 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ι : < c) :
( (i : ι), f i < c.ord) < c.ord
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
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
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
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
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ι : < 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ι : < c) :
( (i : ι), f i < c)
theorem cardinal.nfp_family_lt_ord_lift_of_is_regular {ι : Type u} {f : ι } {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) :
< c.ord
theorem cardinal.nfp_family_lt_ord_of_is_regular {ι : Type u} {f : ι } {c : cardinal} (hc : c.is_regular) (hι : < c) (hc' : c cardinal.aleph_0) {a : ordinal} (hf : (i : ι) (b : ordinal), b < c.ord f i b < c.ord) :
a < c.ord < c.ord
theorem cardinal.nfp_bfamily_lt_ord_lift_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o } {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
theorem cardinal.nfp_bfamily_lt_ord_of_is_regular {o : ordinal} {f : Π (a : ordinal), a < o } {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
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 a < c.ord
theorem cardinal.deriv_family_lt_ord_lift {ι : Type u} {f : ι } {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 < c.ord
theorem cardinal.deriv_family_lt_ord {ι : Type u} {f : ι } {c : cardinal} (hc : c.is_regular) (hι : < c) (hc' : c cardinal.aleph_0) (hf : (i : ι) (b : ordinal), b < c.ord f i b < c.ord) {a : ordinal} :
a < c.ord < c.ord
theorem cardinal.deriv_bfamily_lt_ord_lift {o : ordinal} {f : Π (a : ordinal), a < o } {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 a < c.ord
theorem cardinal.deriv_bfamily_lt_ord {o : ordinal} {f : Π (a : ordinal), a < o } {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 a < c.ord
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 < 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 < c 2 ^ x < c) :
theorem cardinal.lt_power_cof {c : cardinal} :
c < c ^ c.ord.cof
theorem cardinal.lt_cof_power {a b : cardinal} (ha : cardinal.aleph_0 a) (b1 : 1 < b) :
a < (b ^ a).ord.cof