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

nets.pdf

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