mulSupport_prodMk — Mathlib

English

The mulSupport of the pair-valued function (f, g) equals the union of mulSupport f and mulSupport g.

Русский

Опора пары функций (f, g) равна объединению опор f и g.

LaTeX

$$$ \operatorname{mulSupport}\bigl(\lambda x. (f x, g x)\bigr) = \operatorname{mulSupport}(f) \cup \operatorname{mulSupport}(g) $$$

Lean4

@[to_additive support_prodMk]
theorem mulSupport_prodMk (f : ι → M) (g : ι → N) : mulSupport (fun x ↦ (f x, g x)) = mulSupport f ∪ mulSupport g :=
  Set.ext fun x ↦ by simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne]

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