Definitions about filters

A filter on a type α is a collection of sets of α which contains the whole α, is upwards-closed, and is stable under intersection. Filters are mostly used to abstract two related kinds of ideas:

• limits, including finite or infinite limits of sequences, finite or infinite limits of functions at a point or at infinity, etc...
• things happening eventually, including things happening for large enough n : ℕ, or near enough a point x, or for close enough pairs of points, or things happening almost everywhere in the sense of measure theory. Dually, filters can also express the idea of things happening often: for arbitrarily large n, or at a point in any neighborhood of given a point etc...

Main definitions

• Filter : filters on a set;
• Filter.principal, 𝓟 s : filter of all sets containing a given set;
• Filter.map, Filter.comap : operations on filters;
• Filter.Tendsto : limit with respect to filters;
• Filter.Eventually : f.Eventually p means {x | p x} ∈ f;
• Filter.Frequently : f.Frequently p means {x | ¬p x} ∉ f;
• filter_upwards [h₁, ..., hₙ] : a tactic that takes a list of proofs hᵢ : sᵢ ∈ f, and replaces a goal s ∈ f with ∀ x, x ∈ s₁ → ... → x ∈ sₙ → x ∈ s;
• Filter.NeBot f : a utility class stating that f is a non-trivial filter.
• Filter.IsBounded r f: the filter f is eventually bounded w.r.t. the relation r, i.e. eventually, it is bounded by some uniform bound. r will be usually instantiated with (· ≤ ·) or (· ≥ ·).
• Filter.IsCobounded r f states that the filter f does not tend to infinity w.r.t. r. This is also called frequently bounded. Will be usually instantiated with (· ≤ ·) or (· ≥ ·).

Notations

• ∀ᶠ x in f, p x : f.Eventually p;
• ∃ᶠ x in f, p x : f.Frequently p;
• f =ᶠ[l] g : ∀ᶠ x in l, f x = g x;
• f ≤ᶠ[l] g : ∀ᶠ x in l, f x ≤ g x;
• 𝓟 s : Filter.Principal s, localized in Filter.

Implementation Notes

Important note: Bourbaki requires that a filter on X cannot contain all sets of X, which we do not require. This gives Filter X better formal properties, in particular a bottom element ⊥ for its lattice structure, at the cost of including the assumption [NeBot f] in a number of lemmas and definitions.

References

• [N. Bourbaki, General Topology][bourbaki1966]

structure Filter (α : Type u_1) : Type u_1

A filter F on a type α is a collection of sets of α which contains the whole α, is upwards-closed, and is stable under intersection. We do not forbid this collection to be all sets of α.

• sets : Set (Set α)

  The set of sets that belong to the filter.

• univ_sets : Set.univ ∈ self.sets

  The set Set.univ belongs to any filter.

• sets_of_superset : ∀ {x y : Set α}, x ∈ self.sets → x ⊆ y → y ∈ self.sets

  If a set belongs to a filter, then its superset belongs to the filter as well.

• inter_sets : ∀ {x y : Set α}, x ∈ self.sets → y ∈ self.sets → x ∩ y ∈ self.sets

  If two sets belong to a filter, then their intersection belongs to the filter as well.

theorem Filter.filter_eq {α : Type u_1} {f g : Filter α} : f.sets = g.sets → f = g

instance Filter.instMembership {α : Type u_1} : Membership (Set α) (Filter α)

If F is a filter on α, and U a subset of α then we can write U ∈ F as on paper.

Equations

• Filter.instMembership = { mem := fun (F : Filter α) (U : Set α) => U ∈ F.sets }

theorem Filter.ext {α : Type u_1} {f g : Filter α} (h : ∀ (s : Set α), s ∈ f ↔ s ∈ g) : f = g

@[simp]

theorem Filter.mem_mk {α : Type u_1} {s : Set α} {t : Set (Set α)} {h₁ : Set.univ ∈ t} {h₂ : ∀ {x y : Set α}, x ∈ t → x ⊆ y → y ∈ t} {h₃ : ∀ {x y : Set α}, x ∈ t → y ∈ t → x ∩ y ∈ t} : s ∈ { sets := t, univ_sets := h₁, sets_of_superset := h₂, inter_sets := h₃ } ↔ s ∈ t

