A new lemma about abstract Sum / Prod
authorpaulson <lp15@cam.ac.uk>
Fri, 31 Jul 2020 12:54:46 +0100
changeset 72309 8348bba699e6
parent 72308 b8d0b8659e0a
child 72310 5d17e7a0825a
A new lemma about abstract Sum / Prod
src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Jul 29 14:23:19 2020 +0200
+++ b/src/HOL/Groups_Big.thy	Fri Jul 31 12:54:46 2020 +0100
@@ -165,6 +165,11 @@
   shows "F g A = F h B"
   using assms by (simp add: reindex)
 
+lemma image_eq:
+  assumes "inj_on g A"  
+  shows "F (\<lambda>x. x) (g ` A) = F g A"
+  using assms reindex_cong by fastforce
+
 lemma UNION_disjoint:
   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"