# [isabelle] Convergence for Extended Reals

Dear all,

`I have a sequence of extended reals (f :: nat => ereal), of which I know that two
``consecutive numbers differ by ever smaller amounts. In detail, I have
`
abs (f (Suc n) - f n) < c / 2 ^ n

`for some fixed c > 0 and all n, and I'd like to prove that f converges, i.e., the limit
``"lim f" exists. What is the best way to prove this?
`
Unfortunately, f is not monotonically increasing, so I cannot use SUP instead of lim.

`On ereal, I have not found the lemma convergent_ereal, but that did not get me much
``further. So I tried to do a case distinction on whether f is always a real and try to
``prove "Cauchy (real o f)". but I have not found many useful lemmas about Cauchy either.
``Probably I can prove everything by using metric_CauchyI, but this looks like a lot of
``arithmetic on reals. Is there something more abstract?
`
Best,
Andreas

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*