Zulip Chat Archive

Stream: maths

Topic: Characterizing tendsto using sequences


view this post on Zulip Gabriel Ebner (Oct 10 2019 at 11:01):

Do we have anything like this already?

lemma tendsto_iff_seq_tendsto {β} (f : α  β) (k : filter α) (l : filter β)
    (hcb : k.has_countable_basis) :
  tendsto f k l  ( x :   α, tendsto x at_top k  tendsto (f  x) at_top l) :=

view this post on Zulip Patrick Massot (Oct 10 2019 at 11:34):

Did you look in https://github.com/leanprover-community/mathlib/blob/master/src/topology/sequences.lean?

view this post on Zulip Sebastien Gouezel (Oct 10 2019 at 11:44):

continuous_iff_sequentially_continuous is essentially your statement, albeit in a more restricted setting. It could be useful to prove your version, and deduce continuous_iff_sequentially_continuous from it.

view this post on Zulip Gabriel Ebner (Oct 10 2019 at 12:09):

I'm not sure if continuous_iff_sequentially_continuous is a special case of my statement. There are sequential spaces that are not first-countable.

view this post on Zulip Sebastien Gouezel (Oct 10 2019 at 12:55):

You're right, these statements are independent.


Last updated: May 11 2021 at 16:22 UTC