English
There is a canonical correspondence between finitely supported functions on α × β with values in M and finitely supported functions from α to β →₀ M, given by the uncurry operation. Concretely, (f: α →₀ β →₀ M) maps (a,b) to f(a)(b).
Русский
Существует каноническое соответствие между конечноподдерживаемыми функциями на α × β со значениями в M и конечноподдерживаемыми функциями от α в β →₀ M, задаваемое операцией раскаррирования: (f: α →₀ β →₀ M)(a,b) = f(a)(b).
LaTeX
$$$\text{uncurry}: (\alpha \to_0 \beta \to_0 M) \to (\alpha \times \beta) \to_0 M,\quad (f:\alpha \to_0 \beta \to_0 M)(a,b) = f(a)(b)$$$
Lean4
/-- Given a finitely supported function `f` from `α` to the type of
finitely supported functions from `β` to `M`,
`uncurry f` is the "uncurried" finitely supported function from `α × β` to `M`. -/
protected def uncurry (f : α →₀ β →₀ M) : α × β →₀ M
where
toFun x := f x.1 x.2
support :=
f.support.disjiUnion (fun a ↦ (f a).support.map <| .sectR a _) <|
by
intro a₁ _ a₂ _ hne
simp [Finset.disjoint_iff_ne, hne]
mem_support_toFun := by aesop
