# HG changeset patch
# User paulson
# Date 940609606 -7200
# Node ID 86be2946bb0b354d38a294fbbff2b22be700057f
# Parent  0e42be14f13640f814ff1f73b1888346496f997c
new theorems on Image

diff -r 0e42be14f136 -r 86be2946bb0b src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Fri Oct 22 17:04:19 1999 +0200
+++ b/src/HOL/Relation.ML	Fri Oct 22 18:26:46 1999 +0200
@@ -376,6 +376,19 @@
 by (Blast_tac 1);
 qed "Image_eq_UN";
 
+Goal "[| r'<=r; A'<=A |] ==> (r' ^^ A') <= (r ^^ A)";
+by (Blast_tac 1);
+qed "Image_mono";
+
+Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))";
+by (Blast_tac 1);
+qed "Image_UN";
+
+(*Converse inclusion fails*)
+Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))";
+by (Blast_tac 1);
+qed "Image_INT_subset";
+
 
 section "Univalent";