## Stream: general

### Topic: greater than nat and real

#### Saif Ghobash (Dec 29 2020 at 13:39):

Im new to lean and am trying to formalize some theorems from my lecture notes on real analysis, one of them being

-- ℕ ⊂ ℝ is not bounded above.
theorem theorem_1_1_1 : ∀ x : ℝ, ∃ n : ℕ, n > x :=
begin

end


however I am getting a type error

type mismatch at application
n > x
term
x
has type
ℝ
but is expected to have type
ℕ


I am not sure how to cast n : ℕ to be a real number so I can apply > or use some form of > that accepts ℕ and ℝ.

#### Johan Commelin (Dec 29 2020 at 13:43):

@Saif Ghobash This is because Lean is reading "outside in, left-to-right"...

#### Patrick Massot (Dec 29 2020 at 13:43):

-- ℕ ⊂ ℝ is not bounded above.
theorem theorem_1_1_1 : ∀ x : ℝ, ∃ n : ℕ, (n : ℝ) > x :=
begin

end


#### Patrick Massot (Dec 29 2020 at 13:43):

Note that, as Johan points out, you could also write:

-- ℕ ⊂ ℝ is not bounded above.
theorem theorem_1_1_1 : ∀ x : ℝ, ∃ n : ℕ, x < n :=
begin

end


#### Johan Commelin (Dec 29 2020 at 13:43):

So it sees ">" and then "n", and determines you must be comparing two natural numbers, because n is a nat.

#### Johan Commelin (Dec 29 2020 at 13:44):

Patrick just posted the two ways around this (-;

#### Patrick Massot (Dec 29 2020 at 13:44):

Because of order of elaboration, in the second version Lean knows it expects a real when meeting n.

#### Saif Ghobash (Dec 29 2020 at 13:46):

Thank you @Patrick Massot and @Johan Commelin !

#### Johan Commelin (Dec 29 2020 at 13:48):

@Saif Ghobash Also, note that src/data/real/basic.lean contains

200:instance : archimedean ℝ :=
201:archimedean_iff_rat_le.2 $λ x, quotient.induction_on x$ λ f,
202-let ⟨M, M0, H⟩ := f.bounded' 0 in
203-⟨M, mk_le_of_forall_le ⟨0, λ i _,
204-  rat.cast_le.2 \$ le_of_lt (abs_lt.1 (H i)).2⟩⟩


#### Johan Commelin (Dec 29 2020 at 13:49):

That exactly gives you the result you are looking for.

#### Johan Commelin (Dec 29 2020 at 13:50):

You can use the lemma exists_nat_gt because that instance exists.

#### Saif Ghobash (Dec 29 2020 at 14:51):

@Johan Commelin oh cool! that's exactly what I needed, thank you :)

#### Johan Commelin (Dec 29 2020 at 14:55):

@Saif Ghobash most likely 90-95% of the theorems in an introduction to analysis course are already in mathlib (in one form or another). On the other hand, this doesn't mean that all the exercises in such a course will be trivial to do using mathlib.

#### Sebastian Ullrich (Dec 30 2020 at 10:12):

Johan Commelin said:

So it sees ">" and then "n", and determines you must be comparing two natural numbers, because n is a nat.

#### Johan Commelin (Dec 30 2020 at 10:26):

@Sebastian Ullrich Thanks, as always (-;

#### Sebastian Ullrich (Dec 30 2020 at 10:47):

But I didn't even do anything :big_smile:

#### Kevin Buzzard (Dec 30 2020 at 12:40):

One could intentionally or unintentionally abuse this with some random coercion you didn't know was there, which might change the meaning of a statement. This should be fun! Does it mean that (a : T) < b no longer guarantees that < will be T.has_lt?

#### Kevin Buzzard (Dec 30 2020 at 12:41):

Having said that it would make the Bernoulli code look better! So in a real use case it does look like a good idea

#### Kevin Buzzard (Dec 30 2020 at 12:42):

I'm multiplying and dividing what look like naturals, and all of a sudden there's a Bernoulli number at the end and I didn't want to put it at the start but it's rational

Last updated: May 14 2021 at 22:15 UTC