Cardinality of W-types

This file proves some theorems about the cardinality of W-types. The main result is cardinalMk_le_max_aleph0_of_finite which says that if for any a : α, β a is finite, then the cardinality of WType β is at most the maximum of the cardinality of α and ℵ₀. This can be used to prove theorems about the cardinality of algebraic constructions such as polynomials. There is a surjection from a WType to MvPolynomial for example, and this surjection can be used to put an upper bound on the cardinality of MvPolynomial.

Tags

W, W type, cardinal, first order

theorem WType.cardinalMk_eq_sum_lift {α : Type u} {β : α → Type v} : Cardinal.mk (WType β) = Cardinal.sum fun (a : α) => Cardinal.mk (WType β) ^ Cardinal.lift.{u, v} (Cardinal.mk (β a))

@[deprecated WType.cardinalMk_eq_sum_lift]

theorem WType.cardinal_mk_eq_sum' {α : Type u} {β : α → Type v} : Cardinal.mk (WType β) = Cardinal.sum fun (a : α) => Cardinal.mk (WType β) ^ Cardinal.lift.{u, v} (Cardinal.mk (β a))

Alias of WType.cardinalMk_eq_sum_lift.

theorem WType.cardinalMk_le_of_le' {α : Type u} {β : α → Type v} {κ : Cardinal.{max u v}} (hκ : (Cardinal.sum fun (a : α) => κ ^ Cardinal.lift.{u, v} (Cardinal.mk (β a))) ≤ κ) : Cardinal.mk (WType β) ≤ κ

#(WType β) is the least cardinal κ such that sum (fun a : α ↦ κ ^ #(β a)) ≤ κ

@[deprecated WType.cardinalMk_le_of_le']

theorem WType.cardinal_mk_le_of_le' {α : Type u} {β : α → Type v} {κ : Cardinal.{max u v}} (hκ : (Cardinal.sum fun (a : α) => κ ^ Cardinal.lift.{u, v} (Cardinal.mk (β a))) ≤ κ) : Cardinal.mk (WType β) ≤ κ

Alias of WType.cardinalMk_le_of_le'.

---

#(WType β) is the least cardinal κ such that sum (fun a : α ↦ κ ^ #(β a)) ≤ κ

theorem WType.cardinalMk_le_max_aleph0_of_finite' {α : Type u} {β : α → Type v} [∀ (a : α), Finite (β a)] : Cardinal.mk (WType β) ≤ Cardinal.lift.{v, u} (Cardinal.mk α) ⊔ Cardinal.aleph0

If, for any a : α, β a is finite, then the cardinality of WType β is at most the maximum of the cardinality of α and ℵ₀

@[deprecated WType.cardinalMk_le_max_aleph0_of_finite']

theorem WType.cardinal_mk_le_max_aleph0_of_finite' {α : Type u} {β : α → Type v} [∀ (a : α), Finite (β a)] : Cardinal.mk (WType β) ≤ Cardinal.lift.{v, u} (Cardinal.mk α) ⊔ Cardinal.aleph0

Alias of WType.cardinalMk_le_max_aleph0_of_finite'.

---

If, for any a : α, β a is finite, then the cardinality of WType β is at most the maximum of the cardinality of α and ℵ₀

theorem WType.cardinalMk_eq_sum {α : Type u} {β : α → Type u} : Cardinal.mk (WType β) = Cardinal.sum fun (a : α) => Cardinal.mk (WType β) ^ Cardinal.mk (β a)

@[deprecated WType.cardinalMk_eq_sum]

theorem WType.cardinal_mk_eq_sum {α : Type u} {β : α → Type u} : Cardinal.mk (WType β) = Cardinal.sum fun (a : α) => Cardinal.mk (WType β) ^ Cardinal.mk (β a)

Alias of WType.cardinalMk_eq_sum.

theorem WType.cardinalMk_le_of_le {α : Type u} {β : α → Type u} {κ : Cardinal.{u}} (hκ : (Cardinal.sum fun (a : α) => κ ^ Cardinal.mk (β a)) ≤ κ) : Cardinal.mk (WType β) ≤ κ

#(WType β) is the least cardinal κ such that sum (fun a : α ↦ κ ^ #(β a)) ≤ κ

@[deprecated WType.cardinalMk_le_of_le]

theorem WType.cardinal_mk_le_of_le {α : Type u} {β : α → Type u} {κ : Cardinal.{u}} (hκ : (Cardinal.sum fun (a : α) => κ ^ Cardinal.mk (β a)) ≤ κ) : Cardinal.mk (WType β) ≤ κ

Alias of WType.cardinalMk_le_of_le.

---

#(WType β) is the least cardinal κ such that sum (fun a : α ↦ κ ^ #(β a)) ≤ κ

theorem WType.cardinalMk_le_max_aleph0_of_finite {α : Type u} {β : α → Type u} [∀ (a : α), Finite (β a)] : Cardinal.mk (WType β) ≤ Cardinal.mk α ⊔ Cardinal.aleph0

If, for any a : α, β a is finite, then the cardinality of WType β is at most the maximum of the cardinality of α and ℵ₀

@[deprecated WType.cardinalMk_le_max_aleph0_of_finite]

theorem WType.cardinal_mk_le_max_aleph0_of_finite {α : Type u} {β : α → Type u} [∀ (a : α), Finite (β a)] : Cardinal.mk (WType β) ≤ Cardinal.mk α ⊔ Cardinal.aleph0

Alias of WType.cardinalMk_le_max_aleph0_of_finite.

---

If, for any a : α, β a is finite, then the cardinality of WType β is at most the maximum of the cardinality of α and ℵ₀