vars_add_subset — Mathlib

English

The variables of p+q are contained in the union of the variables of p and q.

Русский

Переменные p+q лежат в объединении переменных p и q.

LaTeX

$$$$ (p+q).\mathrm{vars} \subseteq p.\mathrm{vars} \cup q.\mathrm{vars} $$$$

Lean4

theorem vars_add_subset [DecidableEq σ] (p q : MvPolynomial σ R) : (p + q).vars ⊆ p.vars ∪ q.vars :=
  by
  intro x hx
  simp only [vars_def, Finset.mem_union, Multiset.mem_toFinset] at hx ⊢
  simpa using Multiset.mem_of_le degrees_add_le hx

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