Re: Replacement of Cardinality

On 8/14/2024 8:23 AM, WM wrote:

Le 13/08/2024 à 19:02, Jim Burns a écrit :

On 8/13/2024 10:21 AM, WM wrote:

The function NUF(x) is a step-function.
It can increase from 0 at x = 0 to greater values,
either in a step of size 1
or in a step of size more than 1.
But increase by more than 1 is excluded by
the gaps between unit fractions.
(Note the universal quantifier there,
according to which never –
in no limit and in no accumulation point –
two unit fractions occupy the same point x.)
Therefore
the step size can only be 1,

>
...at a unit.fraction.
0 isn't a unit.fraction.

>
Therefore there is no step at 0.

There is a step at 0.
Each unit.fractionᵈᵉᶠ has GLB β > 0
which other unit.fractionsᵈᵉᶠ are
at least as far as.
However,
0 is not a unit.fractionᵈᵉᶠ.
0 does not have GLB β > 0
which unit.fractionsᵈᵉᶠ are
at least as far as.
⎛ Otherwise,
⎝ ½⋅β is lower.bound and not.lower.bound.
∀ᴿx > 0:  NUFᵈᵉᶠ(x) > 0
∀ᴿx > 0:  NUF(x) ≥ NUF(x)ᵈᵉᶠ > 0
There is a step at 0.
⎛ Otherwise,
⎝ ½⋅β is lower.bound and not.lower.bound.
⎛
⎜ Assume otherwise.
⎜ Assume β > 0 for
⎜ β greatest.lower.bound of unit.factionsᵈᵉᶠ
⎜
⎜ ½⋅β < β lower.bound
⎜
⎜ 2⋅β > β not.lower.bound
⎜ 2⋅β > ⅟k smaller unit.fractionᵈᵉᶠ
⎜ ¼⋅2⋅β > ¼⋅⅟k smaller unit.fractionᵈᵉᶠ
⎜ ¼⋅2⋅β = ½⋅β
⎜ ½⋅β > ¼⋅⅟k not.lower.bound
⎜
⎝ ½⋅β is lower.bound and not.lower.bound.

resulting in a real coordinate x with NUF(x) = 1.

>
INVNUF(1) > ⅟ ⌊⅟INVNUF(1) +1⌋ > ⅟ ⌊⅟INVNUF(1) +2⌋
NUF(INVNUF(1)) > 1

>
No.

Is "No" an argument?