continuous functions commute with limits v filters

Stream: maths

[Kevin Buzzard]

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]

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

[Kenny Lau]

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

[Kevin Buzzard]

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]

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

[Kenny Lau]

net is a generalization of sequences

[Kenny Lau]

somehow net continuity implies continuity

[Kevin Buzzard]

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

[Kenny Lau]

and then people generalized nets to filters

[Kevin Buzzard]

But I then forgot.

[Kenny Lau]

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]

"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]

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

[Kevin Buzzard]

nets.pdf

[Kenny Lau]

great

[Kevin Buzzard]

"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]

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]

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

[Patrick Massot]

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 _)⟩