equal
deleted
inserted
replaced
69 assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" |
69 assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" |
70 unfolding open_prod_def by fast |
70 unfolding open_prod_def by fast |
71 qed |
71 qed |
72 |
72 |
73 end |
73 end |
|
74 |
|
75 lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)" |
|
76 unfolding open_prod_def by auto |
|
77 |
|
78 lemma fst_vimage_eq_Times: "fst -` S = S \<times> UNIV" |
|
79 by auto |
|
80 |
|
81 lemma snd_vimage_eq_Times: "snd -` S = UNIV \<times> S" |
|
82 by auto |
|
83 |
|
84 lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)" |
|
85 by (simp add: fst_vimage_eq_Times open_Times) |
|
86 |
|
87 lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)" |
|
88 by (simp add: snd_vimage_eq_Times open_Times) |
74 |
89 |
75 subsection {* Product is a metric space *} |
90 subsection {* Product is a metric space *} |
76 |
91 |
77 instantiation |
92 instantiation |
78 "*" :: (metric_space, metric_space) metric_space |
93 "*" :: (metric_space, metric_space) metric_space |