*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Proving that a function is injection*From*: Victor Porton <porton at narod.ru>*Date*: Fri, 17 Dec 2010 18:37:38 +0300*Envelope-from*: porton@yandex.ru

I have the following problem (I may attempt to solve it myself but I think that would lead to a messy non-optimal solution, but I want to see the best way to solve it):

How to prove that a given function is injection?

theory test

imports Main_ZF

begin

theorem assumes "f: A->B" and "w:A & x:A ==> (f`w=f`x --> w=x)"

shows "f: inj(A,B)"

sorry

end

imports Main_ZF

begin

theorem assumes "f: A->B" and "w:A & x:A ==> (f`w=f`x --> w=x)"

shows "f: inj(A,B)"

sorry

end

--

Victor Porton - http://portonvictor.org

Victor Porton - http://portonvictor.org

- Previous by Date: Re: [isabelle] Fw : Re: Question on hypothesis
- Next by Date: [isabelle] New AFP entry: Hall's Marriage Theorem
- Previous by Thread: Re: [isabelle] On foundation axiom in ZF
- Next by Thread: [isabelle] New AFP entry: Hall's Marriage Theorem
- 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