# Zulip Chat Archive

## Stream: maths

### Topic: continuous functions commute with limits v filters

#### Kevin Buzzard (Mar 07 2019 at 11:41):

If a sequence $a_n$ of real numbers tends to a limit $\ell$ as $n\to\infty$, and if $f:\mathbb{R}\to\mathbb{R}$ is continuous, then $f(a_n)\to f(\ell)$ as $n\to\infty$. This will follow from some general statement about limits of filters, probably called`tendsto.comp`

or something.

But there's an if and only if here -- I think $f:\mathbb{R}\to\mathbb{R}$ is continuous at $\ell$ if and only iff for all sequences $(a_n)$, $a_n\to\ell\implies f(a_n)\to f(\ell)$. Is this a special case of some statement about filters?

#### Kenny Lau (Mar 07 2019 at 11:44):

that's only true for first countable spaces so no?

#### Kenny Lau (Mar 07 2019 at 11:44):

but this is also the whole motivation behind sequences => nets => filters so maybe yes?

#### Kevin Buzzard (Mar 07 2019 at 11:46):

So is there some more general statement about a function being continuous if and only if some generalized notion of sequence tends to a limit? The countability comes in because nat is countable I guess?

#### Kenny Lau (Mar 07 2019 at 11:46):

we developed nets because we noticed that sequential continuity doesn't imply continuity

#### Kenny Lau (Mar 07 2019 at 11:47):

net is a generalization of sequences

#### Kenny Lau (Mar 07 2019 at 11:47):

somehow net continuity implies continuity

#### Kevin Buzzard (Mar 07 2019 at 11:47):

I don't know what nets are. I wrote some notes on them once.

#### Kenny Lau (Mar 07 2019 at 11:47):

and then people generalized nets to filters

#### Kevin Buzzard (Mar 07 2019 at 11:47):

But I then forgot.

#### Kenny Lau (Mar 07 2019 at 11:47):

So is there some more general statement about a function being continuous if and only if some generalized notion of sequence tends to a limit? The countability comes in because nat is countable I guess?

precisely

#### Kevin Buzzard (Mar 07 2019 at 11:47):

"I bet with my net I can get those things yet", Dr Seuss. That's how my notes started, and that's all I can remember about them :P

#### Kevin Buzzard (Mar 07 2019 at 11:48):

The kid catches Thing 1 and Thing 2 with his net when they're running amok.

#### Kevin Buzzard (Mar 07 2019 at 11:50):

#### Kenny Lau (Mar 07 2019 at 11:51):

great

#### Kevin Buzzard (Mar 07 2019 at 12:03):

"Remark: if f:X→Y is a map of topological spaces, then f is continuous at x in X iff for every net (x_s) converging to x, f(x_s) converges to f(x). " (plus reference to proof)

#### Kevin Buzzard (Mar 07 2019 at 12:03):

So what is the relation between nets and filters, are nets in Lean, and is this statement, or some more general statement which implies it, in Lean?

#### Patrick Massot (Mar 07 2019 at 12:58):

Nets and filters are equivalent notions. Nets look like they are almost sequences, but filters are more functorial

#### Patrick Massot (Mar 07 2019 at 12:59):

The lemma you are referring to is so trivial it doesn't seem to be in mathlib. But you add it:

lemma cont_kevin {α : Type*} {β : Type*} [topological_space α] [topological_space β] (f : α → β) (x : α) : continuous_at f x ↔ ∀ F : filter α, F ≤ nhds x → map f F ≤ nhds (f x) := ⟨λ h F F_le, le_trans (map_mono F_le) h, λ h, h _ (le_refl _)⟩

Last updated: May 14 2021 at 19:21 UTC