centralized more lemmas
authorhaftmann
Mon, 10 May 2021 19:46:01 +0000
changeset 73920 6e26d06b24b1
parent 73919 7734c442802f
child 73926 4121fc47432b
centralized more lemmas
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>