greater than nat and real

Stream: general

[Saif Ghobash]

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]

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

[Patrick Massot]

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

end

[Patrick Massot]

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]

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

[Johan Commelin]

Patrick just posted the two ways around this (-;

[Patrick Massot]

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

[Saif Ghobash]

Thank you @Patrick Massot and @Johan Commelin !

[Johan Commelin]

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

That exactly gives you the result you are looking for.

[Johan Commelin]

You can use the lemma exists_nat_gt because that instance exists.

[Saif Ghobash]

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

[Johan Commelin]

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

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

[Sebastian Ullrich]

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]

@Sebastian Ullrich Thanks, as always (-;

[Sebastian Ullrich]

But I didn't even do anything :big_smile:

[Kevin Buzzard]

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]

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]

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