# Zulip Chat Archive

## 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.

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

See also https://leanprover-community.github.io/undergrad.html

#### 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`

.

https://github.com/leanprover/lean4/commit/eba3983658faef2d41b7ad00fc2c2e540a1e43e6

#### 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: Aug 03 2023 at 10:10 UTC