English
Let l be a filter with a basis p i → s i. For any property q, the statement that q holds eventually in l is equivalent to the existence of an index i with p i such that q holds for all elements of s i.
Русский
Пусть l имеет базис p i → s i. Для произвольного свойства q утверждение, что q выполняется eventually в l, эквивалентно существованию индекса i с p i, такого что q выполняется для всех элементов набора s i.
LaTeX
$$$l\text{ has basis } p s\;\Rightarrow\; (\forall q:\alpha\to\text{Prop}, (\forall x, q(x)\text{ не обязательно}) ) \\ \text{(сложно переписать)}$$$
Lean4
theorem eventually_iff (hl : l.HasBasis p s) {q : α → Prop} : (∀ᶠ x in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x⦄, x ∈ s i → q x := by
simpa using hl.mem_iff
