# Re: [isabelle] set comprehension with pairs

Hi Andrei,
the sytnax translation "{x. P}" == "Collect (%x. P)" in theory Set
tells you that "{(x, y). P x y}" is "Collect (%(x, y). P x y)".

`Now, the translation "%(x,y).b" == "split(%x y. b)" in theory
``Product_Type defines the syntax "%(x, y). P x y" for
`"split (%x y. P x y)". "%x y. P x y" eta-contracts to "P".

`Hence, your expression stands for "Collect (split P)", or in nice syntax
``if "split P" is eta-expanded to "%z. split P z": "{z. split P z}".
`
Regards,
Andreas
Andrei Popescu schrieb:

`Hello,
``
``Given P :: 'a => 'b => bool,
``
``I would like to know what does the expression
``
``{(x,y). P x y}
``
``*precisely* stand for.
``
``Is it something like
``
`{z. EX x y. z = (x,y) /\ P x y} ?

`Knowing this would help me deal more easily with some trivial set theory that seems reluctant to blasting. I would also appreciate if someone showed me not only the answer to this, but also the way I could have found out myself looking at the online libraries.
``
``Thank you in advance,
`` Andrei Popescu
``
`

`
`

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