English
If p holds frequently and q holds frequently in f, then p and q hold frequently in f.
Русский
Если p встречается часто и q встречается часто по фильтру f, то p и q вместе встречаются часто по f.
LaTeX
$$$ (\forall^\! x \in f, p(x)) \land (\exists^\! x \in f, q(x)) \rightarrow \exists^\! x \in f, p(x) \land q(x) $$$
Lean4
theorem and_frequently {p q : α → Prop} {f : Filter α} (hp : ∀ᶠ x in f, p x) (hq : ∃ᶠ x in f, q x) :
∃ᶠ x in f, p x ∧ q x := by simpa only [and_comm] using hq.and_eventually hp