refactor(set_theory/cardinal/basic): redefine cardinal.is_limit in terms of is_succ_limit (#18523)

vihdzp · vihdzp · commit 7c2ce0c2da15 · 2023-04-03T08:02:26.000Z
We redefine `cardinal.is_limit x` as `x ≠ 0 ∧ is_succ_limit x`. This will allow us to make use of the extensive `is_succ_limit` API in the future.
diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean
@@ -9,7 +9,7 @@ import data.nat.part_enat
 import data.set.countable
 import logic.small.basic
 import order.conditionally_complete_lattice.basic
-import order.succ_pred.basic
+import order.succ_pred.limit
 import set_theory.cardinal.schroeder_bernstein
 import tactic.positivity
 
@@ -30,6 +30,7 @@ We define cardinal numbers as a quotient of types under the equivalence relation
 * Multiplication `c₁ * c₂` is defined by `cardinal.mul_def : #α * #β = #(α × β)`.
 * The order `c₁ ≤ c₂` is defined by `cardinal.le_def α β : #α ≤ #β ↔ nonempty (α ↪ β)`.
 * Exponentiation `c₁ ^ c₂` is defined by `cardinal.power_def α β : #α ^ #β = #(β → α)`.
+* `cardinal.is_limit c` means that `c` is a (weak) limit cardinal: `c ≠ 0 ∧ ∀ x < c, succ x < c`.
 * `cardinal.aleph_0` or `ℵ₀` is the cardinality of `ℕ`. This definition is universe polymorphic:
   `cardinal.aleph_0.{u} : cardinal.{u}` (contrast with `ℕ : Type`, which lives in a specific
   universe). In some cases the universe level has to be given explicitly.
@@ -560,6 +561,20 @@ instance : succ_order cardinal :=
 succ_order.of_succ_le_iff (λ c, Inf {c' | c < c'})
   (λ a b, ⟨lt_of_lt_of_le $ Inf_mem $ exists_gt a, cInf_le'⟩)
 
+/-- A cardinal is a limit if it is not zero or a successor cardinal. Note that `ℵ₀` is a limit
+  cardinal by this definition, but `0` isn't.
+
+  Use `is_succ_limit` if you want to include the `c = 0` case. -/
+def is_limit (c : cardinal) : Prop := c ≠ 0 ∧ is_succ_limit c
+
+protected theorem is_limit.ne_zero {c} (h : is_limit c) : c ≠ 0 := h.1
+
+protected theorem is_limit.is_succ_limit {c} (h : is_limit c) : is_succ_limit c := h.2
+
+theorem is_limit.succ_lt {x c} (h : is_limit c) : x < c → succ x < c := h.is_succ_limit.succ_lt
+
+theorem is_succ_limit_zero : is_succ_limit (0 : cardinal) := is_succ_limit_bot
+
 theorem succ_def (c : cardinal) : succ c = Inf {c' | c < c'} := rfl
 
 theorem add_one_le_succ (c : cardinal.{u}) : c + 1 ≤ succ c :=
@@ -1000,6 +1015,24 @@ lt_aleph_0_iff_finite.trans finite_coe_iff
 
 alias lt_aleph_0_iff_set_finite ↔ _ _root_.set.finite.lt_aleph_0
 
+theorem is_succ_limit_aleph_0 : is_succ_limit ℵ₀ :=
+is_succ_limit_of_succ_lt $ λ a ha, begin
+  rcases lt_aleph_0.1 ha with ⟨n, rfl⟩,
+  rw ←nat_succ,
+  apply nat_lt_aleph_0
+end
+
+theorem is_limit_aleph_0 : is_limit ℵ₀ := ⟨aleph_0_ne_zero, is_succ_limit_aleph_0⟩
+
+theorem is_limit.aleph_0_le {c : cardinal} (h : is_limit c) : ℵ₀ ≤ c :=
+begin
+  by_contra' h',
+  rcases lt_aleph_0.1 h' with ⟨_ | n, rfl⟩,
+  { exact h.ne_zero.irrefl },
+  { rw nat_succ at h,
+    exact not_is_succ_limit_succ _ h.is_succ_limit }
+end
+
 @[simp] theorem lt_aleph_0_iff_subtype_finite {p : α → Prop} :
   #{x // p x} < ℵ₀ ↔ {x | p x}.finite :=
 lt_aleph_0_iff_set_finite
diff --git a/src/set_theory/cardinal/cofinality.lean b/src/set_theory/cardinal/cofinality.lean
@@ -20,7 +20,6 @@ This file contains the definition of cofinality of an ordinal number and regular
 * `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_limit c` means that `c` is a (weak) limit cardinal: `c ≠ 0 ∧ ∀ x < c, succ x < c`.
 * `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`.
@@ -715,25 +714,6 @@ open ordinal
 
 local infixr (name := cardinal.pow) ^ := @pow cardinal.{u} cardinal cardinal.has_pow
 
-/-- A cardinal is a limit if it is not zero or a successor
-  cardinal. Note that `ℵ₀` is a limit cardinal by this definition. -/
-def is_limit (c : cardinal) : Prop :=
-c ≠ 0 ∧ ∀ x < c, succ x < c
-
-theorem is_limit.ne_zero {c} (h : is_limit c) : c ≠ 0 :=
-h.1
-
-theorem is_limit.succ_lt {x c} (h : is_limit c) : x < c → succ x < c :=
-h.2 x
-
-theorem is_limit.aleph_0_le {c} (h : is_limit c) : ℵ₀ ≤ c :=
-begin
-  by_contra' h',
-  rcases lt_aleph_0.1 h' with ⟨_ | n, rfl⟩,
-  { exact h.1.irrefl },
-  { simpa using h.2 n }
-end
-
 /-- 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. -/
 def is_strong_limit (c : cardinal) : Prop :=
@@ -751,23 +731,23 @@ theorem is_strong_limit_aleph_0 : is_strong_limit ℵ₀ :=
   exact_mod_cast nat_lt_aleph_0 (pow 2 n)
 end⟩
 
-theorem is_strong_limit.is_limit {c} (H : is_strong_limit c) : is_limit c :=
-⟨H.1, λ x h, (succ_le_of_lt $ cantor x).trans_lt (H.2 _ h)⟩
+protected theorem is_strong_limit.is_succ_limit {c} (H : is_strong_limit c) : is_succ_limit c :=
+is_succ_limit_of_succ_lt $ λ x h, (succ_le_of_lt $ cantor x).trans_lt (H.two_power_lt h)
 
-theorem is_limit_aleph_0 : is_limit ℵ₀ :=
-is_strong_limit_aleph_0.is_limit
+theorem is_strong_limit.is_limit {c} (H : is_strong_limit c) : is_limit c :=
+⟨H.ne_zero, H.is_succ_limit⟩
 
-theorem is_strong_limit_beth {o : ordinal} (H : ∀ a < o, succ a < o) : is_strong_limit (beth o) :=
+theorem is_strong_limit_beth {o : ordinal} (H : is_succ_limit o) : is_strong_limit (beth o) :=
 begin
   rcases eq_or_ne o 0 with rfl | h,
   { rw beth_zero,
     exact is_strong_limit_aleph_0 },
   { refine ⟨beth_ne_zero o, λ a ha, _⟩,
-    rw beth_limit ⟨h, H⟩ at ha,
+    rw beth_limit ⟨h, is_succ_limit_iff_succ_lt.1 H⟩ at ha,
     rcases exists_lt_of_lt_csupr' ha with ⟨⟨i, hi⟩, ha⟩,
     have := power_le_power_left two_ne_zero ha.le,
     rw ←beth_succ at this,
-    exact this.trans_lt (beth_lt.2 (H i hi)) }
+    exact this.trans_lt (beth_lt.2 (H.succ_lt hi)) }
 end
 
 theorem mk_bounded_subset {α : Type*} (h : ∀ x < #α, 2 ^ x < #α) {r : α → α → Prop}
diff --git a/src/set_theory/cardinal/ordinal.lean b/src/set_theory/cardinal/ordinal.lean
@@ -182,7 +182,7 @@ theorem aleph'_le_of_limit {o : ordinal} (l : o.is_limit) {c} :
   exact h _ h'
 end⟩
 
-theorem aleph'_limit {o : ordinal} (ho : is_limit o) : aleph' o = ⨆ a : Iio o, aleph' a :=
+theorem aleph'_limit {o : ordinal} (ho : o.is_limit) : aleph' o = ⨆ a : Iio o, aleph' a :=
 begin
   refine le_antisymm _ (csupr_le' (λ i, aleph'_le.2 (le_of_lt i.2))),
   rw aleph'_le_of_limit ho,
@@ -223,7 +223,7 @@ by rw [aleph, add_succ, aleph'_succ, aleph]
 @[simp] theorem aleph_zero : aleph 0 = ℵ₀ :=
 by rw [aleph, add_zero, aleph'_omega]
 
-theorem aleph_limit {o : ordinal} (ho : is_limit o) : aleph o = ⨆ a : Iio o, aleph a :=
+theorem aleph_limit {o : ordinal} (ho : o.is_limit) : aleph o = ⨆ a : Iio o, aleph a :=
 begin
   apply le_antisymm _ (csupr_le' _),
   { rw [aleph, aleph'_limit (ho.add _)],
@@ -261,7 +261,7 @@ begin
   exact λ h, (ord_injective h).not_gt (aleph_pos o)
 end
 
-theorem ord_aleph_is_limit (o : ordinal) : is_limit (aleph o).ord :=
+theorem ord_aleph_is_limit (o : ordinal) : (aleph o).ord.is_limit :=
 ord_is_limit $ aleph_0_le_aleph _
 
 instance (o : ordinal) : no_max_order (aleph o).ord.out.α :=
@@ -347,7 +347,7 @@ limit_rec_on_zero _ _ _
 @[simp] theorem beth_succ (o : ordinal) : beth (succ o) = 2 ^ beth o :=
 limit_rec_on_succ _ _ _ _
 
-theorem beth_limit {o : ordinal} : is_limit o → beth o = ⨆ a : Iio o, beth a :=
+theorem beth_limit {o : ordinal} : o.is_limit → beth o = ⨆ a : Iio o, beth a :=
 limit_rec_on_limit _ _ _ _
 
 theorem beth_strict_mono : strict_mono beth :=
