# HG changeset patch
# User huffman
# Date 1312829261 25200
# Node ID dc0a73004c94716010c8535e4fc0a2ea842843f3
# Parent  5feac96f0e78602ca4064643e04b1ef9e9a5cc10
add lemmas INF_image, SUP_image

diff -r 5feac96f0e78 -r dc0a73004c94 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Aug 08 11:25:18 2011 -0700
+++ b/src/HOL/Complete_Lattice.thy	Mon Aug 08 11:47:41 2011 -0700
@@ -172,6 +172,12 @@
 lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   by (simp add: SUP_def Sup_insert)
 
+lemma INF_image: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
+  by (simp add: INF_def image_image)
+
+lemma SUP_image: "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
+  by (simp add: SUP_def image_image)
+
 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
   by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)