Proof of ℚ dense in ℝ ?

Stream: mathlib4

[Gaëtan Serré]

Hello, I am looking for a proof that ℚ is dense in ℝ and I was wondering if such a proof exists in Mathlib (I could not find it using Moogle nor the regular doc)?

[Gaëtan Serré]

I found docs#dense_irrational for example

[Adam Topaz]

Dense in what sense? We should have somewhere that R is the (uniform) completion of Q, for example. Can you formulate the precise assertion you want in lean?

[Adam Topaz]

a quick search found docs#Rat.denseEmbedding_coe_real

[Kyle Miller]

Here's one formulation, before I saw Adam's message:

example : Dense {(x : ℝ) | (x : ℚ)} := by
  apply dense_of_exists_between
  intros x y h
  simp only [Set.mem_setOf_eq, exists_exists_eq_and]
  exact exists_rat_btwn h

[Kyle Miller]

Using the lemma Adam pointed out, this is just

example : Dense {(x : ℝ) | (x : ℚ)} :=
  Rat.denseEmbedding_coe_real.dense

[Kyle Miller]

You can also state the conclusion as Dense (Set.range ((↑) : ℚ → ℝ)), which is definitionally equal.

[Gaëtan Serré]

Thanks a lot! @Adam Topaz, I want to use the fact that, for any real, it exists a sequence of rationals that tends to it. I guess the definition of Dense in Mathlib should allow me to prove this quickly. @Kyle Miller thank you for the examples.

I definitely need to check on definition of docs#DenseEmbedding.
docs#dense_of_exists_between is very handy tho.

[Gaëtan Serré]

Kyle Miller said:

You can also state the conclusion as Dense (Set.range ((↑) : ℚ → ℝ)), which is definitionally equal.

Could you enlighten me on the meaning of (↑)?

[Gaëtan Serré]

Nevermind, I think I got it. Subsidiary question, why would we use Dense (Set.range ((↑) : ℚ → ℝ)) instead of Dense {(x : ℝ) | (x : ℚ)}?

[Kevin Buzzard]

Because what you wrote doesn't typecheck(edit: apparently incorrect --apologies)

[Jireh Loreaux]

Kevin, I think it does. In fact, those things are defeq.