feat(set_theory/cardinal/ordinal): basic properties on Beth numbers (#…

…14989)

We define Beth cardinals and prove miscellaneous basic properties about them.

src/set_theory/cardinal/basic.lean

@@ -619,6 +619,9 @@ begin
   simpa using le_mk_iff_exists_set.1 hx
 end
 
+instance (a : cardinal.{u}) : small.{u} (set.Iio a) :=
+small_subset Iio_subset_Iic_self
+
 /-- A set of cardinals is bounded above iff it's small, i.e. it corresponds to an usual ZFC set. -/
 theorem bdd_above_iff_small {s : set cardinal.{u}} : bdd_above s ↔ small.{u} s :=
 ⟨λ ⟨a, ha⟩, @small_subset _ (Iic a) s (λ x h, ha h) _, begin
@@ -633,6 +636,9 @@ theorem bdd_above_iff_small {s : set cardinal.{u}} : bdd_above s ↔ small.{u} s
   { simp_rw [subtype.val_eq_coe, equiv.symm_apply_apply], refl }
 end⟩
 
+theorem bdd_above_of_small (s : set cardinal.{u}) [h : small.{u} s] : bdd_above s :=
+bdd_above_iff_small.2 h
+
 theorem bdd_above_image (f : cardinal.{u} → cardinal.{max u v}) {s : set cardinal.{u}}
   (hs : bdd_above s) : bdd_above (f '' s) :=
 by { rw bdd_above_iff_small at hs ⊢, exactI small_lift _ }

src/set_theory/cardinal/cofinality.lean

@@ -756,6 +756,19 @@ theorem is_strong_limit.is_limit {c} (H : is_strong_limit c) : is_limit c :=
 theorem is_limit_aleph_0 : is_limit ℵ₀ :=
 is_strong_limit_aleph_0.is_limit
 
