equal
deleted
inserted
replaced
135 |] ==> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)" |
135 |] ==> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)" |
136 apply (unfold bij_def) |
136 apply (unfold bij_def) |
137 apply (blast intro!: lam_injective lam_surjective) |
137 apply (blast intro!: lam_injective lam_surjective) |
138 done |
138 done |
139 |
139 |
140 lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y)) |
140 lemma RepFun_bijective: "(\<forall>y\<in>x. \<exists>!y'. f(y') = f(y)) |
141 ==> (\<lambda>z\<in>{f(y). y \<in> x}. THE y. f(y) = z) \<in> bij({f(y). y \<in> x}, x)" |
141 ==> (\<lambda>z\<in>{f(y). y \<in> x}. THE y. f(y) = z) \<in> bij({f(y). y \<in> x}, x)" |
142 apply (rule_tac d = f in lam_bijective) |
142 apply (rule_tac d = f in lam_bijective) |
143 apply (auto simp add: the_equality2) |
143 apply (auto simp add: the_equality2) |
144 done |
144 done |
145 |
145 |