7.4. Operations on filters🔗

Sometimes you need to read filter algebra rather than write a limit: a proof you are following pivots through ≤, Filter.map, Filter.comap, or ×ˢ, or you want to reshape a Tendsto goal into an equivalent one. This entry explains what those operations mean and the goal each one serves.

7.4.1. The order on filters🔗

F ≤ G reads as "F is finer than {lean}G": every {lean}G-eventual set is already {lean}F-eventual. A finer filter carries more constraints and sits closer to "a single point".

This order is what lets you weaken a limit. Say you have Tendsto f G (𝓝 L) and want Tendsto f F (𝓝 L) for a finer source F ≤ G. Then Filter.Tendsto.mono_left reduces the goal to proving F ≤ G: convergence along a coarser filter implies convergence along any finer one. For instance a two-sided limit gives the one-sided limit, because 𝓝[>] a ≤ 𝓝 a.

The mnemonic that prevents the sign-flip everyone trips over: on principal filters, the order is just inclusion of the underlying sets:

example (s t : Set α) :
    𝓟 s ≤ 𝓟 t ↔ s ⊆ t :=
  Filter.principal_mono

The lattice on Filter α:

Filter	"Eventually in this filter" means
`F ⊓ G`	eventually for both `F` and `G`
`F ⊔ G`	eventually for either `F` or `G`
`⊥`	every set is `⊥`-eventual (vacuous; see `NeBot` below)
`⊤`	only `Set.univ` is `⊤`-eventual ("everywhere")

This is exactly why nhdsWithin x s = 𝓝 x ⊓ 𝓟 s: "near x and in s":

example (x : X) (s : Set X) :
    𝓝[s] x = 𝓝 x ⊓ 𝓟 s :=
  rfl

7.4.2. Push-forward and pull-back: `Filter.map` and `Filter.comap`🔗

For f : α → β:

Filter.map f F : Filter β is the push-forward. A set t is map f F-eventual iff its preimage f ⁻¹' t is F-eventual.
Filter.comap f G : Filter α is the pull-back. A set s is comap f G-eventual iff it contains the preimage of some G-eventual set.

These are the algebraic content of Tendsto. By definition:

example (f : α → β) (F : Filter α) (G : Filter β) :
    Tendsto f F G ↔ Filter.map f F ≤ G :=
  Iff.rfl

Filter.map and Filter.comap form a GaloisConnection:

example (f : α → β) (F : Filter α) (G : Filter β) :
    Filter.map f F ≤ G ↔ F ≤ Filter.comap f G :=
  Filter.map_le_iff_le_comap

When you read a proof that pivots through Filter.map or Filter.comap, the author is manipulating filters algebraically. A common shape is Tendsto u (atTop.comap φ) _, which expresses "a limit along the subsequence φ" as a Tendsto along atTop.

7.4.3. Joint limits with the product (`×ˢ`)🔗

F ×ˢ G : Filter (α × β) (called prod in theorem names) is the product filter: a set is F ×ˢ G-eventual iff it contains a rectangle s ×ˢ t with s ∈ F and t ∈ G. The notation ×ˢ covers both the product of sets and filters; the elaborator disambiguates from the types.

The single fact that drives every joint-limit proof:

example (x : α) (y : β) :
    𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y :=
  nhds_prod_eq

So a two-variable continuity statement is just a Tendsto on a product filter:

example (x y : ℝ) :
    Tendsto (fun p : ℝ × ℝ => p.1 + p.2)
      (𝓝 (x, y)) (𝓝 (x + y)) := byx:ℝy:ℝ⊢ Tendsto (fun p => p.1 + p.2) (𝓝 (x, y)) (𝓝 (x + y))
  rw [nhds_prod_eqx:ℝy:ℝ⊢ Tendsto (fun p => p.1 + p.2) (𝓝 x ×ˢ 𝓝 y) (𝓝 (x + y))]x:ℝy:ℝ⊢ Tendsto (fun p => p.1 + p.2) (𝓝 x ×ˢ 𝓝 y) (𝓝 (x + y))
  -- New goal: Tendsto _ (𝓝 x ×ˢ 𝓝 y) (𝓝 (x + y))
  exact tendsto_fst.add tendsto_sndAll goals completed! 🐙

This is exactly how Mathlib phrases continuity of two-variable operations (+, *, •). To go the other way (package two continuous functions into a product), reach for Continuous.prodMk.

7.4.4. `NeBot`: when a filter isn't trivial🔗

Filter.NeBot l is the typeclass asserting l ≠ ⊥. Many limit lemmas (anything that pulls a witness out of a ∀ᶠ, in particular) require it, because over ⊥ everything is vacuously true. Common instances fire automatically:

atTop on a nonempty [SemilatticeSup α] (the instance is Filter.atTop_neBot).
𝓝 x in any topological space.
Filter.map f F whenever F is non-trivial.

The instance for atTop requires [Nonempty α]; forget it and typeclass synthesis fails:

open Filter in
example {α : Type*} [SemilatticeSup α] (s : Set α)
    (hs : ∀ᶠ x in (atTop : Filter α), x ∈ s) : s.Nonempty :=
  failed to synthesize instance of type class
  atTop.NeBot

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.hs.exists

failed to synthesize instance of type class
  atTop.NeBot

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

Adding [Nonempty α] to the variables makes Filter.atTop_neBot fire and the proof goes through.

7.4.5. Reference: the standard filters🔗

Every limit in this chapter is a Tendsto (or ∀ᶠ) between two of the filters below. To translate a classical statement, read off the source and target from this table.

Filter	Lives on	"Eventually in this filter" means
`𝓝 x`	a `TopologicalSpace`	near the point `x`
`𝓝[s] x`	within a subset	near `x`, restricted to `s`
`𝓝[>] x`, `𝓝[<] x`	an order topology	from the right/left of `x`
`Filter.atTop`	a `Preorder`	for sufficiently large input
`Filter.atBot`	a `Preorder`	for sufficiently small input
`Filter.cofinite`	any type	for all but finitely many points
`ae μ`	a measure space	for almost every point
`Filter.principal s`	any	exactly inside `s`
`⊤`	any	everywhere (only `Set.univ` is in `⊤`)
`⊥`	any	vacuously (every set is in `⊥`; see the Limit statements gotcha)

7.4. Operations on filters🔗

7.4.1. The order on filters🔗

7.4.2. Push-forward and pull-back: Filter.map and Filter.comap🔗

7.4.3. Joint limits with the product (×ˢ)🔗

7.4.4. NeBot: when a filter isn't trivial🔗

7.4.5. Reference: the standard filters🔗

7.4.2. Push-forward and pull-back: `Filter.map` and `Filter.comap`🔗

7.4.3. Joint limits with the product (`×ˢ`)🔗

7.4.4. `NeBot`: when a filter isn't trivial🔗