equal
deleted
inserted
replaced
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)" |