Talk:Cauchy Sequence Is Eventually Bounded Away From Zero

This proof looks fine, but the title is a bit imprecise: a Cauchy sequence is only eventually bounded away from zero if that is not its limit :-)

I would also formulate it more generally to state that it is bounded away from everything that is not its limit (in the proof, just replace 0 by any non-limit).

Something like "Cauchy Sequence Is Eventually Bounded Away From Non-Limit".

No point. The only reason for this is to allow the use of an eventually non-zero Cauchy sequence as the denominator in a quotient of such sequences. --prime mover (talk) 10:00, 4 October 2018 (EDT)

OK, so then "Cauchy Sequence with Nonzero Limit Is Eventually Bounded Away From Zero" -- but I agree it is getting a bit long. KarlFrei (talk) 11:20, 4 October 2018 (EDT)

I wouldn't bother. There's no big need to worry about this as its scope is limited. --prime mover (talk) 11:31, 4 October 2018 (EDT)

But I will bother. My inner perfectionist won't rest while this blemish remains.

I'm not a fan of the title "Cauchy Sequence with Nonzero Limit Is Eventually Bounded Away From Zero" since it implies to me that the Cauchy sequence has a limit that is nonzero.

I am a fan of "Cauchy Sequence Is Eventually Bounded Away From Non-Limit" and of generalising the to any non-limit.

--Leigh.Samphier (talk) 07:21, 5 October 2018 (EDT)

It's not a blemish. This result is complete and correct. If you want to write another proof with a different name and a different content, feel free. --prime mover (talk) 07:28, 5 October 2018 (EDT)