# 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) :

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

Equations
Instances For
theorem Order.cof_nonempty {α : Type u_1} (r : ααProp) [IsRefl α r] :
{c : Cardinal.{u_1} | ∃ (S : Set α), (∀ (a : α), bS, 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 : α), bS, r a b) :
theorem Order.le_cof {α : Type u_1} {r : ααProp} [IsRefl α r] (c : Cardinal.{u_1}) :
c ∀ {S : Set α}, (∀ (a : α), bS, r a b)c
theorem RelIso.cof_le_lift {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsRefl β s] (f : r ≃r s) :
theorem RelIso.cof_eq_lift {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsRefl α r] [IsRefl β s] (f : r ≃r s) :
=
theorem RelIso.cof_le {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} [IsRefl β s] (f : r ≃r s) :
theorem RelIso.cof_eq {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} [IsRefl α r] [IsRefl β s] (f : r ≃r s) :
def StrictOrder.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
Instances For
theorem StrictOrder.cof_nonempty {α : Type u_1} (r : ααProp) [IsIrrefl α r] :
{c : Cardinal.{u_1} | ∃ (S : Set α), = c}.Nonempty

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

### Cofinality of ordinals #

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
Instances For
theorem Ordinal.cof_type {α : Type u_1} (r : ααProp) [] :
().cof =
theorem Ordinal.le_cof_type {α : Type u_1} {r : ααProp} [] {c : Cardinal.{u_1}} :
c ().cof ∀ (S : Set α), c
theorem Ordinal.cof_type_le {α : Type u_1} {r : ααProp} [] {S : Set α} (h : ) :
().cof
theorem Ordinal.lt_cof_type {α : Type u_1} {r : ααProp} [] {S : Set α} :
< ().cof
theorem Ordinal.cof_eq {α : Type u_1} (r : ααProp) [] :
∃ (S : Set α), = ().cof
theorem Ordinal.ord_cof_eq {α : Type u_1} (r : ααProp) [] :
∃ (S : Set α), Ordinal.type (Subrel r S) = ().cof.ord

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

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

The set in the lsub characterization of cof is nonempty.

