src/HOL/Complete_Lattice.thy
 changeset 43898 935359fd8210 parent 43873 8a2f339641c1 child 43899 60ef6abb2f92
equal 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 `
`   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)"`