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))
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))) ≤ κ)
:
#(WType β) is the least cardinal κ such that sum (fun a : α ↦ κ ^ #(β a)) ≤ κ
theorem
WType.cardinalMk_le_of_le
{α : Type u}
{β : α → Type u}
{κ : Cardinal.{u}}
(hκ : (Cardinal.sum fun (a : α) => κ ^ Cardinal.mk (β a)) ≤ κ)
:
#(WType β) is the least cardinal κ such that sum (fun a : α ↦ κ ^ #(β a)) ≤ κ