support_mul_subset_left — Mathlib

English

For any f,g: ι → M₀, the support of the product f · g is contained in the support of f; i.e., wherever f ≠ 0, (f·g) ≠ 0 implies g may be nonzero but not required.

Русский

Для любых f,g: ι → M₀, опора произведения f · g ⊆ опоры f.

LaTeX

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

Lean4

theorem support_mul_subset_left (f g : ι → M₀) : support (fun x ↦ f x * g x) ⊆ support f := fun x hfg hf ↦
  hfg <| by simp only [hf, zero_mul]

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