## Stream: general

### Topic: There are infinite rationals in a segment

#### Jiatong Yang (Sep 14 2022 at 04:03):

theorem A2 (a b : ℝ) (altb : a < b) : infinite {x : ℚ | (x : ℝ) ∈ set.Ioo a b} := sorry


How to prove this?
I come across 2 difficulties. How to use Lean's infinite? (version 3.48.0) How to prove for all a, b s.t. b - a > 1, there is an integer in (a, b)?

#### Ruben Van de Velde (Sep 14 2022 at 07:15):

For your second question, can you write an #mwe?

#### Kevin Buzzard (Sep 14 2022 at 07:27):

For the second one, one approach is floor(a+1), all the lemmas will be there.

#### Ruben Van de Velde (Sep 14 2022 at 07:44):

Slightly easier with (floor a) + 1 in terms of lemmas

#### Filippo A. E. Nuccio (Sep 14 2022 at 07:57):

For the first you could use that the rationals are archimedean as in docs#rat.archimedean to construct two rationals y<x such that a<y<x<b. Then you can define the function f : ℕ → ℚ sending n to y+(x-y)/2+(x-y)/2n=y+(n+1)(x-y)/2 and prove it is injective and takes values inside your interval. Finally, use that a set receiving an injective function from an infinite set is itself infinite, as in docs#infinite.of_injective.

#### Johan Commelin (Sep 14 2022 at 08:07):

You could also split that approach in two steps:

• prove that (0,1) is infinite
• construct a bijection between (a,b) and (0,1)

#### Yaël Dillies (Sep 14 2022 at 08:27):

Probably the correct generality is nonempty open sets intersect (topologically) dense sets in infinitely many points?

#### Kevin Buzzard (Sep 14 2022 at 10:22):

Johan Commelin said:

You could also split that approach in two steps:

• prove that (0,1) is infinite
• construct a bijection between (a,b) and (0,1)

The natural bijection won't preserve rationality :-( My instinct was to prove that there was a rational in each of the regions (a+di/n, a+d(i+1)/n) with d=b-a but this will also be a pain

#### Mario Carneiro (Sep 14 2022 at 10:23):

My thought was to prove by induction that there is a strictly decreasing sequence of rats by using exists_rat_btwn

#### Mario Carneiro (Sep 14 2022 at 10:27):

@Yaël Dillies that's not true for finite top spaces. I think you need to know that the open set is infinite, and also the space is T0 so that you can take a finite set of points out while keeping it open

#### Johan Commelin (Sep 14 2022 at 10:34):

Aah, of course it doesn't preserve rationality. But scaling and translating by rationals does.

#### Johan Commelin (Sep 14 2022 at 10:34):

So you scale and translate (a,b) until it contains (0,1).

#### Patrick Stevens (Sep 14 2022 at 18:14):

Kevin Buzzard said:

The natural bijection won't preserve rationality :-( My instinct was to prove that there was a rational in each of the regions (a+di/n, a+d(i+1)/n) with d=b-a but this will also be a pain

This can be made to work, though, if you prove it for $a, b$ rational and then show that there are two rationals between every distinct pair of reals, to deal with the irrational case

#### Jiatong Yang (Sep 14 2022 at 23:52):

Thank you all very much! I have written down a proof:

theorem A2 (a b : ℝ) (altb : a < b) : infinite {x : ℚ | a < x ∧ (x : ℝ) < b} := begin
cases (exists_rat_btwn altb) with l hl,
cases (exists_rat_btwn hl.2) with r hr,
have lltr : l < r := real.rat_cast_lt.mp hr.left,
have p : ∀ (n : ℕ), l < l + (r - l) * (1 / (n + 1)) ∧ l + (r - l) * (1 / (n + 1)) ≤ r := begin
intro n,
have sp1 : 0 < 1 / ((n : ℚ) + 1) := nat.one_div_pos_of_nat,
have sp2 : 1 / ((n : ℚ) + 1) ≤ 1 := (one_le_div sp1).mp (by simp),
have : (r - l) * (1 / (n + 1)) > 0 := mul_pos (by linarith) sp1,
have : (r - l) * (1 / (n + 1)) ≤ (r - l) := begin
conv_rhs {
rw [← mul_one (r - l)],
},
mono; linarith,
end,
split; linarith,
end,
let f := λ n : ℕ, (⟨l + (r - l)* (1 / (n + 1)), p n⟩ : {x // l < x ∧ x ≤ r}),
have injf : function.injective f,
{
intros n m H,
simp at H,
cases H; linarith,
},
have lrinf : infinite {x // l < x ∧ x ≤ r} := infinite.of_injective f injf,
let g : {x // l < x ∧ x ≤ r} → {x : ℚ // a < x ∧ (x : ℝ) < b} := λ ⟨x, h⟩, ⟨x, begin
have : (l : ℝ) < x := rat.cast_lt.mpr h.left,
have : (x : ℝ) ≤ r := rat.cast_le.mpr h.right,
split; linarith,
end⟩,
have injg : function.injective g,
{
rintros ⟨x, hx⟩ ⟨y, hy⟩ H,
simp at H,
exact subtype.ext H,
},
exact @infinite.of_injective _ _ lrinf g injg,
end


But it is too long. Is there any way to improve?

(deleted)

(deleted)

(deleted)

#### Jiatong Yang (Sep 15 2022 at 07:58):

I still need help to improve the proof. :rose:

#### Mario Carneiro (Sep 15 2022 at 07:59):

your proof is missing some imports?

#### Mario Carneiro (Sep 15 2022 at 08:10):

Here's a shorter proof, following Matt's idea:

import data.real.basic

theorem A2 (a b : ℝ) (altb : a < b) : infinite {x : ℚ | a < x ∧ (x : ℝ) < b} :=
infinite.of_not_finite \$ λ h, begin
obtain ⟨q, H⟩ := @finite.exists_min _ ℝ h (nonempty_subtype.2 (exists_rat_btwn altb)) _ coe,
obtain ⟨q', hq'₁, hq'₂⟩ := exists_rat_btwn q.2.1,
exact not_lt.2 (H ⟨q', hq'₁, hq'₂.trans q.2.2⟩) hq'₂,
end


#### Jiatong Yang (Sep 15 2022 at 09:41):

So great! Which version do you use? It cannot be compiled in the newest version for the absence of infinite.of_not_finite.

#### Jiatong Yang (Sep 15 2022 at 09:47):

Now we should use not_finite_iff_infinite.mp instead. (I have no idea why mathlib changed the definition of finite and infinite recently)

#### Jiatong Yang (Sep 15 2022 at 09:49):

Thank you a lot! I wrote on paper using minimum too, but I didn't find the api. :sob:

Last updated: Aug 03 2023 at 10:10 UTC