English
For filters l on α and m on β and sets s ⊆ α, t ⊆ β, the frequency with which a pair (x,y) lies in the product s × t under the curry product l.curry m is equivalent to the independent frequencies that s lies in l and t lies in m.
Русский
Для фильтров l на α и m на β и множеств s ⊆ α, t ⊆ β частоты попадания пары в произведение s × t под карри-произведением l.curry m равны частотам того, что s∈l и t∈m по отдельности.
LaTeX
$$$\forall {l:Filter\ α} {m:Filter\ β} {s:Set\ α} {t:Set\ β}, (\exists^\infty x \in l.curry m, x \in s\times t) \iff (\exists^\infty x \in l, x \in s) \land (\exists^\infty y \in m, y \in t)$$
Lean4
theorem frequently_curry_prod_iff : (∃ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ x in l, x ∈ s) ∧ ∃ᶠ y in m, y ∈ t := by
simp [frequently_curry_iff]
