changeset 6290 | 31483ca40e91 |
parent 6267 | a3098667b9b6 |
child 6301 | 08245f5a436d |
--- a/src/HOL/Fun.ML Mon Feb 22 10:20:25 1999 +0100 +++ b/src/HOL/Fun.ML Mon Feb 22 10:21:59 1999 +0100 @@ -183,6 +183,14 @@ by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1); qed "surj_imp_inj_inv"; +Goal "f``(A Int B) <= f``A Int f``B"; +by (Blast_tac 1); +qed "image_Int_subset"; + +Goal "f``A - f``B <= f``(A - B)"; +by (Blast_tac 1); +qed "image_diff_subset"; + Goalw [inj_on_def] "[| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B"; by (Blast_tac 1);