support_mul' — Mathlib

English

The same statement as above holds: the support of the product f · g equals the intersection of their supports, i.e., supp(f·g) = supp(f) ∩ supp(g).

Русский

Та же формула: опора произведения f · g равна пересечению опор f и g.

LaTeX

$$$ \operatorname{support}(f \cdot g) = \operatorname{support}(f) \cap \operatorname{support}(g). $$$

Lean4

@[simp]
theorem support_mul' (f g : ι → M₀) : support (f * g) = support f ∩ support g :=
  support_mul _ _

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