src/HOL/Library/FuncSet.thy
changeset 33271 7be66dee1a5a
parent 33057 764547b68538
child 38656 d5d342611edb
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Oct 27 14:46:03 2009 +0000
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Wed Oct 28 11:42:31 2009 +0000
     1.3 @@ -101,6 +101,19 @@
     1.4  lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
     1.5  by auto
     1.6  
     1.7 +lemma prod_final:
     1.8 +  assumes 1: "fst \<circ> f \<in> Pi A B" and 2: "snd \<circ> f \<in> Pi A C"
     1.9 +  shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)"
    1.10 +proof (rule Pi_I) 
    1.11 +  fix z
    1.12 +  assume z: "z \<in> A" 
    1.13 +  have "f z = (fst (f z), snd (f z))" 
    1.14 +    by simp
    1.15 +  also have "...  \<in> B z \<times> C z"
    1.16 +    by (metis SigmaI PiE o_apply 1 2 z) 
    1.17 +  finally show "f z \<in> B z \<times> C z" .
    1.18 +qed
    1.19 +
    1.20  
    1.21  subsection{*Composition With a Restricted Domain: @{term compose}*}
    1.22