vars_rename — Mathlib

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

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