theorem Ordinal.cof_eq_sInf_lsub (o : Ordinal.{u}) :
o.cof = sInf {a : Cardinal.{u} | ∃ (ι : Type u) (f : ), = a}
@[simp]
theorem Ordinal.cof_le_card (o : Ordinal.{u_2}) :
o.cof o.card
theorem Ordinal.cof_ord_le (c : Cardinal.{u_2}) :
c.ord.cof c
theorem Ordinal.ord_cof_le (o : Ordinal.{u}) :
o.cof.ord o
theorem Ordinal.exists_lsub_cof (o : Ordinal.{u}) :
∃ (ι : Type u) (f : ), = o.cof
theorem Ordinal.cof_lsub_le {ι : Type u} (f : ) :
().cof
theorem Ordinal.cof_lsub_le_lift {ι : Type u} (f : ) :
().cof
theorem Ordinal.le_cof_iff_lsub {o : Ordinal.{u}} {a : Cardinal.{u}} :
a o.cof ∀ {ι : Type u} (f : ), a
theorem Ordinal.lsub_lt_ord_lift {ι : Type u} {f : } {c : Ordinal.{max u v} } (hι : < c.cof) (hf : ∀ (i : ι), f i < c) :
theorem Ordinal.lsub_lt_ord {ι : Type u} {f : } {c : Ordinal.{u}} (hι : < c.cof) :
(∀ (i : ι), f i < c)
theorem Ordinal.cof_sup_le_lift {ι : Type u} {f : } (H : ∀ (i : ι), f i < ) :
().cof
theorem Ordinal.cof_sup_le {ι : Type u} {f : } (H : ∀ (i : ι), f i < ) :
().cof
theorem Ordinal.sup_lt_ord_lift {ι : Type u} {f : } {c : Ordinal.{max u v} } (hι : < c.cof) (hf : ∀ (i : ι), f i < c) :
< c
theorem Ordinal.sup_lt_ord {ι : Type u} {f : } {c : Ordinal.{u}} (hι : < c.cof) :
(∀ (i : ι), f i < c) < c
theorem Ordinal.iSup_lt_lift {ι : Type u} {f : } {c : Cardinal.{max u v} } (hι : < c.ord.cof) (hf : ∀ (i : ι), f i < c) :
iSup f < c
theorem Ordinal.iSup_lt {ι : Type u_2} {f : } {c : Cardinal.{u_2}} (hι : < c.ord.cof) :
(∀ (i : ι), f i < c)iSup f < c
theorem Ordinal.nfpFamily_lt_ord_lift {ι : Type u} {f : ι} {c : Ordinal.{max u v} } (hc : Cardinal.aleph0 < c.cof) (hc' : < c.cof) (hf : ∀ (i : ι), b < c, f i b < c) {a : Ordinal.{max u v} } (ha : a < c) :
< c
theorem Ordinal.nfpFamily_lt_ord {ι : Type u} {f : } {c : Ordinal.{u}} (hc : Cardinal.aleph0 < c.cof) (hc' : < c.cof) (hf : ∀ (i : ι), b < c, f i b < c) {a : Ordinal.{u}} :
a < c < c
theorem Ordinal.nfpBFamily_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o} {c : Ordinal.{max u v} } (hc : Cardinal.aleph0 < c.cof) (hc' : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), b < c, f i hi b < c) {a : Ordinal.{max u v} } :
a < co.nfpBFamily f a < c
theorem Ordinal.nfpBFamily_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o} {c : Ordinal.{u}} (hc : Cardinal.aleph0 < c.cof) (hc' : o.card < c.cof) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), b < c, f i hi b < c) {a : Ordinal.{u}} :
a < co.nfpBFamily f a < c
theorem Ordinal.nfp_lt_ord {f : } {c : Ordinal.{u_2}} (hc : Cardinal.aleph0 < c.cof) (hf : i < c, f i < c) {a : Ordinal.{u_2}} :
a < c < c
theorem Ordinal.exists_blsub_cof (o : Ordinal.{u}) :
∃ (f : (a : Ordinal.{u}) → a < o.cof.ordOrdinal.{u}), o.cof.ord.blsub f = o
theorem Ordinal.le_cof_iff_blsub {b : Ordinal.{u}} {a : Cardinal.{u}} :
a b.cof ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{u}), o.blsub f = ba o.card
theorem Ordinal.cof_blsub_le_lift {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
(o.blsub f).cof Cardinal.lift.{v, u} o.card
theorem Ordinal.cof_blsub_le {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{u}) :
(o.blsub f).cof o.card
theorem Ordinal.blsub_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {c : Ordinal.{max u v} } (ho : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) :
o.blsub f < c
theorem Ordinal.blsub_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{u}} {c : Ordinal.{u}} (ho : o.card < c.cof) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) :
o.blsub f < c
theorem Ordinal.cof_bsup_le_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) :
(o.bsup f).cof Cardinal.lift.{v, u} o.card
theorem Ordinal.cof_bsup_le {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{u}} :
(∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f)(o.bsup f).cof o.card
theorem Ordinal.bsup_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {c : Ordinal.{max u v} } (ho : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) :
o.bsup f < c
theorem Ordinal.bsup_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{u}} {c : Ordinal.{u}} (ho : o.card < c.cof) :
(∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c)o.bsup f < c

### Basic results #

@[simp]
theorem Ordinal.cof_zero :
= 0
@[simp]
theorem Ordinal.cof_eq_zero {o : Ordinal.{u_2}} :
o.cof = 0 o = 0
@[simp]
theorem Ordinal.cof_succ (o : Ordinal.{u_2}) :
().cof = 1
@[simp]
theorem Ordinal.cof_eq_one_iff_is_succ {o : Ordinal.{u}} :
o.cof = 1 ∃ (a : Ordinal.{u}), o =

A fundamental sequence for a is an increasing sequence of length o = cof a that converges at a. We provide o explicitly in order to avoid type rewrites.

Equations
• a.IsFundamentalSequence o f = (o a.cof.ord (∀ {i j : Ordinal.{u}} (hi : i < o) (hj : j < o), i < jf i hi < f j hj) o.blsub f = a)
Instances For
theorem Ordinal.IsFundamentalSequence.cof_eq {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{u}} (hf : a.IsFundamentalSequence o f) :
a.cof.ord = o
theorem Ordinal.IsFundamentalSequence.strict_mono {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{u}} (hf : a.IsFundamentalSequence o f) {i : Ordinal.{u}} {j : Ordinal.{u}} (hi : i < o) (hj : j < o) :
i < jf i hi < f j hj
theorem Ordinal.IsFundamentalSequence.blsub_eq {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{u}} (hf : a.IsFundamentalSequence o f) :
o.blsub f = a
theorem Ordinal.IsFundamentalSequence.ord_cof {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{u}} (hf : a.IsFundamentalSequence o f) :
a.IsFundamentalSequence a.cof.ord fun (i : Ordinal.{u}) (hi : i < a.cof.ord) => f i
theorem Ordinal.IsFundamentalSequence.id_of_le_cof {o : Ordinal.{u}} (h : o o.cof.ord) :
o.IsFundamentalSequence o fun (a : Ordinal.{u}) (x : a < o) => a
theorem Ordinal.IsFundamentalSequence.succ {o : Ordinal.{u}} :
().IsFundamentalSequence 1 fun (x : Ordinal.{u}) (x : x < 1) => o
theorem Ordinal.IsFundamentalSequence.monotone {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{u}} (hf : a.IsFundamentalSequence 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 < oOrdinal.{u}} (hf : a.IsFundamentalSequence o f) {g : (b : Ordinal.{u}) → b < o'Ordinal.{u}} (hg : o.IsFundamentalSequence o' g) :
a.IsFundamentalSequence o' fun (i : Ordinal.{u}) (hi : i < o') => f (g i hi)
theorem Ordinal.exists_fundamental_sequence (a : Ordinal.{u}) :
∃ (f : (b : Ordinal.{u}) → b < a.cof.ordOrdinal.{u}), a.IsFundamentalSequence a.cof.ord f

