*To*: Julian <parsert.julian at gmail.com>*Subject*: Re: [isabelle] Syntax for Min/Max, or the notation for images*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sun, 18 Feb 2018 18:08:23 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <bc7029e1-e9ee-af7e-10de-e281df81efbd@gmail.com>*References*: <876D88B5-D41B-467A-9FD6-264E08ECF1FD@cam.ac.uk> <1518799126.17422.18.camel@in.tum.de> <bdeb60d8-de79-05c2-62a4-0d875241a876@in.tum.de> <1518968629.1092.1.camel@cis.upenn.edu> <bc7029e1-e9ee-af7e-10de-e281df81efbd@gmail.com>

> On 18 Feb 2018, at 15:48, Julian <parsert.julian at gmail.com> wrote: > > do you mean the same as {a i |i. i ∈ I}? This is logically equivalent to the image operator, but denotes something like {x. ∃i∈I. x = a i}, while “image” is a single constant. The advantage of introducing something like {a i. i ∈ I} is that we would have a uniform syntax for all future situations. E.g. the current (⋃x∈A. B x) could also be written ⋃{B x. x∈A}. Larry

**Follow-Ups**:**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Andreas Lochbihler

**References**:**[isabelle] Syntax for Min/Max, or the notation for images***From:*Lawrence Paulson

**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Peter Lammich

**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Tobias Nipkow

**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Joachim Breitner

**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Julian

- Previous by Date: [isabelle] CfP: 4PAD 2018 - 5th International Symposium on Formal Approaches to Parallel and Distributed Systems
- Next by Date: Re: [isabelle] Proof of concept: BNF-based records
- Previous by Thread: Re: [isabelle] Syntax for Min/Max, or the notation for images
- Next by Thread: Re: [isabelle] Syntax for Min/Max, or the notation for images
- Cl-isabelle-users February 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list