equal
deleted
inserted
replaced
606 |
606 |
607 goal thy "f``(A Un B) = f``A Un f``B"; |
607 goal thy "f``(A Un B) = f``A Un f``B"; |
608 by (Blast_tac 1); |
608 by (Blast_tac 1); |
609 qed "image_Un"; |
609 qed "image_Un"; |
610 |
610 |
611 goal Set.thy "(z : f``A) = (EX x:A. z = f x)"; |
611 goal thy "(z : f``A) = (EX x:A. z = f x)"; |
612 by (Blast_tac 1); |
612 by (Blast_tac 1); |
613 qed "image_iff"; |
613 qed "image_iff"; |
|
614 |
|
615 val prems = goal thy "(!!x. x:A ==> f(x) : B) ==> f``A <= B"; |
|
616 by (blast_tac (claset() addIs prems) 1); |
|
617 qed "image_subsetI"; |
614 |
618 |
615 |
619 |
616 (*** Range of a function -- just a translation for image! ***) |
620 (*** Range of a function -- just a translation for image! ***) |
617 |
621 |
618 goal thy "!!b. b=f(x) ==> b : range(f)"; |
622 goal thy "!!b. b=f(x) ==> b : range(f)"; |