Sets of Reals are linearly ordered

Stream: new members

[joseph v]

Hi guys, newbie here. I'm trying to prove that: the convergence of a sequence to a limit 'a' is equivalent to its limits supremum and infimum equaling 'a'. I'm stuck because I can't seem to take the minimum value of a set of real numbers (set of upper bounds), which to my knowledge should be entirely possible...?

I've posted this question on mathstackexchange but I'm looking for a more direct answer as to what I'm doing wrong. Link is here:
https://math.stackexchange.com/questions/4544239/using-lean-to-prove-the-convergence-of-a-sequence-is-equivalent-to-the-equality

I'd really appreciate any tips or pointers as to how to go from here. Also, I can't seem to use Lean after installing it as per the instructions on the website, so I'm using the online web editor - I don't seem to have any mathlib stuff installed in VS and I'm not quite sure how to download them?

[Patrick Massot]

joseph v said:

I'm stuck because I can't seem to take the minimum value of a set of real numbers (set of upper bounds), which to my knowledge should be entirely possible...?

No it isn't. This has nothing to do with Lean. What if your set of real numbers is all real numbers?

[Floris van Doorn]

For a minimum of a set, you want to take the infimum Inf, see https://leanprover-community.github.io/mathlib_docs/order/complete_lattice.html
For installing mathlib, did you go through the instructions here (which are part of the installation instructions)? https://leanprover-community.github.io/install/project.html

[joseph v]

Patrick Massot said:

joseph v said:

I'm stuck because I can't seem to take the minimum value of a set of real numbers (set of upper bounds), which to my knowledge should be entirely possible...?

No it isn't. This has nothing to do with Lean. What if your set of real numbers is all real numbers?

Oops sorry if I wasn't clear; I've defined the set to be the set of upper bounds of a bounded function, so there should be a minimum value that acts as a supremum of the function. I was trying to use 'min' to define this

[Kevin Buzzard]

I think the real way to be clear on a forum such as this is to post some code. That way there is no ambiguity left. Take a look at the #mwe link and then ask your question by posting a sorried theorem which other people can just cut and paste and see on their machines. Otherwise you're just going to get people like me piling in saying things like "if the function is unbounded then the set of upper bounds is empty so has no min" and perhaps derailing the question which you want to ask.

[joseph v]

Floris van Doorn said:

For a minimum of a set, you want to take the infimum Inf, see https://leanprover-community.github.io/mathlib_docs/order/complete_lattice.html
For installing mathlib, did you go through the instructions here (which are part of the installation instructions)? https://leanprover-community.github.io/install/project.html

Thanks! Inf seems to give less errors than min (at least I don't have to prove linear order now), but there's a type mismatch from my definition of a bounded sequence and also a placeholder synthesizing issue... I'll read around the link and see if I can spot what i'm missing.

I did follow the youtube instructions to download lean, but I'll try reinstalling and creating a new project again. Thanks for the pointers!

[joseph v]

(deleted)

[joseph v]

Kevin Buzzard said:

I think the real way to be clear on a forum such as this is to post some code. That way there is no ambiguity left. Take a look at the #mwe link and then ask your question by posting a sorried theorem which other people can just cut and paste and see on their machines. Otherwise you're just going to get people like me piling in saying things like "if the function is unbounded then the set of upper bounds is empty so has no min" and perhaps derailing the question which you want to ask.

I've posted my small bit of code in the question - really should've done that from the start. Just wanted to say that I enjoyed your YouTube tutorials in the Lean 2020 summer lectures (I've worked through the first few), really learnt a lot quite quickly!

[Riccardo Brasca]

You can use #backticks.

[Joseph V]

Riccardo Brasca said:

You can use #backticks.

Thanks!

[Kevin Buzzard]

With your code I get an error:

type mismatch at application
  Inf (up_bounds b)
term
  up_bounds b
has type
  b ∈ set_bounded_seq → set ℝ : Type
but is expected to have type
  set ?m_1 : Type ?

Is your question how to make the error go away? The error says what the problem with your code is. If you hover over Inf you see

has_Inf.Inf : Π {α : Type u_9} [self : has_Inf α], set α → α

The first input is in {} brackets so Lean will sort it out for you. The second input is in [] brackets so Lean will sort it out for you. The next input is a term of type set α. Conclusion: Inf is expecting to be fed a set. But you feed it up_bounds (b). If you type #check up_bounds you see this:

up_bounds : Π (b : ℕ → ℝ), b ∈ set_bounded_seq → set ℝ

So up_bounds first expects a function (which you give it), and then it expects a proof that this function is bounded and it will output a set. In particular, up_bounds (b) is a function which eats a proof that a set is bounded and returns a set, so it's not a set, and indeed this is exactly what the error says.