English
Let f be a filter on α, m: α → Filter β, and p on β. Then the frequently quantified statement over bind corresponds to the outer frequently: (∃ᶠ y in bind f m, p y) iff (∃ᶠ x in f, ∃ᶠ y in m x, p y).
Русский
Пусть f — фильтр на α, m: α → Filter β и p на β. Тогда частотная эквивалентность: (∃ᶠ y в bind f m, p y) эквивалентна (∃ᶠ x в f, ∃ᶠ y в m x, p y).
LaTeX
$$$(\\exists^\\infty y \\in \\mathrm{bind}\\,f\\,m: p(y)) \\iff (\\exists^\\infty x \\in f, \\exists^\\infty y \\in m(x): p(y))$$$
Lean4
@[simp]
theorem frequently_bind {f : Filter α} {m : α → Filter β} {p : β → Prop} :
(∃ᶠ y in bind f m, p y) ↔ ∃ᶠ x in f, ∃ᶠ y in m x, p y :=
by
rw [← not_iff_not]
simp only [not_frequently, eventually_bind]
