add lemmas about closed sets
authorhuffman
Thu Jun 11 16:26:06 2009 -0700 (2009-06-11)
changeset 31568963caf6fa234
parent 31567 0fb78b3a9145
child 31569 f11a849bab61
add lemmas about closed sets
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Product_Vector.thy
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Thu Jun 11 15:33:13 2009 -0700
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Thu Jun 11 16:26:06 2009 -0700
     1.3 @@ -378,6 +378,17 @@
     1.4  apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp)
     1.5  done
     1.6  
     1.7 +lemma closed_vimage_Cart_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"
     1.8 +unfolding closed_open vimage_Compl [symmetric]
     1.9 +by (rule open_vimage_Cart_nth)
    1.10 +
    1.11 +lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
    1.12 +proof -
    1.13 +  have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto
    1.14 +  thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
    1.15 +    by (simp add: closed_INT closed_vimage_Cart_nth)
    1.16 +qed
    1.17 +
    1.18  lemma tendsto_Cart_nth [tendsto_intros]:
    1.19    assumes "((\<lambda>x. f x) ---> a) net"
    1.20    shows "((\<lambda>x. f x $ i) ---> a $ i) net"
     2.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Jun 11 15:33:13 2009 -0700
     2.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu Jun 11 16:26:06 2009 -0700
     2.3 @@ -87,6 +87,22 @@
     2.4  lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
     2.5  by (simp add: snd_vimage_eq_Times open_Times)
     2.6  
     2.7 +lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
     2.8 +unfolding closed_open vimage_Compl [symmetric]
     2.9 +by (rule open_vimage_fst)
    2.10 +
    2.11 +lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
    2.12 +unfolding closed_open vimage_Compl [symmetric]
    2.13 +by (rule open_vimage_snd)
    2.14 +
    2.15 +lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
    2.16 +proof -
    2.17 +  have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
    2.18 +  thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
    2.19 +    by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
    2.20 +qed
    2.21 +
    2.22 +
    2.23  subsection {* Product is a metric space *}
    2.24  
    2.25  instantiation