equal
deleted
inserted
replaced
636 lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A" |
636 lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A" |
637 by auto |
637 by auto |
638 |
638 |
639 lemma UNIV_not_empty [iff]: "UNIV ~= {}" |
639 lemma UNIV_not_empty [iff]: "UNIV ~= {}" |
640 by (blast elim: equalityE) |
640 by (blast elim: equalityE) |
|
641 |
|
642 lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV" |
|
643 by blast |
641 |
644 |
642 |
645 |
643 subsubsection {* The Powerset operator -- Pow *} |
646 subsubsection {* The Powerset operator -- Pow *} |
644 |
647 |
645 definition Pow :: "'a set => 'a set set" where |
648 definition Pow :: "'a set => 'a set set" where |