[isabelle] Functions vs. relations



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 MHonArc.