equal
deleted
inserted
replaced
409 |
409 |
410 lemma subset_Un_eq: "(A<=B) \<longleftrightarrow> (A Un B = B)" |
410 lemma subset_Un_eq: "(A<=B) \<longleftrightarrow> (A Un B = B)" |
411 by (blast intro: equalityI elim: equalityE) |
411 by (blast intro: equalityI elim: equalityE) |
412 |
412 |
413 |
413 |
414 subsection \<open>Simple properties of @{text "Compl"} -- complement of a set\<close> |
414 subsection \<open>Simple properties of \<open>Compl\<close> -- complement of a set\<close> |
415 |
415 |
416 lemma Compl_disjoint: "A Int Compl(A) = {x. False}" |
416 lemma Compl_disjoint: "A Int Compl(A) = {x. False}" |
417 by (blast intro: equalityI) |
417 by (blast intro: equalityI) |
418 |
418 |
419 lemma Compl_partition: "A Un Compl(A) = {x. True}" |
419 lemma Compl_partition: "A Un Compl(A) = {x. True}" |