# Re: [isabelle] Syntax for Min/Max, or the notation for images

```Hi,

I have, in the past, missed a concise quantifier-free syntax for set
image, and would have wanted (expected, even?) something like

{a i. i ∈ I}

Cheers,
Joachim

Am Sonntag, den 18.02.2018, 13:28 +0100 schrieb Tobias Nipkow:
> I agree with Peter because the SUP syntax ultimately stands for "a ` I", which
> is what you want (because it avoids the quantifier). It is a very natural syntax
> and avoids inventing a new syntax for image.
>
> Tobias
>
> On 16/02/2018 17:38, Peter Lammich wrote:
> > On Fr, 2018-02-16 at 16:14 +0000, Lawrence Paulson wrote:
> > > I've noticed that Isabelle/HOL has no syntax for the minimum/maximum
> > > of a finite set. Or rather, while one can write Max {a i| i. i ∈ I},
> > > such a set comprehension can translate into a complicated formula
> > > involving existential quantifiers, with the reasoning similarly
> > > complicated. Or one could instead use the image operator and write
> > > Max (a ` I).
> > >
> > > In fact (a ` I) = {a i| i. i ∈ I}, and a more general form of this
> > > result exists as the lemma setcompr_eq_image.
> > >
> > > Arguably what's needed here isn't special syntax for Min/Max but
> > > rather an alternative syntax for image, e.g. {a i. i ∈ I}. Are there
> > > any views?
> >
> > Why not use the existing Syntax for INF/SUP ?
> >
> >    term "SUP x:X. f x"
> >
> > i.e. one could declare syntax:
> >    MAX i:I. a i
> >
> > -- Peter
> >
> >
> >
> > >
> > > Larry Paulson
> > >
> > >
> > >
> > >
>
>
--
Joachim Breitner
Post-Doctoral researcher
http://cis.upenn.edu/~joachim```

Attachment: signature.asc
Description: This is a digitally signed message part

• Follow-Ups:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.