equal
deleted
inserted
replaced
180 qed "inj_on_inv"; |
180 qed "inj_on_inv"; |
181 |
181 |
182 Goal "surj f ==> inj (inv f)"; |
182 Goal "surj f ==> inj (inv f)"; |
183 by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1); |
183 by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1); |
184 qed "surj_imp_inj_inv"; |
184 qed "surj_imp_inj_inv"; |
|
185 |
|
186 Goal "f``(A Int B) <= f``A Int f``B"; |
|
187 by (Blast_tac 1); |
|
188 qed "image_Int_subset"; |
|
189 |
|
190 Goal "f``A - f``B <= f``(A - B)"; |
|
191 by (Blast_tac 1); |
|
192 qed "image_diff_subset"; |
185 |
193 |
186 Goalw [inj_on_def] |
194 Goalw [inj_on_def] |
187 "[| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B"; |
195 "[| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B"; |
188 by (Blast_tac 1); |
196 by (Blast_tac 1); |
189 qed "inj_on_image_Int"; |
197 qed "inj_on_image_Int"; |