English
For any filter f on α, a family of filters m: α → Filter β, and predicate p on β, the eventuallY quantified statement over the bind equals the outer-eventual statement: (∀ᶠ y in bind f m, p y) iff (∀ᶠ x in f, ∀ᶠ y in m x, p y).
Русский
Для любой фильтрации f на α, семейства m: α → Filter β и предиката p на β выполнено: (∀ᶠ y in bind f m, p y) эквивалентно (∀ᶠ x in f, ∀ᶠ y in m x, p y).
LaTeX
$$$(\\forall^\\infty y \\in \\mathrm{bind}\\,f\\,m: p(y)) \\iff (\\forall^\\infty x \\in f, \\forall^\\infty y \\in m(x): p(y))$$$
Lean4
@[simp]
theorem eventually_bind {f : Filter α} {m : α → Filter β} {p : β → Prop} :
(∀ᶠ y in bind f m, p y) ↔ ∀ᶠ x in f, ∀ᶠ y in m x, p y :=
Iff.rfl
