English
Let f: α → β → γ be a function and la, lb, lc be filters on α, β, γ respectively. If for almost every a with respect to la the map b ↦ f(a,b) tends to lc along lb, then the uncurry of f tends to lc along the curried product la.curry lb.
Русский
Пусть f: α → β → γ. Пусть l_a, l_b, l_c — фильтры на α, β, γ. Если для почти всех a по l_a отображение b ↦ f(a,b) стремится к lc по lb, тогда распакованный из f по переменным a,b тождественно сходится к lc по фильтру la.curry lb.
LaTeX
$$$\forall {f:α\toβ\toγ} \{la:Filter α\} \{lb:Filter β\} \{lc:Filter γ\}, \left(\forall^{\infty} a \in la, Tendsto(\lambda b: f\,a\,b) lb lc\right) \Rightarrow Tendsto(uncurry f) (la.curry lb) lc$$
Lean4
theorem curry {f : α → β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ}
(h : ∀ᶠ a in la, Tendsto (fun b : β => f a b) lb lc) : Tendsto ↿f (la.curry lb) lc := fun _s hs =>
h.mono fun _a ha => ha hs
