support_smul_subset_right — Mathlib

English

The support of the product f • g is contained in the support of g when smul acts on the second factor.

Русский

Поддержка произведения f • g содержится в поддержке g.

LaTeX

$$$ \operatorname{supp}(f \cdot g) \subseteq \operatorname{supp}(g) $$$

Lean4

theorem support_smul_subset_right [Zero M] [SMulZeroClass R M] (f : α → R) (g : α → M) : support (f • g) ⊆ support g :=
  fun x hbf hf ↦ hbf <| by rw [Pi.smul_apply', hf, smul_zero]

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