support_rename_of_injective — Mathlib

English

If f is injective, then the support of rename f p is the image of the support of p under mapDomain f.

Русский

Если f инъективно, то поддержка rename f p равна образу поддержки p под mapDomain f.

LaTeX

$$$ \mathrm{support}(\mathrm{rename}\ f\ p) = \mathrm{Finset.image}(\mathrm{Finsupp.mapDomain} f)\, p.\mathrm{support} $$$

Lean4

theorem support_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} [DecidableEq τ] (h : Function.Injective f) :
    (rename f p).support = Finset.image (Finsupp.mapDomain f) p.support :=
  by
  rw [rename_eq]
  exact Finsupp.mapDomain_support_of_injective (Finsupp.mapDomain_injective h) _

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