## Stream: maths

### Topic: Characterizing tendsto using sequences

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


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

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

#### Sebastien Gouezel (Oct 10 2019 at 12:55):

You're right, these statements are independent.

Last updated: May 11 2021 at 16:22 UTC