# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1596196486 -3600
# Node ID 8348bba699e6480b0b8e4350c243453b6f9b7e29
# Parent  b8d0b8659e0a0b436ae525e96c7a0f721d039c1e
A new lemma about abstract Sum / Prod

diff -r b8d0b8659e0a -r 8348bba699e6 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 = {}"