English
For a function f : σ → τ, the variables of rename f φ are contained in the image of φ.vars under f.
Русский
Для функции f: σ → τ переменные полинома после переименования лежат в образе множества переменных φ.
LaTeX
$$$ (rename\ f\ φ).vars \subseteq \mathrm{image}\ f\ φ.vars $$$
Lean4
theorem vars_rename [DecidableEq τ] (f : σ → τ) (φ : MvPolynomial σ R) : (rename f φ).vars ⊆ φ.vars.image f := by
classical
intro i hi
simp only [vars_def, Multiset.mem_toFinset, Finset.mem_image] at hi ⊢
simpa only [Multiset.mem_map] using degrees_rename _ _ hi