equal
deleted
inserted
replaced
84 lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)" |
84 lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)" |
85 by (simp add: fst_vimage_eq_Times open_Times) |
85 by (simp add: fst_vimage_eq_Times open_Times) |
86 |
86 |
87 lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)" |
87 lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)" |
88 by (simp add: snd_vimage_eq_Times open_Times) |
88 by (simp add: snd_vimage_eq_Times open_Times) |
|
89 |
|
90 lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)" |
|
91 unfolding closed_open vimage_Compl [symmetric] |
|
92 by (rule open_vimage_fst) |
|
93 |
|
94 lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)" |
|
95 unfolding closed_open vimage_Compl [symmetric] |
|
96 by (rule open_vimage_snd) |
|
97 |
|
98 lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)" |
|
99 proof - |
|
100 have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto |
|
101 thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)" |
|
102 by (simp add: closed_vimage_fst closed_vimage_snd closed_Int) |
|
103 qed |
|
104 |
89 |
105 |
90 subsection {* Product is a metric space *} |
106 subsection {* Product is a metric space *} |
91 |
107 |
92 instantiation |
108 instantiation |
93 "*" :: (metric_space, metric_space) metric_space |
109 "*" :: (metric_space, metric_space) metric_space |