summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Thu, 11 Jun 2009 16:26:06 -0700 | |

changeset 31568 | 963caf6fa234 |

parent 31567 | 0fb78b3a9145 |

child 31569 | f11a849bab61 |

add lemmas about closed sets

src/HOL/Library/Euclidean_Space.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Product_Vector.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Library/Euclidean_Space.thy Thu Jun 11 15:33:13 2009 -0700 +++ b/src/HOL/Library/Euclidean_Space.thy Thu Jun 11 16:26:06 2009 -0700 @@ -378,6 +378,17 @@ apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp) done +lemma closed_vimage_Cart_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)" +unfolding closed_open vimage_Compl [symmetric] +by (rule open_vimage_Cart_nth) + +lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" +proof - + have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto + thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" + by (simp add: closed_INT closed_vimage_Cart_nth) +qed + lemma tendsto_Cart_nth [tendsto_intros]: assumes "((\<lambda>x. f x) ---> a) net" shows "((\<lambda>x. f x $ i) ---> a $ i) net"

--- a/src/HOL/Library/Product_Vector.thy Thu Jun 11 15:33:13 2009 -0700 +++ b/src/HOL/Library/Product_Vector.thy Thu Jun 11 16:26:06 2009 -0700 @@ -87,6 +87,22 @@ lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)" by (simp add: snd_vimage_eq_Times open_Times) +lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)" +unfolding closed_open vimage_Compl [symmetric] +by (rule open_vimage_fst) + +lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)" +unfolding closed_open vimage_Compl [symmetric] +by (rule open_vimage_snd) + +lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)" +proof - + have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto + thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)" + by (simp add: closed_vimage_fst closed_vimage_snd closed_Int) +qed + + subsection {* Product is a metric space *} instantiation