Re: [isabelle] Functions vs. relations

The notion of a function in ZF is complicated, and the point of these definitions is to separate the notion of relation from the notion of being single-valued. As to what you should prove: surely you have some ultimate objective. Just prove the facts that you need in order to prove that.
Larry Paulson

On 17 Dec 2010, at 00:00, Victor Porton wrote:

> From ZF.thy:
>   relation_def: "relation(r) == ∀z∈r. ∃x y. z = <x,y>"
>   function_def: "function(r) ==
>                     ∀x y. <x,y>:r --> (∀y'. <x,y'>:r --> y=y')"
> So there are possible functions which are not relations and moreover two functions with equal values may be not equal, what contradicts to customary mathematical conventions. Isn't it a conceptual error in Isabelle/ZF?
> BTW, in my theories, should I prove "function(f)" in addition to "f: A->B"?
> -- 
> Victor Porton -

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