mulSupport_prodMk' — Mathlib

English

For a function f: ι → M×N, mulSupport f equals the union of mulSupport of its first and second projections.

Русский

Для функции f: ι → M×N опора функции равна объединению опор проекций на первые и вторые координаты.

LaTeX

$$$ \operatorname{mulSupport}(f) = \operatorname{mulSupport}(\lambda x. (f x)^{1}) \cup \operatorname{mulSupport}(\lambda x. (f x)^{2}) $$$

Lean4

@[to_additive support_prodMk']
theorem mulSupport_prodMk' (f : ι → M × N) : mulSupport f = (mulSupport fun x ↦ (f x).1) ∪ mulSupport fun x ↦ (f x).2 :=
  by simp only [← mulSupport_prodMk]

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