MvPolynomial.cardinal_mk_le_max
theorem MvPolynomial.cardinal_mk_le_max :
∀ {σ R : Type u} [inst : CommSemiring R],
Cardinal.mk (MvPolynomial σ R) ≤ max (max (Cardinal.mk R) (Cardinal.mk σ)) Cardinal.aleph0
This theorem states that for any given types `σ` and `R`, where `R` has a commutative semiring structure, the cardinality of the multivariate polynomial ring `MvPolynomial σ R` is less than or equal to the maximum of the cardinalities of `R`, `σ`, and `ℵ₀` (the smallest infinite cardinal). In other words, the size of the set of all multivariate polynomials with variables indexed by `σ` and coefficients from `R` is at most as large as the biggest of the sizes of the sets of elements of `R`, `σ`, and the natural numbers.
More concisely: The cardinality of the multivariate polynomial ring over a commutative semiring with types `σ` and `R` is bounded above by the maximum of the cardinalities of `R`, `σ`, and the set of natural numbers.
|
MvPolynomial.cardinal_mk_eq_max_lift
theorem MvPolynomial.cardinal_mk_eq_max_lift :
∀ {σ : Type u} {R : Type v} [inst : CommSemiring R] [inst_1 : Nonempty σ] [inst_2 : Nontrivial R],
Cardinal.mk (MvPolynomial σ R) =
max (max (Cardinal.lift.{u, v} (Cardinal.mk R)) (Cardinal.lift.{v, u} (Cardinal.mk σ))) Cardinal.aleph0
The theorem `MvPolynomial.cardinal_mk_eq_max_lift` states that for any type `σ`, any type `R` that has a `CommSemiring` instance, and assuming that `σ` is nonempty and `R` is nontrivial, the cardinality of the multivariate polynomial type with `σ` as the index set of the variables and `R` as the coefficient ring is equal to the maximum of three terms: the lifted cardinality of `R`, the lifted cardinality of `σ`, and `ℵ₀` (the smallest infinite cardinal). In other words, the cardinality of the multivariate polynomial space is determined by the larger of the cardinalities of the set of variables and coefficients, unless either is finite and smaller than `ℵ₀`, in which case the cardinality is `ℵ₀`.
More concisely: The cardinality of the multivariate polynomial space over a nontrivial commutative semiring with infinite base set is the maximum of the lifted cardinalities of the base set and the coefficient ring, or `ℵ₀` if either is finite.
|