Cardinals and ordinals

Relationships between cardinals and ordinals, properties of cardinals that are proved using ordinals.

Main definitions

• The function Cardinal.aleph' gives the cardinals listed by their ordinal index, and is the inverse of Cardinal.aleph/idx. aleph' n = n, aleph' ω = ℵ₀, aleph' (ω + 1) = succ ℵ₀, etc. It is an order isomorphism between ordinals and cardinals.
• 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 notation ω_ combines the latter with Cardinal.ord, giving an enumeration of (infinite) initial ordinals. Thus ω_ 0 = ω and ω₁ = ω_ 1 is the first uncountable ordinal.
• 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

• 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.
• simp lemmas for inequalities between bit0 a and bit1 b are registered, making simp able to prove inequalities about numeral cardinals.

Tags

cardinal arithmetic (for infinite cardinals)

theorem Cardinal.ord_isLimit {c : Cardinal.{u_1}} (co : Cardinal.aleph0 ≤ c) : Ordinal.IsLimit (Cardinal.ord c)

Aleph cardinals

def Cardinal.alephIdx.initialSeg : (fun (x x_1 : Cardinal.{u_1}) => x < x_1) ≼i fun (x x_1 : Ordinal.{u_1}) => x < x_1

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 alephIdx n = n, alephIdx ω = ω, alephIdx ℵ₁ = ω + 1 and so on.) In this definition, we register additionally that this function is an initial segment, i.e., it is order preserving and its range is an initial segment of the ordinals. For the basic function version, see alephIdx. For an upgraded version stating that the range is everything, see AlephIdx.rel_iso.

Equations

• Cardinal.alephIdx.initialSeg = RelEmbedding.collapse (OrderEmbedding.ltEmbedding Cardinal.ord.orderEmbedding)

def Cardinal.alephIdx : Cardinal.{u_1} → Ordinal.{u_1}

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 alephIdx n = n, alephIdx ω = ω, alephIdx ℵ₁ = ω + 1 and so on.) For an upgraded version stating that the range is everything, see AlephIdx.rel_iso.

Equations

• Cardinal.alephIdx = ⇑Cardinal.alephIdx.initialSeg

@[simp]

theorem Cardinal.alephIdx.initialSeg_coe : ⇑Cardinal.alephIdx.initialSeg = Cardinal.alephIdx

@[simp]

theorem Cardinal.alephIdx_lt {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} : Cardinal.alephIdx a < Cardinal.alephIdx b ↔ a < b

@[simp]

theorem Cardinal.alephIdx_le {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} : Cardinal.alephIdx a ≤ Cardinal.alephIdx b ↔ a ≤ b

theorem Cardinal.alephIdx.init {a : Cardinal.{u_1}} {b : Ordinal.{u_1}} : b < Cardinal.alephIdx a → ∃ (c : Cardinal.{u_1}), Cardinal.alephIdx c = b

def Cardinal.alephIdx.relIso : (fun (x x_1 : Cardinal.{u}) => x < x_1) ≃r fun (x x_1 : Ordinal.{u}) => x < x_1

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 alephIdx n = n, alephIdx ℵ₀ = ω, alephIdx ℵ₁ = ω + 1 and so on.) In this version, we register additionally that this function is an order isomorphism between cardinals and ordinals. For the basic function version, see alephIdx.

Equations

• Cardinal.alephIdx.relIso = RelIso.ofSurjective Cardinal.alephIdx.initialSeg.toRelEmbedding Cardinal.alephIdx.relIso.proof_1

@[simp]

theorem Cardinal.alephIdx.relIso_coe : ⇑Cardinal.alephIdx.relIso = Cardinal.alephIdx

@[simp]

theorem Cardinal.type_cardinal : (Ordinal.type fun (x x_1 : Cardinal.{u}) => x < x_1) = Ordinal.univ.{u, u + 1}

@[simp]

theorem Cardinal.mk_cardinal : Cardinal.mk Cardinal.{u} = Cardinal.univ.{u, u + 1}

