7. Filters🔗

Mathlib states every limit, "eventually", and "almost everywhere" claim through filters. If you want to write lim_{x → 0} sin x / x = 1 as a Lean proposition, prove that a sequence converges, or read a proof that pivots through 𝓝 and atTop, this chapter shows how. It assumes you are comfortable with Lean and with limits in the usual ε-δ sense, but not that you have met filters before.

A Filter l on a type α packages a notion of "eventually": for a set s : Set α, membership s ∈ l reads "we eventually land in s". Different filters carry different notions: 𝓝 x is "for points near x", atTop is "for sufficiently large input", ae μ is "for almost every point". You rarely touch the axioms directly; the skill is picking the filter that matches the limit you mean and letting the lemmas do the work. One relation, Filter.Tendsto, then covers sequence convergence, function limits at a point, "→ ∞", and almost-everywhere statements uniformly.

The chapter has four entries:

Limit statements — turn a mathematical limit into a Mathlib proposition.
Proving limits — prove such a statement once it is written.
ε-δ and filter bases — translate textbook ε-δ statements into filter form.
Operations on filters — read the ≤, Filter.map, Filter.comap, and ×ˢ algebra in other people's proofs.

The notations 𝓝, atTop, ∀ᶠ only parse after open Filter Topology. A reference table of the standard filters closes the chapter.