English
There is a curry transformation assigning to each finitely supported function f : α × β → M a curried function curry f : α →₀ (β →₀ M).
Русский
Существуют преобразования карри, сопоставляющее каждой конечной поддерживающей функции f : α × β → M соответствующую карри-функцию curry f : α →₀ (β →₀ M).
LaTeX
$$$ \text{curry} : (\alpha \times \beta \to\! M) \text{ (as FinSupp) } \to (\alpha \to\! (\beta \to\! M)) $$$
Lean4
/-- Given a finitely supported function `f` from a product type `α × β` to `γ`,
`curry f` is the "curried" finitely supported function from `α` to the type of
finitely supported functions from `β` to `γ`. -/
protected def curry (f : α × β →₀ M) : α →₀ β →₀ M
where
toFun
a :=
{ toFun b := f (a, b)
support := f.support.filterMap (fun x ↦ if x.1 = a then x.2 else none) <| by simp +contextual
mem_support_toFun := by simp }
support := f.support.image Prod.fst
mem_support_toFun := by simp [DFunLike.ext_iff]
