support_mul — Mathlib

English

If M₀ has no zero divisors, then the support of the pointwise product f · g is exactly the intersection of the supports of f and g: ⟦supp(f·g) = supp(f) ∩ supp(g)⟧.

Русский

Если в M₀ нет нулевых делителей, то опора произведения 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 (fun x ↦ f x * g x) = support f ∩ support g :=
  ext fun x ↦ by simp [not_or]

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