## Stream: new members

### Topic: bounding limits cont'd

#### Alex Kontorovich (Oct 07 2020 at 17:57):

Hello, Can I please get some help on what theorem I can use to prove this?

theorem cau_lim_le (f : cau_seq ℝ abs) (g : cau_seq ℝ abs) : (∃ j, ∀ i, j ≤ i → f i ≤ g i) → f.lim ≤ g.lim :=
begin
intros,
sorry,
end


Thank you!

#### Alex J. Best (Oct 07 2020 at 20:19):

I'm not an expert on this part of the library so hopefully someone can chime in with a better way, but I tried to use the lemma
le_of_tendsto_of_tendsto which phrases everything in terms of docs#filter.eventually, it takes a little work to line that up with the form you have though.

import topology.metric_space.cau_seq_filter
theorem cau_lim_le (f : cau_seq ℝ abs) (g : cau_seq ℝ abs) : (∃ j, ∀ i, j ≤ i → f i ≤ g i) → f.lim ≤ g.lim :=
begin
intros,
refine le_of_tendsto_of_tendsto (cau_seq.tendsto_limit _) (cau_seq.tendsto_limit _) _,
rwa [filter.eventually_le, filter.eventually_at_top],
end


Thank you!!!

#### Yury G. Kudryashov (Oct 08 2020 at 02:19):

cau_seq.tendsto_limit is the main way to deal with cau_seqs. E.g., this will require very few modifications once we port exp to analytic functions.

#### Yury G. Kudryashov (Oct 08 2020 at 02:20):

We have many theorems about tendsto and much less about cau_seq.

Last updated: May 13 2021 at 06:15 UTC