equal
deleted
inserted
replaced
41 lemma permutes_inj: "p permutes S \<Longrightarrow> inj p" |
41 lemma permutes_inj: "p permutes S \<Longrightarrow> inj p" |
42 unfolding permutes_def inj_on_def by blast |
42 unfolding permutes_def inj_on_def by blast |
43 |
43 |
44 lemma permutes_surj: "p permutes s \<Longrightarrow> surj p" |
44 lemma permutes_surj: "p permutes s \<Longrightarrow> surj p" |
45 unfolding permutes_def surj_def by metis |
45 unfolding permutes_def surj_def by metis |
|
46 |
|
47 lemma permutes_imp_bij: "p permutes S \<Longrightarrow> bij_betw p S S" |
|
48 by (metis UNIV_I bij_betw_def permutes_image permutes_inj subsetI subset_inj_on) |
|
49 |
|
50 lemma bij_imp_permutes: "bij_betw p S S \<Longrightarrow> (\<And>x. x \<notin> S \<Longrightarrow> p x = x) \<Longrightarrow> p permutes S" |
|
51 unfolding permutes_def bij_betw_def inj_on_def |
|
52 by auto (metis image_iff)+ |
46 |
53 |
47 lemma permutes_inv_o: |
54 lemma permutes_inv_o: |
48 assumes pS: "p permutes S" |
55 assumes pS: "p permutes S" |
49 shows "p \<circ> inv p = id" |
56 shows "p \<circ> inv p = id" |
50 and "inv p \<circ> p = id" |
57 and "inv p \<circ> p = id" |