src/HOL/Combinatorics/Transposition.thy
changeset 73664 6e26d06b24b1
parent 73648 1bd3463e30b8
equal deleted inserted replaced
73663:7734c442802f 73664:6e26d06b24b1
    98 lemma transpose_comp_eq:
    98 lemma transpose_comp_eq:
    99   \<open>transpose a b \<circ> f = f \<circ> transpose (inv f a) (inv f b)\<close>
    99   \<open>transpose a b \<circ> f = f \<circ> transpose (inv f a) (inv f b)\<close>
   100   if \<open>bij f\<close>
   100   if \<open>bij f\<close>
   101   using that by (simp add: fun_eq_iff transpose_apply_commute)
   101   using that by (simp add: fun_eq_iff transpose_apply_commute)
   102 
   102 
       
   103 lemma in_transpose_image_iff:
       
   104   \<open>x \<in> transpose a b ` S \<longleftrightarrow> transpose a b x \<in> S\<close>
       
   105   by (auto intro!: image_eqI)
       
   106 
   103 
   107 
   104 text \<open>Legacy input alias\<close>
   108 text \<open>Legacy input alias\<close>
   105 
   109 
   106 setup \<open>Context.theory_map (Name_Space.map_naming (Name_Space.qualified_path true \<^binding>\<open>Fun\<close>))\<close>
   110 setup \<open>Context.theory_map (Name_Space.map_naming (Name_Space.qualified_path true \<^binding>\<open>Fun\<close>))\<close>
   107 
   111