support_smul_subset_left — Mathlib

English

The support of the product f • g is contained in the support of f when the latter is a function to a ring and the former to a module with smul.

Русский

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

LaTeX

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

Lean4

theorem support_smul_subset_left [Zero R] [Zero M] [SMulWithZero R M] (f : α → R) (g : α → M) :
    support (f • g) ⊆ support f := fun x hfg hf ↦
  hfg <| by
    rw [Pi.smul_apply', hf, zero_smul]
      -- Changed (2024-01-21): this lemma was generalised;
      -- the old version is now called `support_const_smul_subset`.

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