∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {pa : α → Prop},
  (∀ᶠ (x : α) in la, pa x) →
    ∀ {lb : Filter β} {pb : β → Prop}, (∀ᶠ (y : β) in lb, pb y) → ∀ᶠ (p : α × β) in la ×ˢ lb, pa p.1 ∧ pb p.2