English
If ∃ᶠ x in la, ∃ᶠ y in lb, p (x,y), then ∃ᶠ xy in la × lb, p xy.
Русский
Если существуют часто встречающиеся значения x в ла и y в lb, такие что p(x,y), то существует часто встречающаяся пара (x,y) в ла×lb с p(x,y).
LaTeX
$$$$\exists^\infty x \in la, \exists^\infty y \in lb, p(x,y) \Rightarrow \exists^\infty xy \in la \times lb, p(xy).$$$$
Lean4
protected theorem uncurry {la : Filter α} {lb : Filter β} {p : α → β → Prop} (h : ∃ᶠ x in la, ∃ᶠ y in lb, p x y) :
∃ᶠ xy in la ×ˢ lb, p xy.1 xy.2 :=
mt (fun h ↦ by simpa only [not_frequently] using h.curry) h