From 7146db25cdcac7c389b0329e0345750537de6997 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Tue, 9 Dec 2025 05:32:16 -0600 Subject: [PATCH 1/4] prove --- Mathlib/SetTheory/Cardinal/Arithmetic.lean | 18 +++++++++++++++--- Mathlib/SetTheory/Cardinal/Defs.lean | 3 +++ 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Arithmetic.lean b/Mathlib/SetTheory/Cardinal/Arithmetic.lean index 281a780b198972..3cc7fad8527e90 100644 --- a/Mathlib/SetTheory/Cardinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Cardinal/Arithmetic.lean @@ -664,19 +664,31 @@ theorem mk_list_eq_mk (α : Type u) [Infinite α] : #(List α) = #α := theorem mk_list_eq_aleph0 (α : Type u) [Countable α] [Nonempty α] : #(List α) = ℵ₀ := mk_le_aleph0.antisymm (aleph0_le_mk _) -theorem mk_list_eq_max_mk_aleph0 (α : Type u) [Nonempty α] : #(List α) = max #α ℵ₀ := by +theorem mk_list_eq_max (α : Type u) [Nonempty α] : #(List α) = max ℵ₀ #α := by cases finite_or_infinite α - · rw [mk_list_eq_aleph0, eq_comm, max_eq_right] + · rw [mk_list_eq_aleph0, eq_comm, max_eq_left] exact mk_le_aleph0 - · rw [mk_list_eq_mk, eq_comm, max_eq_left] + · rw [mk_list_eq_mk, eq_comm, max_eq_right] exact aleph0_le_mk α +-- TODO: standardize whether we write `max ℵ₀ x` or `max x ℵ₀`. +theorem mk_list_eq_max_mk_aleph0 (α : Type u) [Nonempty α] : #(List α) = max #α ℵ₀ := by + rw [mk_list_eq_max, max_comm] + +theorem sum_pow_eq_max_aleph0 {x : Cardinal} (h : x ≠ 0) : sum (fun n ↦ x ^ n) = max ℵ₀ x := by + have := nonempty_out h + conv_lhs => rw [← x.mk_out, ← mk_list_eq_sum_pow, mk_list_eq_max_mk_aleph0, mk_out] + theorem mk_list_le_max (α : Type u) : #(List α) ≤ max ℵ₀ #α := by cases finite_or_infinite α · exact mk_le_aleph0.trans (le_max_left _ _) · rw [mk_list_eq_mk] apply le_max_right +theorem sum_pow_le_max_aleph0 (x : Cardinal) : sum (fun n ↦ x ^ n) ≤ max ℵ₀ x := by + rw [← x.mk_out, ← mk_list_eq_sum_pow] + exact mk_list_le_max _ + @[simp] theorem mk_finset_of_infinite (α : Type u) [Infinite α] : #(Finset α) = #α := by classical diff --git a/Mathlib/SetTheory/Cardinal/Defs.lean b/Mathlib/SetTheory/Cardinal/Defs.lean index d192b5ad747c23..21f56a50ca7443 100644 --- a/Mathlib/SetTheory/Cardinal/Defs.lean +++ b/Mathlib/SetTheory/Cardinal/Defs.lean @@ -229,6 +229,9 @@ theorem mk_ne_zero_iff {α : Type u} : #α ≠ 0 ↔ Nonempty α := theorem mk_ne_zero (α : Type u) [Nonempty α] : #α ≠ 0 := mk_ne_zero_iff.2 ‹_› +theorem nonempty_out {x : Cardinal} (h : x ≠ 0) : Nonempty x.out := by + rwa [← mk_ne_zero_iff, mk_out] + instance : One Cardinal.{u} := -- `PUnit` might be more canonical, but this is convenient for defeq with natCast ⟨lift #(Fin 1)⟩ From 320f1c13a657c0aa6cf46adeedce39c307783f09 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Tue, 9 Dec 2025 05:35:13 -0600 Subject: [PATCH 2/4] add zero case --- Mathlib/SetTheory/Cardinal/Basic.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index 60f22de3de0683..111fefca0b4475 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -618,10 +618,13 @@ theorem mk_singleton {α : Type u} (x : α) : #({x} : Set α) = 1 := theorem mk_vector (α : Type u) (n : ℕ) : #(List.Vector α n) = #α ^ n := (mk_congr (Equiv.vectorEquivFin α n)).trans <| by simp -theorem mk_list_eq_sum_pow (α : Type u) : #(List α) = sum fun n : ℕ => #α ^ n := +theorem mk_list_eq_sum_pow (α : Type u) : #(List α) = sum fun n ↦ #α ^ n := calc #(List α) = #(Σ n, List.Vector α n) := mk_congr (Equiv.sigmaFiberEquiv List.length).symm - _ = sum fun n : ℕ => #α ^ n := by simp + _ = sum fun n ↦ #α ^ n := by simp + +theorem sum_pow_zero : sum (fun n ↦ (0 : Cardinal) ^ n) = 1 := by + rw [← mk_eq_zero (α := PEmpty), ← mk_list_eq_sum_pow, mk_eq_one] theorem mk_quot_le {α : Type u} {r : α → α → Prop} : #(Quot r) ≤ #α := mk_le_of_surjective Quot.exists_rep From d522311961957e9b933d6d788d9f2954c5e5830e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Tue, 9 Dec 2025 06:15:31 -0600 Subject: [PATCH 3/4] Update Arithmetic.lean --- Mathlib/SetTheory/Cardinal/Arithmetic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Arithmetic.lean b/Mathlib/SetTheory/Cardinal/Arithmetic.lean index 3cc7fad8527e90..92e3285ae2ca00 100644 --- a/Mathlib/SetTheory/Cardinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Cardinal/Arithmetic.lean @@ -677,7 +677,7 @@ theorem mk_list_eq_max_mk_aleph0 (α : Type u) [Nonempty α] : #(List α) = max theorem sum_pow_eq_max_aleph0 {x : Cardinal} (h : x ≠ 0) : sum (fun n ↦ x ^ n) = max ℵ₀ x := by have := nonempty_out h - conv_lhs => rw [← x.mk_out, ← mk_list_eq_sum_pow, mk_list_eq_max_mk_aleph0, mk_out] + conv_lhs => rw [← x.mk_out, ← mk_list_eq_sum_pow, mk_list_eq_max, mk_out] theorem mk_list_le_max (α : Type u) : #(List α) ≤ max ℵ₀ #α := by cases finite_or_infinite α From 3a3f7fb77adda6dfa1d6b3b22ac6dca2d8ebaac6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sun, 14 Dec 2025 10:28:47 -0600 Subject: [PATCH 4/4] Update Mathlib/SetTheory/Cardinal/Basic.lean Co-authored-by: Artie Khovanov --- Mathlib/SetTheory/Cardinal/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index 111fefca0b4475..9fc8e11eb89842 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -623,7 +623,7 @@ theorem mk_list_eq_sum_pow (α : Type u) : #(List α) = sum fun n ↦ #α ^ n := #(List α) = #(Σ n, List.Vector α n) := mk_congr (Equiv.sigmaFiberEquiv List.length).symm _ = sum fun n ↦ #α ^ n := by simp -theorem sum_pow_zero : sum (fun n ↦ (0 : Cardinal) ^ n) = 1 := by +theorem sum_zero_pow : sum (fun n ↦ (0 : Cardinal) ^ n) = 1 := by rw [← mk_eq_zero (α := PEmpty), ← mk_list_eq_sum_pow, mk_eq_one] theorem mk_quot_le {α : Type u} {r : α → α → Prop} : #(Quot r) ≤ #α :=