author | nipkow |
Thu, 07 Jul 2011 21:53:53 +0200 | |
changeset 43705 | 8e421a529a48 |
parent 43694 | 93dcfcf91484 |
child 43706 | 4068e95f1e43 |
src/HOL/Fun.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Fun.thy Wed Jul 06 23:11:59 2011 +0200 +++ b/src/HOL/Fun.thy Thu Jul 07 21:53:53 2011 +0200 @@ -148,6 +148,10 @@ abbreviation "bij f \<equiv> bij_betw f UNIV UNIV" +text{* The negated case: *} +translations +"\<not> CONST surj f" <= "CONST range f \<noteq> CONST UNIV" + lemma injI: assumes "\<And>x y. f x = f y \<Longrightarrow> x = y" shows "inj f"