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

> 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.