equal
deleted
inserted
replaced
175 by (simp add: inj_on_def) |
175 by (simp add: inj_on_def) |
176 |
176 |
177 lemma surj_id[simp]: "surj_on id A" |
177 lemma surj_id[simp]: "surj_on id A" |
178 by (simp add: surj_on_def) |
178 by (simp add: surj_on_def) |
179 |
179 |
180 lemma bij_id[simp]: "bij_betw id A A" |
180 lemma bij_id[simp]: "bij id" |
181 by (simp add: bij_betw_def) |
181 by (simp add: bij_betw_def) |
182 |
182 |
183 lemma inj_onI: |
183 lemma inj_onI: |
184 "(!! x y. [| x:A; y:A; f(x) = f(y) |] ==> x=y) ==> inj_on f A" |
184 "(!! x y. [| x:A; y:A; f(x) = f(y) |] ==> x=y) ==> inj_on f A" |
185 by (simp add: inj_on_def) |
185 by (simp add: inj_on_def) |