supported_eq_vars_subset — Mathlib

English

Let s be a subset of the index set. The set of polynomials whose variables lie in s is exactly the subalgebra generated by the variables X_i with i in s.

Русский

Пусть s ⊆ σ. Многочлены, переменные которых лежат в s, образуют ровно подалгебру, порождаемую переменными X_i для i ∈ s.

LaTeX

$$$$ \mathrm{supported}(R,s) = \{ p \in \mathrm{MvPolynomial}(\sigma,R) \mid \uparrow p.\mathrm{vars} \subseteq s \} $$$$

Lean4

theorem supported_eq_vars_subset : (supported R s : Set (MvPolynomial σ R)) = {p | ↑p.vars ⊆ s} :=
  Set.ext fun _ ↦ mem_supported

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