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.
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 - http://portonvictor.org
This archive was generated by a fusion of
Pipermail (Mailman edition) and