Filters

A filter is a generalized subset.

Learning goal

By the end you can

  • say why Mathlib defines limits through filters,

  • write down the three filter axioms,

  • read Tendsto as a single definition.

The problem

Three \varepsilon-\delta definitions:

  • a_n \to l

  • f(x) \to l as x \to x_0

  • f(x) \to \infty as x \to \infty

One shape: for good enough inputs, the output lies in a given set.

The idea

A generalized subset F of \alpha is pinned down by the actual sets that contain it.

Newton wanted dx to be a number infinitesimally close to 0. A filter is how we get that back.

The three axioms

The sets that may contain F:

1

S \supseteq F and S \subseteq T \Rightarrow T \supseteq F

2

S \supseteq F and T \supseteq F \Rightarrow S \cap T \supseteq F

3

\alpha \supseteq F

In Lean

structure MyFilter (α : Type) where sets : Set (Set α) univ_sets : Set.univ ∈ sets sets_of_superset {x y} : x ∈ sets → x ⊆ y → y ∈ sets inter_sets {x y} : x ∈ sets → y ∈ sets → x ∩ y ∈ sets

S ∈ F morally means F ⊆ S.

Three filters to know

principal s is s itself, atTop is n large enough, cofinite is all but finitely many.

open Filter #check (principal : Set ℕ → Filter ℕ)
𝓟 : Set ℕ → Filter ℕ
#check (atTop : Filter ℕ)
atTop : Filter ℕ
#check (cofinite : Filter ℕ)
cofinite : Filter ℕ

One definition instead of three

open Filter in example (f : α → β) (F : Filter α) (G : Filter β) : Prop := Tendsto f F G

a_n \to l is Tendsto a atTop (nhds l).

In one line

Filter = generalized subset

Three axioms. One notion of limit. The rest is notation.