equal
deleted
inserted
replaced
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 |