support_mul — Mathlib

English

For f,g in SkewMonoidAlgebra, the support of their product is contained in the product of their supports.

Русский

Для элементов f,g в SkewMonoidAlgebra опора их произведения содержится в произведении их опор.

LaTeX

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

Lean4

theorem support_mul : (f * g).support ⊆ f.support * g.support :=
  support_sum.trans <|
    biUnion_subset.2 fun _x hx ↦
      support_sum.trans <|
        biUnion_subset.2 fun _y hy ↦ support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy

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