equal
deleted
inserted
replaced
507 lemma UN_mono: |
507 lemma UN_mono: |
508 "[| A<=C; !!x. x:A ==> B(x)<=D(x) |] ==> (\<Union>x\<in>A. B(x)) <= (\<Union>x\<in>C. D(x))" |
508 "[| A<=C; !!x. x:A ==> B(x)<=D(x) |] ==> (\<Union>x\<in>A. B(x)) <= (\<Union>x\<in>C. D(x))" |
509 by blast |
509 by blast |
510 |
510 |
511 (*Intersection is ANTI-monotonic. There are TWO premises! *) |
511 (*Intersection is ANTI-monotonic. There are TWO premises! *) |
512 lemma Inter_anti_mono: "[| A<=B; a:A |] ==> Inter(B) <= Inter(A)" |
512 lemma Inter_anti_mono: "[| A<=B; A\<noteq>0 |] ==> Inter(B) <= Inter(A)" |
513 by blast |
513 by blast |
514 |
514 |
515 lemma cons_mono: "C<=D ==> cons(a,C) <= cons(a,D)" |
515 lemma cons_mono: "C<=D ==> cons(a,C) <= cons(a,D)" |
516 by blast |
516 by blast |
517 |
517 |