# 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 `(· ≥ ·)`.

## Notation #

- `∀ᶠ 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]

source
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.

Instances For

source
theorem Filter.filter_eq {α : Type u_1} {f g : Filter α} :
f.sets = g.sets → f = g
source
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 }

source
theorem Filter.ext {α : Type u_1} {f g : Filter α} (h : ∀ (s : Set α), s ∈ f ↔ s ∈ g) :
f = g
source
theorem Filter.ext_iff {α : Type u_1} {f g : Filter α} :
f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
source
@[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
source
@[simp]
theorem Filter.mem_sets {α : Type u_1} {f : Filter α} {s : Set α} :
s ∈ f.sets ↔ s ∈ f
source
@[simp]
theorem Filter.univ_mem {α : Type u_1} {f : Filter α} :
Set.univ ∈ f
source
theorem Filter.mem_of_superset {α : Type u_1} {f : Filter α} {x y : Set α} (hx : x ∈ f) (hxy : x ⊆ y) :
y ∈ f
source
theorem Filter.univ_mem' {α : Type u_1} {f : Filter α} {s : Set α} (h : ∀ (a : α), a ∈ s) :
s ∈ f
source
theorem Filter.inter_mem {α : Type u_1} {f : Filter α} {s t : Set α} (hs : s ∈ f) (ht : t ∈ f) :
s ∩ t ∈ f
source
theorem Filter.mp_mem {α : Type u_1} {f : Filter α} {s t : Set α} (hs : s ∈ f) (h : {x : α | x ∈ s → x ∈ t} ∈ f) :
t ∈ f
source
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 := ⋯ }

Instances For

source
@[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
source
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 := ⋯ }

Instances For

source
@[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 ∈ comk p he hmono hunion ↔ p s ᶜ
source
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 := ⋯ }

Instances For

source
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 "𝓟")

Instances For

source
@[simp]
theorem Filter.mem_principal {α : Type u_1} {s t : Set α} :
s ∈ principal t ↔ t ⊆ s
source
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.6} (x : α) => (Filter.principal {x}).copy {s : Set α | x ∈ s} ⋯ }

source
@[simp]
theorem Filter.mem_pure {α : Type u_1} {a : α} {s : Set α} :
s ∈ pure a ↔ a ∈ s
source
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

Instances For

source
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 := ⋯ }

Instances For

source
@[simp]
theorem Filter.mem_join {α : Type u_1} {s : Set α} {f : Filter (Filter α)} :
s ∈ f.join ↔ {t : Filter α | s ∈ t} ∈ f
source
instance Filter.instPartialOrder {α : Type u_1} :
PartialOrder (Filter α)
Equations

- Filter.instPartialOrder = { le := fun (f g : Filter α) => ∀ ⦃U : Set α⦄, U ∈ g → U ∈ f, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

source
theorem Filter.le_def {α : Type u_1} {f g : Filter α} :
f ≤ g ↔ ∀ x ∈ g, x ∈ f
source
instance Filter.instSupSet {α : Type u_1} :
SupSet (Filter α)
Equations

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

source
@[simp]
theorem Filter.mem_sSup {α : Type u_1} {s : Set α} {S : Set (Filter α)} :
s ∈ sSup S ↔ ∀ f ∈ S, s ∈ f
source
@[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)

Instances For

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

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

source
theorem Filter.sSup_lowerBounds {α : Type u_1} (s : Set (Filter α)) :
sSup (lowerBounds s) = sInf s
source
instance Filter.instTop {α : Type u_1} :
Top (Filter α)
Equations

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

source
theorem Filter.mem_top_iff_forall {α : Type u_1} {s : Set α} :
s ∈ ⊤ ↔ ∀ (x : α), x ∈ s
source
@[simp]
theorem Filter.mem_top {α : Type u_1} {s : Set α} :
s ∈ ⊤ ↔ s = Set.univ
source
instance Filter.instBot {α : Type u_1} :
Bot (Filter α)
Equations

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

source
@[simp]
theorem Filter.mem_bot {α : Type u_1} {s : Set α} :
s ∈ ⊥
source
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 := ⋯ } }

source
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} ⋯ }

source
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`.

Instances

source
theorem Filter.neBot_iff {α : Type u_1} {f : Filter α} :
f.NeBot ↔ f ≠ ⊥
source
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)

Instances For

source
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.

Instances For

source
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

Instances For

source
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.

Instances For

source
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

Instances For

source
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.

Instances For

source
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

Instances For

source
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.

Instances For

source
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 := ⋯ }

Instances For

source
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₂)

Instances For

source
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 := ⋯ }

Instances For

source
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

Instances For

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

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

Equations

- Filter.instSProd = { sprod := fun (f : Filter α) (g : Filter β) => Filter.comap Prod.fst f ⊓ Filter.comap Prod.snd g }

source
theorem Filter.prod_eq_inf {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) :
f ×ˢ g = comap Prod.fst f ⊓ comap Prod.snd g
source
def Filter.pi {ι : Type u_3} {α : ι → Type u_4} (f : (i : ι) → Filter (α i)) :
Filter ((i : ι) → α i)

The product of an indexed family of filters.

Equations

- Filter.pi f = ⨅ (i : ι), Filter.comap (Function.eval i) (f i)

Instances For

source
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

Instances For

source
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 := ⋯ }

Instances For

source
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 `Tendsto`s. See `hasFDerivAt_of_tendstoUniformlyOnFilter`.

Equations

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

Instances For

source
instance Filter.instBind :
Bind Filter
Equations

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

source
instance Filter.instFunctor :
Functor Filter
Equations

- Filter.instFunctor = { map := @Filter.map }

source
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

Instances For

source
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)

Instances For

source
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

Instances For

source
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)

Instances For

source
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

Instances For

source
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)

Instances For

source
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ₙ], intro 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.

Instances For