def Cardinal.Aleph'.relIso : (fun (x x_1 : Ordinal.{u_1}) => x < x_1) ≃r fun (x x_1 : Cardinal.{u_1}) => x < x_1

The aleph' function gives the cardinals listed by their ordinal index, and is the inverse of aleph_idx. aleph' n = n, aleph' ω = ω, aleph' (ω + 1) = succ ℵ₀, etc. In this version, we register additionally that this function is an order isomorphism between ordinals and cardinals. For the basic function version, see aleph'.

Equations

• Cardinal.Aleph'.relIso = RelIso.symm Cardinal.alephIdx.relIso

def Cardinal.aleph' : Ordinal.{u_1} → Cardinal.{u_1}

The aleph' function gives the cardinals listed by their ordinal index, and is the inverse of aleph_idx. aleph' n = n, aleph' ω = ω, aleph' (ω + 1) = succ ℵ₀, etc.

Equations

• Cardinal.aleph' = ⇑Cardinal.Aleph'.relIso

@[simp]

theorem Cardinal.aleph'.relIso_coe : ⇑Cardinal.Aleph'.relIso = Cardinal.aleph'

@[simp]

theorem Cardinal.aleph'_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} : Cardinal.aleph' o₁ < Cardinal.aleph' o₂ ↔ o₁ < o₂

@[simp]

theorem Cardinal.aleph'_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} : Cardinal.aleph' o₁ ≤ Cardinal.aleph' o₂ ↔ o₁ ≤ o₂

@[simp]

theorem Cardinal.aleph'_alephIdx (c : Cardinal.{u_1}) : Cardinal.aleph' (Cardinal.alephIdx c) = c

@[simp]

theorem Cardinal.alephIdx_aleph' (o : Ordinal.{u_1}) : Cardinal.alephIdx (Cardinal.aleph' o) = o

@[simp]

theorem Cardinal.aleph'_zero : Cardinal.aleph' 0 = 0

@[simp]

theorem Cardinal.aleph'_succ {o : Ordinal.{u_1}} : Cardinal.aleph' (Order.succ o) = Order.succ (Cardinal.aleph' o)

@[simp]

theorem Cardinal.aleph'_nat (n : ℕ) : Cardinal.aleph' ↑n = ↑n

theorem Cardinal.aleph'_le_of_limit {o : Ordinal.{u_1}} (l : Ordinal.IsLimit o) {c : Cardinal.{u_1}} : Cardinal.aleph' o ≤ c ↔ ∀ o' < o, Cardinal.aleph' o' ≤ c

theorem Cardinal.aleph'_limit {o : Ordinal.{u_1}} (ho : Ordinal.IsLimit o) : Cardinal.aleph' o = ⨆ (a : ↑(Set.Iio o)), Cardinal.aleph' ↑a

@[simp]

theorem Cardinal.aleph'_omega : Cardinal.aleph' Ordinal.omega = Cardinal.aleph0

def Cardinal.aleph'Equiv : Ordinal.{u_1} ≃ Cardinal.{u_1}

aleph' and aleph_idx form an equivalence between Ordinal and Cardinal

Equations

• Cardinal.aleph'Equiv = { toFun := Cardinal.aleph', invFun := Cardinal.alephIdx, left_inv := Cardinal.alephIdx_aleph', right_inv := Cardinal.aleph'_alephIdx }

def Cardinal.aleph (o : Ordinal.{u_1}) : Cardinal.{u_1}

The aleph function gives the infinite cardinals listed by their ordinal index. aleph 0 = ℵ₀, aleph 1 = succ ℵ₀ is the first uncountable cardinal, and so on.

Equations

• Cardinal.aleph o = Cardinal.aleph' (Ordinal.omega + o)

@[simp]

theorem Cardinal.aleph_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} : Cardinal.aleph o₁ < Cardinal.aleph o₂ ↔ o₁ < o₂

@[simp]

