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

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.

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

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

@[simp]

theorem Cardinal.mul_mk_eq_max {α β : Type u} [Infinite α] [Infinite β] : mk α * mk β = mk α ⊔ mk β

@[simp]

theorem Cardinal.aleph_mul_aleph (o₁ o₂ : Ordinal.{u_1}) : aleph o₁ * aleph o₂ = aleph (o₁ ⊔ o₂)

@[simp]

theorem Cardinal.aleph0_mul_eq {a : Cardinal.{u_1}} (ha : aleph0 ≤ a) : aleph0 * a = a

@[simp]

theorem Cardinal.mul_aleph0_eq {a : Cardinal.{u_1}} (ha : aleph0 ≤ a) : a * aleph0 = a

theorem Cardinal.aleph0_mul_mk_eq {α : Type u_1} [Infinite α] : aleph0 * mk α = mk α

theorem Cardinal.mk_mul_aleph0_eq {α : Type u_1} [Infinite α] : mk α * aleph0 = mk α

@[simp]

theorem Cardinal.aleph0_mul_aleph (o : Ordinal.{u_1}) : aleph0 * aleph o = aleph o

@[simp]

theorem Cardinal.aleph_mul_aleph0 (o : Ordinal.{u_1}) : aleph o * aleph0 = aleph o

theorem Cardinal.mul_lt_of_lt {a b c : Cardinal.{u_1}} (hc : aleph0 ≤ c) (h1 : a < c) (h2 : b < c) : a * b < c

theorem Cardinal.mul_le_max_of_aleph0_le_left {a b : Cardinal.{u_1}} (h : aleph0 ≤ a) : a * b ≤ a ⊔ b

