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

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

Best regards,

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