# Documentation

Mathlib.Data.W.Cardinal

# Cardinality of W-types #

This file proves some theorems about the cardinality of W-types. The main result is cardinal_mk_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.cardinal_mk_eq_sum {α : Type u} {β : αType u} :
theorem WType.cardinal_mk_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 (λ a : α, κ ^ #(β a)) ≤ κ

theorem WType.cardinal_mk_le_max_aleph0_of_finite {α : Type u} {β : αType u} [∀ (a : α), Finite (β a)] :

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