English
If a property p on α×β holds eventually on la × lb, then it holds eventually for all x in la and all y in lb when paired: ∀ᶠ x in la, ∀ᶠ y in lb, p (x,y).
Русский
Если свойство p на α×β выполняется Eventually на ла × lb, то оно выполняется Eventually для всех x в ла и всех y в lb в пары: ∀ᶠ x ∈ la, ∀ᶠ y ∈ lb, p (x,y).
LaTeX
$$$$\forall^\infty x \in la, \forall^\infty y \in lb, p(x,y).$$$$
Lean4
theorem curry {la : Filter α} {lb : Filter β} {p : α × β → Prop} (h : ∀ᶠ x in la ×ˢ lb, p x) :
∀ᶠ x in la, ∀ᶠ y in lb, p (x, y) :=
by
rcases eventually_prod_iff.1 h with ⟨pa, ha, pb, hb, h⟩
exact ha.mono fun a ha => hb.mono fun b hb => h ha hb
