Mathlib.SetTheory.Cardinal.Regular

Cardinal.IsRegular definition

(c : Cardinal) : Prop

Full source

/-- A cardinal is regular if it is infinite and it equals its own cofinality. -/
def IsRegular (c : Cardinal) : Prop :=
  ℵ₀ℵ₀ ≤ c ∧ c ≤ c.ord.cof

Regular cardinal

Informal description

A cardinal number $\kappa$ is called *regular* if it is infinite (i.e., $\aleph_0 \leq \kappa$) and equals its own cofinality (i.e., $\kappa = \text{cof}(\kappa^{\text{ord}})$), where $\text{cof}$ denotes the cofinality of the ordinal associated with $\kappa$.

Cardinal.IsRegular.aleph0_le theorem

{c : Cardinal} (H : c.IsRegular) : ℵ₀ ≤ c

Full source

theorem IsRegular.aleph0_le {c : Cardinal} (H : c.IsRegular) : ℵ₀ ≤ c :=
  H.1

Regular cardinals are at least $\aleph_0$

Informal description

For any regular cardinal $\kappa$, we have $\aleph_0 \leq \kappa$.

Cardinal.IsRegular.cof_eq theorem

{c : Cardinal} (H : c.IsRegular) : c.ord.cof = c

Full source

theorem IsRegular.cof_eq {c : Cardinal} (H : c.IsRegular) : c.ord.cof = c :=
  (cof_ord_le c).antisymm H.2

Cofinality of Regular Cardinal Equals Itself: $\mathrm{cof}(\kappa^{\mathrm{ord}}) = \kappa$

Informal description

For any regular cardinal $\kappa$, the cofinality of the ordinal associated with $\kappa$ equals $\kappa$ itself, i.e., $\mathrm{cof}(\kappa^{\mathrm{ord}}) = \kappa$.

Cardinal.IsRegular.cof_omega_eq theorem

{o : Ordinal} (H : (ℵ_ o).IsRegular) : (ω_ o).cof = ℵ_ o

Full source

theorem IsRegular.cof_omega_eq {o : Ordinal} (H : (ℵ_ o).IsRegular) : (ω_ o).cof = ℵ_ o := by
  rw [← ord_aleph, H.cof_eq]

Cofinality of $\omega_o$ Equals $\aleph_o$ for Regular $\aleph_o$

Informal description

For any ordinal $o$, if the cardinal $\aleph_o$ is regular, then the cofinality of the ordinal $\omega_o$ equals $\aleph_o$, i.e., $\mathrm{cof}(\omega_o) = \aleph_o$.

Cardinal.IsRegular.pos theorem

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

Full source

theorem IsRegular.pos {c : Cardinal} (H : c.IsRegular) : 0 < c :=
  aleph0_pos.trans_le H.1

Regular Cardinals are Positive: $0 < \kappa$

Informal description

For any regular cardinal $\kappa$, we have $0 < \kappa$.

Cardinal.IsRegular.nat_lt theorem

{c : Cardinal} (H : c.IsRegular) (n : ℕ) : n < c

Full source

theorem IsRegular.nat_lt {c : Cardinal} (H : c.IsRegular) (n : ℕ) : n < c :=
  lt_of_lt_of_le (nat_lt_aleph0 n) H.aleph0_le

Natural Numbers are Below Regular Cardinals

Informal description

For any regular cardinal $\kappa$ and any natural number $n$, we have $n < \kappa$.

Cardinal.IsRegular.ord_pos theorem

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

Full source

theorem IsRegular.ord_pos {c : Cardinal} (H : c.IsRegular) : 0 < c.ord := by
  rw [Cardinal.lt_ord, card_zero]
  exact H.pos

Regular Cardinals Have Positive Ordinals

Informal description

For any regular cardinal $\kappa$, the corresponding ordinal $\kappa^{\text{ord}}$ is strictly positive, i.e., $0 < \kappa^{\text{ord}}$.

Cardinal.isRegular_cof theorem

{o : Ordinal} (h : o.IsLimit) : IsRegular o.cof

Full source

theorem isRegular_cof {o : Ordinal} (h : o.IsLimit) : IsRegular o.cof :=
  ⟨aleph0_le_cof.2 h, (cof_cof o).ge⟩

Cofinality of Limit Ordinals is Regular

Informal description

For any limit ordinal $o$, the cofinality $\mathrm{cof}(o)$ is a regular cardinal.

Cardinal.IsRegular.ne_zero theorem

{c : Cardinal} (H : c.IsRegular) : c ≠ 0

Full source

/-- If `c` is a regular cardinal, then `c.ord.toType` has a least element. -/
lemma IsRegular.ne_zero {c : Cardinal} (H : c.IsRegular) : c ≠ 0 :=
  H.pos.ne'

Regular Cardinals are Nonzero: $\kappa \neq 0$

Informal description

For any regular cardinal $\kappa$, we have $\kappa \neq 0$.

Cardinal.isRegular_aleph0 theorem

