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

The map operation on multisets, image_mset, already uses the proposed syntax:

{# a i. i :# M #} = image_mset (%i. a i) M

So extending this syntax to ordinary sets would be just more uniform syntax. But how does it interoperate with ordinary set comprehension? How do we want to distinguish the following two cases:

{ i. i : M } = Collect (%i. i : M)


{ i. i : M } = image (%i. i) M


On 18/02/18 19:08, Lawrence Paulson wrote:
On 18 Feb 2018, at 15:48, Julian <parsert.julian at> 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}.


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