There are infinite rationals in a segment

Stream: general

[Jiatong Yang]

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]

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

[Kevin Buzzard]

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

[Ruben Van de Velde]

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

[Filippo A. E. Nuccio]

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]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

@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]

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

[Johan Commelin]

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

[Patrick Stevens]

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]

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?

[Matt Diamond]

(deleted)

[Matt Diamond]

(deleted)

[Matt Diamond]

(deleted)

[Matt Diamond]

nvm, misread the problem

[Jiatong Yang]

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

[Mario Carneiro]

your proof is missing some imports?

[Mario Carneiro]

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]

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]

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]

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