added lemma
authornipkow
Mon, 19 Feb 2018 13:56:16 +0100
changeset 67656 59feb83c6ab9
parent 67655 8f4810b9d9d1
child 67658 67909bfc3923
child 67674 52b0d4cd4be7
added lemma
src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Feb 19 13:56:16 2018 +0100
@@ -2407,6 +2407,9 @@
 lemma Union_mset_empty_conv[simp]: "\<Union># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
   by (induction M) auto
 
+lemma Union_image_single_mset[simp]: "\<Union># (image_mset (\<lambda>x. {#x#}) m) = m"
+by(induction m) auto
+
 
 context comm_monoid_mult
 begin