Re: [isabelle] Range of a record-valued function



On Wed, 2012-09-26 at 11:08 +0200, Holger Blasum wrote:
> lemma f_range: "Union ({x. EX n. x = f n}) = {1,2}"
> proof-
>   from f_def show ?thesis by auto
> qed

Main already provides image (`) and range operators, cf. Section 4 of
http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/Isabelle2012/doc/main.pdf

So you could simply claim "range f = {1,2}".

Best regards,
Tjark







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