summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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