# Curried Filters #

This file provides an operation (`Filter.curry`

) on filters which provides the equivalence
`∀ᶠ a in l, ∀ᶠ b in l', p (a, b) ↔ ∀ᶠ c in (l.curry l'), p c`

(see `Filter.eventually_curry_iff`

).

To understand when this operation might arise, it is helpful to think of `∀ᶠ`

as a combination of
the quantifiers `∃ ∀`

. For instance, `∀ᶠ n in at_top, p n ↔ ∃ N, ∀ n ≥ N, p n`

. A curried filter
yields the quantifier order `∃ ∀ ∃ ∀`

. For instance,
`∀ᶠ n in at_top.curry at_top, p n ↔ ∃ M, ∀ m ≥ M, ∃ N, ∀ n ≥ N, p (m, n)`

.

This is different from a product filter, which instead yields a quantifier order `∃ ∃ ∀ ∀`

. For
instance, `∀ᶠ n in at_top ×ˢ at_top, p n ↔ ∃ M, ∃ N, ∀ m ≥ M, ∀ n ≥ N, p (m, n)`

. This makes it
clear that if something eventually occurs on the product filter, it eventually occurs on the curried
filter (see `Filter.curry_le_prod`

and `Filter.eventually.curry`

), but the converse is not true.

Another way to think about the curried versus the product filter is that tending to some limit on
the product filter is a version of uniform convergence (see `tendsto_prod_filter_iff`

) whereas
tending to some limit on a curried filter is just iterated limits (see `Filter.Tendsto.curry`

).

## Main definitions #

`Filter.curry`

: A binary operation on filters which represents iterated limits

## Main statements #

`Filter.eventually_curry_iff`

: An alternative definition of a curried filter`Filter.curry_le_prod`

: Something that is eventually true on the a product filter is eventually true on the curried filter

## Tags #

uniform convergence, curried filters, product filters

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`

.