# [isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy

*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy
*From*: Christoph LANGE <math.semantic.web at gmail.com>
*Date*: Mon, 26 Aug 2013 12:52:13 +0200
*Organization*: University of Birmingham
*Sender*: Christoph Lange <allegristas at gmail.com>
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130807 Thunderbird/17.0.8

Hi all,
I wanted to improve the readability of an easy lemma about set theory
and used the following set comprehension syntax, for some concrete
function f and set S:
{ f x | x . x ∈ S }
After this step my lemma turned out to be very hard to prove.
But it turned out that, once I had the following lemma in place, my
original lemma was again quite easy to prove with metis:
lemma "{ f x | x . x ∈ S } = f ` S" by auto
So maybe this lemma should be part of Set.thy? I didn't know how to
name it appropriately, but I think the name should somehow contain the
parts "image", "Collect" and "mem".
Cheers,
Christoph
--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701
→ Mathematics in Computer Science Special Issue on “Enabling Domain
Experts to use Formalised Reasoning”; submission until 31 October.
http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/

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