cardinalMk_eq_max — Mathlib

English

If σ is nonempty and R is nontrivial, then the cardinality of MvPolynomial σ R equals max of the cardinalities of R and σ, lifted, with ℵ0: #(MvPolynomial σ R) = max (max #R #σ) ℵ₀.

Русский

Если σ непусто и R ненулевое, то кардинал MvPolynomial σ R равен max подъема кардиналов #R и #σ, с учётом ℵ0.

LaTeX

$$$\\#(\\mathrm{MvPolynomial}(\\sigma, R)) = \\max (\\max (#R) (#\\sigma)) \\aleph_0$$$

Lean4

theorem cardinalMk_eq_max [Nonempty σ] [Nontrivial R] : #(MvPolynomial σ R) = max (max #R #σ) ℵ₀ := by simp

Похожие утверждения