and_eventually — Mathlib

English

If p holds frequently with respect to f and q holds eventually with respect to f, then p and q hold frequently with respect to f.

Русский

Если p встречается часто по f, а q выполняется в пределе по f, то p и q вместе встречаются часто по f.

LaTeX

$$$ (\exists^\! x \in f, p(x)) \land (\forall^\! x \in f, q(x)) \rightarrow \exists^\! x \in f, p(x) \land q(x) $$$

Lean4

theorem and_eventually {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
  refine mt (fun h => hq.mp <| h.mono ?_) hp
  exact fun x hpq hq hp => hpq ⟨hp, hq⟩

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