frequently_iff_forall_eventually_exists_and

English

There exists a frequent witness for p if and only if for every q, whenever q holds eventually, there exists x with p(x) and q(x).

Русский

Существует частый свидетель p тогда и только тогда, когда для каждого q, если q выполняется в конечном итоге, существует x с p(x) и q(x).

LaTeX

$$$ (\exists^\! x \in f, p(x)) \iff \forall \{q : \alpha \to \mathrm{Prop}\}, (\forall^\! x \in f, q(x)) \rightarrow \exists x, p(x) \land q(x) $$$

Lean4

theorem frequently_iff_forall_eventually_exists_and {p : α → Prop} {f : Filter α} :
    (∃ᶠ x in f, p x) ↔ ∀ {q : α → Prop}, (∀ᶠ x in f, q x) → ∃ x, p x ∧ q x :=
  ⟨fun hp _ hq => (hp.and_eventually hq).exists, fun H hp => by simpa only [and_not_self_iff, exists_false] using H hp⟩

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