## Stream: maths

### Topic: Increasing convergent subsequence

#### Koundinya Vajjha (Jul 19 2019 at 18:38):

Is there a result in mathlib which constructs a monotone convergent subsequence out of a convergent sequence?

#### Kevin Buzzard (Jul 19 2019 at 18:45):

Of reals? I think Bolzano Weierstrass is in there somewhere and it's relatively straightforward from there, the statement about a subsequence tending to the same thing as the sequence will just be some filter magic

#### Koundinya Vajjha (Jul 19 2019 at 18:46):

Yes I'm working with nnreal.

#### Kevin Buzzard (Jul 19 2019 at 18:46):

Wait I don't mean Bolzano Weierstrass

#### Kevin Buzzard (Jul 19 2019 at 18:47):

I mean the assertion that a sequence has a monotonic subsequence

#### Kevin Buzzard (Jul 19 2019 at 18:47):

This is just some basic fact about total orders

#### Kevin Buzzard (Jul 19 2019 at 18:47):

You look at the peaks of the sequence

#### Koundinya Vajjha (Jul 19 2019 at 18:47):

Can you point me to the result? I'm new to filters/sequences and I have no idea where to look

#### Mario Carneiro (Jul 19 2019 at 18:48):

it's not proven in mathlib AFAIK

#### Kevin Buzzard (Jul 19 2019 at 18:49):

I don't know my way around that part of the library

#### Mario Carneiro (Jul 19 2019 at 18:51):

What do you need it for? It looks like a pretty gimmicky result to me

#### Koundinya Vajjha (Jul 19 2019 at 18:52):

Here is my set-up. I have a set K and have proven that there is a sequence x : nat -> K such that x n tends to Sup K. I need to prove that the interval Icc (Sup K) tis the intersection of the intervals Icc (x n) t where t is a fixed nnreal.

#### Mario Carneiro (Jul 19 2019 at 18:52):

wait that's a lot easier

#### Mario Carneiro (Jul 19 2019 at 18:53):

because it's not just monotone it's monotone increasing

Yes

#### Mario Carneiro (Jul 19 2019 at 18:54):

Actually you don't even need that, this is just the definition of Sup

#### Koundinya Vajjha (Jul 19 2019 at 18:54):

Can you elaborate?

#### Koundinya Vajjha (Jul 19 2019 at 18:55):

I thought I needed an increasing subsequence

#### Mario Carneiro (Jul 19 2019 at 18:55):

Sup K <= a iff for all k in K, k <= a

Oh! I see!

#### Mario Carneiro (Jul 19 2019 at 18:56):

For any k in K, either k = Sup K or there exists k <= x n < Sup K

Last updated: May 14 2021 at 18:28 UTC