On 4/5/2024 10:37 PM, Ross Finlayson wrote:
On 04/05/2024 11:04 AM, Jim Burns wrote:
[...]
>
I usually write that n/d with
n as "numerator" and d as "denominator".
Of course you do. I stand corrected.
It's not identified which f(n) is 1/root2,
only that it exists.
There's that for each r in [0,1],
exists n s.t. f(n) = r,
and f^-1(r) = n, mostly infinite.
I don't see how ⅟√̅2 is known to exist in [0,1]ᴿꟳ
from the definition
[0,1]ᴿꟳ =
lim[d→∞, d∈ℕ⁺] lim[n→d, n∈ℕ] n/d =
lim[d→∞, d∈ℕ⁺] {n/d: 0≤n≤d, n∈ℕ}
Or, more generally, what supports a claim that
[0,1]ᴿꟳ = [0,1]ᶜᵒⁿᵗⁱⁿᵘᵘᵐ
I gave an example of what would support
such a claim, from a different definition.
[0,1]ⁿᵒᵗᐧᴿꟳ =
{ x = lub bnes ⊆ ℚ: 0≤x≤1}
lub least.upper.bound
bnes bounded.non.empty.set
I'm not telling you to do it my way, but,
if not my way, then how?
There's not much said except that
d goes to infinity, and n goes to d.
(Thus that it's not just zero.)
I think it's essential to your project
that more be said.
I have inserted what I can, as best I can,
of what you might mean.
For example, for some reason, you really like
to call a connected domain "continuous",
an adjective I expect to see applied to
a function. Not a deal.breaker.
You have the opportunity to correct my insertions
where I have misunderstood you.
I read "goes to" as "ranges up to"
which is why I write
lim[d→∞, d∈ℕ] lim[n→d, n∈ℕ] n/d =
lim[d→∞, d∈ℕ] {n/d: 0≤n≤d, n∈ℕ}
And there's the rub.
I can expand the limit in an often.used way
lim[d→∞, d∈ℕ] {d/n: 0≤n≤d, n∈ℕ} =
⋂[d∈ℕ] ⋃[d′≥d:d′∈ℕ] {n/d′: 0≤n≤d′, n∈ℕ}
However,
⋂[d∈ℕ+] ⋃[d′≥d:d′∈ℕ] {n/d′: 0≤n≤d′, n∈ℕ} =
[0,1]ʳᵃᵗⁱᵒⁿᵃˡ
[0,1]ʳᵃᵗⁱᵒⁿᵃˡ ≠ [0,1]ᶜᵒⁿᵗⁱⁿᵘᵘᵐ
[0,1]ʳᵃᵗⁱᵒⁿᵃˡ ∌ ⅟√̅2
But
[0,1]ᴿꟳ =
lim[d→∞, d∈ℕ⁺] lim[n→d, n∈ℕ] n/d =
lim[d→∞, d∈ℕ⁺] {n/d: 0≤n≤d, n∈ℕ} =
⋂[d∈ℕ+] ⋃[d′≥d:d′∈ℕ] {n/d′: 0≤n≤d′, n∈ℕ} =
[0,1]ʳᵃᵗⁱᵒⁿᵃˡ
Either
that's how "limit" is defined here and
[0,1]ᴿꟳ ≠ [0,1]ᶜᵒⁿᵗⁱⁿᵘᵘᵐ
or
"limit" is defined some other way and
you should say what that way is.