[isabelle] Proving that a function is injection
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?
theorem assumes "f: A->B" and "w:A & x:A ==> (f`w=f`x --> w=x)"
shows "f: inj(A,B)"
Victor Porton - http://portonvictor.org
This archive was generated by a fusion of
Pipermail (Mailman edition) and