# Cardinal arithmetic #

Arithmetic operations on cardinals are defined in `SetTheory/Cardinal/Order.lean`. However, proving the important theorem `c * c = c` for infinite cardinals and its corollaries requires the use of ordinal numbers. This is done within this file.

## Main statements #

- `Cardinal.mul_eq_max` and `Cardinal.add_eq_max` state that the product (resp. sum) of two infinite cardinals is just their maximum. Several variations around this fact are also given.
- `Cardinal.mk_list_eq_mk`: when `α` is infinite, `α` and `List α` have the same cardinality.

## Tags #

cardinal arithmetic (for infinite cardinals)

### Properties of `mul` #

source
theorem Cardinal.mul_eq_self {c : Cardinal.{u_1}} (h : aleph0 ≤ c) :
c * c = c

If `α` is an infinite type, then `α × α` and `α` have the same cardinality.

source
theorem Cardinal.mul_eq_max {a b : Cardinal.{u_1}} (ha : aleph0 ≤ a) (hb : aleph0 ≤ b) :
a * b = max a b

If `α` and `β` are infinite types, then the cardinality of `α × β` is the maximum of the cardinalities of `α` and `β`.

source
@[simp]
theorem Cardinal.mul_mk_eq_max {α β : Type u} [Infinite α] [Infinite β] :
mk α * mk β = max (mk α) (mk β)
source
@[simp]
theorem Cardinal.aleph_mul_aleph (o₁ o₂ : Ordinal.{u_1}) :
aleph o₁ * aleph o₂ = aleph (max o₁ o₂)
source
@[simp]
theorem Cardinal.aleph0_mul_eq {a : Cardinal.{u_1}} (ha : aleph0 ≤ a) :
aleph0 * a = a
source
@[simp]
theorem Cardinal.mul_aleph0_eq {a : Cardinal.{u_1}} (ha : aleph0 ≤ a) :
a * aleph0 = a
source
theorem Cardinal.aleph0_mul_mk_eq {α : Type u_1} [Infinite α] :
aleph0 * mk α = mk α
source
theorem Cardinal.mk_mul_aleph0_eq {α : Type u_1} [Infinite α] :
mk α * aleph0 = mk α
source
@[simp]
theorem Cardinal.aleph0_mul_aleph (o : Ordinal.{u_1}) :
aleph0 * aleph o = aleph o
source
@[simp]
theorem Cardinal.aleph_mul_aleph0 (o : Ordinal.{u_1}) :
aleph o * aleph0 = aleph o
source
theorem Cardinal.mul_lt_of_lt {a b c : Cardinal.{u_1}} (hc : aleph0 ≤ c) (h1 : a < c) (h2 : b < c) :
a * b < c
source
theorem Cardinal.mul_le_max_of_aleph0_le_left {a b : Cardinal.{u_1}} (h : aleph0 ≤ a) :
a * b ≤ max a b
source
theorem Cardinal.mul_eq_max_of_aleph0_le_left {a b : Cardinal.{u_1}} (h : aleph0 ≤ a) (h' : b ≠ 0) :
a * b = max a b
source
theorem Cardinal.mul_le_max_of_aleph0_le_right {a b : Cardinal.{u_1}} (h : aleph0 ≤ b) :
a * b ≤ max a b
source
theorem Cardinal.mul_eq_max_of_aleph0_le_right {a b : Cardinal.{u_1}} (h' : a ≠ 0) (h : aleph0 ≤ b) :
a * b = max a b
source
theorem Cardinal.mul_eq_max' {a b : Cardinal.{u_1}} (h : aleph0 ≤ a * b) :
a * b = max a b
source
theorem Cardinal.mul_le_max (a b : Cardinal.{u_1}) :
a * b ≤ max (max a b) aleph0
source
theorem Cardinal.mul_eq_left {a b : Cardinal.{u_1}} (ha : aleph0 ≤ a) (hb : b ≤ a) (hb' : b ≠ 0) :
a * b = a
source
theorem Cardinal.mul_eq_right {a b : Cardinal.{u_1}} (hb : aleph0 ≤ b) (ha : a ≤ b) (ha' : a ≠ 0) :
a * b = b
source
theorem Cardinal.le_mul_left {a b : Cardinal.{u_1}} (h : b ≠ 0) :
a ≤ b * a
source
theorem Cardinal.le_mul_right {a b : Cardinal.{u_1}} (h : b ≠ 0) :
a ≤ a * b
source
theorem Cardinal.mul_eq_left_iff {a b : Cardinal.{u_1}} :
a * b = a ↔ max aleph0 b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

### Properties of `add` #

source
theorem Cardinal.add_eq_self {c : Cardinal.{u_1}} (h : aleph0 ≤ c) :
c + c = c

If `α` is an infinite type, then `α ⊕ α` and `α` have the same cardinality.

source
theorem Cardinal.add_eq_max {a b : Cardinal.{u_1}} (ha : aleph0 ≤ a) :
a + b = max a b

If `α` is an infinite type, then the cardinality of `α ⊕ β` is the maximum of the cardinalities of `α` and `β`.

source
theorem Cardinal.add_eq_max' {a b : Cardinal.{u_1}} (ha : aleph0 ≤ b) :
a + b = max a b
source
@[simp]
theorem Cardinal.add_mk_eq_max {α β : Type u} [Infinite α] :
mk α + mk β = max (mk α) (mk β)
source
@[simp]
theorem Cardinal.add_mk_eq_max' {α β : Type u} [Infinite β] :
mk α + mk β = max (mk α) (mk β)
source
theorem Cardinal.add_mk_eq_self {α : Type u_1} [Infinite α] :
mk α + mk α = mk α
source
theorem Cardinal.add_le_max (a b : Cardinal.{u_1}) :
a + b ≤ max (max a b) aleph0
source
theorem Cardinal.add_le_of_le {a b c : Cardinal.{u_1}} (hc : aleph0 ≤ c) (h1 : a ≤ c) (h2 : b ≤ c) :
a + b ≤ c
source
theorem Cardinal.add_lt_of_lt {a b c : Cardinal.{u_1}} (hc : aleph0 ≤ c) (h1 : a < c) (h2 : b < c) :
a + b < c
source
theorem Cardinal.eq_of_add_eq_of_aleph0_le {a b c : Cardinal.{u_1}} (h : a + b = c) (ha : a < c) (hc : aleph0 ≤ c) :
b = c
source
theorem Cardinal.add_eq_left {a b : Cardinal.{u_1}} (ha : aleph0 ≤ a) (hb : b ≤ a) :
a + b = a
source
theorem Cardinal.add_eq_right {a b : Cardinal.{u_1}} (hb : aleph0 ≤ b) (ha : a ≤ b) :
a + b = b
source
theorem Cardinal.add_eq_left_iff {a b : Cardinal.{u_1}} :
a + b = a ↔ max aleph0 b ≤ a ∨ b = 0
source
theorem Cardinal.add_eq_right_iff {a b : Cardinal.{u_1}} :
a + b = b ↔ max aleph0 a ≤ b ∨ a = 0
source
theorem Cardinal.add_nat_eq {a : Cardinal.{u_1}} (n : ℕ) (ha : aleph0 ≤ a) :
a + ↑n = a
source
theorem Cardinal.nat_add_eq {a : Cardinal.{u_1}} (n : ℕ) (ha : aleph0 ≤ a) :
↑n + a = a
source
theorem Cardinal.add_one_eq {a : Cardinal.{u_1}} (ha : aleph0 ≤ a) :
a + 1 = a
source
theorem Cardinal.mk_add_one_eq {α : Type u_1} [Infinite α] :
mk α + 1 = mk α
source
theorem Cardinal.eq_of_add_eq_add_left {a b c : Cardinal.{u_1}} (h : a + b = a + c) (ha : a < aleph0) :
b = c
source
theorem Cardinal.eq_of_add_eq_add_right {a b c : Cardinal.{u_1}} (h : a + b = c + b) (hb : b < aleph0) :
a = c

### Properties of `ciSup` #

source
theorem Cardinal.ciSup_add {ι : Type u} (f : ι → Cardinal.{v}) [Nonempty ι] (hf : BddAbove (Set.range f)) (c : Cardinal.{v}) :
(⨆ (i : ι), f i) + c = ⨆ (i : ι), f i + c
source
theorem Cardinal.add_ciSup {ι : Type u} (f : ι → Cardinal.{v}) [Nonempty ι] (hf : BddAbove (Set.range f)) (c : Cardinal.{v}) :
c + ⨆ (i : ι), f i = ⨆ (i : ι), c + f i
source
theorem Cardinal.ciSup_add_ciSup {ι : Type u} {ι' : Type w} (f : ι → Cardinal.{v}) [Nonempty ι] [Nonempty ι'] (hf : BddAbove (Set.range f)) (g : ι' → Cardinal.{v}) (hg : BddAbove (Set.range g)) :
(⨆ (i : ι), f i) + ⨆ (j : ι'), g j = ⨆ (i : ι), ⨆ (j : ι'), f i + g j
source
theorem Cardinal.ciSup_mul {ι : Type u} (f : ι → Cardinal.{v}) (c : Cardinal.{v}) :
(⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
source
theorem Cardinal.mul_ciSup {ι : Type u} (f : ι → Cardinal.{v}) (c : Cardinal.{v}) :
c * ⨆ (i : ι), f i = ⨆ (i : ι), c * f i
source
theorem Cardinal.ciSup_mul_ciSup {ι : Type u} {ι' : Type w} (f : ι → Cardinal.{v}) (g : ι' → Cardinal.{v}) :
(⨆ (i : ι), f i) * ⨆ (j : ι'), g j = ⨆ (i : ι), ⨆ (j : ι'), f i * g j
source
theorem Cardinal.sum_eq_lift_iSup_of_lift_mk_le_lift_iSup {ι : Type u} [Small.{v, u} ι] {f : ι → Cardinal.{v}} (hι : aleph0 ≤ mk ι) (h : lift.{v, u} (mk ι) ≤ lift.{u, v} (⨆ (i : ι), f i)) :
sum f = lift.{u, v} (⨆ (i : ι), f i)
source
theorem Cardinal.sum_eq_iSup_of_lift_mk_le_iSup {ι : Type u} {f : ι → Cardinal.{max u v}} (hι : aleph0 ≤ mk ι) (h : lift.{v, u} (mk ι) ≤ ⨆ (i : ι), f i) :
sum f = ⨆ (i : ι), f i
source
theorem Cardinal.sum_eq_iSup_of_mk_le_iSup {ι : Type u} {f : ι → Cardinal.{u}} (hι : aleph0 ≤ mk ι) (h : mk ι ≤ iSup f) :
sum f = ⨆ (i : ι), f i
source
@[deprecated Cardinal.sum_eq_iSup_of_lift_mk_le_iSup (since := "2025-09-06")]
theorem Cardinal.sum_eq_iSup_lift {ι : Type u} {f : ι → Cardinal.{max u v}} (hι : aleph0 ≤ mk ι) (h : lift.{v, u} (mk ι) ≤ ⨆ (i : ι), f i) :
sum f = ⨆ (i : ι), f i

Alias of `Cardinal.sum_eq_iSup_of_lift_mk_le_iSup`.

source
@[deprecated Cardinal.sum_eq_iSup_of_mk_le_iSup (since := "2025-09-06")]
theorem Cardinal.sum_eq_iSup {ι : Type u} {f : ι → Cardinal.{u}} (hι : aleph0 ≤ mk ι) (h : mk ι ≤ iSup f) :
sum f = ⨆ (i : ι), f i

Alias of `Cardinal.sum_eq_iSup_of_mk_le_iSup`.

### Properties of `aleph` #

source
@[simp]
theorem Cardinal.aleph_add_aleph (o₁ o₂ : Ordinal.{u_1}) :
aleph o₁ + aleph o₂ = aleph (max o₁ o₂)
source
theorem Cardinal.add_right_inj_of_lt_aleph0 {α β γ : Cardinal.{u_1}} (γ₀ : γ < aleph0) :
α + γ = β + γ ↔ α = β
source
@[simp]
theorem Cardinal.add_nat_inj {α β : Cardinal.{u_1}} (n : ℕ) :
α + ↑n = β + ↑n ↔ α = β
source
@[simp]
theorem Cardinal.add_one_inj {α β : Cardinal.{u_1}} :
α + 1 = β + 1 ↔ α = β
source
theorem Cardinal.add_le_add_iff_of_lt_aleph0 {α β γ : Cardinal.{u_1}} (γ₀ : γ < aleph0) :
α + γ ≤ β + γ ↔ α ≤ β
source
@[simp]
theorem Cardinal.add_nat_le_add_nat_iff {α β : Cardinal.{u_1}} (n : ℕ) :
α + ↑n ≤ β + ↑n ↔ α ≤ β
source
@[simp]
theorem Cardinal.add_one_le_add_one_iff {α β : Cardinal.{u_1}} :
α + 1 ≤ β + 1 ↔ α ≤ β

### Properties about `power` #

source
theorem Cardinal.pow_le {κ μ : Cardinal.{u}} (H1 : aleph0 ≤ κ) (H2 : μ < aleph0) :
κ ^ μ ≤ κ
source
theorem Cardinal.pow_eq {κ μ : Cardinal.{u}} (H1 : aleph0 ≤ κ) (H2 : 1 ≤ μ) (H3 : μ < aleph0) :
κ ^ μ = κ
source
theorem Cardinal.power_self_eq {c : Cardinal.{u_1}} (h : aleph0 ≤ c) :
c ^ c = 2 ^ c
source
theorem Cardinal.prod_eq_two_power {ι : Type u} [Infinite ι] {c : ι → Cardinal.{v}} (h₁ : ∀ (i : ι), 2 ≤ c i) (h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} (mk ι)) :
prod c = 2 ^ lift.{v, u} (mk ι)
source
theorem Cardinal.power_eq_two_power {c₁ c₂ : Cardinal.{u_1}} (h₁ : aleph0 ≤ c₁) (h₂ : 2 ≤ c₂) (h₂' : c₂ ≤ c₁) :
c₂ ^ c₁ = 2 ^ c₁
source
theorem Cardinal.nat_power_eq {c : Cardinal.{u}} (h : aleph0 ≤ c) {n : ℕ} (hn : 2 ≤ n) :
↑n ^ c = 2 ^ c
source
theorem Cardinal.power_nat_le {c : Cardinal.{u}} {n : ℕ} (h : aleph0 ≤ c) :
c ^ n ≤ c
source
theorem Cardinal.power_nat_eq {c : Cardinal.{u}} {n : ℕ} (h1 : aleph0 ≤ c) (h2 : 1 ≤ n) :
c ^ n = c
source
theorem Cardinal.power_nat_le_max {c : Cardinal.{u}} {n : ℕ} :
c ^ ↑n ≤ max c aleph0
source
theorem Cardinal.power_le_aleph0 {a b : Cardinal.{u}} (ha : a ≤ aleph0) (hb : b < aleph0) :
a ^ b ≤ aleph0
source
theorem Cardinal.powerlt_aleph0 {c : Cardinal.{u_1}} (h : aleph0 ≤ c) :
c ^< aleph0 = c
source
theorem Cardinal.powerlt_aleph0_le (c : Cardinal.{u_1}) :
c ^< aleph0 ≤ max c aleph0

### Computing cardinality of various types #

source
theorem Cardinal.mk_equiv_eq_zero_iff_lift_ne {α : Type u} {β' : Type v} :
mk (α ≃ β') = 0 ↔ lift.{v, u} (mk α) ≠ lift.{u, v} (mk β')
source
theorem Cardinal.mk_equiv_eq_zero_iff_ne {α β : Type u} :
mk (α ≃ β) = 0 ↔ mk α ≠ mk β
source
theorem Cardinal.mk_equiv_comm {α : Type u} {β' : Type v} :
mk (α ≃ β') = mk (β' ≃ α)

This lemma makes lemmas assuming `Infinite α` applicable to the situation where we have `Infinite β` instead.

source
theorem Cardinal.mk_embedding_eq_zero_iff_lift_lt {α : Type u} {β' : Type v} :
mk (α ↪ β') = 0 ↔ lift.{u, v} (mk β') < lift.{v, u} (mk α)
source
theorem Cardinal.mk_embedding_eq_zero_iff_lt {α β : Type u} :
mk (α ↪ β) = 0 ↔ mk β < mk α
source
theorem Cardinal.mk_arrow_eq_zero_iff {α : Type u} {β' : Type v} :
mk (α → β') = 0 ↔ mk α ≠ 0 ∧ mk β' = 0
source
theorem Cardinal.mk_surjective_eq_zero_iff_lift {α : Type u} {β' : Type v} :
mk ↑{f : α → β' | Function.Surjective f} = 0 ↔ lift.{v, u} (mk α) < lift.{u, v} (mk β') ∨ mk α ≠ 0 ∧ mk β' = 0
source
theorem Cardinal.mk_surjective_eq_zero_iff {α β : Type u} :
mk ↑{f : α → β | Function.Surjective f} = 0 ↔ mk α < mk β ∨ mk α ≠ 0 ∧ mk β = 0
source
theorem Cardinal.mk_equiv_le_embedding (α : Type u) (β' : Type v) :
mk (α ≃ β') ≤ mk (α ↪ β')
source
theorem Cardinal.mk_embedding_le_arrow (α : Type u) (β' : Type v) :
mk (α ↪ β') ≤ mk (α → β')
source
theorem Cardinal.mk_perm_eq_self_power {α : Type u} [Infinite α] :
mk (Equiv.Perm α) = mk α ^ mk α
source
theorem Cardinal.mk_perm_eq_two_power {α : Type u} [Infinite α] :
mk (Equiv.Perm α) = 2 ^ mk α
source
theorem Cardinal.mk_equiv_eq_arrow_of_lift_eq {α : Type u} {β' : Type v} [Infinite α] (leq : lift.{v, u} (mk α) = lift.{u, v} (mk β')) :
mk (α ≃ β') = mk (α → β')
source
theorem Cardinal.mk_equiv_eq_arrow_of_eq {α β : Type u} [Infinite α] (eq : mk α = mk β) :
mk (α ≃ β) = mk (α → β)
source
theorem Cardinal.mk_equiv_of_lift_eq {α : Type u} {β' : Type v} [Infinite α] (leq : lift.{v, u} (mk α) = lift.{u, v} (mk β')) :
mk (α ≃ β') = 2 ^ lift.{v, u} (mk α)
source
theorem Cardinal.mk_equiv_of_eq {α β : Type u} [Infinite α] (eq : mk α = mk β) :
mk (α ≃ β) = 2 ^ mk α
source
theorem Cardinal.mk_embedding_eq_arrow_of_lift_le {α : Type u} {β' : Type v} [Infinite α] (lle : lift.{u, v} (mk β') ≤ lift.{v, u} (mk α)) :
mk (β' ↪ α) = mk (β' → α)
source
theorem Cardinal.mk_embedding_eq_arrow_of_le {α β : Type u} [Infinite α] (le : mk β ≤ mk α) :
mk (β ↪ α) = mk (β → α)
source
theorem Cardinal.mk_surjective_eq_arrow_of_lift_le {α : Type u} {β' : Type v} [Infinite α] (lle : lift.{u, v} (mk β') ≤ lift.{v, u} (mk α)) :
mk ↑{f : α → β' | Function.Surjective f} = mk (α → β')
source
theorem Cardinal.mk_surjective_eq_arrow_of_le {α β : Type u} [Infinite α] (le : mk β ≤ mk α) :
mk ↑{f : α → β | Function.Surjective f} = mk (α → β)
source
@[simp]
theorem Cardinal.mk_list_eq_mk (α : Type u) [Infinite α] :
mk (List α) = mk α
source
theorem Cardinal.mk_list_eq_aleph0 (α : Type u) [Countable α] [Nonempty α] :
mk (List α) = aleph0
source
theorem Cardinal.mk_list_eq_max_mk_aleph0 (α : Type u) [Nonempty α] :
mk (List α) = max (mk α) aleph0
source
theorem Cardinal.mk_list_le_max (α : Type u) :
mk (List α) ≤ max aleph0 (mk α)
source
@[simp]
theorem Cardinal.mk_finset_of_infinite (α : Type u) [Infinite α] :
mk (Finset α) = mk α
source
theorem Cardinal.mk_bounded_set_le_of_infinite (α : Type u) [Infinite α] (c : Cardinal.{u}) :
mk { t : Set α // mk ↑t ≤ c } ≤ mk α ^ c
source
theorem Cardinal.mk_bounded_set_le (α : Type u) (c : Cardinal.{u}) :
mk { t : Set α // mk ↑t ≤ c } ≤ max (mk α) aleph0 ^ c
source
theorem Cardinal.mk_bounded_subset_le {α : Type u} (s : Set α) (c : Cardinal.{u}) :
mk { t : Set α // t ⊆ s ∧ mk ↑t ≤ c } ≤ max (mk ↑s) aleph0 ^ c

### Properties of `compl` #

source
theorem Cardinal.mk_compl_of_infinite {α : Type u_1} [Infinite α] (s : Set α) (h2 : mk ↑s < mk α) :
mk ↑s ᶜ = mk α
source
theorem Cardinal.mk_compl_finset_of_infinite {α : Type u_1} [Infinite α] (s : Finset α) :
mk ↑(↑s)ᶜ = mk α
source
theorem Cardinal.mk_compl_eq_mk_compl_infinite {α : Type u_1} [Infinite α] {s t : Set α} (hs : mk ↑s < mk α) (ht : mk ↑t < mk α) :
mk ↑s ᶜ = mk ↑t ᶜ
source
theorem Cardinal.mk_compl_eq_mk_compl_finite_lift {α : Type u} {β : Type v} [Finite α] {s : Set α} {t : Set β} (h1 : lift.{max v w, u} (mk α) = lift.{max u w, v} (mk β)) (h2 : lift.{max v w, u} (mk ↑s) = lift.{max u w, v} (mk ↑t)) :
lift.{max v w, u} (mk ↑s ᶜ) = lift.{max u w, v} (mk ↑t ᶜ)
source
theorem Cardinal.mk_compl_eq_mk_compl_finite {α β : Type u} [Finite α] {s : Set α} {t : Set β} (h1 : mk α = mk β) (h : mk ↑s = mk ↑t) :
mk ↑s ᶜ = mk ↑t ᶜ
source
theorem Cardinal.mk_compl_eq_mk_compl_finite_same {α : Type u} [Finite α] {s t : Set α} (h : mk ↑s = mk ↑t) :
mk ↑s ᶜ = mk ↑t ᶜ

### Extending an injection to an equiv #

source
theorem Cardinal.extend_function {α : Type u_1} {β : Type u_2} {s : Set α} (f : ↑s ↪ β) (h : Nonempty (↑s ᶜ ≃ ↑(Set.range ⇑f)ᶜ)) :
∃ (g : α ≃ β), ∀ (x : ↑s), g ↑x = f x
source
theorem Cardinal.extend_function_finite {α : Type u} {β : Type v} [Finite α] {s : Set α} (f : ↑s ↪ β) (h : Nonempty (α ≃ β)) :
∃ (g : α ≃ β), ∀ (x : ↑s), g ↑x = f x
source
theorem Cardinal.extend_function_of_lt {α : Type u_1} {β : Type u_2} {s : Set α} (f : ↑s ↪ β) (hs : mk ↑s < mk α) (h : Nonempty (α ≃ β)) :
∃ (g : α ≃ β), ∀ (x : ↑s), g ↑x = f x