## Stream: maths

### Topic: finset.max for nonempty sets

#### Kevin Buzzard (Jan 23 2019 at 19:29):

I've been trying to use finset.max and it's a bit annoying in all my use cases because it takes in an arbitrary finset X and returns an option X (to deal with the case where the finset is empty). It would be very easy to write a variant which takes a non-empty finset and returns its max, and I find myself wanting this variant. What should I call it?

#### Kenny Lau (Jan 23 2019 at 19:30):

you want to write a partial function? :shock:

#### Kevin Buzzard (Jan 23 2019 at 19:31):

And is there room for it in finset.lean?

#### Kenny Lau (Jan 23 2019 at 19:31):

I think finset.sup might be what you seek

#### Kevin Buzzard (Jan 23 2019 at 19:32):

It's not that either, because finset.sup wants the lattice to have a bot, and in my use case there is no bot.

#### Kenny Lau (Jan 23 2019 at 19:32):

so you really want a partial function :shock:

#### Kevin Buzzard (Jan 23 2019 at 19:32):

I simply want a function which takes in a non-empty finite set of reals and produces its max.

#### Kevin Buzzard (Jan 23 2019 at 19:32):

I am happy to supply the proof that it's non-empty.

#### Kevin Buzzard (Jan 23 2019 at 19:34):

Surely there will be more use cases. Kenny this is for proving that a convergent sequence of reals is bounded. Working with the option is a pain, because I simply want the answer rather than having to keep talking about elements of the option output.

#### Kevin Buzzard (Jan 23 2019 at 19:36):

Is finset.max' a crap name?

#### Kevin Buzzard (Jan 23 2019 at 19:39):

Ultimately it will be easier to use than the contortions I'm having to go through to prove the results I need about finset.max. Kenny, try proving that if f : nat -> real and B = max {f 0, f 1, f 2} then for all i <= 2, f i <= B. I had to extract B from the option and then prove that it was in the option and it clutters up the local context -- both of these could be avoided because the fact that f 0 is in the set is easy to prove. I think my proposal makes it easier, but I might be wrong because it's only just occurred to me.

#### Chris Hughes (Jan 23 2019 at 19:41):

You can use option.get 

#### Johannes Hölzl (Jan 23 2019 at 19:43):

No, Kevin wants option.iget. Or a max version which assumes inhabited.

#### Johan Commelin (Jan 23 2019 at 19:56):

So we should fix ourselves a finset.imax?

#### Johan Commelin (Jan 23 2019 at 19:57):

iget and imax sound like they were invented by Apple. :sad:

#### Kevin Buzzard (Jan 23 2019 at 20:42):

I don't want to keep applying iget, I know the set is nonempty and I just want the max :-) There seem to be more contortions using what is there already. I should try writing the code and see if it's actually better.

#### Kevin Buzzard (Jan 23 2019 at 21:12):

rofl I decided to call it finset.max' and then I discovered it was there already :-)

#### Kevin Buzzard (Jan 23 2019 at 21:15):

Johannes put it there in October!

#### Patrick Massot (Jan 23 2019 at 21:17):

One day I taught Simon what was convert. At some point in the history section of the explanation, I was forced to mention that Simon himself wrote that tactic.

#### Kevin Buzzard (Jan 23 2019 at 21:17):

I see, the point is that max' wants a proof that S ≠ ∅, perhaps Johannes could see that I wanted something a bit more convenient.

#### Mario Carneiro (Jan 24 2019 at 01:11):

I am 100% on board with having finset.imax defined and including the obvious lemmas. (Johan, I don't think you can patent single letter prefixes.) I agree you shouldn't deal with (finset.max s).iget, there should be a definition for this combination.

#### Kevin Buzzard (Jan 24 2019 at 07:13):

So I'm currently using finset.max'` and it's fine

Last updated: May 11 2021 at 15:12 UTC