Every ordinal has a fundamental sequence.

@[simp]
theorem Ordinal.cof_cof (a : Ordinal.{u}) :
a.cof.ord.cof = a.cof
theorem Ordinal.IsNormal.isFundamentalSequence {f : } (hf : ) {a : Ordinal.{u}} {o : Ordinal.{u}} (ha : a.IsLimit) {g : (b : Ordinal.{u}) → b < oOrdinal.{u}} (hg : a.IsFundamentalSequence o g) :
(f a).IsFundamentalSequence o fun (b : Ordinal.{u}) (hb : b < o) => f (g b hb)
theorem Ordinal.IsNormal.cof_eq {f : } (hf : ) {a : Ordinal.{u_2}} (ha : a.IsLimit) :
(f a).cof = a.cof
theorem Ordinal.IsNormal.cof_le {f : } (hf : ) (a : Ordinal.{u_2}) :
a.cof (f a).cof
@[simp]
theorem Ordinal.cof_add (a : Ordinal.{u_2}) (b : Ordinal.{u_2}) :
b 0(a + b).cof = b.cof
@[simp]
theorem Ordinal.aleph'_cof {o : Ordinal.{u_2}} (ho : o.IsLimit) :
().ord.cof = o.cof
@[simp]
theorem Ordinal.aleph_cof {o : Ordinal.{u_2}} (ho : o.IsLimit) :
().ord.cof = o.cof
@[simp]
theorem Ordinal.cof_eq' {α : Type u_1} (r : ααProp) [] (h : ().IsLimit) :
∃ (S : Set α), (∀ (a : α), bS, r a b) = ().cof
@[simp]

### Infinite pigeonhole principle #

theorem Ordinal.unbounded_of_unbounded_sUnion {α : Type u_1} (r : ααProp) [wo : ] {s : Set (Set α)} (h₁ : Set.Unbounded r (⋃₀ s)) (h₂ : ) :
xs,

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

The infinite pigeonhole principle

