Characterizing tendsto using sequences

Stream: maths

[Gabriel Ebner]

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) :=

[Patrick Massot]

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

[Sebastien Gouezel]

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.

[Gabriel Ebner]

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.

[Sebastien Gouezel]

You're right, these statements are independent.