@[simp]

theorem Filter.mem_sets {α : Type u_1} {f : Filter α} {s : Set α} : s ∈ f.sets ↔ s ∈ f

@[simp]

theorem Filter.univ_mem {α : Type u_1} {f : Filter α} : Set.univ ∈ f

theorem Filter.mem_of_superset {α : Type u_1} {f : Filter α} {x y : Set α} (hx : x ∈ f) (hxy : x ⊆ y) : y ∈ f

theorem Filter.univ_mem' {α : Type u_1} {f : Filter α} {s : Set α} (h : ∀ (a : α), a ∈ s) : s ∈ f

theorem Filter.inter_mem {α : Type u_1} {f : Filter α} {s t : Set α} (hs : s ∈ f) (ht : t ∈ f) : s ∩ t ∈ f

theorem Filter.mp_mem {α : Type u_1} {f : Filter α} {s t : Set α} (hs : s ∈ f) (h : {x : α | x ∈ s → x ∈ t} ∈ f) : t ∈ f

def Filter.copy {α : Type u_1} (f : Filter α) (S : Set (Set α)) (hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f) : Filter α

Override sets field of a filter to provide better definitional equality.

Equations

• f.copy S hmem = { sets := S, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

@[simp]

theorem Filter.mem_copy {α : Type u_1} {f : Filter α} {s : Set α} {S : Set (Set α)} {hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f} : s ∈ f.copy S hmem ↔ s ∈ S

def Filter.comk {α : Type u_1} (p : Set α → Prop) (he : p ∅) (hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s) (hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)) : Filter α

Construct a filter from a property that is stable under finite unions. A set s belongs to Filter.comk p _ _ _ iff its complement satisfies the predicate p. This constructor is useful to define filters like Filter.cofinite.

Equations

• Filter.comk p he hmono hunion = { sets := {t : Set α | p tᶜ}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

@[simp]

theorem Filter.mem_comk {α : Type u_1} {p : Set α → Prop} {he : p ∅} {hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s} {hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)} {s : Set α} : s ∈ Filter.comk p he hmono hunion ↔ p sᶜ

def Filter.principal {α : Type u_1} (s : Set α) : Filter α

The principal filter of s is the collection of all supersets of s.

Equations

