Zulip Chat Archive

Stream: maths

Topic: continuous functions commute with limits v filters


view this post on Zulip Kevin Buzzard (Mar 07 2019 at 11:41):

If a sequence ana_n of real numbers tends to a limit \ell as nn\to\infty, and if f:RRf:\mathbb{R}\to\mathbb{R} is continuous, then f(an)f()f(a_n)\to f(\ell) as nn\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:RRf:\mathbb{R}\to\mathbb{R} is continuous at \ell if and only iff for all sequences (an)(a_n), anf(an)f()a_n\to\ell\implies f(a_n)\to f(\ell). Is this a special case of some statement about filters?

view this post on Zulip Kenny Lau (Mar 07 2019 at 11:44):

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

view this post on Zulip Kenny Lau (Mar 07 2019 at 11:44):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Mar 07 2019 at 11:46):

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

view this post on Zulip Kenny Lau (Mar 07 2019 at 11:47):

net is a generalization of sequences

view this post on Zulip Kenny Lau (Mar 07 2019 at 11:47):

somehow net continuity implies continuity

view this post on Zulip Kevin Buzzard (Mar 07 2019 at 11:47):

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

view this post on Zulip Kenny Lau (Mar 07 2019 at 11:47):

and then people generalized nets to filters

view this post on Zulip Kevin Buzzard (Mar 07 2019 at 11:47):

But I then forgot.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 07 2019 at 11:48):

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

view this post on Zulip Kevin Buzzard (Mar 07 2019 at 11:50):

nets.pdf

view this post on Zulip Kenny Lau (Mar 07 2019 at 11:51):

great

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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