# Zulip Chat Archive

## Stream: maths

### Topic: Q dense in R

#### Kevin Buzzard (Dec 28 2018 at 00:15):

`theorem rationals_dense (x y : ℝ) (H : x < y) : ∃ q : ℚ, x < q ∧ (q : ℝ) < y :=`

Where is this now? I think it was explicitly there before the reals were refactored. Now there is `dense_embedding_of_rat`

but then I have to work to get the statement I want.

#### Reid Barton (Dec 28 2018 at 00:20):

`algebra.archimedean`

has some similar things

#### Mario Carneiro (Dec 28 2018 at 04:09):

the rationals are archimedean, so `exists_rat_btwn`

will work. Also the rationals are dense, so `dense`

will work

#### Mario Carneiro (Dec 28 2018 at 04:10):

oh wait that last one is just rationals between rationals, with no casting

#### Kevin Buzzard (Dec 28 2018 at 14:21):

Aah, thanks to both of you. I'm looking in the wrong places. That was silly of me -- I even lectured this term on the fact that unboundedness of Z in R implied this fact.

#### Kevin Buzzard (Dec 28 2018 at 18:41):

I want the coercion from Q to R to be different somehow. Look at this question the first years will be asked next term: "Let $S$ be a non-empty bounded above set of reals. True or false: if $S\subseteq\mathbb{Q}$ then $sup(S)\in\mathbb{Q}$. How do I make the Lean formalisation of this question less ugly? [added later: this is just one part of a multi-part question about a non-empty bounded-above set of reals $S$ so we don't really want to change the definition of $S$ itself]

#### Kevin Buzzard (Dec 28 2018 at 18:42):

import data.real.basic -- structure or class? structure real.rat1 (r : ℝ) := (q : ℚ) (pf : r = ↑q) definition real.rat2 (r : ℝ) := ∃ q : ℚ, r = q

Are these functions in Lean already? What are they / should they be called?

#### Mario Carneiro (Dec 28 2018 at 20:58):

As usual, this is nonidiomatic lean and so it's less than nice to say. It is equivalent to talk about the supremum of a family `f : I -> Q`

#### Mario Carneiro (Dec 28 2018 at 20:59):

alternatively, you can let `S : set Q`

and have its interpretation in `R`

be `(coe '' S)`

#### Mario Carneiro (Dec 28 2018 at 21:00):

alternatively `S : set R`

and `S \sub range coe`

#### Kevin Buzzard (Dec 28 2018 at 21:00):

Oh that's better

#### Mario Carneiro (Dec 28 2018 at 21:01):

if I wasn't constrained by aiming for a direct translation I would certainly go for the first option

#### Mario Carneiro (Dec 28 2018 at 21:04):

I think we could define `real.rats, real.nats : set R`

in the obvious way and use that

#### Kevin Buzzard (Dec 28 2018 at 21:59):

and now I have to reprove things like `real.rats x -> real.rats y -> real.rats (x + y)`

?

#### Kevin Buzzard (Dec 28 2018 at 22:04):

I am not 100% clear on what needs proving actually. There's a lemma which says that + on Q and R coincide, and that's kind of why I need to prove the thing above. But there's another lemma which says that < on Q and R coincide, and that doesn't seem to correspond to something I need to prove here.

#### Mario Carneiro (Dec 29 2018 at 08:24):

well, it's a set so you would want to write that `x \in rats -> y \in rats -> x + y \in rats`

, but yes, and it follows from `rat.cast_add`

#### Mario Carneiro (Dec 29 2018 at 08:25):

and you are right, there isn't really an analogue for `rat.cast_le`

#### Mario Carneiro (Dec 29 2018 at 08:26):

it's just the set of rational numbers, as a subset of R

#### Mario Carneiro (Dec 29 2018 at 08:26):

all the operations are real operations

#### Mario Carneiro (Dec 29 2018 at 08:27):

you can do many things with such a set, the idea is when you need a set and not a type. For example `closure rats = univ`

is hard to state otherwise

#### Chris Hughes (Dec 29 2018 at 10:01):

(deleted)

Last updated: May 12 2021 at 07:17 UTC