mulSupport_fun_curry — Mathlib

English

Alias of the curry lemma: mulSupport (fun i j => f(i,j)) equals (mulSupport f).image Prod.fst.

Русский

Псевдоним леммы карри: mulSupport (fun i j => f(i,j)) = (mulSupport f).image Prod.fst.

LaTeX

$$$ \operatorname{mulSupport}(\lambda i j. f(i,j)) = \operatorname{mulSupport}(f).\mathrm{image}(\mathrm{Prod}.\mathrm{fst}) $$$

Lean4

@[to_additive]
theorem mulSupport_fun_curry (f : ι × κ → M) : mulSupport (fun i j ↦ f (i, j)) = (mulSupport f).image Prod.fst :=
  mulSupport_curry f

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