>>12033Let's assume for a moment that a number like ε satisfying
¥ 0 < ε < 1¥ 0 < ε < 0.1¥ 0 < ε < 0.01¥ 0 < ε < 0.001,and so on indefinitely, exists, and let's look at some properties that number would have.
I won't be proving these in Coq, at least for the moment, because we're talking about number systems that are different from the one I'm describing in the project. The basic assumptions I'm making about a number system containing ε are that it satisfies the properties of an ordered field, which means all the properties listed in
>>9492 except the least-upper-bound property.
First of all, ε is smaller than any positive rational number.
(A rational number is a number that can be written as a fraction with integers for the numerator and denominator. Since we are not French speakers, positive means greater than zero, and negative means less than zero; zero itself is neither positive nor negative.)
The proof: Given a positive rational number p/q, let n be the number of digits of q. Then 10^n, that is, 1 followed by n zeros, will be greater than q, and 1/10^n will be less than p/q. Since ε < 1/10^n, it is also less than p/q.
Since ε is positive, it's also obvious that ε is larger than any negative rational number.
Post too long. Click here to view the full text.