: IsRegular ℵ₀

Full source

theorem isRegular_aleph0 : IsRegular ℵ₀ :=
  ⟨le_rfl, by simp⟩

Regularity of $\aleph_0$

Informal description

The cardinal $\aleph_0$ is regular, meaning it is infinite ($\aleph_0 \leq \aleph_0$) and satisfies $\text{cof}(\aleph_0^{\text{ord}}) = \aleph_0$.

Cardinal.fact_isRegular_aleph0 theorem

: Fact (IsRegular ℵ₀)

Full source

lemma fact_isRegular_aleph0 : Fact (IsRegular ℵ₀) where
  out := isRegular_aleph0

Regularity of $\aleph_0$ as a Fact

Informal description

The cardinal $\aleph_0$ is regular, i.e., it satisfies $\aleph_0 \leq \aleph_0$ and $\text{cof}(\aleph_0^{\text{ord}}) = \aleph_0$.

Cardinal.isRegular_succ theorem

{c : Cardinal.{u}} (h : ℵ₀ ≤ c) : IsRegular (succ c)

Full source

theorem isRegular_succ {c : CardinalCardinal.{u}} (h : ℵ₀ ≤ c) : IsRegular (succ c) :=
  ⟨h.trans (le_succ c),
    succ_le_of_lt
      (by
        have αe := Cardinal.mk_out (succ c)
        set α := (succ c).out
        rcases ord_eq α with ⟨r, wo, re⟩
        have := isLimit_ord (h.trans (le_succ _))
        rw [← αe, re] at this ⊢
        rcases cof_eq' r this with ⟨S, H, Se⟩
        rw [← Se]
        apply lt_imp_lt_of_le_imp_le fun h => mul_le_mul_right' h c
        rw [mul_eq_self h, ← succ_le_iff, ← αe, ← sum_const']
        refine le_trans ?_ (sum_le_sum (fun (x : S) => card (typein r (x : α))) _ fun i => ?_)
        · simp only [← card_typein, ← mk_sigma]
          exact
            ⟨Embedding.ofSurjective (fun x => x.2.1) fun a =>
                let ⟨b, h, ab⟩ := H a
                ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩⟩
        · rw [← lt_succ_iff, ← lt_ord, ← αe, re]
          apply typein_lt_type)⟩

Successor of Infinite Cardinal is Regular

Informal description

For any infinite cardinal number $c$ (i.e., $\aleph_0 \leq c$), the successor cardinal $\text{succ}(c)$ is regular.

Cardinal.isRegular_aleph_one theorem

: IsRegular ℵ₁

Full source

theorem isRegular_aleph_one : IsRegular ℵ₁ := by
  rw [← succ_aleph0]
  exact isRegular_succ le_rfl

Regularity of $\aleph_1$

Informal description

The cardinal number $\aleph_1$ is regular, meaning it is infinite ($\aleph_0 \leq \aleph_1$) and satisfies $\aleph_1 = \text{cof}(\aleph_1^{\text{ord}})$, where $\text{cof}$ denotes the cofinality of the ordinal associated with $\aleph_1$.

Cardinal.isRegular_preAleph_succ theorem

{o : Ordinal} (h : ω ≤ o) : IsRegular (preAleph (succ o))

Full source

theorem isRegular_preAleph_succ {o : Ordinal} (h : ω ≤ o) : IsRegular (preAleph (succ o)) := by
  rw [preAleph_succ]
  exact isRegular_succ (aleph0_le_preAleph.2 h)

Regularity of Successor Cardinals via Pre-Aleph Function: $\text{preAleph}(\text{succ}(o))$ is Regular for $\omega \leq o$

Informal description

For any ordinal $o$ such that $\omega \leq o$, the cardinal $\text{preAleph}(\text{succ}(o))$ is regular, where $\text{succ}(o)$ denotes the successor ordinal of $o$ and $\text{preAleph}$ is the order isomorphism between ordinals and cardinals.

Cardinal.isRegular_aleph_succ theorem

(o : Ordinal) : IsRegular (ℵ_ (succ o))

Full source

theorem isRegular_aleph_succ (o : Ordinal) : IsRegular (ℵ_ (succ o)) := by
  rw [aleph_succ]
  exact isRegular_succ (aleph0_le_aleph o)

Regularity of Successor Aleph Cardinals: $\aleph_{\text{succ}(o)}$ is Regular for All Ordinals $o$

Informal description

For any ordinal number $o$, the successor cardinal $\aleph_{\text{succ}(o)}$ is regular, where $\text{succ}(o)$ denotes the successor ordinal of $o$ and $\aleph$ is the aleph function enumerating infinite cardinals.

Cardinal.lsub_lt_ord_lift_of_isRegular theorem

 {ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : Cardinal.lift.{v, u} #ι < c) :
  (∀ i, f i < c.ord) → Ordinal.lsub.{u, v} f < c.ord

Full source

theorem lsub_lt_ord_lift_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} #ι < c) : (∀ i, f i < c.ord) → Ordinal.lsub.{u, v} f < c.ord :=
  lsub_lt_ord_lift (by rwa [hc.cof_eq])

Least Strict Upper Bound Bounded by Regular Cardinal

Informal description

Let $\iota$ be a type, $f : \iota \to \text{Ordinal}$ be a family of ordinals, and $c$ be a regular cardinal. If the lift of the cardinality of $\iota$ is less than $c$ (i.e., $\text{lift}(\#\iota) < c$) and for every $i \in \iota$, $f(i) < c^{\text{ord}}$, then the least strict upper bound $\text{lsub}(f)$ is less than $c^{\text{ord}}$.

Cardinal.lsub_lt_ord_of_isRegular theorem

{ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) : (∀ i, f i < c.ord) → Ordinal.lsub f < c.ord

Full source

theorem lsub_lt_ord_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) :
    (∀ i, f i < c.ord) → Ordinal.lsub f < c.ord :=
  lsub_lt_ord (by rwa [hc.cof_eq])

Least Strict Upper Bound Bounded by Regular Cardinal in Same Universe

Informal description

Let $\kappa$ be a regular cardinal, $\iota$ be a type with cardinality $\#\iota < \kappa$, and $f : \iota \to \text{Ordinal}$ be a family of ordinals such that $f(i) < \kappa^{\text{ord}}$ for all $i \in \iota$. Then the least strict upper bound $\text{lsub}(f)$ is less than $\kappa^{\text{ord}}$.

Cardinal.iSup_lt_ord_lift_of_isRegular theorem

 {ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : Cardinal.lift.{v, u} #ι < c) : (∀ i, f i < c.ord) → iSup f < c.ord

Full source

theorem iSup_lt_ord_lift_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} #ι < c) : (∀ i, f i < c.ord) → iSup f < c.ord :=
  iSup_lt_ord_lift (by rwa [hc.cof_eq])

Supremum Bounded by Regular Cardinal (Lifted Universe Version)

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of ordinals indexed by a type $\iota$, and let $c$ be a regular cardinal. If the lift of the cardinality of $\iota$ is less than $c$ (i.e., $\text{lift}(\#\iota) < c$) and for every $i \in \iota$, $f_i < c^{\text{ord}}$, then the supremum $\bigsqcup_{i \in \iota} f_i$ is also less than $c^{\text{ord}}$.

Cardinal.iSup_lt_ord_of_isRegular theorem

{ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) : (∀ i, f i < c.ord) → iSup f < c.ord

Full source

theorem iSup_lt_ord_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) :
    (∀ i, f i < c.ord) → iSup f < c.ord :=
  iSup_lt_ord (by rwa [hc.cof_eq])

Supremum Bounded by Regular Cardinal: $\bigsqcup_{i \in \iota} f_i < \kappa^{\text{ord}}$ when $\#\iota < \kappa$

Informal description

Let $\kappa$ be a regular cardinal, $\iota$ be a type with cardinality $\#\iota < \kappa$, and $f : \iota \to \text{Ordinal}$ be a family of ordinals such that $f(i) < \kappa^{\text{ord}}$ for all $i \in \iota$. Then the supremum $\bigsqcup_{i \in \iota} f_i$ is less than $\kappa^{\text{ord}}$.

Cardinal.blsub_lt_ord_lift_of_isRegular theorem

 {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c) (ho : Cardinal.lift.{v, u} o.card < c) :
  (∀ i hi, f i hi < c.ord) → Ordinal.blsub.{u, v} o f < c.ord

Full source

theorem blsub_lt_ord_lift_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c)
    (ho : Cardinal.lift.{v, u} o.card < c) :
    (∀ i hi, f i hi < c.ord) → Ordinal.blsub.{u, v} o f < c.ord :=
  blsub_lt_ord_lift (by rwa [hc.cof_eq])

Bounded Supremum Bound for Regular Cardinals: $\mathrm{blsub}(f) < \kappa^{\mathrm{ord}}$ when $\mathrm{lift}(\#o) < \kappa$

Informal description

Let $o$ be an ordinal and $f$ a family of ordinals indexed by elements $a < o$. If $\kappa$ is a regular cardinal such that the lift of the cardinality of $o$ is strictly less than $\kappa$ (i.e., $\mathrm{lift}(\#o) < \kappa$) and each $f(a) < \kappa^{\mathrm{ord}}$ for all $a < o$, then the bounded supremum $\mathrm{blsub}(f)$ is strictly less than $\kappa^{\mathrm{ord}}$.

Cardinal.blsub_lt_ord_of_isRegular theorem

 {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c) (ho : o.card < c) :
  (∀ i hi, f i hi < c.ord) → Ordinal.blsub o f < c.ord

Full source

theorem blsub_lt_ord_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c)
    (ho : o.card < c) : (∀ i hi, f i hi < c.ord) → Ordinal.blsub o f < c.ord :=
  blsub_lt_ord (by rwa [hc.cof_eq])

Bounded Supremum Bound for Regular Cardinals: $\mathrm{blsub}(f) < \kappa^{\text{ord}}$ when $\#o < \kappa$

Informal description

Let $\kappa$ be a regular cardinal, $o$ an ordinal with $\#o < \kappa$, and $f$ a family of ordinals indexed by elements $a < o$ such that $f(a) < \kappa^{\text{ord}}$ for all $a < o$. Then the bounded supremum $\mathrm{blsub}(f)$ is strictly less than $\kappa^{\text{ord}}$.

Cardinal.bsup_lt_ord_lift_of_isRegular theorem

 {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c) (hι : Cardinal.lift.{v, u} o.card < c) :
  (∀ i hi, f i hi < c.ord) → Ordinal.bsup.{u, v} o f < c.ord

Full source

theorem bsup_lt_ord_lift_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} o.card < c) :
    (∀ i hi, f i hi < c.ord) → Ordinal.bsup.{u, v} o f < c.ord :=
  bsup_lt_ord_lift (by rwa [hc.cof_eq])

Bounded Supremum Bound for Regular Cardinals: $\mathrm{bsup}(f) < \kappa^{\mathrm{ord}}$ when $\mathrm{lift}(\#o) < \kappa$

Informal description

Let $o$ be an ordinal and $f$ a family of ordinals indexed by elements $a < o$. If $\kappa$ is a regular cardinal such that the lift of the cardinality of $o$ is strictly less than $\kappa$ (i.e., $\mathrm{lift}(\#o) < \kappa$) and each $f(a) < \kappa^{\mathrm{ord}}$ for all $a < o$, then the bounded supremum $\mathrm{bsup}(f)$ is strictly less than $\kappa^{\mathrm{ord}}$.

Cardinal.bsup_lt_ord_of_isRegular theorem

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

Full source

theorem bsup_lt_ord_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c)
    (hι : o.card < c) : (∀ i hi, f i hi < c.ord) → Ordinal.bsup o f < c.ord :=
  bsup_lt_ord (by rwa [hc.cof_eq])

Bounded Supremum Bound for Regular Cardinals: $\mathrm{bsup}(f) < \kappa^{\text{ord}}$ when $\#o < \kappa$

Informal description

Let $\kappa$ be a regular cardinal, $o$ an ordinal with $\#o < \kappa$, and $f$ a family of ordinals indexed by elements $a < o$ such that $f(a) < \kappa^{\text{ord}}$ for all $a < o$. Then the bounded supremum $\mathrm{bsup}(f)$ is strictly less than $\kappa^{\text{ord}}$.

Cardinal.iSup_lt_lift_of_isRegular theorem

 {ι} {f : ι → Cardinal} {c} (hc : IsRegular c) (hι : Cardinal.lift.{v, u} #ι < c) :
  (∀ i, f i < c) → iSup.{max u v + 1, u + 1} f < c

Full source

theorem iSup_lt_lift_of_isRegular {ι} {f : ι → Cardinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} #ι < c) : (∀ i, f i < c) → iSup.{max u v + 1, u + 1} f < c :=
  iSup_lt_lift.{u, v} (by rwa [hc.cof_eq])

Supremum of Cardinals Bounded by Regular Cardinal (Lifted Universe Version)

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of cardinal numbers indexed by a type $\iota$, and let $c$ be a regular cardinal. If the lift of the cardinality of $\iota$ is less than $c$ (i.e., $\text{lift}(\#\iota) < c$) and each $f_i < c$, then the supremum $\bigsqcup_{i \in \iota} f_i$ is also less than $c$.

Cardinal.iSup_lt_of_isRegular theorem

{ι} {f : ι → Cardinal} {c} (hc : IsRegular c) (hι : #ι < c) : (∀ i, f i < c) → iSup f < c

Full source

theorem iSup_lt_of_isRegular {ι} {f : ι → Cardinal} {c} (hc : IsRegular c) (hι : #ι < c) :
    (∀ i, f i < c) → iSup f < c :=
  iSup_lt (by rwa [hc.cof_eq])

Supremum of Cardinals Bounded by Regular Cardinal: $\bigsqcup_{i \in \iota} f_i < c$ when $\#\iota < c$ and $\forall i, f_i < c$

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of cardinal numbers indexed by a type $\iota$, and let $c$ be a regular cardinal. If the cardinality of $\iota$ is less than $c$ (i.e., $\#\iota < c$) and each $f_i < c$, then the supremum $\bigsqcup_{i \in \iota} f_i$ is also less than $c$.

Cardinal.sum_lt_lift_of_isRegular theorem

 {ι : Type u} {f : ι → Cardinal} {c : Cardinal} (hc : IsRegular c) (hι : Cardinal.lift.{v, u} #ι < c)
  (hf : ∀ i, f i < c) : sum f < c

Full source

theorem sum_lt_lift_of_isRegular {ι : Type u} {f : ι → Cardinal} {c : Cardinal} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} #ι < c) (hf : ∀ i, f i < c) : sum f < c :=
  (sum_le_iSup_lift _).trans_lt <| mul_lt_of_lt hc.1 hι (iSup_lt_lift_of_isRegular hc hι hf)

Sum of Cardinals Bounded by Regular Cardinal (Lifted Universe Version)

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of cardinal numbers indexed by a type $\iota$, and let $c$ be a regular cardinal. If the lift of the cardinality of $\iota$ is less than $c$ (i.e., $\text{lift}(\#\iota) < c$) and each $f_i < c$, then the sum $\sum_{i \in \iota} f_i$ is also less than $c$.

Cardinal.sum_lt_of_isRegular theorem

{ι : Type u} {f : ι → Cardinal} {c : Cardinal} (hc : IsRegular c) (hι : #ι < c) : (∀ i, f i < c) → sum f < c

Full source

theorem sum_lt_of_isRegular {ι : Type u} {f : ι → Cardinal} {c : Cardinal} (hc : IsRegular c)
    (hι : #ι < c) : (∀ i, f i < c) → sum f < c :=
  sum_lt_lift_of_isRegular.{u, u} hc (by rwa [lift_id])

Sum of Cardinals Bounded by Regular Cardinal

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of cardinal numbers indexed by a type $\iota$, and let $c$ be a regular cardinal. If the cardinality of $\iota$ is less than $c$ (i.e., $\#\iota < c$) and each $f_i < c$, then the sum $\sum_{i \in \iota} f_i$ is also less than $c$.

Cardinal.card_lt_of_card_iUnion_lt theorem

{ι : Type u} {α : Type u} {t : ι → Set α} {c : Cardinal} (h : #(⋃ i, t i) < c) (i : ι) : #(t i) < c

Full source

@[simp]
theorem card_lt_of_card_iUnion_lt {ι : Type u} {α : Type u} {t : ι → Set α} {c : Cardinal}
    (h : #(⋃ i, t i) < c) (i : ι) : #(t i) < c :=
  lt_of_le_of_lt (Cardinal.mk_le_mk_of_subset <| subset_iUnion _ _) h

Cardinality of Union Implies Cardinality of Each Set: $\#(\bigcup_i t_i) < c \implies \forall i, \#t_i < c$

Informal description

For any type $\alpha$ and any indexed family of sets $\{t_i\}_{i \in \iota}$ in $\alpha$, if the cardinality of the union $\bigcup_{i \in \iota} t_i$ is strictly less than a cardinal $c$, then for every index $i \in \iota$, the cardinality of $t_i$ is strictly less than $c$.

Cardinal.card_iUnion_lt_iff_forall_of_isRegular theorem

 {ι : Type u} {α : Type u} {t : ι → Set α} {c : Cardinal} (hc : c.IsRegular) (hι : #ι < c) :
  #(⋃ i, t i) < c ↔ ∀ i, #(t i) < c

Full source

@[simp]
theorem card_iUnion_lt_iff_forall_of_isRegular {ι : Type u} {α : Type u} {t : ι → Set α}
    {c : Cardinal} (hc : c.IsRegular) (hι : #ι < c) : #(⋃ i, t i)#(⋃ i, t i) < c ↔ ∀ i, #(t i) < c := by
  refine ⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩
  apply lt_of_le_of_lt (Cardinal.mk_sUnion_le _)
  apply Cardinal.mul_lt_of_lt hc.aleph0_le
    (lt_of_le_of_lt Cardinal.mk_range_le hι)
  apply Cardinal.iSup_lt_of_isRegular hc (lt_of_le_of_lt Cardinal.mk_range_le hι)
  simpa

Union Cardinality Criterion for Regular Cardinals: $\#(\bigcup_i t_i) < c \leftrightarrow \forall i, \#t_i < c$ when $\#\iota < c$ and $c$ is regular

Informal description

Let $\{t_i\}_{i \in \iota}$ be a family of sets in a type $\alpha$, and let $c$ be a regular cardinal. If the cardinality of the index set $\iota$ is less than $c$ (i.e., $\#\iota < c$), then the cardinality of the union $\bigcup_{i \in \iota} t_i$ is less than $c$ if and only if for every $i \in \iota$, the cardinality of $t_i$ is less than $c$.

Cardinal.card_lt_of_card_biUnion_lt theorem

 {α β : Type u} {s : Set α} {t : ∀ a ∈ s, Set β} {c : Cardinal} (h : #(⋃ a ∈ s, t a ‹_›) < c) (a : α) (ha : a ∈ s) :
  #(t a ha) < c

Full source

theorem card_lt_of_card_biUnion_lt {α β : Type u} {s : Set α} {t : ∀ a ∈ s, Set β} {c : Cardinal}
    (h : #(⋃ a ∈ s, t a ‹_›) < c) (a : α) (ha : a ∈ s) : # (t a ha) < c := by
  rw [biUnion_eq_iUnion] at h
  have := card_lt_of_card_iUnion_lt h
  simp_all only [iUnion_coe_set, Subtype.forall]

Cardinality of Bounded Union Implies Cardinality of Each Set: $\#(\bigcup_{a \in s} t(a)) < c \implies \forall a \in s, \#t(a) < c$

Informal description

For any types $\alpha$ and $\beta$, a set $s \subseteq \alpha$, a family of sets $\{t(a)\}_{a \in s}$ in $\beta$, and a cardinal $c$, if the cardinality of the bounded union $\bigcup_{a \in s} t(a)$ is strictly less than $c$, then for every element $a \in s$, the cardinality of $t(a)$ is strictly less than $c$.

Cardinal.card_biUnion_lt_iff_forall_of_isRegular theorem

 {α β : Type u} {s : Set α} {t : ∀ a ∈ s, Set β} {c : Cardinal} (hc : c.IsRegular) (hs : #s < c) :
  #(⋃ a ∈ s, t a ‹_›) < c ↔ ∀ a (ha : a ∈ s), #(t a ha) < c

Full source

theorem card_biUnion_lt_iff_forall_of_isRegular {α β : Type u} {s : Set α} {t : ∀ a ∈ s, Set β}
    {c : Cardinal} (hc : c.IsRegular) (hs : #s < c) :
    #(⋃ a ∈ s, t a ‹_›)#(⋃ a ∈ s, t a ‹_›) < c ↔ ∀ a (ha : a ∈ s), # (t a ha) < c := by
  rw [biUnion_eq_iUnion, card_iUnion_lt_iff_forall_of_isRegular hc hs, SetCoe.forall']

Bounded Union Cardinality Criterion for Regular Cardinals: $\#(\bigcup_{a \in s} t(a)) < c \leftrightarrow \forall a \in s, \#t(a) < c$ when $\#s < c$ and $c$ is regular

Informal description

Let $\alpha$ and $\beta$ be types, $s$ be a subset of $\alpha$, and $\{t(a)\}_{a \in s}$ be a family of subsets of $\beta$ indexed by elements of $s$. For a regular cardinal $c$ with $\#s < c$, the cardinality of the bounded union $\bigcup_{a \in s} t(a)$ is less than $c$ if and only if for every $a \in s$, the cardinality of $t(a)$ is less than $c$.

Cardinal.nfpFamily_lt_ord_lift_of_isRegular theorem

 {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c) (hι : Cardinal.lift.{v, u} #ι < c) (hc' : c ≠ ℵ₀)
  (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) {a} (ha : a < c.ord) : nfpFamily f a < c.ord

Full source

theorem nfpFamily_lt_ord_lift_of_isRegular {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} #ι < c) (hc' : c ≠ ℵ₀) (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) {a}
    (ha : a < c.ord) : nfpFamily f a < c.ord := by
  apply nfpFamily_lt_ord_lift _ _ hf ha <;> rw [hc.cof_eq]
  · exact lt_of_le_of_ne hc.1 hc'.symm
  · exact hι

Next Fixed Point of Family of Ordinal Functions is Bounded by Regular Cardinal (Lifted Universe Version)

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of ordinal functions indexed by a type $\iota$, and let $c$ be a regular cardinal with $c \neq \aleph_0$. If the lift of the cardinality of $\iota$ is less than $c$ (i.e., $\text{lift}(\#\iota) < c$) and for every $i \in \iota$ and every ordinal $b < c^{\text{ord}}$, we have $f_i(b) < c^{\text{ord}}$, then for any ordinal $a < c^{\text{ord}}$, the next fixed point of the family $\text{nfpFamily}(f, a)$ is also less than $c^{\text{ord}}$.

Cardinal.nfpFamily_lt_ord_of_isRegular theorem

 {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) (hc' : c ≠ ℵ₀) {a}
  (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) : a < c.ord → nfpFamily.{u, u} f a < c.ord

Full source

theorem nfpFamily_lt_ord_of_isRegular {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c)
    (hι : #ι < c) (hc' : c ≠ ℵ₀) {a} (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) :
    a < c.ord → nfpFamily.{u, u} f a < c.ord :=
  nfpFamily_lt_ord_lift_of_isRegular hc (by rwa [lift_id]) hc' hf

Next Fixed Point of Family of Ordinal Functions is Bounded by Regular Cardinal

Informal description

Let $\iota$ be a type, $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ be a family of ordinal functions, and $c$ be a regular cardinal with $c \neq \aleph_0$. If the cardinality of $\iota$ is less than $c$ (i.e., $\#\iota < c$) and for every $i \in \iota$ and every ordinal $b < c^{\text{ord}}$, we have $f_i(b) < c^{\text{ord}}$, then for any ordinal $a < c^{\text{ord}}$, the next fixed point of the family $\text{nfpFamily}(f, a)$ is also less than $c^{\text{ord}}$.

Cardinal.nfp_lt_ord_of_isRegular theorem

 {f : Ordinal → Ordinal} {c} (hc : IsRegular c) (hc' : c ≠ ℵ₀) (hf : ∀ i < c.ord, f i < c.ord) {a} :
  a < c.ord → nfp f a < c.ord

Full source

theorem nfp_lt_ord_of_isRegular {f : Ordinal → Ordinal} {c} (hc : IsRegular c) (hc' : c ≠ ℵ₀)
    (hf : ∀ i < c.ord, f i < c.ord) {a} : a < c.ord → nfp f a < c.ord :=
  nfp_lt_ord (by rw [hc.cof_eq]; exact lt_of_le_of_ne hc.1 hc'.symm) hf

Next Fixed Point of Ordinal Function is Bounded by Regular Cardinal

Informal description

Let $f$ be a function from ordinals to ordinals, and let $c$ be a regular cardinal with $c \neq \aleph_0$. If for every ordinal $i < c^{\text{ord}}$, we have $f(i) < c^{\text{ord}}$, then for any ordinal $a < c^{\text{ord}}$, the next fixed point of $f$ starting from $a$ (denoted $\text{nfp}(f, a)$) is also less than $c^{\text{ord}}$.

Cardinal.derivFamily_lt_ord_lift theorem

 {ι : Type u} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c) (hι : lift.{v} #ι < c) (hc' : c ≠ ℵ₀)
  (hf : ∀ i, ∀ b < c.ord, f i b < c.ord) {a} : a < c.ord → derivFamily f a < c.ord

Full source

theorem derivFamily_lt_ord_lift {ι : Type u} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c)
    (hι : lift.{v} #ι < c) (hc' : c ≠ ℵ₀) (hf : ∀ i, ∀ b < c.ord, f i b < c.ord) {a} :
    a < c.ord → derivFamily f a < c.ord := by
  have hω : ℵ₀ < c.ord.cof := by
    rw [hc.cof_eq]
    exact lt_of_le_of_ne hc.1 hc'.symm
  induction a using limitRecOn with
  | zero =>
    rw [derivFamily_zero]
    exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf
  | succ b hb =>
    intro hb'
    rw [derivFamily_succ]
    exact
      nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf
        ((isLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))
  | isLimit b hb H =>
    intro hb'
    -- TODO: generalize the universes of the lemmas in this file so we don't have to rely on bsup
    have : ⨆ a : Iio b, _ = _ :=
      iSup_eq_bsup.{max u v, max u v} (f := fun x (_ : x < b) ↦ derivFamily f x)
    rw [derivFamily_limit f hb, this]
    exact
      bsup_lt_ord_of_isRegular.{u, v} hc (ord_lt_ord.1 ((ord_card_le b).trans_lt hb')) fun o' ho' =>
        H o' ho' (ho'.trans hb')

Derived Family of Ordinal Functions is Bounded by Regular Cardinal (Lifted Universe Version)

Informal description

Let $\kappa$ be a regular cardinal with $\kappa \neq \aleph_0$, and let $\iota$ be a type such that the lift of its cardinality satisfies $\text{lift}(\#\iota) < \kappa$. Given a family of ordinal functions $f_i : \text{Ordinal} \to \text{Ordinal}$ indexed by $i \in \iota$, if for every $i \in \iota$ and every ordinal $b < \kappa^{\text{ord}}$, we have $f_i(b) < \kappa^{\text{ord}}$, then for any ordinal $a < \kappa^{\text{ord}}$, the derived family $\text{derivFamily}(f, a)$ is also less than $\kappa^{\text{ord}}$.

Cardinal.derivFamily_lt_ord theorem

 {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) (hc' : c ≠ ℵ₀)
  (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) {a} : a < c.ord → derivFamily.{u, u} f a < c.ord

Full source

theorem derivFamily_lt_ord {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c)
    (hc' : c ≠ ℵ₀) (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) {a} :
    a < c.ord → derivFamily.{u, u} f a < c.ord :=
  derivFamily_lt_ord_lift hc (by rwa [lift_id]) hc' hf

Derived Family of Ordinal Functions is Bounded by Regular Cardinal

Informal description

Let $\kappa$ be a regular cardinal with $\kappa \neq \aleph_0$, and let $\iota$ be a type such that its cardinality satisfies $\#\iota < \kappa$. Given a family of ordinal functions $f_i : \text{Ordinal} \to \text{Ordinal}$ indexed by $i \in \iota$, if for every $i \in \iota$ and every ordinal $b < \kappa^{\text{ord}}$, we have $f_i(b) < \kappa^{\text{ord}}$, then for any ordinal $a < \kappa^{\text{ord}}$, the derived family $\text{derivFamily}(f, a)$ is also less than $\kappa^{\text{ord}}$.

Cardinal.deriv_lt_ord theorem

 {f : Ordinal.{u} → Ordinal} {c} (hc : IsRegular c) (hc' : c ≠ ℵ₀) (hf : ∀ i < c.ord, f i < c.ord) {a} :
  a < c.ord → deriv f a < c.ord

Full source

theorem deriv_lt_ord {f : OrdinalOrdinal.{u} → Ordinal} {c} (hc : IsRegular c) (hc' : c ≠ ℵ₀)
    (hf : ∀ i < c.ord, f i < c.ord) {a} : a < c.ord → deriv f a < c.ord :=
  derivFamily_lt_ord_lift hc
    (by simpa using Cardinal.one_lt_aleph0.trans (lt_of_le_of_ne hc.1 hc'.symm)) hc' fun _ => hf

Derived Ordinal is Bounded by Regular Cardinal

Informal description

Let $\kappa$ be a regular cardinal with $\kappa \neq \aleph_0$, and let $f : \text{Ordinal} \to \text{Ordinal}$ be a function such that for every ordinal $i < \kappa^{\text{ord}}$, we have $f(i) < \kappa^{\text{ord}}$. Then for any ordinal $a < \kappa^{\text{ord}}$, the derived ordinal $\text{deriv}(f, a)$ is also less than $\kappa^{\text{ord}}$.

Cardinal.IsInaccessible definition

(c : Cardinal)

Full source

/-- A cardinal is inaccessible if it is an uncountable regular strong limit cardinal. -/
def IsInaccessible (c : Cardinal) :=
  ℵ₀ℵ₀ < c ∧ IsRegular c ∧ IsStrongLimit c

Inaccessible cardinal

Informal description

A cardinal number $ c $ is called *inaccessible* if it satisfies the following three conditions: 1. It is uncountable ($ \aleph_0 < c $), 2. It is regular (i.e., $ \aleph_0 \leq c $ and $ c = \text{cof}(c^{\text{ord}}) $), and 3. It is a strong limit cardinal (i.e., for every cardinal $ x < c $, we have $ 2^x < c $).

Cardinal.IsInaccessible.mk theorem

{c} (h₁ : ℵ₀ < c) (h₂ : c ≤ c.ord.cof) (h₃ : ∀ x < c, (2 ^ x) < c) : IsInaccessible c

Full source

theorem IsInaccessible.mk {c} (h₁ : ℵ₀ < c) (h₂ : c ≤ c.ord.cof) (h₃ : ∀ x < c, (2 ^ x) < c) :
    IsInaccessible c :=
  ⟨h₁, ⟨h₁.le, h₂⟩, (aleph0_pos.trans h₁).ne', @h₃⟩

Characterization of Inaccessible Cardinals

Informal description

A cardinal number $c$ is inaccessible if it satisfies the following three conditions: 1. It is uncountable ($\aleph_0 < c$), 2. It is regular ($c \leq \text{cof}(c^{\text{ord}})$), and 3. It is a strong limit cardinal (for every cardinal $x < c$, we have $2^x < c$).

Cardinal.univ_inaccessible theorem

: IsInaccessible univ.{u, v}

Full source

theorem univ_inaccessible : IsInaccessible univuniv.{u, v} :=
  IsInaccessible.mk (by simpa using lift_lt_univ' ℵ₀) (by simp) fun c h => by
    rcases lt_univ'.1 h with ⟨c, rfl⟩
    rw [← lift_two_power]
    apply lift_lt_univ'

Inaccessibility of the Universal Cardinal

Informal description

The universal cardinal $\text{univ.\{u, v\}}$ is inaccessible. That is: 1. It is uncountable ($\aleph_0 < \text{univ.\{u, v\}}$), 2. It is regular ($\aleph_0 \leq \text{univ.\{u, v\}}$ and $\text{univ.\{u, v\}} = \text{cof}(\text{univ.\{u, v\}}^{\text{ord}})$), and 3. It is a strong limit cardinal (for every cardinal $x < \text{univ.\{u, v\}}$, we have $2^x < \text{univ.\{u, v\}}$).

Ordinal.iSup_sequence_lt_omega1 theorem

{α : Type u} [Countable α] (o : α → Ordinal.{max u v}) (ho : ∀ n, o n < (aleph 1).ord) : iSup o < (aleph 1).ord

Full source

lemma iSup_sequence_lt_omega1 {α : Type u} [Countable α]
    (o : α → OrdinalOrdinal.{max u v}) (ho : ∀ n, o n < (aleph 1).ord) :
    iSup o < (aleph 1).ord := by
  apply iSup_lt_ord_lift _ ho
  rw [Cardinal.isRegular_aleph_one.cof_eq]
  exact lt_of_le_of_lt mk_le_aleph0 aleph0_lt_aleph_one

Supremum of Countable Sequence Below $\aleph_1$ is Below $\aleph_1$

Informal description

Let $\alpha$ be a countable type and let $(o_n)_{n \in \alpha}$ be a sequence of ordinals such that each $o_n$ is less than the ordinal associated with $\aleph_1$. Then the supremum of this sequence is also less than the ordinal associated with $\aleph_1$.

Main definitions

TODO