src/HOL/Fun.thy
changeset 43705 8e421a529a48
parent 42903 ec9eb1fbfcb8
child 43874 74f1f2dd8f52
equal deleted inserted replaced
43694:93dcfcf91484 43705:8e421a529a48
   145 abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where -- "surjective"
   145 abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where -- "surjective"
   146   "surj f \<equiv> (range f = UNIV)"
   146   "surj f \<equiv> (range f = UNIV)"
   147 
   147 
   148 abbreviation
   148 abbreviation
   149   "bij f \<equiv> bij_betw f UNIV UNIV"
   149   "bij f \<equiv> bij_betw f UNIV UNIV"
       
   150 
       
   151 text{* The negated case: *}
       
   152 translations
       
   153 "\<not> CONST surj f" <= "CONST range f \<noteq> CONST UNIV"
   150 
   154 
   151 lemma injI:
   155 lemma injI:
   152   assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
   156   assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
   153   shows "inj f"
   157   shows "inj f"
   154   using assms unfolding inj_on_def by auto
   158   using assms unfolding inj_on_def by auto