src/HOL/Complete_Lattice.thy
changeset 43898 935359fd8210
parent 43873 8a2f339641c1
child 43899 60ef6abb2f92
equal deleted inserted replaced
43893:f3e75541cb78 43898:935359fd8210
   395 lemma less_SUP_iff:
   395 lemma less_SUP_iff:
   396   fixes a :: "'a::{complete_lattice,linorder}"
   396   fixes a :: "'a::{complete_lattice,linorder}"
   397   shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   397   shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   398   unfolding SUP_def less_Sup_iff by auto
   398   unfolding SUP_def less_Sup_iff by auto
   399 
   399 
   400 -- "FIXME move"
       
   401 
       
   402 lemma image_ident [simp]: "(%x. x) ` Y = Y"
       
   403   by blast
       
   404 
       
   405 lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
       
   406   by blast
       
   407 
       
   408 class complete_boolean_algebra = boolean_algebra + complete_lattice
   400 class complete_boolean_algebra = boolean_algebra + complete_lattice
   409 begin
   401 begin
   410 
   402 
   411 lemma uminus_Inf:
   403 lemma uminus_Inf:
   412   "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
   404   "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"