• Filter.principal s = { sets := {t : Set α | s ⊆ t}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

def Filter.term𝓟 : Lean.ParserDescr

The principal filter of s is the collection of all supersets of s.

Equations

• Filter.term𝓟 = Lean.ParserDescr.node `Filter.term𝓟 1024 (Lean.ParserDescr.symbol "𝓟")

@[simp]

theorem Filter.mem_principal {α : Type u_1} {s t : Set α} : s ∈ Filter.principal t ↔ t ⊆ s

instance Filter.instPure : Pure Filter

pure x is the set of sets that contain x. It is equal to 𝓟 {x} but with this definition we have s ∈ pure a defeq a ∈ s.

Equations

• Filter.instPure = { pure := fun {α : Type ?u.7} (x : α) => (Filter.principal {x}).copy {s : Set α | x ∈ s} ⋯ }

@[simp]

theorem Filter.mem_pure {α : Type u_1} {a : α} {s : Set α} : s ∈ pure a ↔ a ∈ s

def Filter.ker {α : Type u_1} (f : Filter α) : Set α

The kernel of a filter is the intersection of all its sets.

Equations

• f.ker = ⋂₀ f.sets

def Filter.join {α : Type u_1} (f : Filter (Filter α)) : Filter α

The join of a filter of filters is defined by the relation s ∈ join f ↔ {t | s ∈ t} ∈ f.

Equations

• f.join = { sets := {s : Set α | {t : Filter α | s ∈ t} ∈ f}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

@[simp]

theorem Filter.mem_join {α : Type u_1} {s : Set α} {f : Filter (Filter α)} : s ∈ f.join ↔ {t : Filter α | s ∈ t} ∈ f

instance Filter.instPartialOrder {α : Type u_1} : PartialOrder (Filter α)

Equations

• Filter.instPartialOrder = PartialOrder.mk ⋯

theorem Filter.le_def {α : Type u_1} {f g : Filter α} : f ≤ g ↔ ∀ x ∈ g, x ∈ f

instance Filter.instSupSet {α : Type u_1} : SupSet (Filter α)

Equations

• Filter.instSupSet = { sSup := fun (S : Set (Filter α)) => (Filter.principal S).join }

@[simp]

theorem Filter.mem_sSup {α : Type u_1} {s : Set α} {S : Set (Filter α)} : s ∈ sSup S ↔ ∀ f ∈ S, s ∈ f

@[irreducible]

def Filter.sInf {α : Type u_1} (s : Set (Filter α)) : Filter α

Infimum of a set of filters. This definition is marked as irreducible so that Lean doesn't try to unfold it when unifying expressions.

Equations

• Filter.sInf s = sSup (lowerBounds s)

instance Filter.instInfSet {α : Type u_1} : InfSet (Filter α)

Equations

• Filter.instInfSet = { sInf := Filter.sInf }

theorem Filter.sSup_lowerBounds {α : Type u_1} (s : Set (Filter α)) : sSup (lowerBounds s) = sInf s

instance Filter.instTop {α : Type u_1} : Top (Filter α)

Equations

• Filter.instTop = { top := (sSup (Set.range pure)).copy {s : Set α | ∀ (x : α), x ∈ s} ⋯ }

theorem Filter.mem_top_iff_forall {α : Type u_1} {s : Set α} : s ∈ ⊤ ↔ ∀ (x : α), x ∈ s

@[simp]

theorem Filter.mem_top {α : Type u_1} {s : Set α} : s ∈ ⊤ ↔ s = Set.univ

instance Filter.instBot {α : Type u_1} : Bot (Filter α)

Equations

• Filter.instBot = { bot := (sSup ∅).copy Set.univ ⋯ }

@[simp]

theorem Filter.mem_bot {α : Type u_1} {s : Set α} : s ∈ ⊥

instance Filter.instInf {α : Type u_1} : Min (Filter α)

The infimum of filters is the filter generated by intersections of elements of the two filters.

Equations

• Filter.instInf = { min := fun (f g : Filter α) => { sets := {s : Set α | ∃ a ∈ f, ∃ b ∈ g, s = a ∩ b}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } }

instance Filter.instSup {α : Type u_1} : Max (Filter α)

The supremum of two filters is the filter that contains sets that belong to both filters.

Equations

• Filter.instSup = { max := fun (f g : Filter α) => (sSup {f, g}).copy {s : Set α | s ∈ f ∧ s ∈ g} ⋯ }

class Filter.NeBot {α : Type u_1} (f : Filter α) : Prop

A filter is NeBot if it is not equal to ⊥, or equivalently the empty set does not belong to the filter. Bourbaki include this assumption in the definition of a filter but we prefer to have a CompleteLattice structure on Filter _, so we use a typeclass argument in lemmas instead.

• ne' : f ≠ ⊥

  The filter is nontrivial: f ≠ ⊥ or equivalently, ∅ ∉ f.

theorem Filter.neBot_iff {α : Type u_1} {f : Filter α} : f.NeBot ↔ f ≠ ⊥

def Filter.Eventually {α : Type u_1} (p : α → Prop) (f : Filter α) : Prop

f.Eventually p or ∀ᶠ x in f, p x mean that {x | p x} ∈ f. E.g., ∀ᶠ x in atTop, p x means that p holds true for sufficiently large x.

Equations

• Filter.Eventually p f = ({x : α | p x} ∈ f)

def Filter.«term∀ᶠ_In_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def Filter.«term∀ᶠ_In_,_» : Lean.ParserDescr

f.Eventually p or ∀ᶠ x in f, p x mean that {x | p x} ∈ f. E.g., ∀ᶠ x in atTop, p x means that p holds true for sufficiently large x.

Equations

• One or more equations did not get rendered due to their size.

def Filter.Frequently {α : Type u_1} (p : α → Prop) (f : Filter α) : Prop

f.Frequently p or ∃ᶠ x in f, p x mean that {x | ¬p x} ∉ f. E.g., ∃ᶠ x in atTop, p x means that there exist arbitrarily large x for which p holds true.

Equations

• Filter.Frequently p f = ¬∀ᶠ (x : α) in f, ¬p x

def Filter.«term∃ᶠ_In_,_» : Lean.ParserDescr

f.Frequently p or ∃ᶠ x in f, p x mean that {x | ¬p x} ∉ f. E.g., ∃ᶠ x in atTop, p x means that there exist arbitrarily large x for which p holds true.

Equations

• One or more equations did not get rendered due to their size.

def Filter.«term∃ᶠ_In_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def Filter.EventuallyEq {α : Type u_1} {β : Type u_2} (l : Filter α) (f g : α → β) : Prop

Two functions f and g are eventually equal along a filter l if the set of x such that f x = g x belongs to l.

Equations

• (f =ᶠ[l] g) = ∀ᶠ (x : α) in l, f x = g x

def Filter.«term_=ᶠ[_]_» : Lean.TrailingParserDescr

Two functions f and g are eventually equal along a filter l if the set of x such that f x = g x belongs to l.

Equations

• One or more equations did not get rendered due to their size.

def Filter.EventuallyLE {α : Type u_1} {β : Type u_2} [LE β] (l : Filter α) (f g : α → β) : Prop

A function f is eventually less than or equal to a function g at a filter l.

Equations

• (f ≤ᶠ[l] g) = ∀ᶠ (x : α) in l, f x ≤ g x

def Filter.«term_≤ᶠ[_]_» : Lean.TrailingParserDescr

A function f is eventually less than or equal to a function g at a filter l.

Equations

• One or more equations did not get rendered due to their size.

def Filter.map {α : Type u_1} {β : Type u_2} (m : α → β) (f : Filter α) : Filter β

The forward map of a filter

Equations

• Filter.map m f = { sets := Set.preimage m ⁻¹' f.sets, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

def Filter.Tendsto {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Prop

Filter.Tendsto is the generic "limit of a function" predicate. Tendsto f l₁ l₂ asserts that for every l₂ neighborhood a, the f-preimage of a is an l₁ neighborhood.

Equations

• Filter.Tendsto f l₁ l₂ = (Filter.map f l₁ ≤ l₂)

def Filter.comap {α : Type u_1} {β : Type u_2} (m : α → β) (f : Filter β) : Filter α

The inverse map of a filter. A set s belongs to Filter.comap m f if either of the following equivalent conditions hold.

1. There exists a set t ∈ f such that m ⁻¹' t ⊆ s. This is used as a definition.
2. The set kernImage m s = {y | ∀ x, m x = y → x ∈ s} belongs to f, see Filter.mem_comap'.
3. The set (m '' sᶜ)ᶜ belongs to f, see Filter.mem_comap_iff_compl and Filter.compl_mem_comap.

Equations

• Filter.comap m f = { sets := {s : Set α | ∃ t ∈ f, m ⁻¹' t ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

def Filter.prod {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) : Filter (α × β)

Product of filters. This is the filter generated by cartesian products of elements of the component filters.

Equations

• f.prod g = Filter.comap Prod.fst f ⊓ Filter.comap Prod.snd g

def Filter.coprod {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) : Filter (α × β)

Coproduct of filters.

Equations

• f.coprod g = Filter.comap Prod.fst f ⊔ Filter.comap Prod.snd g

instance Filter.instSProd {α : Type u_1} {β : Type u_2} : SProd (Filter α) (Filter β) (Filter (α × β))

Equations

• Filter.instSProd = { sprod := Filter.prod }

theorem Filter.prod_eq_inf {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) : f ×ˢ g = Filter.comap Prod.fst f ⊓ Filter.comap Prod.snd g

def Filter.bind {α : Type u_1} {β : Type u_2} (f : Filter α) (m : α → Filter β) : Filter β

The monadic bind operation on filter is defined the usual way in terms of map and join.

Unfortunately, this bind does not result in the expected applicative. See Filter.seq for the applicative instance.

Equations

• f.bind m = (Filter.map m f).join

def Filter.seq {α : Type u_1} {β : Type u_2} (f : Filter (α → β)) (g : Filter α) : Filter β

The applicative sequentiation operation. This is not induced by the bind operation.

Equations

• f.seq g = { sets := {s : Set β | ∃ u ∈ f, ∃ t ∈ g, ∀ m ∈ u, ∀ x ∈ t, m x ∈ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

def Filter.curry {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) : Filter (α × β)

This filter is characterized by Filter.eventually_curry_iff: (∀ᶠ (x : α × β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y). Useful in adding quantifiers to the middle of Tendstos. See hasFDerivAt_of_tendstoUniformlyOnFilter.

Equations

• f.curry g = f.bind fun (a : α) => Filter.map (fun (x : β) => (a, x)) g

instance Filter.instBind : Bind Filter

Equations

• Filter.instBind = { bind := @Filter.bind }

instance Filter.instFunctor : Functor Filter

Equations

• Filter.instFunctor = { map := @Filter.map, mapConst := fun {α β : Type ?u.8} => Filter.map ∘ Function.const β }

def Filter.lift {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Set α → Filter β) : Filter β

A variant on bind using a function g taking a set instead of a member of α. This is essentially a push-forward along a function mapping each set to a filter.

Equations

• f.lift g = ⨅ s ∈ f, g s

def Filter.lift' {α : Type u_1} {β : Type u_2} (f : Filter α) (h : Set α → Set β) : Filter β

Specialize lift to functions Set α → Set β. This can be viewed as a generalization of map. This is essentially a push-forward along a function mapping each set to a set.

Equations

• f.lift' h = f.lift (Filter.principal ∘ h)

def Filter.IsBounded {α : Type u_1} (r : α → α → Prop) (f : Filter α) : Prop

f.IsBounded r: the filter f is eventually bounded w.r.t. the relation r, i.e. eventually, it is bounded by some uniform bound. r will be usually instantiated with (· ≤ ·) or (· ≥ ·).

Equations

• Filter.IsBounded r f = ∃ (b : α), ∀ᶠ (x : α) in f, r x b

def Filter.IsBoundedUnder {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : Filter β) (u : β → α) : Prop

f.IsBoundedUnder (≺) u: the image of the filter f under u is eventually bounded w.r.t. the relation ≺, i.e. eventually, it is bounded by some uniform bound.

Equations

• Filter.IsBoundedUnder r f u = Filter.IsBounded r (Filter.map u f)

def Filter.IsCobounded {α : Type u_1} (r : α → α → Prop) (f : Filter α) : Prop

IsCobounded (≺) f states that the filter f does not tend to infinity w.r.t. ≺. This is also called frequently bounded. Will be usually instantiated with ≤ or ≥.

There is a subtlety in this definition: we want f.IsCobounded to hold for any f in the case of complete lattices. This will be relevant to deduce theorems on complete lattices from their versions on conditionally complete lattices with additional assumptions. We have to be careful in the edge case of the trivial filter containing the empty set: the other natural definition ¬ ∀ a, ∀ᶠ n in f, a ≤ n would not work as well in this case.

Equations

• Filter.IsCobounded r f = ∃ (b : α), ∀ (a : α), (∀ᶠ (x : α) in f, r x a) → r b a

def Filter.IsCoboundedUnder {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : Filter β) (u : β → α) : Prop

IsCoboundedUnder (≺) f u states that the image of the filter f under the map u does not tend to infinity w.r.t. ≺. This is also called frequently bounded. Will be usually instantiated with ≤ or ≥.

Equations

• Filter.IsCoboundedUnder r f u = Filter.IsCobounded r (Filter.map u f)

def Mathlib.Tactic.filterUpwards : Lean.ParserDescr

filter_upwards [h₁, ⋯, hₙ] replaces a goal of the form s ∈ f and terms h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f with ∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s. The list is an optional parameter, [] being its default value.

filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ is a short form for { filter_upwards [h₁, ⋯, hₙ], intros a₁ a₂ ⋯ aₖ }.

filter_upwards [h₁, ⋯, hₙ] using e is a short form for { filter_upwards [h1, ⋯, hn], exact e }.

Combining both shortcuts is done by writing filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e. Note that in this case, the aᵢ terms can be used in e.

Equations

• One or more equations did not get rendered due to their size.