Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving that a function is injection

view this post on Zulip Email Gateway (Aug 18 2022 at 16:44):

From: Victor Porton <porton@narod.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 ==> (fw=fx --> w=x)"
shows "f: inj(A,B)"
sorry

end

\--
Victor Porton - http://portonvictor.org

Last updated: Apr 26 2024 at 01:06 UTC