equal
deleted
inserted
replaced
81 |
81 |
82 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)" |
82 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)" |
83 unfolding permutes_def by simp |
83 unfolding permutes_def by simp |
84 |
84 |
85 lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y" |
85 lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y" |
86 unfolding permutes_def inv_onto_def apply auto |
86 unfolding permutes_def inv_def apply auto |
87 apply (erule allE[where x=y]) |
87 apply (erule allE[where x=y]) |
88 apply (erule allE[where x=y]) |
88 apply (erule allE[where x=y]) |
89 apply (rule someI_ex) apply blast |
89 apply (rule someI_ex) apply blast |
90 apply (rule some1_equality) |
90 apply (rule some1_equality) |
91 apply blast |
91 apply blast |