src/HOL/Relation.ML
changeset 7913 86be2946bb0b
parent 7822 09aabe6d04b8
child 8004 6273f58ea2c1
     1.1 --- a/src/HOL/Relation.ML	Fri Oct 22 17:04:19 1999 +0200
     1.2 +++ b/src/HOL/Relation.ML	Fri Oct 22 18:26:46 1999 +0200
     1.3 @@ -376,6 +376,19 @@
     1.4  by (Blast_tac 1);
     1.5  qed "Image_eq_UN";
     1.6  
     1.7 +Goal "[| r'<=r; A'<=A |] ==> (r' ^^ A') <= (r ^^ A)";
     1.8 +by (Blast_tac 1);
     1.9 +qed "Image_mono";
    1.10 +
    1.11 +Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))";
    1.12 +by (Blast_tac 1);
    1.13 +qed "Image_UN";
    1.14 +
    1.15 +(*Converse inclusion fails*)
    1.16 +Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))";
    1.17 +by (Blast_tac 1);
    1.18 +qed "Image_INT_subset";
    1.19 +
    1.20  
    1.21  section "Univalent";
    1.22