English
The cardinality of the multivariate polynomial ring over R with variables σ is bounded above by the maximum of the cardinalities of R, σ, and ℵ0 after lifting: #(MvPolynomial σ R) ≤ max (max (Cardinal.lift #R) (Cardinal.lift #σ)) ℵ₀.
Русский
Число кардиналов многочленных кольца с переменными σ над R ограничено сверху максимумом кардиналов R и σ после подъема: #(MvPolynomial σ R) ≤ max (max (Cardinal.lift #R) (Cardinal.lift #σ)) ℵ₀.
LaTeX
$$$\\#(\\mathrm{MvPolynomial}(\\sigma, R)) \\leq \\max\\big(\\max \\big(\\operatorname{Cardinal.lift} (#R)\\big) \\operatorname{Cardinal.lift}(#\\sigma)\\big) \\aleph_0$$$
Lean4
@[simp]
theorem cardinalMk_eq_max_lift [Nonempty σ] [Nontrivial R] :
#(MvPolynomial σ R) = max (max (Cardinal.lift.{u} #R) <| Cardinal.lift.{v} #σ) ℵ₀ :=
(mk_finsupp_lift_of_infinite _ R).trans <| by rw [mk_finsupp_nat, max_assoc, lift_max, lift_aleph0, max_comm]
