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 SS be a non-empty bounded above set of reals. True or false: if SQS\subseteq\mathbb{Q} then sup(S)Qsup(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 SS so we don't really want to change the definition of SS 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: Dec 20 2023 at 11:08 UTC