filters.md

Filter	Meaning
at_top	filter generated by [x, +∞)
at_bot	filter generated by (-∞, x]
𝓝 x	neighborhoods of x
𝓝[s] x	neighborhoods of x within s
𝓝[Ici x] x	right neighborhoods of x
𝓝[Ioi x] x	punctured right neighborhoods of x
𝓝[Iio x] x	punctured left neighborhoods of x
𝓝[{x}ᶜ] x	punctured neighborhoods of x
⊥	bottom filter: all sets belong to ⊥
⊤	top filter: the only member is univ
pure a	filter of sets s such that a ∈ s
𝓟 s	filter of supsersets of s, i.e. t ∈ 𝓟 s ↔ s ⊆ t
μ.ae	filter of properties that hold a.e.
residual	filter generated by everywhere dense $G_δ$ sets

Here is a list of some expressions written using filters, together with equivalent statements not using filters. Sometimes these statements are equivalent whenever both sides are defined, sometimes the equivalence needs additional assumptions. We explicitly mention these assumptions only if they do not hold for filters on ℝ, ℕ, or ℤ.

1. s ∈ at_top means that s includes some half-line $[x, +∞)$; s ∈ at_top ↔ ∃ a, Ici a ⊆ s.
2. ∀ᶠ x in at_bot, p x, where p : α → Prop is a predicate, means that predicate p holds for all values of x less than or equal to some a: (∀ᶠ x in at_bot, p x) ↔ ∃ a, ∀ x ≤ a, p x.
3. tendsto f (𝓝 a) at_top means $\lim_{x→a} f(x) = +∞$.
4. tendsto f at_top at_bot means $\lim_{x→+∞} f(x) = -∞$.
5. tendsto f at_top (𝓝 a) means $\lim_{x→+∞} f(x) = a$.
6. tendsto f l (𝓟 s) means ∀ᶠ x in l, f x ∈ s; e.g., tendsto f (𝓝 a) (𝓟 s) means that f x ∈ s for x from some neighborhood of a.
7. tendsto f (𝓝 a) (𝓝[s] b) means that $\lim_{x→a} f(x)=b$ and f x ∈ s for x from some neighborhood of a.
8. tendsto f ⊥ l and tendsto f l ⊤ are always true.
9. tendsto f l ⊥ means l = ⊥.
10. s ∈ 𝓟 t means t ⊆ s; note that a very similar notation is used for the powerset: s ∈ 𝒫 t means s ⊆ t.
11. s ∈ 𝓝 x: s is a neighborhood of x; equivalently, s includes some open neighborhood of x.
12. s ∈ 𝓝[t] x: s includes the intersection of t with a neighborhood of x; equivalently, s ∪ tᶜ is a neighborhood of x; equivalently, s includes the intersection of t with an open neighborhood of x.
13. ∀ᶠ x in 𝓝 a, p x: predicate p holds in some neighborhood of x.
14. ∃ᶠ x in 𝓝[s] a, p x: any neighborhood U of a contains a point x such that x ∈ s and p x.
15. ∃ᶠ x in at_top, p x means that the set {x | p x} is not bounded above.
16. tendsto f (𝓝 a) (𝓝 b ⊔ 𝓟 (Ici b)) means that $\liminf_{x→a} f(x)≥b$.
17. ∀ᶠ s in (𝓝 a).lift' powerset, p s means that predicate p holds for all subsets of some neighborhood of a.