mulSupport_binop_subset — Mathlib

English

For a binary operation with op(1,1)=1, the support of the pointwise operation is contained in the union of the supports of the factors:

Русский

Для двоичной операции с условием op(1,1)=1, опора точечного применения <= объединение опор f и g.

LaTeX

$$$ \operatorname{mulSupport}(\lambda x. \operatorname{op}(f x)(g x)) \subseteq \operatorname{mulSupport}(f) \cup \operatorname{mulSupport}(g) $$$

Lean4

@[to_additive]
theorem mulSupport_binop_subset (op : M → N → P) (op1 : op 1 1 = 1) (f : ι → M) (g : ι → N) :
    mulSupport (fun x ↦ op (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g := fun x hx ↦
  not_or_of_imp fun hf hg ↦ hx <| by simp only [hf, hg, op1]

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