Increasing convergent subsequence

Stream: maths

[Koundinya Vajjha]

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

[Kevin Buzzard]

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]

Yes I'm working with nnreal.

[Kevin Buzzard]

Wait I don't mean Bolzano Weierstrass

[Kevin Buzzard]

I mean the assertion that a sequence has a monotonic subsequence

[Kevin Buzzard]

This is just some basic fact about total orders

[Kevin Buzzard]

You look at the peaks of the sequence

[Koundinya Vajjha]

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

[Mario Carneiro]

it's not proven in mathlib AFAIK

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Koundinya Vajjha]

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]

wait that's a lot easier

[Mario Carneiro]

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

[Koundinya Vajjha]

Yes

[Mario Carneiro]

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

[Koundinya Vajjha]

Can you elaborate?

[Koundinya Vajjha]

I thought I needed an increasing subsequence

[Mario Carneiro]

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

[Koundinya Vajjha]

Oh! I see!

[Mario Carneiro]

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