*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Functions vs. relations*From*: Victor Porton <porton at narod.ru>*Date*: Fri, 17 Dec 2010 03:00:19 +0300*Envelope-from*: porton@yandex.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

Victor Porton - http://portonvictor.org

**Follow-Ups**:**Re: [isabelle] Functions vs. relations***From:*Lawrence Paulson

- Previous by Date: [isabelle] ZF_Addons.thy
- Next by Date: [isabelle] A new theorem about lambda
- Previous by Thread: Re: [isabelle] ZF_Addons.thy
- Next by Thread: Re: [isabelle] Functions vs. relations
- Cl-isabelle-users December 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list