Cardinality of W-types #

This file proves some theorems about the cardinality of W-types. The main result is cardinal_mk_le_max_omega_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 cardinal.omega. 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

source

theorem W_type.cardinal_mk_eq_sum {α : Type u} {β : α → Type u} :

# (W_type β) = cardinal.sum (λ (a : α), # (W_type β) ^ # (β a))

source

theorem W_type.cardinal_mk_le_of_le {α : Type u} {β : α → Type u} {κ : cardinal} (hκ : cardinal.sum (λ (a : α), κ ^ # (β a)) ≤ κ) :

# (W_type β) ≤ κ

#(W_type β) is the least cardinal κ such that sum (λ a : α, κ ^ #(β a)) ≤ κ

source

theorem W_type.cardinal_mk_le_max_omega_of_fintype {α : Type u} {β : α → Type u} [Π (a : α), fintype (β a)] :

# (W_type β) ≤ max (# α) ω

If, for any a : α, β a is finite, then the cardinality of W_type β is at most the maximum of the cardinality of α and ω