equal
deleted
inserted
replaced
193 fixes A :: "'a::pt set" |
193 fixes A :: "'a::pt set" |
194 shows "p \<bullet> (- A) = - (p \<bullet> A)" |
194 shows "p \<bullet> (- A) = - (p \<bullet> A)" |
195 unfolding Compl_eq_Diff_UNIV |
195 unfolding Compl_eq_Diff_UNIV |
196 by (perm_simp) (rule refl) |
196 by (perm_simp) (rule refl) |
197 |
197 |
|
198 lemma subset_eqvt[eqvt]: |
|
199 shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)" |
|
200 unfolding subset_eq |
|
201 by (perm_simp) (rule refl) |
|
202 |
|
203 lemma psubset_eqvt[eqvt]: |
|
204 shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)" |
|
205 unfolding psubset_eq |
|
206 by (perm_simp) (rule refl) |
|
207 |
198 lemma image_eqvt: |
208 lemma image_eqvt: |
199 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
209 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
200 unfolding permute_set_eq_image |
210 unfolding permute_set_eq_image |
201 unfolding permute_fun_def [where f=f] |
211 unfolding permute_fun_def [where f=f] |
202 by (simp add: image_image) |
212 by (simp add: image_image) |