feat: singular cardinals (leanprover-community#37098)

We define a singular cardinal as an infinite cardinal which is larger than its cofinality. That's to say, every cardinal is exactly one of the following three: finite, regular, or singular.

Co-authored-by: Nir Paz <paznir83@gmail.com>

Author: vihdzp

Mathlib/SetTheory/Cardinal/Aleph.lean

@@ -446,10 +446,15 @@ theorem isNormal_aleph : Order.IsNormal aleph :=
 theorem aleph_limit {o : Ordinal} (ho : IsSuccLimit o) : ℵ_ o = ⨆ a : Iio o, ℵ_ a :=
   isNormal_aleph.apply_of_isSuccLimit ho
 
+@[simp]
 theorem aleph0_le_aleph (o : Ordinal) : ℵ₀ ≤ ℵ_ o := by
   rw [aleph_eq_preAleph, aleph0_le_preAleph]
   exact le_self_add
 
+@[simp]
+theorem aleph0_lt_aleph {o : Ordinal} : ℵ₀ < ℵ_ o ↔ 0 < o := by
+  rw [← aleph_zero, aleph_lt_aleph]
+
 theorem aleph_pos (o : Ordinal) : 0 < ℵ_ o :=
   aleph0_pos.trans_le (aleph0_le_aleph o)
 

Mathlib/SetTheory/Cardinal/Arithmetic.lean

@@ -103,13 +103,11 @@ theorem aleph0_mul_mk_eq {α : Type*} [Infinite α] : ℵ₀ * #α = #α :=
 theorem mk_mul_aleph0_eq {α : Type*} [Infinite α] : #α * ℵ₀ = #α :=
   mul_aleph0_eq (aleph0_le_mk α)
 
-@[simp]
-theorem aleph0_mul_aleph (o : Ordinal) : ℵ₀ * ℵ_ o = ℵ_ o :=
-  aleph0_mul_eq (aleph0_le_aleph o)
+theorem aleph0_mul_aleph (o : Ordinal) : ℵ₀ * ℵ_ o = ℵ_ o := by
+  simp
 
-@[simp]
-theorem aleph_mul_aleph0 (o : Ordinal) : ℵ_ o * ℵ₀ = ℵ_ o :=
-  mul_aleph0_eq (aleph0_le_aleph o)
+theorem aleph_mul_aleph0 (o : Ordinal) : ℵ_ o * ℵ₀ = ℵ_ o := by
+  simp
 
 theorem mul_lt_of_lt {a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a < c) (h2 : b < c) : a * b < c :=
   (mul_le_mul' (le_max_left a b) (le_max_right a b)).trans_lt <|

Mathlib/SetTheory/Cardinal/Regular.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Floris van Doorn, Violeta Hernández Palacios
+Authors: Mario Carneiro, Floris van Doorn, Violeta Hernández Palacios, Nir Paz
 -/
 module
 
@@ -11,18 +11,19 @@ public import Mathlib.SetTheory.Ordinal.FixedPoint
 /-!
 # Regular cardinals
 
-This file defines regular and inaccessible cardinals.
+This file defines regular, singular, and inaccessible cardinals.
 
 ## Main definitions
 
-* `Cardinal.IsRegular c` means that `c` is a regular cardinal: `ℵ₀ ≤ c ∧ c.ord.cof = c`.
+* `Cardinal.IsRegular c` means that `c` is an infinite cardinal, equal to its own cofinality.
+* `Cardinal.IsSingular c` means that `c` is an infinite cardinal which is not regular. That is,
+  its cofinality is smaller than itself.
 * `Cardinal.IsInaccessible c` means that `c` is strongly inaccessible:
   `ℵ₀ < c ∧ IsRegular c ∧ IsStrongLimit c`.
 
 ## TODO
 
 * Prove more theorems on inaccessible cardinals.
-* Define singular cardinals.
 -/
 
 @[expose] public section
@@ -32,31 +33,33 @@ universe u v
 open Function Cardinal Set Order Ordinal
 
 namespace Cardinal
+variable {c : Cardinal}
 
 /-! ### Regular cardinals -/
 
 /-- A cardinal is regular if it is infinite and it equals its own cofinality. -/
+@[mk_iff]
 structure IsRegular (c : Cardinal) : Prop where
   /-- A regular cardinal is infinite. -/
   aleph0_le : ℵ₀ ≤ c
   /-- A cardinal equals its own cofinality. See `IsRegular.cof_eq`. -/
   le_cof_ord : c ≤ c.ord.cof
 
-theorem IsRegular.cof_ord {c : Cardinal} (H : c.IsRegular) : c.ord.cof = c :=
+theorem IsRegular.cof_ord (H : c.IsRegular) : c.ord.cof = c :=
   (cof_ord_le c).antisymm H.2
 
 @[deprecated (since := "2026-03-22")] alias IsRegular.cof_eq := IsRegular.cof_ord
 
 theorem IsRegular.cof_omega_eq {o : Ordinal} (H : (ℵ_ o).IsRegular) : (ω_ o).cof = ℵ_ o := by
   rw [← ord_aleph, H.cof_ord]
 
-theorem IsRegular.pos {c : Cardinal} (H : c.IsRegular) : 0 < c :=
+theorem IsRegular.pos (H : c.IsRegular) : 0 < c :=
   aleph0_pos.trans_le H.1
 
-theorem IsRegular.nat_lt {c : Cardinal} (H : c.IsRegular) (n : ℕ) : n < c :=
+theorem IsRegular.nat_lt (H : c.IsRegular) (n : ℕ) : n < c :=
   lt_of_lt_of_le natCast_lt_aleph0 H.aleph0_le
 
-theorem IsRegular.ord_pos {c : Cardinal} (H : c.IsRegular) : 0 < c.ord := by
+theorem IsRegular.ord_pos (H : c.IsRegular) : 0 < c.ord := by
   rw [Cardinal.lt_ord, card_zero]
   exact H.pos
 
@@ -65,7 +68,7 @@ theorem isRegular_cof {o : Ordinal} (h : IsSuccLimit o) : IsRegular o.cof := by
   rwa [aleph0_le_cof_iff, one_lt_cof_iff]
 
 /-- 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 :=
+lemma IsRegular.ne_zero (H : c.IsRegular) : c ≠ 0 :=
   H.pos.ne'
 
 theorem isRegular_aleph0 : IsRegular ℵ₀ :=
@@ -201,7 +204,7 @@ theorem bsup_lt_ord_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc
     (hι : o.card < c) : (∀ i hi, f i hi < c.ord) → Ordinal.bsup o f < c.ord :=
   bsup_lt_ord (by rwa [hc.cof_ord])
 
-@[deprecated lift_iSup_lt_of_lt_cof (since := "2026-03-22")]
+@[deprecated lift_iSup_lt_of_lt_cof_ord (since := "2026-03-22")]
 theorem iSup_lt_lift_of_isRegular {ι} {f : ι → Cardinal} {c} (hc : IsRegular c)
     (hι : Cardinal.lift.{v, u} #ι < c) (hf : ∀ i, f i < c) : iSup f < c := by
   apply lift_iSup_lt_of_lt_cof_ord _ hf
@@ -212,13 +215,13 @@ theorem iSup_lt_of_isRegular {ι} {f : ι → Cardinal} {c} (hc : IsRegular c) (
     (∀ i, f i < c) → iSup f < c :=
   iSup_lt_of_lt_cof_ord (by rwa [hc.cof_ord])
 
-theorem sum_lt_lift_of_isRegular {ι : Type u} {f : ι → Cardinal} {c : Cardinal} (hc : IsRegular c)
+theorem sum_lt_lift_of_isRegular {ι : Type u} {f : ι → Cardinal} (hc : IsRegular c)
     (hι : Cardinal.lift.{v, u} #ι < c) (hf : ∀ i, f i < c) : sum f < c := by
   apply (sum_le_lift_mk_mul_iSup _).trans_lt <|
     mul_lt_of_lt hc.1 hι (lift_iSup_lt_of_lt_cof_ord _ hf)
   rwa [lift_umax, c.lift_id', hc.cof_ord]
 
-theorem sum_lt_of_isRegular {ι : Type u} {f : ι → Cardinal} {c : Cardinal} (hc : IsRegular c)
+theorem sum_lt_of_isRegular {ι : Type u} {f : ι → 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])
 
@@ -229,7 +232,7 @@ theorem card_lt_of_card_iUnion_lt {ι : Type u} {α : Type u} {t : ι → Set α
 
 @[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) < c ↔ ∀ i, #(t i) < c := by
+    (hc : c.IsRegular) (hι : #ι < c) : #(⋃ 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 (mk_range_le.trans_lt hι)
@@ -244,7 +247,7 @@ theorem card_lt_of_card_biUnion_lt {α β : Type u} {s : Set α} {t : ∀ a ∈
   simp_all only [iUnion_coe_set, Subtype.forall]
 
 theorem card_biUnion_lt_iff_forall_of_isRegular {α β : Type u} {s : Set α} {t : ∀ a ∈ s, Set β}
-    {c : Cardinal} (hc : c.IsRegular) (hs : #s < c) :
+    (hc : c.IsRegular) (hs : #s < c) :
     #(⋃ 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']
 
@@ -297,6 +300,91 @@ theorem deriv_lt_ord {f : Ordinal.{u} → Ordinal} {c} (hc : IsRegular c) (hc' :
   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
 
+/-! ### Singular cardinals -/
+
+/-- A cardinal is singular if it is infinite and not regular. -/
+@[mk_iff]
+structure IsSingular (c : Cardinal) : Prop where
+  /-- A singular cardinal is infinite. -/
+  aleph0_le : ℵ₀ ≤ c
+  /-- A singular cardinal is not regular, see `IsSingular.not_isRegular`. -/
+  cof_ord_ne : c.ord.cof ≠ c
+
+theorem IsSingular.cof_ord_lt (hc : c.IsSingular) : c.ord.cof < c :=
+  (cof_ord_le c).lt_of_ne hc.cof_ord_ne
+
+theorem IsSingular.natCast_lt (hc : c.IsSingular) (n : ℕ) : n < c :=
+  natCast_lt_aleph0.trans_le hc.aleph0_le
+
+theorem IsSingular.pos (hc : c.IsSingular) : 0 < c :=
+  hc.natCast_lt 0
+
+theorem IsSingular.not_isRegular (hc : c.IsSingular) : ¬ c.IsRegular :=
+  fun hc' ↦ hc'.le_cof_ord.not_gt hc.cof_ord_lt
+
+theorem IsRegular.not_isSingular (hc : c.IsRegular) : ¬ c.IsSingular :=
+  imp_not_comm.1 IsSingular.not_isRegular hc
+
+@[simp]
+theorem not_isSingular_aleph0 : ¬ IsSingular ℵ₀ :=
+  isRegular_aleph0.not_isSingular
+
+@[simp]
+theorem not_isSingular_aleph_one : ¬ IsSingular ℵ₁ :=
+  isRegular_aleph_one.not_isSingular
+
+@[simp]
+theorem not_isSingular_succ (c : Cardinal) : ¬ IsSingular (succ c) := by
+  obtain hc | hc := lt_or_ge c ℵ₀
+  · obtain ⟨n, rfl⟩ := lt_aleph0.1 hc
+    refine fun h ↦ h.aleph0_le.not_gt ?_
+    rw [succ_natCast, ← Nat.cast_add_one]
+    exact natCast_lt_aleph0
+  · exact (isRegular_succ hc).not_isSingular
+
+@[simp]
+theorem not_isRegular_aleph_add_one (o : Ordinal) : ¬ IsSingular (ℵ_ (o + 1)) := by
+  simp [← succ_aleph]
+
+theorem IsSingular.isSuccLimit (hc : IsSingular c) : IsSuccLimit c := by
+  rw [Cardinal.isSuccLimit_iff, isSuccPrelimit_iff_succ_ne]
+  refine ⟨hc.pos.ne', ?_⟩
+  rintro c rfl
+  exact not_isSingular_succ c hc
+
+theorem isRegular_or_isSingular (h : ℵ₀ ≤ c) : c.IsRegular ∨ c.IsSingular := by
+  rw [isSingular_iff, ← (cof_ord_le c).lt_iff_ne, ← not_le]
+  tauto
+
+theorem lt_aleph0_or_isRegular_or_isSingular : c < ℵ₀ ∨ c.IsRegular ∨ c.IsSingular := by
+  have := isRegular_or_isSingular (c := c)
+  rw [← not_le]
+  tauto
+
+theorem IsSingular.of_not_isRegular (h₀ : ℵ₀ ≤ c) (hc : ¬ IsRegular c) : IsSingular c :=
+  (isRegular_or_isSingular h₀).resolve_left hc
+
+theorem IsRegular.of_not_isSingular (h₀ : ℵ₀ ≤ c) (hc : ¬ IsSingular c) : IsRegular c :=
+  (isRegular_or_isSingular h₀).resolve_right hc
+
+theorem isSingular_aleph_iff {o : Ordinal} : (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o := by
+  obtain rfl | ⟨a, rfl⟩ | ho := zero_or_succ_or_isSuccLimit o
+  · simp
+  · simp
+  · rw [isSingular_iff, ← (cof_ord_le _).lt_iff_ne]
+    simp [ho]
+
+theorem IsSingular.isSuccLimit_of_aleph {o : Ordinal} (hc : IsSingular (ℵ_ o)) : IsSuccLimit o :=
+  (isSingular_aleph_iff.1 hc).1
+
+theorem isSingular_aleph_omega0 : (ℵ_ ω).IsSingular := by simp [isSingular_aleph_iff]
+
+theorem IsSingular.aleph_omega0_le (hc : IsSingular c) : ℵ_ ω ≤ c := by
+  obtain ⟨o, rfl⟩ := mem_range_aleph_iff.2 hc.aleph0_le
+  rw [isSingular_aleph_iff] at hc
+  rw [aleph_le_aleph]
+  exact omega0_le_of_isSuccLimit hc.1
+
 /-! ### Inaccessible cardinals -/
 
 /-- A cardinal is inaccessible if it is an uncountable regular strong limit cardinal. -/
@@ -308,23 +396,22 @@ structure IsInaccessible (c : Cardinal) : Prop where
   /-- An inaccessible cardinal is a strong limit, see `IsInaccessible.isStrongLimit`. -/
   two_power_lt ⦃x⦄ : x < c → 2 ^ x < c
 
-theorem IsInaccessible.nat_lt {c : Cardinal} (h : IsInaccessible c) (n : ℕ) : n < c :=
+theorem IsInaccessible.nat_lt (h : IsInaccessible c) (n : ℕ) : n < c :=
   natCast_lt_aleph0.trans h.1
 
-theorem IsInaccessible.pos {c : Cardinal} (h : IsInaccessible c) : 0 < c :=
+theorem IsInaccessible.pos (h : IsInaccessible c) : 0 < c :=
   aleph0_pos.trans h.1
 
-theorem IsInaccessible.ne_zero {c : Cardinal} (h : IsInaccessible c) : c ≠ 0 :=
+theorem IsInaccessible.ne_zero (h : IsInaccessible c) : c ≠ 0 :=
   h.pos.ne'
 
-theorem IsInaccessible.isRegular {c : Cardinal} (h : IsInaccessible c) : IsRegular c :=
+theorem IsInaccessible.isRegular (h : IsInaccessible c) : IsRegular c :=
   ⟨h.aleph0_lt.le, h.le_cof_ord⟩
 
-theorem IsInaccessible.isStrongLimit {c : Cardinal} (h : IsInaccessible c) : IsStrongLimit c :=
+theorem IsInaccessible.isStrongLimit (h : IsInaccessible c) : IsStrongLimit c :=
   ⟨h.ne_zero, h.two_power_lt⟩
 
-theorem isInaccessible_def {c : Cardinal} :
-    IsInaccessible c ↔ ℵ₀ < c ∧ IsRegular c ∧ IsStrongLimit c where
+theorem isInaccessible_def : IsInaccessible c ↔ ℵ₀ < c ∧ IsRegular c ∧ IsStrongLimit c where
   mp h := ⟨h.aleph0_lt, h.isRegular, h.isStrongLimit⟩
   mpr := fun ⟨h₁, h₂, h₃⟩ ↦ ⟨h₁, h₂.2, h₃.two_power_lt⟩