supremum of reals

Stream: new members

[Alex Meiburg]

How do I say "supremum of this set of reals"? I couldn't find anything like Real.sup. I have a collection S that produces different values when a function f is applied, and I want to take the supremum.

I would also like to eventually prove that this supremum is attained, and then also define a particular function by "take the element in S that maximizes this value". This will obviously require some topology, but Lean's topology feels very strange and foreign to me...

[Ruben Van de Velde]

docs#sSup

[Jireh Loreaux]

There is also docs#iSup for indexed suprema, also known as ⨆

[Colin Jones ⚛️]

Ruben Van de Velde said:

docs#sSup

The link you gave gives a 404 error. https://leanprover-community.github.io/mathlib4_docs/404.html#sSup

[Ruben Van de Velde]

Yeah, though you can click through. Here's a direct link: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SetNotation.html#SupSet.sSup

[Alex Meiburg]

Thanks. Any pointers on how to go about saying an "argmax" type thing...? Or showing that the supremum is attained? Is this something I need to understand Filter for?

[A.]

I suppose it depends on your exact argument but I didn't think of filters when I wrote

import Mathlib.Topology.MetricSpace.PseudoMetric

noncomputable def argmax {β : Type*} [TopologicalSpace β]
    {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → ℝ} (hf : ContinuousOn f s) : β :=
  Classical.choose (hs.exists_isMaxOn ne_s hf)