theorem Cardinal.aleph_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} : Cardinal.aleph o₁ ≤ Cardinal.aleph o₂ ↔ o₁ ≤ o₂

@[simp]

theorem Cardinal.max_aleph_eq (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) : max (Cardinal.aleph o₁) (Cardinal.aleph o₂) = Cardinal.aleph (max o₁ o₂)

@[simp]

theorem Cardinal.aleph_succ {o : Ordinal.{u_1}} : Cardinal.aleph (Order.succ o) = Order.succ (Cardinal.aleph o)

@[simp]

theorem Cardinal.aleph_zero : Cardinal.aleph 0 = Cardinal.aleph0

theorem Cardinal.aleph_limit {o : Ordinal.{u_1}} (ho : Ordinal.IsLimit o) : Cardinal.aleph o = ⨆ (a : ↑(Set.Iio o)), Cardinal.aleph ↑a

theorem Cardinal.aleph0_le_aleph' {o : Ordinal.{u_1}} : Cardinal.aleph0 ≤ Cardinal.aleph' o ↔ Ordinal.omega ≤ o

theorem Cardinal.aleph0_le_aleph (o : Ordinal.{u_1}) : Cardinal.aleph0 ≤ Cardinal.aleph o

theorem Cardinal.aleph'_pos {o : Ordinal.{u_1}} (ho : 0 < o) : 0 < Cardinal.aleph' o

theorem Cardinal.aleph_pos (o : Ordinal.{u_1}) : 0 < Cardinal.aleph o

@[simp]

theorem Cardinal.aleph_toNat (o : Ordinal.{u_1}) : Cardinal.toNat (Cardinal.aleph o) = 0

@[simp]

theorem Cardinal.aleph_toPartENat (o : Ordinal.{u_1}) : Cardinal.toPartENat (Cardinal.aleph o) = ⊤

instance Cardinal.nonempty_out_aleph (o : Ordinal.{u_1}) : Nonempty (Quotient.out (Cardinal.ord (Cardinal.aleph o))).α

Equations

• (_ : Nonempty (Quotient.out (Cardinal.ord (Cardinal.aleph o))).α) = (_ : Nonempty (Quotient.out (Cardinal.ord (Cardinal.aleph o))).α)

theorem Cardinal.ord_aleph_isLimit (o : Ordinal.{u_1}) : Ordinal.IsLimit (Cardinal.ord (Cardinal.aleph o))

instance Cardinal.instNoMaxOrderαOutWellOrderIsEquivalentOrdAlephToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeLinearOrderOut (o : Ordinal.{u_1}) : NoMaxOrder (Quotient.out (Cardinal.ord (Cardinal.aleph o))).α

Equations

• (_ : NoMaxOrder (Quotient.out (Cardinal.ord (Cardinal.aleph o))).α) = (_ : NoMaxOrder (Quotient.out (Cardinal.ord (Cardinal.aleph o))).α)

theorem Cardinal.exists_aleph {c : Cardinal.{u_1}} : Cardinal.aleph0 ≤ c ↔ ∃ (o : Ordinal.{u_1}), c = Cardinal.aleph o

theorem Cardinal.aleph'_isNormal : Ordinal.IsNormal (Cardinal.ord ∘ Cardinal.aleph')

theorem Cardinal.aleph_isNormal : Ordinal.IsNormal (Cardinal.ord ∘ Cardinal.aleph)

theorem Cardinal.succ_aleph0 : Order.succ Cardinal.aleph0 = Cardinal.aleph 1

theorem Cardinal.aleph0_lt_aleph_one : Cardinal.aleph0 < Cardinal.aleph 1

theorem Cardinal.countable_iff_lt_aleph_one {α : Type u_1} (s : Set α) : Set.Countable s ↔ Cardinal.mk ↑s < Cardinal.aleph 1

theorem Cardinal.ord_card_unbounded : Set.Unbounded (fun (x x_1 : Ordinal.{u_1}) => x < x_1) {b : Ordinal.{u_1} | Cardinal.ord (Ordinal.card b) = b}

