equal
deleted
inserted
replaced
49 "compose A g f = (\<lambda>x\<in>A. g (f x))" |
49 "compose A g f = (\<lambda>x\<in>A. g (f x))" |
50 |
50 |
51 |
51 |
52 subsection{*Basic Properties of @{term Pi}*} |
52 subsection{*Basic Properties of @{term Pi}*} |
53 |
53 |
54 lemma Pi_I[simp]: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B" |
54 lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B" |
55 by (simp add: Pi_def) |
55 by (simp add: Pi_def) |
|
56 |
|
57 lemma Pi_I'[simp]: "(!!x. x : A --> f x : B x) ==> f : Pi A B" |
|
58 by(simp add:Pi_def) |
56 |
59 |
57 lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B" |
60 lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B" |
58 by (simp add: Pi_def) |
61 by (simp add: Pi_def) |
59 |
62 |
60 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" |