equal
deleted
inserted
replaced
194 lemma psubset_eqvt[eqvt]: |
194 lemma psubset_eqvt[eqvt]: |
195 shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)" |
195 shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)" |
196 unfolding psubset_eq |
196 unfolding psubset_eq |
197 by (perm_simp) (rule refl) |
197 by (perm_simp) (rule refl) |
198 |
198 |
199 lemma image_eqvt: |
199 lemma image_eqvt[eqvt]: |
200 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
200 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
201 unfolding permute_set_eq_image |
201 unfolding permute_set_eq_image |
202 unfolding permute_fun_def [where f=f] |
202 unfolding permute_fun_def [where f=f] |
203 by (simp add: image_image) |
203 by (simp add: image_image) |
204 |
204 |
209 |
209 |
210 lemma Union_eqvt[eqvt]: |
210 lemma Union_eqvt[eqvt]: |
211 shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)" |
211 shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)" |
212 unfolding Union_eq |
212 unfolding Union_eq |
213 by (perm_simp) (rule refl) |
213 by (perm_simp) (rule refl) |
|
214 |
|
215 lemma Sigma_eqvt: |
|
216 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
|
217 unfolding Sigma_def |
|
218 unfolding UNION_eq_Union_image |
|
219 by (perm_simp) (rule refl) |
214 |
220 |
215 lemma finite_permute_iff: |
221 lemma finite_permute_iff: |
216 shows "finite (p \<bullet> A) \<longleftrightarrow> finite A" |
222 shows "finite (p \<bullet> A) \<longleftrightarrow> finite A" |
217 unfolding permute_set_eq_vimage |
223 unfolding permute_set_eq_vimage |
218 using bij_permute by (rule finite_vimage_iff) |
224 using bij_permute by (rule finite_vimage_iff) |