English
The cardinality of MvPolynomial σ R is bounded above by the maximum of the lifted cardinalities of R and σ and ℵ0: #(MvPolynomial σ R) ≤ max (max (Cardinal.lift #R) (Cardinal.lift #σ)) ℵ₀.
Русский
Кардинал MvPolynomial σ R ограничен сверху максимумом подъема кардиналов #R и #σ и ℵ0.
LaTeX
$$$\\#(\\mathrm{MvPolynomial}(\\sigma, R)) \\leq \\max (\\max (\\operatorname{Cardinal.lift} (#R)) (\\operatorname{Cardinal.lift} (#\\sigma))) \\aleph_0$$$
Lean4
theorem cardinalMk_le_max_lift {σ : Type u} {R : Type v} [CommSemiring R] :
#(MvPolynomial σ R) ≤ max (max (Cardinal.lift.{u} #R) <| Cardinal.lift.{v} #σ) ℵ₀ :=
by
cases subsingleton_or_nontrivial R
· exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
cases isEmpty_or_nonempty σ
· exact cardinalMk_eq_lift.trans_le (le_max_of_le_left <| le_max_left _ _)
· exact cardinalMk_eq_max_lift.le
