eventually_iff_exists_mem — Mathlib

English

For any f and predicate p, (∀ᶠ x in f, p x) holds if and only if there exists a set V ∈ f such that ∀ y ∈ V, p y.

Русский

Для фильтра f и предиката p: (∀ᶠ x ∈ f, p x) эквивалентно существованию множества V ∈ f такое, что ∀ y ∈ V, p y.

LaTeX

$$$(\\forallᶠ x ∈ f, p x) \\iff \\exists V \\in f, \\forall y \\in V, p y$$$

Lean4

theorem eventually_iff_exists_mem {p : α → Prop} {f : Filter α} : (∀ᶠ x in f, p x) ↔ ∃ v ∈ f, ∀ y ∈ v, p y :=
  exists_mem_subset_iff.symm

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