Notation for mapping a function over FinSet

Stream: general

[Konstantin Weitz]

The best way I know how to map a function over a Finset is like so:

(Finset.univ.image (fun a:A => g (f a x)).max

Is there any notation to make that a bit more readable? Maybe something like python's list comprehension syntax, which would be something like:

max { a | g(f a x)}

[Yaël Dillies]

Finset.univ.sup fun a ↦ g (f a x) is the more idiomatic way to do that. Unfortunately, we don't have any notation here

[Yaël Dillies]

If you're interested in acquiring notation for this (which I think would be a very useful endeavour!), please have a look at the ⨆ _, _ notation for docs#iSup (we probably want the same or a similar notation), and do note that docs#Finset.sup' exists too, meaning that we would notation for it as well

[Yaël Dillies]

Maybe something like

• ⨆ i in s, f i for Finset.sup s fun i ↦ f i
• ⨆ i in s where hs, f i for Finset.sup' s hs fun i ↦ f i

or alternatively

• ⨆ᶠ i ∈ s, f i for Finset.sup s fun i ↦ f i
• ⨆ᶠ i ∈ s where hs, f i for Finset.sup' s hs fun i ↦ f i
• ⨆ᶠ i, f i for Finset.sup Finset.univ fun i ↦ f i if OrderBot α can be synthesized where α is the codomain, else Finset.sup' Finset.univ Finset.univ_nonempty fun i ↦ f i.

[Yaël Dillies]

I don't think we should have notation for Finset.max <| Finset.image s fun i ↦ f isince it would drive users away from using the correct definition, as explained above