Email Gateway (Aug 18 2022 at 16:43): Email Gateway (Aug 18 2022 at 16:43):From: Victor Porton <porton@narod.ru>
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
Email Gateway (Aug 18 2022 at 16:44):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: May 06 2024 at 12:29 UTC