# HG changeset patch
# User haftmann
# Date 1620675961 0
# Node ID 6e26d06b24b1150fd3734120674503a9f31eadc6
# Parent  7734c442802fed38c98fa3f81ac633587d9bad22
centralized more lemmas

diff -r 7734c442802f -r 6e26d06b24b1 src/HOL/Combinatorics/Transposition.thy
--- a/src/HOL/Combinatorics/Transposition.thy	Mon May 10 19:45:54 2021 +0000
+++ b/src/HOL/Combinatorics/Transposition.thy	Mon May 10 19:46:01 2021 +0000
@@ -100,6 +100,10 @@
   if \<open>bij f\<close>
   using that by (simp add: fun_eq_iff transpose_apply_commute)
 
+lemma in_transpose_image_iff:
+  \<open>x \<in> transpose a b ` S \<longleftrightarrow> transpose a b x \<in> S\<close>
+  by (auto intro!: image_eqI)
+
 
 text \<open>Legacy input alias\<close>