theorem Cardinal.mul_eq_max_of_aleph0_le_left {a b : Cardinal.{u_1}} (h : aleph0 ≤ a) (h' : b ≠ 0) : a * b = a ⊔ b

theorem Cardinal.mul_le_max_of_aleph0_le_right {a b : Cardinal.{u_1}} (h : aleph0 ≤ b) : a * b ≤ a ⊔ b

theorem Cardinal.mul_eq_max_of_aleph0_le_right {a b : Cardinal.{u_1}} (h' : a ≠ 0) (h : aleph0 ≤ b) : a * b = a ⊔ b

theorem Cardinal.mul_eq_max' {a b : Cardinal.{u_1}} (h : aleph0 ≤ a * b) : a * b = a ⊔ b

theorem Cardinal.mul_le_max (a b : Cardinal.{u_1}) : a * b ≤ a ⊔ b ⊔ aleph0

theorem Cardinal.mul_eq_left {a b : Cardinal.{u_1}} (ha : aleph0 ≤ a) (hb : b ≤ a) (hb' : b ≠ 0) : a * b = a

theorem Cardinal.mul_eq_right {a b : Cardinal.{u_1}} (hb : aleph0 ≤ b) (ha : a ≤ b) (ha' : a ≠ 0) : a * b = b

theorem Cardinal.le_mul_left {a b : Cardinal.{u_1}} (h : b ≠ 0) : a ≤ b * a

theorem Cardinal.le_mul_right {a b : Cardinal.{u_1}} (h : b ≠ 0) : a ≤ a * b

theorem Cardinal.mul_eq_left_iff {a b : Cardinal.{u_1}} : a * b = a ↔ aleph0 ⊔ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Properties of add

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.

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

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

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

@[simp]

theorem Cardinal.add_mk_eq_max {α β : Type u} [Infinite α] : mk α + mk β = mk α ⊔ mk β

@[simp]

theorem Cardinal.add_mk_eq_max' {α β : Type u} [Infinite β] : mk α + mk β = mk α ⊔ mk β

theorem Cardinal.add_mk_eq_self {α : Type u_1} [Infinite α] : mk α + mk α = mk α

theorem Cardinal.add_le_max (a b : Cardinal.{u_1}) : a + b ≤ a ⊔ b ⊔ aleph0

theorem Cardinal.add_le_of_le {a b c : Cardinal.{u_1}} (hc : aleph0 ≤ c) (h1 : a ≤ c) (h2 : b ≤ c) : a + b ≤ c

theorem Cardinal.add_lt_of_lt {a b c : Cardinal.{u_1}} (hc : aleph0 ≤ c) (h1 : a < c) (h2 : b < c) : a + b < c

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

theorem Cardinal.add_eq_left {a b : Cardinal.{u_1}} (ha : aleph0 ≤ a) (hb : b ≤ a) : a + b = a

theorem Cardinal.add_eq_right {a b : Cardinal.{u_1}} (hb : aleph0 ≤ b) (ha : a ≤ b) : a + b = b

theorem Cardinal.add_eq_left_iff {a b : Cardinal.{u_1}} : a + b = a ↔ aleph0 ⊔ b ≤ a ∨ b = 0

theorem Cardinal.add_eq_right_iff {a b : Cardinal.{u_1}} : a + b = b ↔ aleph0 ⊔ a ≤ b ∨ a = 0

theorem Cardinal.add_nat_eq {a : Cardinal.{u_1}} (n : ℕ) (ha : aleph0 ≤ a) : a + ↑n = a

theorem Cardinal.nat_add_eq {a : Cardinal.{u_1}} (n : ℕ) (ha : aleph0 ≤ a) : ↑n + a = a

theorem Cardinal.add_one_eq {a : Cardinal.{u_1}} (ha : aleph0 ≤ a) : a + 1 = a

theorem Cardinal.mk_add_one_eq {α : Type u_1} [Infinite α] : mk α + 1 = mk α

theorem Cardinal.eq_of_add_eq_add_left {a b c : Cardinal.{u_1}} (h : a + b = a + c) (ha : a < aleph0) : b = c

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

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

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

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

theorem Cardinal.ciSup_mul {ι : Type u} (f : ι → Cardinal.{v}) (c : Cardinal.{v}) : (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c

theorem Cardinal.mul_ciSup {ι : Type u} (f : ι → Cardinal.{v}) (c : Cardinal.{v}) : c * ⨆ (i : ι), f i = ⨆ (i : ι), c * f i

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

theorem Cardinal.sum_eq_iSup_lift {ι : Type u} {f : ι → Cardinal.{max u v}} (hι : aleph0 ≤ mk ι) (h : lift.{v, u} (mk ι) ≤ iSup f) : sum f = iSup f

theorem Cardinal.sum_eq_iSup {ι : Type u} {f : ι → Cardinal.{u}} (hι : aleph0 ≤ mk ι) (h : mk ι ≤ iSup f) : sum f = iSup f

Properties of aleph

@[simp]

theorem Cardinal.aleph_add_aleph (o₁ o₂ : Ordinal.{u_1}) : aleph o₁ + aleph o₂ = aleph (o₁ ⊔ o₂)

theorem Cardinal.add_right_inj_of_lt_aleph0 {α β γ : Cardinal.{u_1}} (γ₀ : γ < aleph0) : α + γ = β + γ ↔ α = β

@[simp]

theorem Cardinal.add_nat_inj {α β : Cardinal.{u_1}} (n : ℕ) : α + ↑n = β + ↑n ↔ α = β

@[simp]

theorem Cardinal.add_one_inj {α β : Cardinal.{u_1}} : α + 1 = β + 1 ↔ α = β

theorem Cardinal.add_le_add_iff_of_lt_aleph0 {α β γ : Cardinal.{u_1}} (γ₀ : γ < aleph0) : α + γ ≤ β + γ ↔ α ≤ β

@[simp]

theorem Cardinal.add_nat_le_add_nat_iff {α β : Cardinal.{u_1}} (n : ℕ) : α + ↑n ≤ β + ↑n ↔ α ≤ β

@[simp]

theorem Cardinal.add_one_le_add_one_iff {α β : Cardinal.{u_1}} : α + 1 ≤ β + 1 ↔ α ≤ β

Properties about power

theorem Cardinal.pow_le {κ μ : Cardinal.{u}} (H1 : aleph0 ≤ κ) (H2 : μ < aleph0) : κ ^ μ ≤ κ

theorem Cardinal.pow_eq {κ μ : Cardinal.{u}} (H1 : aleph0 ≤ κ) (H2 : 1 ≤ μ) (H3 : μ < aleph0) : κ ^ μ = κ

theorem Cardinal.power_self_eq {c : Cardinal.{u_1}} (h : aleph0 ≤ c) : c ^ c = 2 ^ c

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 ι)

theorem Cardinal.power_eq_two_power {c₁ c₂ : Cardinal.{u_1}} (h₁ : aleph0 ≤ c₁) (h₂ : 2 ≤ c₂) (h₂' : c₂ ≤ c₁) : c₂ ^ c₁ = 2 ^ c₁

theorem Cardinal.nat_power_eq {c : Cardinal.{u}} (h : aleph0 ≤ c) {n : ℕ} (hn : 2 ≤ n) : ↑n ^ c = 2 ^ c

theorem Cardinal.power_nat_le {c : Cardinal.{u}} {n : ℕ} (h : aleph0 ≤ c) : c ^ n ≤ c

theorem Cardinal.power_nat_eq {c : Cardinal.{u}} {n : ℕ} (h1 : aleph0 ≤ c) (h2 : 1 ≤ n) : c ^ n = c

theorem Cardinal.power_nat_le_max {c : Cardinal.{u}} {n : ℕ} : c ^ ↑n ≤ c ⊔ aleph0

theorem Cardinal.power_le_aleph0 {a b : Cardinal.{u}} (ha : a ≤ aleph0) (hb : b < aleph0) : a ^ b ≤ aleph0

theorem Cardinal.powerlt_aleph0 {c : Cardinal.{u_1}} (h : aleph0 ≤ c) : c ^< aleph0 = c

theorem Cardinal.powerlt_aleph0_le (c : Cardinal.{u_1}) : c ^< aleph0 ≤ c ⊔ aleph0

Computing cardinality of various types

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

theorem Cardinal.mk_equiv_eq_zero_iff_ne {α β : Type u} : mk (α ≃ β) = 0 ↔ mk α ≠ mk β

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.

theorem Cardinal.mk_embedding_eq_zero_iff_lift_lt {α : Type u} {β' : Type v} : mk (α ↪ β') = 0 ↔ lift.{u, v} (mk β') < lift.{v, u} (mk α)

theorem Cardinal.mk_embedding_eq_zero_iff_lt {α β : Type u} : mk (α ↪ β) = 0 ↔ mk β < mk α

theorem Cardinal.mk_arrow_eq_zero_iff {α : Type u} {β' : Type v} : mk (α → β') = 0 ↔ mk α ≠ 0 ∧ mk β' = 0

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

theorem Cardinal.mk_surjective_eq_zero_iff {α β : Type u} : mk ↑{f : α → β | Function.Surjective f} = 0 ↔ mk α < mk β ∨ mk α ≠ 0 ∧ mk β = 0

theorem Cardinal.mk_equiv_le_embedding (α : Type u) (β' : Type v) : mk (α ≃ β') ≤ mk (α ↪ β')

theorem Cardinal.mk_embedding_le_arrow (α : Type u) (β' : Type v) : mk (α ↪ β') ≤ mk (α → β')

theorem Cardinal.mk_perm_eq_self_power {α : Type u} [Infinite α] : mk (Equiv.Perm α) = mk α ^ mk α

theorem Cardinal.mk_perm_eq_two_power {α : Type u} [Infinite α] : mk (Equiv.Perm α) = 2 ^ mk α

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 (α → β')

theorem Cardinal.mk_equiv_eq_arrow_of_eq {α β : Type u} [Infinite α] (eq : mk α = mk β) : mk (α ≃ β) = mk (α → β)

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 α)

theorem Cardinal.mk_equiv_of_eq {α β : Type u} [Infinite α] (eq : mk α = mk β) : mk (α ≃ β) = 2 ^ mk α

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 (β' → α)

theorem Cardinal.mk_embedding_eq_arrow_of_le {α β : Type u} [Infinite α] (le : mk β ≤ mk α) : mk (β ↪ α) = mk (β → α)

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 (α → β')

theorem Cardinal.mk_surjective_eq_arrow_of_le {α β : Type u} [Infinite α] (le : mk β ≤ mk α) : mk ↑{f : α → β | Function.Surjective f} = mk (α → β)

@[simp]

theorem Cardinal.mk_list_eq_mk (α : Type u) [Infinite α] : mk (List α) = mk α

theorem Cardinal.mk_list_eq_aleph0 (α : Type u) [Countable α] [Nonempty α] : mk (List α) = aleph0

theorem Cardinal.mk_list_eq_max_mk_aleph0 (α : Type u) [Nonempty α] : mk (List α) = mk α ⊔ aleph0

theorem Cardinal.mk_list_le_max (α : Type u) : mk (List α) ≤ aleph0 ⊔ mk α

@[simp]

theorem Cardinal.mk_finset_of_infinite (α : Type u) [Infinite α] : mk (Finset α) = mk α

theorem Cardinal.mk_bounded_set_le_of_infinite (α : Type u) [Infinite α] (c : Cardinal.{u}) : mk { t : Set α // mk ↑t ≤ c } ≤ mk α ^ c

theorem Cardinal.mk_bounded_set_le (α : Type u) (c : Cardinal.{u}) : mk { t : Set α // mk ↑t ≤ c } ≤ (mk α ⊔ aleph0) ^ c

theorem Cardinal.mk_bounded_subset_le {α : Type u} (s : Set α) (c : Cardinal.{u}) : mk { t : Set α // t ⊆ s ∧ mk ↑t ≤ c } ≤ (mk ↑s ⊔ aleph0) ^ c

Properties of compl

theorem Cardinal.mk_compl_of_infinite {α : Type u_1} [Infinite α] (s : Set α) (h2 : mk ↑s < mk α) : mk ↑sᶜ = mk α

theorem Cardinal.mk_compl_finset_of_infinite {α : Type u_1} [Infinite α] (s : Finset α) : mk ↑(↑s)ᶜ = mk α

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ᶜ

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ᶜ)

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ᶜ

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

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

theorem Cardinal.extend_function_finite {α : Type u} {β : Type v} [Finite α] {s : Set α} (f : ↑s ↪ β) (h : Nonempty (α ≃ β)) : ∃ (g : α ≃ β), ∀ (x : ↑s), g ↑x = f x

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