convergent subsequence

Stream: new members

[Iocta]

I want "in a metric space, a subsequence of a convergent sequence is convergent." Where should I look? Or, if it doesn't exist, where should I start?

[Heather Macbeth]

May I ask what your intended application is? Most things in mathlib are written using filters rather than sequences, so unless your end goal actually involves sequences, you may have some "translation" to do.

[Iocta]

Just trying to get some practice with simple problems

[Iocta]

Maybe this is gonna be too awkward a place to start

[Heather Macbeth]

That makes sense, but mathlib may be the wrong source for such "simple problems" (since many things are written in the absolute maximal possible generality).

[Heather Macbeth]

Do you know about @Patrick Massot 's tutorial project?

[Heather Macbeth]

It is an introduction to Lean using real analysis

[Heather Macbeth]

in the "elementary" rather than "maximal possible generality" style.

[Iocta]

Found it, I'll see if I can get started there. Thanks

[Heather Macbeth]

You're welcome, and I'll see if I can find the "maximal possible generality" version of the theorem you were asking after, just so you can compare.

[Heather Macbeth]

This is arguably the lemma you initially asked for, with α and β the natural numbers, γ your metric space, f : α → β your subsequence, g : β → γ your sequence, x and ybeing filter.at_top, and z being the neighbourhoods of the limit.

[Kevin Buzzard]

You'll need to prove that the subsequence also tends to infinity, a consequence of injectivity of f