Q dense in R

Stream: maths

[Kevin Buzzard]

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]

algebra.archimedean has some similar things

[Mario Carneiro]

the rationals are archimedean, so exists_rat_btwn will work. Also the rationals are dense, so dense will work

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

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]

alternatively, you can let S : set Q and have its interpretation in R be (coe '' S)

[Mario Carneiro]

alternatively S : set R and S \sub range coe

[Kevin Buzzard]

Oh that's better

[Mario Carneiro]

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

[Mario Carneiro]

I think we could define real.rats, real.nats : set R in the obvious way and use that

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

all the operations are real operations

[Mario Carneiro]

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]

(deleted)