cardinalMk_le_max — Mathlib

English

A standard upper bound for cardinality: #(MvPolynomial σ R) ≤ max (max #R #σ) ℵ₀.

Русский

Стандартная верхняя граница кардинала: #(MvPolynomial σ R) ≤ max (max #R #σ) ℵ₀.

LaTeX

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

Lean4

/-- The cardinality of the multivariate polynomial ring, `MvPolynomial σ R` is at most the maximum
of `#R`, `#σ` and `ℵ₀` -/
theorem cardinalMk_le_max : #(MvPolynomial σ R) ≤ max (max #R #σ) ℵ₀ :=
  cardinalMk_le_max_lift.trans <| by rw [lift_id, lift_id]

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