Cardinality of W-types #
This file proves some theorems about the cardinality of W-types. The main result is
cardinal_mk_le_max_aleph_0_of_fintype which says that if for any a : α,
β a is finite, then the cardinality of W_type β 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 W_type to mv_polynomial for example, and
this surjection can be used to put an upper bound on the cardinality of mv_polynomial.
Tags #
W, W type, cardinal, first order
theorem
W_type.cardinal_mk_eq_sum
{α : Type u}
{β : α → Type u} :
cardinal.mk (W_type β) = cardinal.sum (λ (a : α), cardinal.mk (W_type β) ^ cardinal.mk (β a))
theorem
W_type.cardinal_mk_le_of_le
{α : Type u}
{β : α → Type u}
{κ : cardinal}
(hκ : cardinal.sum (λ (a : α), κ ^ cardinal.mk (β a)) ≤ κ) :
cardinal.mk (W_type β) ≤ κ
#(W_type β) is the least cardinal κ such that sum (λ a : α, κ ^ #(β a)) ≤ κ
theorem
W_type.cardinal_mk_le_max_aleph_0_of_finite
{α : Type u}
{β : α → Type u}
[∀ (a : α), finite (β a)] :
If, for any a : α, β a is finite, then the cardinality of W_type β
is at most the maximum of the cardinality of α and ℵ₀