Re: Does the number of nines increase?

On 6/28/2024 9:41 AM, WM wrote:

Le 28/06/2024 à 02:03, Richard Damon a écrit :

[...]

>
A non-terminating digit sequence
does not determine a real number.

A non.terminating decimal determines
no less than one real number (line.point) and
no more than one real number (line.point).
⎛ For each split of the line,
⎜ the split is _situated_ ==
⎜ there is a point _at_ the split,
⎝ last in the fore.split or first in the hind.split.
A non.terminating decimal determines
no less than one real number (line.point).
A non.terminating decimal determines
a split of _terminating_ decimals
into _fore.decimals_ and _hind.decimals_
(finite.length and too.low or too.high)
There is a line.point at the split.
The non.terminating decimal determines it.
A non.terminating decimal determines
no more than one real number (line.point).
⎛ For each fore.decimal,hind.decimal pair which
⎜ is a distance d apart,
⎜ there is a fore.decimal,hind.decimal pair which
⎝ is a distance ⅒⋅d apart.
| Assume there are two line.points between
| all fore.decimal,hind.decimal pairs
| (points determined by the non.terminating decimal).
| The two points are a distance > 0 apart.
|
| The greatest.lower.bound β of
| fore.decimal,hind.decimal distances is > 0
| 10⋅β > β > ⅒⋅β > 0
|
| ⅒⋅β is a lower.bound
|
| 10⋅β isn't a lower.bound
| There is a pair closer than 10⋅β
| There is a pair closer than ⅒⋅10⋅β
| There is a pair closer than ⅒⋅⅒⋅10⋅β
| ⅒⋅β isn't a lower.bound.
| Contradiction.
Therefore,
A non.terminating decimal determines
no more than one real number (line.point).
Therefore,
A non.terminating decimal determines
exactly one real number (line.point).