support_curry — Mathlib

English

The support of the curry of f is the image of the support of f under the first projection: supp(f^{curry}) = image_{Prod.fst}(supp(f)).

Русский

Опора каррирования f равна образу опоры f по проекции на первую компоненту: supp(f^{curry}) = image_{Prod.fst}(supp(f)).

LaTeX

$$$\operatorname{supp}(f^{\text{curry}}) = \operatorname{image}(\operatorname{supp}(f), \operatorname{Prod.fst})$$$

Lean4

@[simp]
theorem support_curry (f : α × β →₀ M) : f.curry.support = f.support.image Prod.fst :=
  rfl

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