Ordinals that are cardinals are unbounded.

theorem Cardinal.eq_aleph'_of_eq_card_ord {o : Ordinal.{u_1}} (ho : Cardinal.ord (Ordinal.card o) = o) : ∃ (a : Ordinal.{u_1}), Cardinal.ord (Cardinal.aleph' a) = o

theorem Cardinal.ord_aleph'_eq_enum_card : Cardinal.ord ∘ Cardinal.aleph' = Ordinal.enumOrd {b : Ordinal.{u_1} | Cardinal.ord (Ordinal.card b) = b}

ord ∘ aleph' enumerates the ordinals that are cardinals.

theorem Cardinal.ord_card_unbounded' : Set.Unbounded (fun (x x_1 : Ordinal.{u_1}) => x < x_1) {b : Ordinal.{u_1} | Cardinal.ord (Ordinal.card b) = b ∧ Ordinal.omega ≤ b}

Infinite ordinals that are cardinals are unbounded.

theorem Cardinal.eq_aleph_of_eq_card_ord {o : Ordinal.{u_1}} (ho : Cardinal.ord (Ordinal.card o) = o) (ho' : Ordinal.omega ≤ o) : ∃ (a : Ordinal.{u_1}), Cardinal.ord (Cardinal.aleph a) = o

theorem Cardinal.ord_aleph_eq_enum_card : Cardinal.ord ∘ Cardinal.aleph = Ordinal.enumOrd {b : Ordinal.{u_1} | Cardinal.ord (Ordinal.card b) = b ∧ Ordinal.omega ≤ b}

ord ∘ aleph enumerates the infinite ordinals that are cardinals.

Beth cardinals

def Cardinal.beth (o : Ordinal.{u}) : Cardinal.{u}

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Cardinal.beth_zero : Cardinal.beth 0 = Cardinal.aleph0

@[simp]

theorem Cardinal.beth_succ (o : Ordinal.{u_1}) : Cardinal.beth (Order.succ o) = 2 ^ Cardinal.beth o

theorem Cardinal.beth_limit {o : Ordinal.{u_1}} : Ordinal.IsLimit o → Cardinal.beth o = ⨆ (a : ↑(Set.Iio o)), Cardinal.beth ↑a

theorem Cardinal.beth_strictMono : StrictMono Cardinal.beth

theorem Cardinal.beth_mono : Monotone Cardinal.beth

@[simp]

theorem Cardinal.beth_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} : Cardinal.beth o₁ < Cardinal.beth o₂ ↔ o₁ < o₂

@[simp]

theorem Cardinal.beth_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} : Cardinal.beth o₁ ≤ Cardinal.beth o₂ ↔ o₁ ≤ o₂

theorem Cardinal.aleph_le_beth (o : Ordinal.{u_1}) : Cardinal.aleph o ≤ Cardinal.beth o

theorem Cardinal.aleph0_le_beth (o : Ordinal.{u_1}) : Cardinal.aleph0 ≤ Cardinal.beth o

theorem Cardinal.beth_pos (o : Ordinal.{u_1}) : 0 < Cardinal.beth o

theorem Cardinal.beth_ne_zero (o : Ordinal.{u_1}) : Cardinal.beth o ≠ 0

theorem Cardinal.beth_normal : Ordinal.IsNormal fun (o : Ordinal.{u}) => Cardinal.ord (Cardinal.beth o)

Properties of mul

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

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

theorem Cardinal.mul_eq_max {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : Cardinal.aleph0 ≤ a) (hb : Cardinal.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} {β : Type u} [Infinite α] [Infinite β] : Cardinal.mk α * Cardinal.mk β = max (Cardinal.mk α) (Cardinal.mk β)

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

Properties of add

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

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

theorem Cardinal.add_eq_max {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : Cardinal.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 : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : Cardinal.aleph0 ≤ b) : a + b = max a b

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

