equal
deleted
inserted
replaced
61 by (simp add: Pi_def) |
61 by (simp add: Pi_def) |
62 |
62 |
63 lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x" |
63 lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x" |
64 by (simp add: Pi_def) |
64 by (simp add: Pi_def) |
65 |
65 |
66 lemma ballE [elim]: |
66 lemma PiE [elim]: |
67 "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q" |
67 "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q" |
68 by(auto simp: Pi_def) |
68 by(auto simp: Pi_def) |
69 |
69 |
70 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B" |
70 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B" |
71 by (simp add: Pi_def) |
71 by (simp add: Pi_def) |