MvPolynomial.mem_supported

theorem MvPolynomial.mem_supported : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] {p : MvPolynomial σ R} {s : Set σ}, p ∈ MvPolynomial.supported R s ↔ ↑p.vars ⊆ s

This theorem states that for any commutative semiring `R`, any set `s` of type `σ`, and any multivariate polynomial `p` with variables from `σ` and coefficients from `R`, the polynomial `p` is supported by `s` if and only if the set of variables appearing in `p` (denoted by `MvPolynomial.vars p`) is a subset of `s`. In other words, a polynomial is considered "supported" by a set of variables if all the variables that appear in the polynomial belong to that set.

More concisely: For any commutative semiring R, set s, and multivariate polynomial p over R with variables from s, p is supported by s if and only if the variables of p are contained in s.