src/HOL/Library/Permutations.thy
changeset 60601 6e83d94760c4
parent 60500 903bb1495239
child 61424 c3658c18b7bc
     1.1 --- a/src/HOL/Library/Permutations.thy	Sat Jun 27 20:26:33 2015 +0200
     1.2 +++ b/src/HOL/Library/Permutations.thy	Sun Jun 28 14:30:53 2015 +0200
     1.3 @@ -44,8 +44,11 @@
     1.4  lemma permutes_surj: "p permutes s \<Longrightarrow> surj p"
     1.5    unfolding permutes_def surj_def by metis
     1.6  
     1.7 +lemma permutes_bij: "p permutes s \<Longrightarrow> bij p"
     1.8 +unfolding bij_def by (metis permutes_inj permutes_surj)
     1.9 +
    1.10  lemma permutes_imp_bij: "p permutes S \<Longrightarrow> bij_betw p S S"
    1.11 -  by (metis UNIV_I bij_betw_def permutes_image permutes_inj subsetI subset_inj_on)
    1.12 +by (metis UNIV_I bij_betw_subset permutes_bij permutes_image subsetI)
    1.13  
    1.14  lemma bij_imp_permutes: "bij_betw p S S \<Longrightarrow> (\<And>x. x \<notin> S \<Longrightarrow> p x = x) \<Longrightarrow> p permutes S"
    1.15    unfolding permutes_def bij_betw_def inj_on_def