+theorem is_strong_limit_beth {o : ordinal} (H : ∀ a < o, succ a < 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,
+    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)) }
+end
+
 theorem mk_bounded_subset {α : Type*} (h : ∀ x < #α, 2 ^ x < #α) {r : α → α → Prop}
   [is_well_order α r] (hr : (#α).ord = type r) : #{s : set α // bounded r s} = #α :=
 begin

src/set_theory/cardinal/continuum.lean

@@ -40,6 +40,8 @@ lemma aleph_0_lt_continuum : ℵ₀ < 𝔠 := cantor ℵ₀
 
 lemma aleph_0_le_continuum : ℵ₀ ≤ 𝔠 := aleph_0_lt_continuum.le
 
+@[simp] lemma beth_one : beth 1 = 𝔠 := by simpa using beth_succ 0
+
 lemma nat_lt_continuum (n : ℕ) : ↑n < 𝔠 := (nat_lt_aleph_0 n).trans aleph_0_lt_continuum
 
 lemma mk_set_nat : #(set ℕ) = 𝔠 := by simp

src/set_theory/cardinal/ordinal.lean

@@ -23,6 +23,9 @@ using ordinals.
 * The function `cardinal.aleph` gives the infinite cardinals listed by their
   ordinal index. `aleph 0 = ℵ₀`, `aleph 1 = succ ℵ₀` is the first
   uncountable cardinal, and so on.
+* The function `cardinal.beth` enumerates the Beth cardinals. `beth 0 = ℵ₀`,
+  `beth (succ o) = 2 ^ beth o`, and for a limit ordinal `o`, `beth o` is the supremum of `beth a`
+  for `a < o`.
 
 ## Main Statements
 
@@ -60,6 +63,8 @@ begin
     { rw ord_aleph_0, exact omega_is_limit } }
 end
 
+/-! ### Aleph cardinals -/
+
 /-- The `aleph'` index function, which gives the ordinal index of a cardinal.
   (The `aleph'` part is because unlike `aleph` this counts also the
   finite stages. So `aleph_idx n = n`, `aleph_idx ω = ω`,
@@ -173,6 +178,13 @@ 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 :=
+begin
+  refine le_antisymm _ (csupr_le' (λ i, aleph'_le.2 (le_of_lt i.2))),
+  rw aleph'_le_of_limit ho,
+  exact λ a ha, le_csupr (bdd_above_of_small _) (⟨a, ha⟩ : Iio o)
+end
+
 @[simp] theorem aleph'_omega : aleph' ω = ℵ₀ :=
 eq_of_forall_ge_iff $ λ c, begin
   simp only [aleph'_le_of_limit omega_is_limit, lt_omega, exists_imp_distrib, aleph_0_le],
@@ -202,10 +214,24 @@ begin
 end
 
 @[simp] theorem aleph_succ {o : ordinal} : aleph (succ o) = succ (aleph o) :=
-by { rw [aleph, add_succ, aleph'_succ], refl }
+by rw [aleph, add_succ, aleph'_succ, aleph]
 
 @[simp] theorem aleph_zero : aleph 0 = ℵ₀ :=
-by simp only [aleph, add_zero, aleph'_omega]
+by rw [aleph, add_zero, aleph'_omega]
+
+theorem aleph_limit {o : ordinal} (ho : is_limit o) : aleph o = ⨆ a : Iio o, aleph a :=
+begin
+  apply le_antisymm _ (csupr_le' _),
+  { rw [aleph, aleph'_limit (ho.add _)],
+    refine csupr_mono' (bdd_above_of_small _) _,
+    rintro ⟨i, hi⟩,
+    cases lt_or_le i ω,
+    { rcases lt_omega.1 h with ⟨n, rfl⟩,
+      use ⟨0, ho.pos⟩,
+      simpa using (nat_lt_aleph_0 n).le },
+    { exact ⟨⟨_, (sub_lt_of_le h).2 hi⟩, aleph'_le.2 (le_add_sub _ _)⟩ } },
+  { exact λ i, aleph_le.2 (le_of_lt i.2) }
+end
 
 theorem aleph_0_le_aleph' {o : ordinal} : ℵ₀ ≤ aleph' o ↔ ω ≤ o :=
 by rw [← aleph'_omega, aleph'_le]
@@ -301,6 +327,69 @@ begin
     exact aleph_0_le_aleph _ }
 end
 
+/-! ### Beth cardinals -/
+
+/-- Beth numbers are defined so that `beth 0 = ℵ₀`, `beth (succ o) = 2 ^ (beth o)`, and when `o` is
+a limit ordinal, `beth o` is the supremum of `beth o'` for `o' < o`.
+
+Assuming the generalized continuum hypothesis, which is undecidable in ZFC, `beth o = aleph o` for
+every `o`. -/
+def beth (o : ordinal.{u}) : cardinal.{u} :=
+limit_rec_on o aleph_0 (λ _ x, 2 ^ x) (λ a ha IH, ⨆ b : Iio a, IH b.1 b.2)
+
+@[simp] theorem beth_zero : beth 0 = aleph_0 :=
+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 :=
+limit_rec_on_limit _ _ _ _
+
+theorem beth_strict_mono : strict_mono beth :=
+begin
+  intros a b,
+  induction b using ordinal.induction with b IH generalizing a,
+  intro h,
+  rcases zero_or_succ_or_limit b with rfl | ⟨c, rfl⟩ | hb,
+  { exact (ordinal.not_lt_zero a h).elim },
+  { rw lt_succ_iff at h,
+    rw beth_succ,
+    apply lt_of_le_of_lt _ (cantor _),
+    rcases eq_or_lt_of_le h with rfl | h, { refl },
+    exact (IH c (lt_succ c) h).le },
+  { apply (cantor _).trans_le,
+    rw [beth_limit hb, ←beth_succ],
+    exact le_csupr (bdd_above_of_small _) (⟨_, hb.succ_lt h⟩ : Iio b) }
+end
+
+@[simp] theorem beth_lt {o₁ o₂ : ordinal} : beth o₁ < beth o₂ ↔ o₁ < o₂ :=
+beth_strict_mono.lt_iff_lt
+
+@[simp] theorem beth_le {o₁ o₂ : ordinal} : beth o₁ ≤ beth o₂ ↔ o₁ ≤ o₂ :=
+beth_strict_mono.le_iff_le
+
+theorem aleph_le_beth (o : ordinal) : aleph o ≤ beth o :=
+begin
+  apply limit_rec_on o,
+  { simp },
+  { intros o h,
+    rw [aleph_succ, beth_succ, succ_le_iff],
+    exact (cantor _).trans_le (power_le_power_left two_ne_zero' h) },
+  { intros o ho IH,
+    rw [aleph_limit ho, beth_limit ho],
+    exact csupr_mono (bdd_above_of_small _) (λ x, IH x.1 x.2) }
+end
+
+theorem aleph_0_le_beth (o : ordinal) : ℵ₀ ≤ beth o :=
+(aleph_0_le_aleph o).trans $ aleph_le_beth o
+
+theorem beth_pos (o : ordinal) : 0 < beth o :=
+aleph_0_pos.trans_le $ aleph_0_le_beth o
+
+theorem beth_ne_zero (o : ordinal) : beth o ≠ 0 :=
+(beth_pos o).ne'
+
 /-! ### Properties of `mul` -/
 
 /-- If `α` is an infinite type, then `α × α` and `α` have the same cardinality. -/

src/set_theory/ordinal/arithmetic.lean

@@ -267,6 +267,9 @@ else by rw [pred_eq_iff_not_succ.2 h,
 /-- A limit ordinal is an ordinal which is not zero and not a successor. -/
 def is_limit (o : ordinal) : Prop := o ≠ 0 ∧ ∀ a < o, succ a < o
 
+theorem is_limit.succ_lt {o a : ordinal} (h : is_limit o) : a < o → succ a < o :=
+h.2 a
+
 theorem not_zero_is_limit : ¬ is_limit 0
 | ⟨h, _⟩ := h rfl
 
@@ -495,6 +498,8 @@ theorem add_is_normal (a : ordinal) : is_normal ((+) a) :=
 theorem add_is_limit (a) {b} : is_limit b → is_limit (a + b) :=
 (add_is_normal a).is_limit
 
+alias add_is_limit ← is_limit.add
+
 /-! ### Subtraction on ordinals-/
 
 /-- The set in the definition of subtraction is nonempty. -/
@@ -531,6 +536,12 @@ protected theorem add_sub_cancel_of_le {a b : ordinal} (h : b ≤ a) : b + (a -
   { exact (add_le_of_limit l).2 (λ c l, (lt_sub.1 l).le) }
 end
 
+theorem le_sub_of_le {a b c : ordinal} (h : b ≤ a) : c ≤ a - b ↔ b + c ≤ a :=
+by rw [←add_le_add_iff_left b, ordinal.add_sub_cancel_of_le h]
+
+theorem sub_lt_of_le {a b c : ordinal} (h : b ≤ a) : a - b < c ↔ a < b + c :=
+lt_iff_lt_of_le_iff_le (le_sub_of_le h)
+
 instance : has_exists_add_of_le ordinal :=
 ⟨λ a b h, ⟨_, (ordinal.add_sub_cancel_of_le h).symm⟩⟩
 
@@ -1102,16 +1113,22 @@ theorem le_sup_shrink_equiv {s : set ordinal.{u}} (hs : small.{u} s) (a) (ha : a
   a ≤ sup.{u u} (λ x, ((@equiv_shrink s hs).symm x).val) :=
 by { convert le_sup.{u u} _ ((@equiv_shrink s hs) ⟨a, ha⟩), rw symm_apply_apply }
 
-theorem small_Iio (o : ordinal.{u}) : small.{u} (set.Iio o) :=
+instance small_Iio (o : ordinal.{u}) : small.{u} (set.Iio o) :=
 let f : o.out.α → set.Iio o := λ x, ⟨typein (<) x, typein_lt_self x⟩ in
 let hf : surjective f := λ b, ⟨enum (<) b.val (by { rw type_lt, exact b.prop }),
   subtype.ext (typein_enum _ _)⟩ in
 small_of_surjective hf
 
+instance small_Iic (o : ordinal.{u}) : small.{u} (set.Iic o) :=
+by { rw ←Iio_succ, apply_instance }
+
 theorem bdd_above_iff_small {s : set ordinal.{u}} : bdd_above s ↔ small.{u} s :=
-⟨λ ⟨a, h⟩, @small_subset _ _ _ (by exact λ b hb, lt_succ_iff.2 (h hb)) (small_Iio (succ a)),
+⟨λ ⟨a, h⟩, small_subset $ show s ⊆ Iic a, from λ x hx, h hx,
 λ h, ⟨sup.{u u} (λ x, ((@equiv_shrink s h).symm x).val), le_sup_shrink_equiv h⟩⟩
 
+theorem bdd_above_of_small (s : set ordinal.{u}) [h : small.{u} s] : bdd_above s :=
+bdd_above_iff_small.2 h
+
 theorem sup_eq_Sup {s : set ordinal.{u}} (hs : small.{u} s) :
   sup.{u u} (λ x, (@equiv_shrink s hs).symm x) = Sup s :=
 let hs' := bdd_above_iff_small.2 hs in