and_frequently — Mathlib

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

Похожие утверждения