biSup over a singleton

Stream: Is there code for X?

[Michael Stoll]

I would like to use the following obvious fact:

import Mathlib

example (f : ℕ → ℝ) : ⨆ i ∈ ({0} : Finset ℕ), f i = f 0 := sorry

There is a lemma in Mathlib that seems to fit the bill: docs#Finset.iSup_singleton .
However, it does not apply here because it requires the target type to be a docs#CompleteLattice , which the reals are not.
On the other hand, this requirement seems rather unnecessary here.

In any case, I am a bit stuck here and would appreciate some help. (apply? and rw?do not produce anything useful here, and simp (which is the proof of the lemma mentioned above) only gives me ⨆ i, ⨆ (_ : i = 0), v (f i) = v (f 0).)

[Jz Pan]

Unfortunately that's not correct due to weird definition of biSup in mathlib. Let me find the previous discussion.

[Michael Stoll]

I don't think that is the problem here (as in my concrete case, the function takes nonnegative values), but it certainly prevents a general lemma from applying...

[Michael Stoll]

So maybe the more pertinent question is, what is the idiomatic way to express the maximum over a finite set?

[Yaël Dillies]

docs#Finset.max

[Michael Stoll]

or docs#Finset.max' if I don't want to deal with docs#WithBot ...

[Michael Stoll]

Is there also an indexed version? Or should I just work with the image of f?

[Yaël Dillies]

Yes: docs#Finset.sup, docs#Finset.sup'

[Jz Pan]

Michael Stoll said:

I don't think that is the problem here (as in my concrete case, the function takes nonnegative values), but it certainly prevents a general lemma from applying...

#mathlib4 > sup and inf over sets @ 💬 (I think you already found it)

[Michael Stoll]

Jz Pan said:

#mathlib4 > sup and inf over sets @ 💬 (I think you already found it)

I remembered the discussion after you mentioned it...