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
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
Alex Kontorovich (Oct 07 2020 at 23:46):
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
Last updated: May 13 2021 at 06:15 UTC