support_mul_single_subset — Mathlib

English

Under suitable regularity conditions, the support of (single a r) * f equals the image of f.support by left-multiplication by a.

Русский

При подходящих условиях регулярности опора (single a r) * f совпадает с образованием опоры f под левым умножением на a.

LaTeX

$$$(single\\ a\\ r * f).\\operatorname{support} = \\mathrm{image} (\\lambda x. a * x)\\ f.\\operatorname{support}$$$

Lean4

theorem support_mul_single_subset (r : k) (a : G) : (f * single a r).support ⊆ Finset.image (· * a) f.support :=
  (support_mul _ _).trans <|
    (Finset.image₂_subset_left support_single_subset).trans <| by rw [Finset.image₂_singleton_right]

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