tsupport_smul_subset_right — Mathlib

English

For f: X → M and g: X → α with M a topological monoid and α a type, the tsupport of f(x)·g(x) is contained in tsupport f.

Русский

Для функций f: X→M и g: X→α, tsupport (f(x)·g(x)) ⊆ tsupport(f).

LaTeX

$$$\operatorname{tsupport}(x \mapsto f(x) \cdot g(x)) \subseteq \operatorname{tsupport}(f)$$$

Lean4

theorem tsupport_smul_subset_right {M α} [TopologicalSpace X] [Zero α] [SMulZeroClass M α] (f : X → M) (g : X → α) :
    (tsupport fun x => f x • g x) ⊆ tsupport g :=
  closure_mono <| support_smul_subset_right f g

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