beginner question : proving no smallest rational number

Stream: new members

[rzeta0]

After learning about proof by contradiction in MoP, I set myself the following challenge:

Show there is no smallest positive rational number.

I formulated it as disproving the following:

$$\exists r \in \mathbb{Q}^+, \forall s \in \mathbb{Q}^+: r \le s.$$

that is, proving

$$\neg \exists r \in \mathbb{Q}^+, \forall s \in \mathbb{Q}^+ : r \le s$$

which is equivalent to

$$\forall r \in \mathbb{Q}^+, \neg \forall s \in \mathbb{Q}^+ : r \le s$$

which in turn is equivalent to

$$\forall r \in \mathbb{Q}^+, \exists s \in \mathbb{Q}^+ : \neg r \le s$$

(I think the above is correct)

---

I'm struggling with converting this into Lean. My code thus far has 2 problems I'd like advice on:

import Mathlib.Tactic

example : ∀ r : ℚ, ∃ s : ℚ, ¬ r ≤ s := by -- < -- problem 1
  intro r
  use r/2
  intro g1
  have g2: r ≥ r/2 := by ring -- < -- problem 2
  sorry

Code Problems:

• How do I change the set ℚ to ℚ+? I tried asserting hypotheses as follows, but this fails: example (h1: r > 0) (h2: s > 0): ∀ r : ℚ, ∃ s : ℚ, ¬ r ≤ s := by

• How do I create an intermediate result that r ≥ r/2? The ring and linarith tactics don't do it. It feels like a trivial result that should require lots of code to prove.

[Kevin Buzzard]

How do I change the set ℚ to ℚ+

\forall r : \Q, r > 0 -> \exists s : \Q, s > 0 \and \not r \leq s

How do I create an intermediate result that r ≥ r/2

have foo : r \geq r / 2

[Matt Diamond]

take a look at docs#half_le_self and docs#half_lt_self

[Matt Diamond]

here's one approach:

import Mathlib.Tactic

example : ∀ (r : ℚ) (hr : r > 0), ∃ (s : ℚ) (hs : s > 0), ¬ r ≤ s := by
  intro r hr
  use r / 2
  have gt_zero : r / 2 > 0 := by
    sorry
  use gt_zero
  intro g1
  have g2 : r / 2 < r := half_lt_self hr
  sorry

[Matt Diamond]

(Kevin's suggestion to phrase it as ∀ r : ℚ, r > 0 → ∃ (s : ℚ), s > 0 ∧ ¬ r ≤ s works just as well if you prefer that)

[rzeta0]

Thanks Matt = the half_le_self is helpful.

Thanks also Kevin for the help on Q+.

I'm not familiar with the right arrow -> so will see if I can make it work without.

[Matt Diamond]

I'm not familiar with the right arrow ->

You're more familiar with it than you think. Every time you've posted on Zulip about "P ⟹ Q", you've been talking about ->!

[Johan Commelin]

Btw, another option is to use {x : ℚ // x > 0}. This is a "subtype", which you may or may not want to engage with yet.