tsupport_mul_subset_left — Mathlib

English

The tsupport of the product f x g is contained in the tsupport of f: tsupport (f·g) ⊆ tsupport f.

Русский

Опора-t (произведение) влево: tsupport (f·g) ⊆ tsupport f.

LaTeX

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

Lean4

theorem tsupport_mul_subset_left {α : Type*} [MulZeroClass α] {f g : X → α} :
    (tsupport fun x => f x * g x) ⊆ tsupport f :=
  closure_mono (support_mul_subset_left _ _)

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