theorem Cardinal.principal_add_ord {c : Cardinal.{u_1}} (hc : Cardinal.aleph0 ≤ c) : Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) (Cardinal.ord c)

theorem Cardinal.principal_add_aleph (o : Ordinal.{u_1}) : Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) (Cardinal.ord (Cardinal.aleph o))

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

Properties about power

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

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

theorem Cardinal.power_self_eq {c : Cardinal.{u_1}} (h : Cardinal.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 : ι), Cardinal.lift.{u, v} (c i) ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)) : Cardinal.prod c = 2 ^ Cardinal.lift.{v, u} (Cardinal.mk ι)

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

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

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

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

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

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

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

Computing cardinality of various types

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

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

theorem Cardinal.mk_equiv_comm {α : Type u} {β' : Type v} : Cardinal.mk (α ≃ β') = Cardinal.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} : Cardinal.mk (α ↪ β') = 0 ↔ Cardinal.lift.{u, v} (Cardinal.mk β') < Cardinal.lift.{v, u} (Cardinal.mk α)

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

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

theorem Cardinal.mk_surjective_eq_zero_iff_lift {α : Type u} {β' : Type v} : Cardinal.mk ↑{f : α → β' | Function.Surjective f} = 0 ↔ Cardinal.lift.{v, u} (Cardinal.mk α) < Cardinal.lift.{u, v} (Cardinal.mk β') ∨ Cardinal.mk α ≠ 0 ∧ Cardinal.mk β' = 0

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

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

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

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

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

theorem Cardinal.mk_equiv_eq_arrow_of_lift_eq {α : Type u} {β' : Type v} [Infinite α] (leq : Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β')) : Cardinal.mk (α ≃ β') = Cardinal.mk (α → β')

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

theorem Cardinal.mk_equiv_of_lift_eq {α : Type u} {β' : Type v} [Infinite α] (leq : Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β')) : Cardinal.mk (α ≃ β') = 2 ^ Cardinal.lift.{v, u} (Cardinal.mk α)

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

theorem Cardinal.mk_embedding_eq_arrow_of_lift_le {α : Type u} {β' : Type v} [Infinite α] (lle : Cardinal.lift.{u, v} (Cardinal.mk β') ≤ Cardinal.lift.{v, u} (Cardinal.mk α)) : Cardinal.mk (β' ↪ α) = Cardinal.mk (β' → α)

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

theorem Cardinal.mk_surjective_eq_arrow_of_lift_le {α : Type u} {β' : Type v} [Infinite α] (lle : Cardinal.lift.{u, v} (Cardinal.mk β') ≤ Cardinal.lift.{v, u} (Cardinal.mk α)) : Cardinal.mk ↑{f : α → β' | Function.Surjective f} = Cardinal.mk (α → β')

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

theorem Cardinal.mk_finsupp_lift_of_infinite (α : Type u) (β : Type v) [Infinite α] [Zero β] [Nontrivial β] : Cardinal.mk (α →₀ β) = max (Cardinal.lift.{v, u} (Cardinal.mk α)) (Cardinal.lift.{u, v} (Cardinal.mk β))

theorem Cardinal.mk_finsupp_of_infinite (α : Type u) (β : Type u) [Infinite α] [Zero β] [Nontrivial β] : Cardinal.mk (α →₀ β) = max (Cardinal.mk α) (Cardinal.mk β)

@[simp]

theorem Cardinal.mk_finsupp_lift_of_infinite' (α : Type u) (β : Type v) [Nonempty α] [Zero β] [Infinite β] : Cardinal.mk (α →₀ β) = max (Cardinal.lift.{v, u} (Cardinal.mk α)) (Cardinal.lift.{u, v} (Cardinal.mk β))

theorem Cardinal.mk_finsupp_of_infinite' (α : Type u) (β : Type u) [Nonempty α] [Zero β] [Infinite β] : Cardinal.mk (α →₀ β) = max (Cardinal.mk α) (Cardinal.mk β)

