support_const_smul_subset — Mathlib

English

If c is a scalar, the support of the constant-smoothed function c • f is contained in the support of f.

Русский

Если константный множитель c, то поддержка функции c • f содержится в поддержке f.

LaTeX

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

Lean4

theorem support_const_smul_subset [Zero M] [SMulZeroClass R M] (a : R) (f : α → M) : support (a • f) ⊆ support f :=
  support_smul_subset_right (fun _ ↦ a) f

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