naturals_in_reals

Stream: general

[Guillermo Barajas Ayuso]

Hi guys, how would you express the natural numbers as a subtype of the reals?

[Kevin Buzzard]

I guess you could just do

import data.real.basic

def N := {x : ℝ // ∃ n : ℕ, x = n}

but then the term of type equiv N nat would be noncomputable. Is there a computable way?

[Kenny Lau]

it's computable

[Kenny Lau]

(but Lean doesn't know it yet)

[Chris Hughes]

How do you do that computably?

[Mario Carneiro]

It's not computable. It would be if cauchy sequences defining real numbers had a modulus of convergence

[Mario Carneiro]

this is why I've taken to calling our definition of the reals "computable but not really"

[Mario Carneiro]

Suppose you have a real number that is known to equal some natural number, and you want to guess which. The convergence criterion says that at some point all the rational numbers will be closer to one natural than any other, and then you can round to get the number, but you don't know when that point is. A more constructive approach would be a sequence of rationals that converges at a specific rate (usually exponential), so you can ask "give me an n-digit approximation of this number", or at least a sequence of rationals together with a function that tells you how long the sequence takes to reach a certain level of approximation

[Kenny Lau]

fair enough. I thought wrongly.

[Johan Commelin]

Is our definition of rat "computable but not rationally"?

[Mario Carneiro]

To answer the original question, the standard way to talk about natural numbers inside the reals is to use the coercion. If you want to talk about the whole set of reals-that-are-natural, you can use set.range (coe : ℕ → ℝ) which is basically the same as Kevin's suggestion.

[Guillermo Barajas Ayuso]

I see, thaks a lot! Also how would you prove the following?

example (h : n < m) : (n : ℝ) < (m : ℝ) := sorry

[Guillermo Barajas Ayuso]

Sorry I forgot to define n and m

example {n m : ℕ} (h : n < m) : (n : ℝ) < (m : ℝ) := sorry

[Kenny Lau]

nat.cast_lt or something

[Kenny Lau]

(alternatively, induct on h)

[Guillermo Barajas Ayuso]

Ok, thanks!