54 by auto |
54 by auto |
55 moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i" |
55 moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i" |
56 ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}" |
56 ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}" |
57 using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"] |
57 using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"] |
58 by (auto simp flip: INT_Int_distrib) |
58 by (auto simp flip: INT_Int_distrib) |
|
59 qed |
|
60 |
|
61 lemma diff_Union_pairwise_disjoint: |
|
62 assumes "pairwise disjnt \<A>" "\<B> \<subseteq> \<A>" |
|
63 shows "\<Union>\<A> - \<Union>\<B> = \<Union>(\<A> - \<B>)" |
|
64 proof - |
|
65 have "False" |
|
66 if x: "x \<in> A" "x \<in> B" and AB: "A \<in> \<A>" "A \<notin> \<B>" "B \<in> \<B>" for x A B |
|
67 proof - |
|
68 have "A \<inter> B = {}" |
|
69 using assms disjointD AB by blast |
|
70 with x show ?thesis |
|
71 by blast |
|
72 qed |
|
73 then show ?thesis by auto |
|
74 qed |
|
75 |
|
76 lemma Int_Union_pairwise_disjoint: |
|
77 assumes "pairwise disjnt (\<A> \<union> \<B>)" |
|
78 shows "\<Union>\<A> \<inter> \<Union>\<B> = \<Union>(\<A> \<inter> \<B>)" |
|
79 proof - |
|
80 have "False" |
|
81 if x: "x \<in> A" "x \<in> B" and AB: "A \<in> \<A>" "A \<notin> \<B>" "B \<in> \<B>" for x A B |
|
82 proof - |
|
83 have "A \<inter> B = {}" |
|
84 using assms disjointD AB by blast |
|
85 with x show ?thesis |
|
86 by blast |
|
87 qed |
|
88 then show ?thesis by auto |
|
89 qed |
|
90 |
|
91 lemma psubset_Union_pairwise_disjoint: |
|
92 assumes \<B>: "pairwise disjnt \<B>" and "\<A> \<subset> \<B> - {{}}" |
|
93 shows "\<Union>\<A> \<subset> \<Union>\<B>" |
|
94 unfolding psubset_eq |
|
95 proof |
|
96 show "\<Union>\<A> \<subseteq> \<Union>\<B>" |
|
97 using assms by blast |
|
98 have "\<A> \<subseteq> \<B>" "\<Union>(\<B> - \<A> \<inter> (\<B> - {{}})) \<noteq> {}" |
|
99 using assms by blast+ |
|
100 then show "\<Union>\<A> \<noteq> \<Union>\<B>" |
|
101 using diff_Union_pairwise_disjoint [OF \<B>] by blast |
59 qed |
102 qed |
60 |
103 |
61 subsubsection "Family of Disjoint Sets" |
104 subsubsection "Family of Disjoint Sets" |
62 |
105 |
63 definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where |
106 definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where |