mulSupport_curry — Mathlib

English

The mulSupport of the curry of f equals the image under Prod.fst of the mulSupport of f.

Русский

Опора карри функции f равна образу Prod.fst от mulSupport f.

LaTeX

$$$ \operatorname{mulSupport}(f.\mathrm{curry}) = \operatorname{mulSupport}(f).\mathrm{image}(\mathrm{Prod}.\mathrm{fst}) $$$

Lean4

@[to_additive]
theorem mulSupport_curry (f : ι × κ → M) : (mulSupport f.curry) = (mulSupport f).image Prod.fst := by
  simp [mulSupport, funext_iff, image]

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