theorem Ordinal.infinite_pigeonhole_card {β : Type u} {α : Type u} (f : βα) (θ : Cardinal.{u}) (hθ : θ ) (h₁ : ) (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} {α : Type u} {s : Set β} (f : sα) (θ : Cardinal.{u}) (hθ : θ ) (h₁ : ) (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
• c.IsStrongLimit = (c 0 x < c, 2 ^ x < c)
Instances For
theorem Cardinal.IsStrongLimit.ne_zero {c : Cardinal.{u_2}} (h : c.IsStrongLimit) :
c 0
theorem Cardinal.IsStrongLimit.two_power_lt {x : Cardinal.{u_2}} {c : Cardinal.{u_2}} (h : c.IsStrongLimit) :
x < c2 ^ x < c
theorem Cardinal.IsStrongLimit.isSuccLimit {c : Cardinal.{u_2}} (H : c.IsStrongLimit) :
theorem Cardinal.IsStrongLimit.isLimit {c : Cardinal.{u_2}} (H : c.IsStrongLimit) :
c.IsLimit
theorem Cardinal.isStrongLimit_beth {o : Ordinal.{u_2}} (H : ) :
().IsStrongLimit
theorem Cardinal.mk_bounded_subset {α : Type u_2} (h : x < , 2 ^ x < ) {r : ααProp} [] (hr : ().ord = ) :
Cardinal.mk { s : Set α // } =
theorem Cardinal.mk_subset_mk_lt_cof {α : Type u_2} (h : x < , 2 ^ x < ) :
Cardinal.mk { s : Set α // < ().ord.cof } =

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

Equations
• c.IsRegular = ( c c.ord.cof)
Instances For
theorem Cardinal.IsRegular.aleph0_le {c : Cardinal.{u_2}} (H : c.IsRegular) :
theorem Cardinal.IsRegular.cof_eq {c : Cardinal.{u_2}} (H : c.IsRegular) :
c.ord.cof = c
theorem Cardinal.IsRegular.pos {c : Cardinal.{u_2}} (H : c.IsRegular) :
0 < c
theorem Cardinal.IsRegular.nat_lt {c : Cardinal.{u_2}} (H : c.IsRegular) (n : ) :
n < c
theorem Cardinal.IsRegular.ord_pos {c : Cardinal.{u_2}} (H : c.IsRegular) :
0 < c.ord
theorem Cardinal.isRegular_cof {o : Ordinal.{u_2}} (h : o.IsLimit) :
o.cof.IsRegular
theorem Cardinal.isRegular_succ {c : Cardinal.{u}} (h : ) :
().IsRegular
theorem Cardinal.isRegular_aleph'_succ {o : Ordinal.{u_2}} (h : ) :
().IsRegular
theorem Cardinal.infinite_pigeonhole_card_lt {β : Type u} {α : Type u} (f : βα) (w : ) (w' : ) :
∃ (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} {α : Type u} (f : βα) (w : ) (w' : ) :
∃ (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} [] (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_isRegular {ι : Type u} {f : } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : < c) :
(∀ (i : ι), f i < c.ord) < c.ord
theorem Cardinal.lsub_lt_ord_of_isRegular {ι : Type (max u_2 u_3)} {f : } (hc : c.IsRegular) (hι : < c) :
(∀ (i : ι), f i < c.ord) < c.ord
theorem Cardinal.sup_lt_ord_lift_of_isRegular {ι : Type u} {f : } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : < c) :
(∀ (i : ι), f i < c.ord) < c.ord
theorem Cardinal.sup_lt_ord_of_isRegular {ι : Type (max u_2 u_3)} {f : } (hc : c.IsRegular) (hι : < c) :
(∀ (i : ι), f i < c.ord) < c.ord
theorem Cardinal.blsub_lt_ord_lift_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (ho : Cardinal.lift.{v, u} o.card < c) :
(∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord)o.blsub f < c.ord
theorem Cardinal.blsub_lt_ord_of_isRegular {f : (a : Ordinal.{max u_2 u_3} ) → } (hc : c.IsRegular) (ho : o.card < c) :
(∀ (i : Ordinal.{max u_2 u_3} ) (hi : i < o), f i hi < c.ord)o.blsub f < c.ord
theorem Cardinal.bsup_lt_ord_lift_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} o.card < c) :
(∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord)o.bsup f < c.ord
theorem Cardinal.bsup_lt_ord_of_isRegular {f : (a : Ordinal.{max u_2 u_3} ) → } (hc : c.IsRegular) (hι : o.card < c) :
(∀ (i : Ordinal.{max u_2 u_3} ) (hi : i < o), f i hi < c.ord)o.bsup f < c.ord
theorem Cardinal.iSup_lt_lift_of_isRegular {ι : Type u} {f : } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : < c) :
(∀ (i : ι), f i < c)iSup f < c
theorem Cardinal.iSup_lt_of_isRegular {ι : Type u_2} {f : } {c : Cardinal.{u_2}} (hc : c.IsRegular) (hι : < c) :
(∀ (i : ι), f i < c)iSup f < c
theorem Cardinal.sum_lt_lift_of_isRegular {ι : Type u} {f : } {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : < c) (hf : ∀ (i : ι), f i < c) :
theorem Cardinal.sum_lt_of_isRegular {ι : Type u} {f : } {c : Cardinal.{u}} (hc : c.IsRegular) (hι : < c) :
(∀ (i : ι), f i < c)
@[simp]
theorem Cardinal.card_lt_of_card_iUnion_lt {ι : Type u} {α : Type u} {t : ιSet α} {c : Cardinal.{u}} (h : Cardinal.mk (⋃ (i : ι), t i) < c) (i : ι) :
Cardinal.mk (t i) < c
@[simp]
theorem Cardinal.card_iUnion_lt_iff_forall_of_isRegular {ι : Type u} {α : Type u} {t : ιSet α} {c : Cardinal.{u}} (hc : c.IsRegular) (hι : < c) :
Cardinal.mk (⋃ (i : ι), t i) < c ∀ (i : ι), Cardinal.mk (t i) < c
theorem Cardinal.card_lt_of_card_biUnion_lt {α : Type u} {β : Type u} {s : Set α} {t : (a : α) → a sSet β} {c : Cardinal.{u}} (h : Cardinal.mk (⋃ (a : α), ⋃ (h : a s), t a h) < c) (a : α) (ha : a s) :
Cardinal.mk (t a ha) < c
theorem Cardinal.card_biUnion_lt_iff_forall_of_isRegular {α : Type u} {β : Type u} {s : Set α} {t : (a : α) → a sSet β} {c : Cardinal.{u}} (hc : c.IsRegular) (hs : < c) :
Cardinal.mk (⋃ (a : α), ⋃ (h : a s), t a h) < c ∀ (a : α) (ha : a s), Cardinal.mk (t a ha) < c
theorem Cardinal.nfpFamily_lt_ord_lift_of_isRegular {ι : Type u} {f : ι} {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : < c) (hc' : ) (hf : ∀ (i : ι), b < c.ord, f i b < c.ord) {a : Ordinal.{max u v} } (ha : a < c.ord) :
< c.ord
theorem Cardinal.nfpFamily_lt_ord_of_isRegular {ι : Type u} {f : } {c : Cardinal.{u}} (hc : c.IsRegular) (hι : < c) (hc' : ) {a : Ordinal.{u}} (hf : ∀ (i : ι), b < c.ord, f i b < c.ord) :
a < c.ord < c.ord
theorem Cardinal.nfpBFamily_lt_ord_lift_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o} {c : Cardinal.{max u v} } (hc : c.IsRegular) (ho : Cardinal.lift.{v, u} o.card < c) (hc' : ) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), b < c.ord, f i hi b < c.ord) {a : Ordinal.{max u v} } :
a < c.ordo.nfpBFamily f a < c.ord
theorem Cardinal.nfpBFamily_lt_ord_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o} {c : Cardinal.{u}} (hc : c.IsRegular) (ho : o.card < c) (hc' : ) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), b < c.ord, f i hi b < c.ord) {a : Ordinal.{u}} :
a < c.ordo.nfpBFamily f a < c.ord
theorem Cardinal.nfp_lt_ord_of_isRegular {f : } {c : Cardinal.{u_2}} (hc : c.IsRegular) (hc' : ) (hf : i < c.ord, f i < c.ord) {a : Ordinal.{u_2}} :
a < c.ord < c.ord
theorem Cardinal.derivFamily_lt_ord_lift {ι : Type u} {f : ι} {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : < c) (hc' : ) (hf : ∀ (i : ι), b < c.ord, f i b < c.ord) {a : Ordinal.{max u v} } :
a < c.ord < c.ord
theorem Cardinal.derivFamily_lt_ord {ι : Type u} {f : } {c : Cardinal.{u}} (hc : c.IsRegular) (hι : < c) (hc' : ) (hf : ∀ (i : ι), b < c.ord, f i b < c.ord) {a : Ordinal.{u}} :
a < c.ord < c.ord
theorem Cardinal.derivBFamily_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o} {c : Cardinal.{max u v} } (hc : c.IsRegular) (hι : Cardinal.lift.{v, u} o.card < c) (hc' : ) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), b < c.ord, f i hi b < c.ord) {a : Ordinal.{max u v} } :
a < c.ordo.derivBFamily f a < c.ord
theorem Cardinal.derivBFamily_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o} {c : Cardinal.{u}} (hc : c.IsRegular) (hι : o.card < c) (hc' : ) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), b < c.ord, f i hi b < c.ord) {a : Ordinal.{u}} :
a < c.ordo.derivBFamily f a < c.ord
theorem Cardinal.deriv_lt_ord {f : } {c : Cardinal.{u}} (hc : c.IsRegular) (hc' : ) (hf : i < c.ord, f i < c.ord) {a : Ordinal.{u}} :
a < c.ord < c.ord

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

Equations
• c.IsInaccessible = ( c.IsRegular c.IsStrongLimit)
Instances For
theorem Cardinal.IsInaccessible.mk {c : Cardinal.{u_2}} (h₁ : ) (h₂ : c c.ord.cof) (h₃ : x < c, 2 ^ x < c) :
c.IsInaccessible
theorem Cardinal.lt_power_cof {c : Cardinal.{u}} :
c < c ^ c.ord.cof
theorem Cardinal.lt_cof_power {a : Cardinal.{u_2}} {b : Cardinal.{u_2}} (ha : ) (b1 : 1 < b) :
a < (b ^ a).ord.cof
theorem Ordinal.sup_sequence_lt_omega1 {α : Type u_2} [] (o : ) (ho : ∀ (n : α), o n < ().ord) :
< ().ord