support_single_mul_subset — Mathlib

English

The support of (single a r) * f is contained in the image of f.support by left-multiplication by a.

Русский

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

LaTeX

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

Lean4

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

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