equal
deleted
inserted
replaced
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 |