theorem Cardinal.mk_finsupp_nat (α : Type u) [Nonempty α] : Cardinal.mk (α →₀ ℕ) = max (Cardinal.mk α) Cardinal.aleph0

@[simp]

theorem Cardinal.mk_multiset_of_nonempty (α : Type u) [Nonempty α] : Cardinal.mk (Multiset α) = max (Cardinal.mk α) Cardinal.aleph0

theorem Cardinal.mk_multiset_of_infinite (α : Type u) [Infinite α] : Cardinal.mk (Multiset α) = Cardinal.mk α

theorem Cardinal.mk_multiset_of_isEmpty (α : Type u) [IsEmpty α] : Cardinal.mk (Multiset α) = 1

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

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

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

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

Properties of compl

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

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

theorem Cardinal.mk_compl_eq_mk_compl_infinite {α : Type u_1} [Infinite α] {s : Set α} {t : Set α} (hs : Cardinal.mk ↑s < Cardinal.mk α) (ht : Cardinal.mk ↑t < Cardinal.mk α) : Cardinal.mk ↑sᶜ = Cardinal.mk ↑tᶜ

theorem Cardinal.mk_compl_eq_mk_compl_finite_lift {α : Type u} {β : Type v} [Finite α] {s : Set α} {t : Set β} (h1 : Cardinal.lift.{max v w, u} (Cardinal.mk α) = Cardinal.lift.{max u w, v} (Cardinal.mk β)) (h2 : Cardinal.lift.{max v w, u} (Cardinal.mk ↑s) = Cardinal.lift.{max u w, v} (Cardinal.mk ↑t)) : Cardinal.lift.{max v w, u} (Cardinal.mk ↑sᶜ) = Cardinal.lift.{max u w, v} (Cardinal.mk ↑tᶜ)

theorem Cardinal.mk_compl_eq_mk_compl_finite {α : Type u} {β : Type u} [Finite α] {s : Set α} {t : Set β} (h1 : Cardinal.mk α = Cardinal.mk β) (h : Cardinal.mk ↑s = Cardinal.mk ↑t) : Cardinal.mk ↑sᶜ = Cardinal.mk ↑tᶜ

theorem Cardinal.mk_compl_eq_mk_compl_finite_same {α : Type u} [Finite α] {s : Set α} {t : Set α} (h : Cardinal.mk ↑s = Cardinal.mk ↑t) : Cardinal.mk ↑sᶜ = Cardinal.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 : Cardinal.mk ↑s < Cardinal.mk α) (h : Nonempty (α ≃ β)) : ∃ (g : α ≃ β), ∀ (x : ↑s), g ↑x = f x

def Ordinal.termω__ : Lean.ParserDescr

ω_ o is a notation for the initial ordinal of cardinality aleph o. Thus, for example ω_ 0 = ω.

Equations

• Ordinal.termω__ = Lean.ParserDescr.node `Ordinal.termω__ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ω_") (Lean.ParserDescr.cat `term 0))

def Ordinal.termω₁ : Lean.ParserDescr

ω₁ is the first uncountable ordinal.

Equations

• Ordinal.termω₁ = Lean.ParserDescr.node `Ordinal.termω₁ 1024 (Lean.ParserDescr.symbol "ω₁")

theorem Ordinal.omega_lt_omega1 : Ordinal.omega < Cardinal.ord (Cardinal.aleph 1)

Cardinal operations with ordinal indices

Results on cardinality of ordinal-indexed families of sets.

theorem Ordinal.Cardinal.mk_iUnion_Ordinal_le_of_le {β : Type u_1} {o : Ordinal.{u_1}} {c : Cardinal.{u_1}} (ho : Ordinal.card o ≤ c) (hc : Cardinal.aleph0 ≤ c) (A : Ordinal.{u_1} → Set β) (hA : ∀ j < o, Cardinal.mk ↑(A j) ≤ c) : Cardinal.mk ↑(⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < o), A j) ≤ c

Bounding the cardinal of an ordinal-indexed union of sets.