coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Non decreasing natural number sequence convergence

From: Saulo Araujo <saulo2 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Non decreasing natural number sequence convergence
Date: Fri, 13 Feb 2015 09:58:45 -0300

Hi,

Does the Coq standard library or any public available library has the proof for the theorem below (or one similar)? It basically says that non decreasing natural number sequences are convergent.

Theorem convergence_t1 :

forall (f : nat -> nat),

(forall n, f (S n) >= f n /\ exists l, forall n, f n <= l) ->

exists N L, forall n, n >= N -> f n = L.

Thanks,

Saulo

[Coq-Club] Non decreasing natural number sequence convergence, Saulo Araujo, 02/13/2015
- Re: [Coq-Club] Non decreasing natural number sequence convergence, Amin Timany, 02/13/2015
  - Re: [Coq-Club] Non decreasing natural number sequence convergence, Saulo Araujo, 02/13/2015
    - Re: [Coq-Club] Non decreasing natural number sequence convergence and the mathematical proof language., Michel Levy, 02/15/2015
      - Re: [Coq-Club] Non decreasing natural number sequence convergence and the mathematical proof language., Saulo Araujo, 02/15/2015