Documentation

Mathlib.SetTheory.Cardinal.Arithmetic

Cardinal arithmetic #

Arithmetic operations on cardinals are defined in Mathlib/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}} (hc : 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 = max 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 β = max (mk α) (mk β)

@[simp]

theorem Cardinal.aleph_mul_aleph (o₁ o₂ : Ordinal.{u_1}) :

aleph o₁ * aleph o₂ = aleph (max 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 ≤ max a b

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

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

a * b ≤ max a b

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

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

a * b = max a b

theorem Cardinal.mul_le_max (a b : Cardinal.{u_1}) :

a * b ≤ max (max 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 ↔ max 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 = max 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 = max a b

@[simp]

theorem Cardinal.add_mk_eq_max {α β : Type u} [Infinite α] :

mk α + mk β = max (mk α) (mk β)

@[simp]

theorem Cardinal.add_mk_eq_max' {α β : Type u} [Infinite β] :

mk α + mk β = max (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 ≤ max (max 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 ↔ max aleph0 b ≤ a ∨ b = 0

theorem Cardinal.add_eq_right_iff {a b : Cardinal.{u_1}} :

a + b = b ↔ max 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_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)

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

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

Properties of `aleph` #

@[simp]

theorem Cardinal.aleph_add_aleph (o₁ o₂ : Ordinal.{u_1}) :

aleph o₁ + aleph o₂ = aleph (max 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 ↔ α ≤ β

theorem Cardinal.add_lt_add_iff_of_right_lt_aleph0 {a b c : Cardinal.{u_1}} (hc : c < aleph0) :

a + c < b + c ↔ a < b

theorem Cardinal.add_lt_add_iff_of_left_lt_aleph0 {a b c : Cardinal.{u_1}} (hc : c < aleph0) :

c + a < c + b ↔ a < b

theorem Cardinal.add_lt_add {κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}} (hκ : κ₁ < κ₂) (hμ : μ₁ < μ₂) :

κ₁ + μ₁ < κ₂ + μ₂

theorem Cardinal.natCast_mul_strictMono {n : ℕ} (hn : n ≠ 0) :

StrictMono fun (a : Cardinal.{u_1}) => ↑n * a

theorem Cardinal.mul_natCast_strictMono {n : ℕ} (hn : n ≠ 0) :

StrictMono fun (a : Cardinal.{u_1}) => a * ↑n

@[simp]

theorem Cardinal.natCast_mul_inj {n : ℕ} {a b : Cardinal.{u_1}} (hn : n ≠ 0) :

↑n * a = ↑n * b ↔ a = b

@[simp]

theorem Cardinal.mul_natCast_inj {n : ℕ} {a b : Cardinal.{u_1}} (hn : n ≠ 0) :

a * ↑n = b * ↑n ↔ a = b

@[simp]

theorem Cardinal.natCast_mul_le_natCast_mul {n : ℕ} {a b : Cardinal.{u_1}} (hn : n ≠ 0) :

↑n * a ≤ ↑n * b ↔ a ≤ b

@[simp]

theorem Cardinal.mul_natCast_le_mul_natCast {n : ℕ} {a b : Cardinal.{u_1}} (hn : n ≠ 0) :

a * ↑n ≤ b * ↑n ↔ a ≤ b

@[simp]

theorem Cardinal.natCast_mul_lt_natCast_mul {n : ℕ} {a b : Cardinal.{u_1}} (hn : n ≠ 0) :

↑n * a < ↑n * b ↔ a < b

@[simp]

theorem Cardinal.mul_natCast_lt_mul_natCast {n : ℕ} {a b : Cardinal.{u_1}} (hn : n ≠ 0) :

a * ↑n < b * ↑n ↔ a < b

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 ≤ max 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 ≤ max 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 (α : Type u) [Nonempty α] :

mk (List α) = max aleph0 (mk α)

theorem Cardinal.mk_list_eq_max_mk_aleph0 (α : Type u) [Nonempty α] :

mk (List α) = max (mk α) aleph0

theorem Cardinal.sum_pow_eq_max_aleph0 {x : Cardinal.{u_1}} (h : x ≠ 0) :

(sum fun (n : ℕ) => x ^ n) = max aleph0 x

theorem Cardinal.mk_list_le_max (α : Type u) :

mk (List α) ≤ max aleph0 (mk α)

theorem Cardinal.sum_pow_le_max_aleph0 (x : Cardinal.{u_1}) :

(sum fun (n : ℕ) => x ^ n) ≤ max aleph0 x

@[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 } ≤ max (mk α) aleph0 ^ c

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` #

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.{v, u} (mk α) = lift.{u, v} (mk β)) (h2 : lift.{v, u} (mk ↑s) = lift.{u, v} (mk ↑t)) :

lift.{v, u} (mk ↑sᶜ) = lift.{u, 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