src/HOL/Library/Product_Vector.thy
changeset 31568 963caf6fa234
parent 31565 da5a5589418e
child 31587 a7e187205fc0
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Jun 11 15:33:13 2009 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu Jun 11 16:26:06 2009 -0700
     1.3 @@ -87,6 +87,22 @@
     1.4  lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
     1.5  by (simp add: snd_vimage_eq_Times open_Times)
     1.6  
     1.7 +lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
     1.8 +unfolding closed_open vimage_Compl [symmetric]
     1.9 +by (rule open_vimage_fst)
    1.10 +
    1.11 +lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
    1.12 +unfolding closed_open vimage_Compl [symmetric]
    1.13 +by (rule open_vimage_snd)
    1.14 +
    1.15 +lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
    1.16 +proof -
    1.17 +  have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
    1.18 +  thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
    1.19 +    by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
    1.20 +qed
    1.21 +
    1.22 +
    1.23  subsection {* Product is a metric space *}
    1.24  
    1.25  instantiation