English
The frequent version of curry: (∃ᶠ x in l.curry m, p x) ⇔ (∃ᶠ x in l, ∃ᶠ y in m, p (x,y)).
Русский
Частотная версия curry: (∃ᶠ x в l.curry m, p x) ⇔ (∃ᶠ x в l, ∃ᶠ y в m, p (x,y)).
LaTeX
$$$(\\exists\\mathrm{ᶠ}\\ x\\in l.curry m,\ p\ x) \\iff (\\exists\\mathrm{ᶠ}\\ x\\in l, \\exists\\mathrm{ᶠ}\\ y\\in m,\ p\\ (x,y))$$$
Lean4
theorem frequently_curry_iff (p : (α × β) → Prop) : (∃ᶠ x in l.curry m, p x) ↔ ∃ᶠ x in l, ∃ᶠ y in m, p (x, y) := by
simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]