Maximum over a type with a minimum element

Stream: Is there code for X?

[Ching-Tsun Chou]

Given s : Finset ℕ, I want to get the maximum of elements in s. But Finset.max s produces an element in WithBot ℕ, while Finset.max' s requires an additional assumption that s is nonempty. Since ℕ already has a bottom element 0, the maximum of s can be naturally defined to be 0 if s is empty. Is there a function that allows me to do that?

More generally, all I need is an element that is ≥ all elements in s. Is there already such a theorem somewhere in mathlib? Namely, something like:

example (s : Finset ℕ) : ∃ n, ∀ k ∈ s, k ≤ n

[Yan Yablonovskiy 🇺🇦]

Ching-Tsun Chou said:

Given s : Finset ℕ, I want to get the maximum of elements in s. But Finset.max s produces an element in WithBot ℕ, while Finset.max' s requires an additional assumption that s is nonempty. Since ℕ already has a bottom element 0, the maximum of s can be naturally defined to be 0 if s is empty. Is there a function that allows me to do that?

More generally, all I need is an element that is ≥ all elements in s. Is there already such a theorem somewhere in mathlib? Namely, something like:

example (s : Finset ℕ) : ∃ n, ∀ k ∈ s, k ≤ n

If you are working with N and WithBot N consider if docs#WithBot.coe_natCast is helpful.

[Aaron Liu]

docs#Finset.sup

[Ching-Tsun Chou]

Thanks! Finset.sup works.