Theorems · Definition · general topology

Filter.curry

{α : Type u_1} → {β : Type u_2} → Filter α → Filter β → Filter (α × β)

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 Tendstos. See hasFDerivAt_of_tendstoUniformlyOnFilter.

Defined in

Mathlib.Order.Filter.Defs

Cited by

14 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext, Quot.sound