Theorems · Theorem · general topology

Filter.eventually_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

2 results in Mathlib

Foundations

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