equal
deleted
inserted
replaced
2165 fixes M::"('a::fs multiset)" |
2165 fixes M::"('a::fs multiset)" |
2166 shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" |
2166 shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" |
2167 proof - |
2167 proof - |
2168 have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp |
2168 have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp |
2169 also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto |
2169 also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto |
2170 also have "... = supp (set_of M)" by (simp add: subst supp_of_finite_sets) |
2170 also have "... = supp (set_of M)" by (simp add: supp_of_finite_sets) |
2171 also have " ... \<subseteq> supp M" by (rule supp_set_of) |
2171 also have " ... \<subseteq> supp M" by (rule supp_set_of) |
2172 finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" . |
2172 finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" . |
2173 qed |
2173 qed |
2174 |
2174 |
2175 lemma supp_of_multisets: |
2175 lemma supp_of_multisets: |