monotone convergence for real sequences

Stream: Is there code for X?

[Moritz Firsching]

I have the feeling that this should already be in mathlib, but I can't find it (nor the other version with strictly increasing).

import tactic
import topology.instances.nnreal
import data.real.basic
import data.nat.basic
import order.filter
import topology.basic

open real
open filter
open nat

open_locale filter topological_space


lemma monotone_convergence (a : ℕ → ℝ) (c : ℝ)
(h_strictly_decreasing: ∀ (n : ℕ),  a n > a n.succ)
(h_bounded: ∀ (n : ℕ), a n > c):
∃ (b : ℝ), tendsto (λ (n : ℕ),  a n) at_top (𝓝  b) :=
begin
 use (Inf {(a n : ℝ)| (n:ℕ)}),
 intros R hr,
 simp only [mem_map, mem_at_top_sets, ge_iff_le, set.mem_preimage],
 sorry,
end

Any help/pointers are highly appreciated!

[Yaël Dillies]

The relevant file is file#topology/algebra/order/monotone_convergence

[Moritz Firsching]

thanks, that looks very promising!