English
The curry of a filter f on α and a filter g on β is the filter on α×β defined by curry(f,g) = bind f (λ a. map (a,·) g).
Русский
Каррирование фильтра f на α и фильтра g на β даёт фильтр на α×β, определяемый как curry(f,g) = bind f (λ a. map (a,·) g).
LaTeX
$$$\mathrm{curry}(f,g) = \mathrm{bind}\,f\; (\lambda a.\,\mathrm{map}(a,\cdot)\; g).$$$
Lean4
/-- This filter is characterized by `Filter.eventually_curry_iff`:
`(∀ᶠ (x : α × β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y)`. Useful
in adding quantifiers to the middle of `Tendsto`s. See
`hasFDerivAt_of_tendstoUniformlyOnFilter`. -/
def curry (f : Filter α) (g : Filter β) : Filter (α × β) :=
bind f fun a ↦ map (a, ·) g
