Zulip Chat Archive

Stream: maths

Topic: Increasing convergent subsequence


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Koundinya Vajjha (Jul 19 2019 at 18:46):

Yes I'm working with nnreal.

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 18:46):

Wait I don't mean Bolzano Weierstrass

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 18:47):

I mean the assertion that a sequence has a monotonic subsequence

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 18:47):

This is just some basic fact about total orders

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 18:47):

You look at the peaks of the sequence

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 19 2019 at 18:48):

it's not proven in mathlib AFAIK

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 18:49):

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

view this post on Zulip Mario Carneiro (Jul 19 2019 at 18:51):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 19 2019 at 18:52):

wait that's a lot easier

view this post on Zulip Mario Carneiro (Jul 19 2019 at 18:53):

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

view this post on Zulip Koundinya Vajjha (Jul 19 2019 at 18:53):

Yes

view this post on Zulip Mario Carneiro (Jul 19 2019 at 18:54):

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

view this post on Zulip Koundinya Vajjha (Jul 19 2019 at 18:54):

Can you elaborate?

view this post on Zulip Koundinya Vajjha (Jul 19 2019 at 18:55):

I thought I needed an increasing subsequence

view this post on Zulip Mario Carneiro (Jul 19 2019 at 18:55):

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

view this post on Zulip Koundinya Vajjha (Jul 19 2019 at 18:56):

Oh! I see!

view this post on Zulip 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