changeset 8004 | 6273f58ea2c1 |
parent 7913 | 86be2946bb0b |
child 8174 | 56d9baa2ddb0 |
--- a/src/HOL/Relation.ML Sat Nov 06 15:34:12 1999 +0100 +++ b/src/HOL/Relation.ML Thu Nov 11 10:24:14 1999 +0100 @@ -309,7 +309,7 @@ (*** Image of a set under a relation ***) -overload_1st_set "Relation.op ^^"; +overload_1st_set "Relation.Image"; Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)"; by (Blast_tac 1); @@ -389,6 +389,9 @@ by (Blast_tac 1); qed "Image_INT_subset"; +Goal "(r^^A <= B) = (A <= - ((r^-1) ^^ (-B)))"; +by (Blast_tac 1); +qed "Image_subset_eq"; section "Univalent";