[Haskell-cafe] Re: Re: Re: 0/0 > 1 == False

[Ben Franksen]

Kalman Noel wrote:
> Ben Franksen wrote:
>> Kalman Noel wrote:
>> >     (2) lim a_n  = ∞
> [...]
>> >     (2) means that the sequence does not converge, because you can
>> >         always find a value that is /larger/ than what you hoped might
>> >         be the limit.
>>
>> (2) usually rather mean that for each positive limit A there is a number
>> N such that a_N > A for /all/ n > N.
> 
> You're right here. I tried to come up with a more wordy, informal
> description, but failed on that.
> 
>> Your definition of (2) is usually termed as '(a_n) contains a subsequence
>> that tends toward +infinity'.
> 
> May you elaborate? I don't see where a subsequence comes into play here.

I'll show (2) <=> (2'), where

(2'): (a_n) contains a subsequence that tends toward +infinity

"=>" : Assume (2) holds. Construct a subsequence (b_m) of (a_n) by chosing,
for each natural number m, an index n_m such that b_m = n_(n_m) is larger
than m (which is possible by (2)). Then (b_m) is a subsequence of (a_n)
that tends toward infinity (as I defined it).

"<=" : Assume (2') holds. Let A > 0 be any positive number (that you "hope
might be the limit"). We want to show that we can find N such that a_N > A.
To do so, chose a M, such that b_M > A (which is possible by assumption).
Then there exists an N such that a_N = b_M, because (b_n) is a subsequence
of (a_n).

q.e.d

Cheers
Ben