Theorems · Theorem · general topology

Filter.frequently_curry_iff

∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} (p : α × β → Prop),
  (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)

Defined in

Mathlib.Order.Filter.Curry

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound