[isabelle] Functions vs. relations
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