author | paulson <lp15@cam.ac.uk> |
Tue, 19 Mar 2019 16:14:51 +0000 | |
changeset 69922 | 4a9167f377b0 |
child 69939 | 812ce526da33 |
permissions | -rw-r--r-- |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1 |
theory Product_Topology |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
2 |
imports Function_Topology |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
3 |
begin |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
4 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
5 |
lemma subset_UnE: (*FIXME MOVE*) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
6 |
assumes "C \<subseteq> A \<union> B" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
obtains A' B' where "A' \<subseteq> A" "B' \<subseteq> B" "C = A' \<union> B'" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
by (metis assms Int_Un_distrib inf.order_iff inf_le2) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
9 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
10 |
section \<open>Product Topology\<close> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
11 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
12 |
subsection\<open>A binary product topology where the two types can be different.\<close> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
13 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
14 |
definition prod_topology :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<times> 'b) topology" where |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
15 |
"prod_topology X Y \<equiv> topology (arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T}))" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
16 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
17 |
lemma open_product_open: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
18 |
assumes "open A" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
19 |
shows "\<exists>\<U>. \<U> \<subseteq> {S \<times> T |S T. open S \<and> open T} \<and> \<Union> \<U> = A" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
20 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
21 |
obtain f g where *: "\<And>u. u \<in> A \<Longrightarrow> open (f u) \<and> open (g u) \<and> u \<in> (f u) \<times> (g u) \<and> (f u) \<times> (g u) \<subseteq> A" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
22 |
using open_prod_def [of A] assms by metis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
23 |
let ?\<U> = "(\<lambda>u. f u \<times> g u) ` A" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
24 |
show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
25 |
by (rule_tac x="?\<U>" in exI) (auto simp: dest: *) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
26 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
27 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
28 |
lemma open_product_open_eq: "(arbitrary union_of (\<lambda>U. \<exists>S T. U = S \<times> T \<and> open S \<and> open T)) = open" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
29 |
by (force simp: union_of_def arbitrary_def intro: open_product_open open_Times) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
30 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
31 |
lemma openin_prod_topology: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
32 |
"openin (prod_topology X Y) = arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T})" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
33 |
unfolding prod_topology_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
34 |
proof (rule topology_inverse') |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
35 |
show "istopology (arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T}))" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
36 |
apply (rule istopology_base, simp) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
37 |
by (metis openin_Int times_Int_times) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
38 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
39 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
40 |
lemma topspace_prod_topology [simp]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
41 |
"topspace (prod_topology X Y) = topspace X \<times> topspace Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
42 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
43 |
have "topspace(prod_topology X Y) = \<Union> (Collect (openin (prod_topology X Y)))" (is "_ = ?Z") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
44 |
unfolding topspace_def .. |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
45 |
also have "\<dots> = topspace X \<times> topspace Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
46 |
proof |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
47 |
show "?Z \<subseteq> topspace X \<times> topspace Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
48 |
apply (auto simp: openin_prod_topology union_of_def arbitrary_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
49 |
using openin_subset by force+ |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
50 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
51 |
have *: "\<exists>A B. topspace X \<times> topspace Y = A \<times> B \<and> openin X A \<and> openin Y B" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
52 |
by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
53 |
show "topspace X \<times> topspace Y \<subseteq> ?Z" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
54 |
apply (rule Union_upper) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
55 |
using * by (simp add: openin_prod_topology arbitrary_union_of_inc) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
56 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
57 |
finally show ?thesis . |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
58 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
59 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
60 |
lemma subtopology_Times: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
61 |
shows "subtopology (prod_topology X Y) (S \<times> T) = prod_topology (subtopology X S) (subtopology Y T)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
62 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
63 |
have "((\<lambda>U. \<exists>S T. U = S \<times> T \<and> openin X S \<and> openin Y T) relative_to S \<times> T) = |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
64 |
(\<lambda>U. \<exists>S' T'. U = S' \<times> T' \<and> (openin X relative_to S) S' \<and> (openin Y relative_to T) T')" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
65 |
by (auto simp: relative_to_def times_Int_times fun_eq_iff) metis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
66 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
67 |
by (simp add: topology_eq openin_prod_topology arbitrary_union_of_relative_to flip: openin_relative_to) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
68 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
69 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
70 |
lemma prod_topology_subtopology: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
71 |
"prod_topology (subtopology X S) Y = subtopology (prod_topology X Y) (S \<times> topspace Y)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
72 |
"prod_topology X (subtopology Y T) = subtopology (prod_topology X Y) (topspace X \<times> T)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
73 |
by (auto simp: subtopology_Times) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
74 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
75 |
lemma prod_topology_discrete_topology: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
76 |
"discrete_topology (S \<times> T) = prod_topology (discrete_topology S) (discrete_topology T)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
77 |
by (auto simp: discrete_topology_unique openin_prod_topology intro: arbitrary_union_of_inc) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
78 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
79 |
lemma prod_topology_euclidean [simp]: "prod_topology euclidean euclidean = euclidean" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
80 |
by (simp add: prod_topology_def open_product_open_eq) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
81 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
82 |
lemma prod_topology_subtopology_eu [simp]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
83 |
"prod_topology (subtopology euclidean S) (subtopology euclidean T) = subtopology euclidean (S \<times> T)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
84 |
by (simp add: prod_topology_subtopology subtopology_subtopology times_Int_times) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
85 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
86 |
lemma continuous_map_subtopology_eu [simp]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
87 |
"continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
88 |
apply safe |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
89 |
apply (metis continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
90 |
apply (simp add: continuous_map_closedin_preimage_eq image_subset_iff) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
91 |
by (metis (no_types, hide_lams) continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
92 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
93 |
lemma openin_prod_topology_alt: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
94 |
"openin (prod_topology X Y) S \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
95 |
(\<forall>x y. (x,y) \<in> S \<longrightarrow> (\<exists>U V. openin X U \<and> openin Y V \<and> x \<in> U \<and> y \<in> V \<and> U \<times> V \<subseteq> S))" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
96 |
apply (auto simp: openin_prod_topology arbitrary_union_of_alt, fastforce) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
97 |
by (metis mem_Sigma_iff) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
98 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
99 |
lemma open_map_fst: "open_map (prod_topology X Y) X fst" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
100 |
unfolding open_map_def openin_prod_topology_alt |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
101 |
by (force simp: openin_subopen [of X "fst ` _"] intro: subset_fst_imageI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
102 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
103 |
lemma open_map_snd: "open_map (prod_topology X Y) Y snd" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
104 |
unfolding open_map_def openin_prod_topology_alt |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
105 |
by (force simp: openin_subopen [of Y "snd ` _"] intro: subset_snd_imageI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
106 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
107 |
lemma openin_Times: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
108 |
"openin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> openin X S \<and> openin Y T" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
109 |
proof (cases "S = {} \<or> T = {}") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
110 |
case False |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
111 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
112 |
apply (simp add: openin_prod_topology_alt openin_subopen [of X S] openin_subopen [of Y T] times_subset_iff, safe) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
113 |
apply (meson|force)+ |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
114 |
done |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
115 |
qed force |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
116 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
117 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
118 |
lemma closure_of_Times: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
119 |
"(prod_topology X Y) closure_of (S \<times> T) = (X closure_of S) \<times> (Y closure_of T)" (is "?lhs = ?rhs") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
120 |
proof |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
121 |
show "?lhs \<subseteq> ?rhs" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
122 |
by (clarsimp simp: closure_of_def openin_prod_topology_alt) blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
123 |
show "?rhs \<subseteq> ?lhs" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
124 |
by (clarsimp simp: closure_of_def openin_prod_topology_alt) (meson SigmaI subsetD) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
125 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
126 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
127 |
lemma closedin_Times: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
128 |
"closedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> closedin X S \<and> closedin Y T" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
129 |
by (auto simp: closure_of_Times times_eq_iff simp flip: closure_of_eq) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
130 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
131 |
lemma continuous_map_pairwise: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
132 |
"continuous_map Z (prod_topology X Y) f \<longleftrightarrow> continuous_map Z X (fst \<circ> f) \<and> continuous_map Z Y (snd \<circ> f)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
133 |
(is "?lhs = ?rhs") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
134 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
135 |
let ?g = "fst \<circ> f" and ?h = "snd \<circ> f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
136 |
have f: "f x = (?g x, ?h x)" for x |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
137 |
by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
138 |
show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
139 |
proof (cases "(\<forall>x \<in> topspace Z. ?g x \<in> topspace X) \<and> (\<forall>x \<in> topspace Z. ?h x \<in> topspace Y)") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
140 |
case True |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
141 |
show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
142 |
proof safe |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
143 |
assume "continuous_map Z (prod_topology X Y) f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
144 |
then have "openin Z {x \<in> topspace Z. fst (f x) \<in> U}" if "openin X U" for U |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
145 |
unfolding continuous_map_def using True that |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
146 |
apply clarify |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
147 |
apply (drule_tac x="U \<times> topspace Y" in spec) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
148 |
by (simp add: openin_Times mem_Times_iff cong: conj_cong) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
149 |
with True show "continuous_map Z X (fst \<circ> f)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
150 |
by (auto simp: continuous_map_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
151 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
152 |
assume "continuous_map Z (prod_topology X Y) f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
153 |
then have "openin Z {x \<in> topspace Z. snd (f x) \<in> V}" if "openin Y V" for V |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
154 |
unfolding continuous_map_def using True that |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
155 |
apply clarify |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
156 |
apply (drule_tac x="topspace X \<times> V" in spec) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
157 |
by (simp add: openin_Times mem_Times_iff cong: conj_cong) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
158 |
with True show "continuous_map Z Y (snd \<circ> f)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
159 |
by (auto simp: continuous_map_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
160 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
161 |
assume Z: "continuous_map Z X (fst \<circ> f)" "continuous_map Z Y (snd \<circ> f)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
162 |
have *: "openin Z {x \<in> topspace Z. f x \<in> W}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
163 |
if "\<And>w. w \<in> W \<Longrightarrow> \<exists>U V. openin X U \<and> openin Y V \<and> w \<in> U \<times> V \<and> U \<times> V \<subseteq> W" for W |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
164 |
proof (subst openin_subopen, clarify) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
165 |
fix x :: "'a" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
166 |
assume "x \<in> topspace Z" and "f x \<in> W" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
167 |
with that [OF \<open>f x \<in> W\<close>] |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
168 |
obtain U V where UV: "openin X U" "openin Y V" "f x \<in> U \<times> V" "U \<times> V \<subseteq> W" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
169 |
by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
170 |
with Z UV show "\<exists>T. openin Z T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace Z. f x \<in> W}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
171 |
apply (rule_tac x="{x \<in> topspace Z. ?g x \<in> U} \<inter> {x \<in> topspace Z. ?h x \<in> V}" in exI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
172 |
apply (auto simp: \<open>x \<in> topspace Z\<close> continuous_map_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
173 |
done |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
174 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
175 |
show "continuous_map Z (prod_topology X Y) f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
176 |
using True by (simp add: continuous_map_def openin_prod_topology_alt mem_Times_iff *) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
177 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
178 |
qed (auto simp: continuous_map_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
179 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
180 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
181 |
lemma continuous_map_paired: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
182 |
"continuous_map Z (prod_topology X Y) (\<lambda>x. (f x,g x)) \<longleftrightarrow> continuous_map Z X f \<and> continuous_map Z Y g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
183 |
by (simp add: continuous_map_pairwise o_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
184 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
185 |
lemma continuous_map_pairedI [continuous_intros]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
186 |
"\<lbrakk>continuous_map Z X f; continuous_map Z Y g\<rbrakk> \<Longrightarrow> continuous_map Z (prod_topology X Y) (\<lambda>x. (f x,g x))" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
187 |
by (simp add: continuous_map_pairwise o_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
188 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
189 |
lemma continuous_map_fst [continuous_intros]: "continuous_map (prod_topology X Y) X fst" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
190 |
using continuous_map_pairwise [of "prod_topology X Y" X Y id] |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
191 |
by (simp add: continuous_map_pairwise) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
192 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
193 |
lemma continuous_map_snd [continuous_intros]: "continuous_map (prod_topology X Y) Y snd" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
194 |
using continuous_map_pairwise [of "prod_topology X Y" X Y id] |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
195 |
by (simp add: continuous_map_pairwise) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
196 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
197 |
lemma continuous_map_fst_of [continuous_intros]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
198 |
"continuous_map Z (prod_topology X Y) f \<Longrightarrow> continuous_map Z X (fst \<circ> f)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
199 |
by (simp add: continuous_map_pairwise) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
200 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
201 |
lemma continuous_map_snd_of [continuous_intros]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
202 |
"continuous_map Z (prod_topology X Y) f \<Longrightarrow> continuous_map Z Y (snd \<circ> f)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
203 |
by (simp add: continuous_map_pairwise) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
204 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
205 |
lemma continuous_map_if_iff [simp]: "continuous_map X Y (\<lambda>x. if P then f x else g x) \<longleftrightarrow> continuous_map X Y (if P then f else g)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
206 |
by simp |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
207 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
208 |
lemma continuous_map_if [continuous_intros]: "\<lbrakk>P \<Longrightarrow> continuous_map X Y f; ~P \<Longrightarrow> continuous_map X Y g\<rbrakk> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
209 |
\<Longrightarrow> continuous_map X Y (\<lambda>x. if P then f x else g x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
210 |
by simp |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
211 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
212 |
lemma continuous_map_subtopology_fst [continuous_intros]: "continuous_map (subtopology (prod_topology X Y) Z) X fst" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
213 |
using continuous_map_from_subtopology continuous_map_fst by force |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
214 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
215 |
lemma continuous_map_subtopology_snd [continuous_intros]: "continuous_map (subtopology (prod_topology X Y) Z) Y snd" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
216 |
using continuous_map_from_subtopology continuous_map_snd by force |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
217 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
218 |
lemma quotient_map_fst [simp]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
219 |
"quotient_map(prod_topology X Y) X fst \<longleftrightarrow> (topspace Y = {} \<longrightarrow> topspace X = {})" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
220 |
by (auto simp: continuous_open_quotient_map open_map_fst continuous_map_fst) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
221 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
222 |
lemma quotient_map_snd [simp]: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
223 |
"quotient_map(prod_topology X Y) Y snd \<longleftrightarrow> (topspace X = {} \<longrightarrow> topspace Y = {})" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
224 |
by (auto simp: continuous_open_quotient_map open_map_snd continuous_map_snd) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
225 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
226 |
lemma retraction_map_fst: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
227 |
"retraction_map (prod_topology X Y) X fst \<longleftrightarrow> (topspace Y = {} \<longrightarrow> topspace X = {})" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
228 |
proof (cases "topspace Y = {}") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
229 |
case True |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
230 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
231 |
using continuous_map_image_subset_topspace |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
232 |
by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst continuous_map_on_empty) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
233 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
234 |
case False |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
235 |
have "\<exists>g. continuous_map X (prod_topology X Y) g \<and> (\<forall>x\<in>topspace X. fst (g x) = x)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
236 |
if y: "y \<in> topspace Y" for y |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
237 |
by (rule_tac x="\<lambda>x. (x,y)" in exI) (auto simp: y continuous_map_paired) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
238 |
with False have "retraction_map (prod_topology X Y) X fst" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
239 |
by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
240 |
with False show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
241 |
by simp |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
242 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
243 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
244 |
lemma retraction_map_snd: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
245 |
"retraction_map (prod_topology X Y) Y snd \<longleftrightarrow> (topspace X = {} \<longrightarrow> topspace Y = {})" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
246 |
proof (cases "topspace X = {}") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
247 |
case True |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
248 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
249 |
using continuous_map_image_subset_topspace |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
250 |
by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst continuous_map_on_empty) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
251 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
252 |
case False |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
253 |
have "\<exists>g. continuous_map Y (prod_topology X Y) g \<and> (\<forall>y\<in>topspace Y. snd (g y) = y)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
254 |
if x: "x \<in> topspace X" for x |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
255 |
by (rule_tac x="\<lambda>y. (x,y)" in exI) (auto simp: x continuous_map_paired) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
256 |
with False have "retraction_map (prod_topology X Y) Y snd" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
257 |
by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_snd) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
258 |
with False show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
259 |
by simp |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
260 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
261 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
262 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
263 |
lemma continuous_map_of_fst: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
264 |
"continuous_map (prod_topology X Y) Z (f \<circ> fst) \<longleftrightarrow> topspace Y = {} \<or> continuous_map X Z f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
265 |
proof (cases "topspace Y = {}") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
266 |
case True |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
267 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
268 |
by (simp add: continuous_map_on_empty) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
269 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
270 |
case False |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
271 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
272 |
by (simp add: continuous_compose_quotient_map_eq quotient_map_fst) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
273 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
274 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
275 |
lemma continuous_map_of_snd: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
276 |
"continuous_map (prod_topology X Y) Z (f \<circ> snd) \<longleftrightarrow> topspace X = {} \<or> continuous_map Y Z f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
277 |
proof (cases "topspace X = {}") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
278 |
case True |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
279 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
280 |
by (simp add: continuous_map_on_empty) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
281 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
282 |
case False |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
283 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
284 |
by (simp add: continuous_compose_quotient_map_eq quotient_map_snd) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
285 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
286 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
287 |
lemma continuous_map_prod_top: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
288 |
"continuous_map (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y)) \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
289 |
topspace (prod_topology X Y) = {} \<or> continuous_map X X' f \<and> continuous_map Y Y' g" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
290 |
proof (cases "topspace (prod_topology X Y) = {}") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
291 |
case True |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
292 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
293 |
by (simp add: continuous_map_on_empty) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
294 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
295 |
case False |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
296 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
297 |
by (simp add: continuous_map_paired case_prod_unfold continuous_map_of_fst [unfolded o_def] continuous_map_of_snd [unfolded o_def]) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
298 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
299 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
300 |
lemma homeomorphic_maps_prod: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
301 |
"homeomorphic_maps (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y)) (\<lambda>(x,y). (f' x, g' y)) \<longleftrightarrow> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
302 |
topspace(prod_topology X Y) = {} \<and> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
303 |
topspace(prod_topology X' Y') = {} \<or> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
304 |
homeomorphic_maps X X' f f' \<and> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
305 |
homeomorphic_maps Y Y' g g'" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
306 |
unfolding homeomorphic_maps_def continuous_map_prod_top |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
307 |
by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
308 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
309 |
lemma embedding_map_graph: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
310 |
"embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
311 |
(is "?lhs = ?rhs") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
312 |
proof |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
313 |
assume L: ?lhs |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
314 |
have "snd \<circ> (\<lambda>x. (x, f x)) = f" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
315 |
by force |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
316 |
moreover have "continuous_map X Y (snd \<circ> (\<lambda>x. (x, f x)))" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
317 |
using L |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
318 |
unfolding embedding_map_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
319 |
by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
320 |
ultimately show ?rhs |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
321 |
by simp |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
322 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
323 |
assume R: ?rhs |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
324 |
then show ?lhs |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
325 |
unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
326 |
by (rule_tac x=fst in exI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
327 |
(auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
328 |
continuous_map_fst topspace_subtopology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
329 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
330 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
331 |
lemma in_prod_topology_closure_of: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
332 |
assumes "z \<in> (prod_topology X Y) closure_of S" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
333 |
shows "fst z \<in> X closure_of (fst ` S)" "snd z \<in> Y closure_of (snd ` S)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
334 |
using assms continuous_map_eq_image_closure_subset continuous_map_fst apply fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
335 |
using assms continuous_map_eq_image_closure_subset continuous_map_snd apply fastforce |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
336 |
done |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
337 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
338 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
339 |
proposition compact_space_prod_topology: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
340 |
"compact_space(prod_topology X Y) \<longleftrightarrow> topspace(prod_topology X Y) = {} \<or> compact_space X \<and> compact_space Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
341 |
proof (cases "topspace(prod_topology X Y) = {}") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
342 |
case True |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
343 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
344 |
using compact_space_topspace_empty by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
345 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
346 |
case False |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
347 |
then have non_mt: "topspace X \<noteq> {}" "topspace Y \<noteq> {}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
348 |
by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
349 |
have "compact_space X" "compact_space Y" if "compact_space(prod_topology X Y)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
350 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
351 |
have "compactin X (fst ` (topspace X \<times> topspace Y))" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
352 |
by (metis compact_space_def continuous_map_fst image_compactin that topspace_prod_topology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
353 |
moreover |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
354 |
have "compactin Y (snd ` (topspace X \<times> topspace Y))" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
355 |
by (metis compact_space_def continuous_map_snd image_compactin that topspace_prod_topology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
356 |
ultimately show "compact_space X" "compact_space Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
357 |
by (simp_all add: non_mt compact_space_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
358 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
359 |
moreover |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
360 |
define \<X> where "\<X> \<equiv> (\<lambda>V. topspace X \<times> V) ` Collect (openin Y)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
361 |
define \<Y> where "\<Y> \<equiv> (\<lambda>U. U \<times> topspace Y) ` Collect (openin X)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
362 |
have "compact_space(prod_topology X Y)" if "compact_space X" "compact_space Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
363 |
proof (rule Alexander_subbase_alt) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
364 |
show toptop: "topspace X \<times> topspace Y \<subseteq> \<Union>(\<X> \<union> \<Y>)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
365 |
unfolding \<X>_def \<Y>_def by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
366 |
fix \<C> :: "('a \<times> 'b) set set" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
367 |
assume \<C>: "\<C> \<subseteq> \<X> \<union> \<Y>" "topspace X \<times> topspace Y \<subseteq> \<Union>\<C>" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
368 |
then obtain \<X>' \<Y>' where XY: "\<X>' \<subseteq> \<X>" "\<Y>' \<subseteq> \<Y>" and \<C>eq: "\<C> = \<X>' \<union> \<Y>'" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
369 |
using subset_UnE by metis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
370 |
then have sub: "topspace X \<times> topspace Y \<subseteq> \<Union>(\<X>' \<union> \<Y>')" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
371 |
using \<C> by simp |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
372 |
obtain \<U> \<V> where \<U>: "\<And>U. U \<in> \<U> \<Longrightarrow> openin X U" "\<Y>' = (\<lambda>U. U \<times> topspace Y) ` \<U>" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
373 |
and \<V>: "\<And>V. V \<in> \<V> \<Longrightarrow> openin Y V" "\<X>' = (\<lambda>V. topspace X \<times> V) ` \<V>" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
374 |
using XY by (clarsimp simp add: \<X>_def \<Y>_def subset_image_iff) (force simp add: subset_iff) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
375 |
have "\<exists>\<D>. finite \<D> \<and> \<D> \<subseteq> \<X>' \<union> \<Y>' \<and> topspace X \<times> topspace Y \<subseteq> \<Union> \<D>" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
376 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
377 |
have "topspace X \<subseteq> \<Union>\<U> \<or> topspace Y \<subseteq> \<Union>\<V>" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
378 |
using \<U> \<V> \<C> \<C>eq by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
379 |
then have *: "\<exists>\<D>. finite \<D> \<and> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
380 |
(\<forall>x \<in> \<D>. x \<in> (\<lambda>V. topspace X \<times> V) ` \<V> \<or> x \<in> (\<lambda>U. U \<times> topspace Y) ` \<U>) \<and> |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
381 |
(topspace X \<times> topspace Y \<subseteq> \<Union>\<D>)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
382 |
proof |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
383 |
assume "topspace X \<subseteq> \<Union>\<U>" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
384 |
with \<open>compact_space X\<close> \<U> obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<U>" "topspace X \<subseteq> \<Union>\<F>" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
385 |
by (meson compact_space_alt) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
386 |
with that show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
387 |
by (rule_tac x="(\<lambda>D. D \<times> topspace Y) ` \<F>" in exI) auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
388 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
389 |
assume "topspace Y \<subseteq> \<Union>\<V>" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
390 |
with \<open>compact_space Y\<close> \<V> obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "topspace Y \<subseteq> \<Union>\<F>" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
391 |
by (meson compact_space_alt) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
392 |
with that show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
393 |
by (rule_tac x="(\<lambda>C. topspace X \<times> C) ` \<F>" in exI) auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
394 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
395 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
396 |
using that \<U> \<V> by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
397 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
398 |
then show "\<exists>\<D>. finite \<D> \<and> \<D> \<subseteq> \<C> \<and> topspace X \<times> topspace Y \<subseteq> \<Union> \<D>" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
399 |
using \<C> \<C>eq by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
400 |
next |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
401 |
have "(finite intersection_of (\<lambda>x. x \<in> \<X> \<or> x \<in> \<Y>) relative_to topspace X \<times> topspace Y) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
402 |
= (\<lambda>U. \<exists>S T. U = S \<times> T \<and> openin X S \<and> openin Y T)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
403 |
(is "?lhs = ?rhs") |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
404 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
405 |
have "?rhs U" if "?lhs U" for U |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
406 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
407 |
have "topspace X \<times> topspace Y \<inter> \<Inter> T \<in> {A \<times> B |A B. A \<in> Collect (openin X) \<and> B \<in> Collect (openin Y)}" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
408 |
if "finite T" "T \<subseteq> \<X> \<union> \<Y>" for T |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
409 |
using that |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
410 |
proof induction |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
411 |
case (insert B \<B>) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
412 |
then show ?case |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
413 |
unfolding \<X>_def \<Y>_def |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
414 |
apply (simp add: Int_ac subset_eq image_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
415 |
apply (metis (no_types) openin_Int openin_topspace times_Int_times) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
416 |
done |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
417 |
qed auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
418 |
then show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
419 |
using that |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
420 |
by (auto simp: subset_eq elim!: relative_toE intersection_ofE) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
421 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
422 |
moreover |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
423 |
have "?lhs Z" if Z: "?rhs Z" for Z |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
424 |
proof - |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
425 |
obtain U V where "Z = U \<times> V" "openin X U" "openin Y V" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
426 |
using Z by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
427 |
then have UV: "U \<times> V = (topspace X \<times> topspace Y) \<inter> (U \<times> V)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
428 |
by (simp add: Sigma_mono inf_absorb2 openin_subset) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
429 |
moreover |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
430 |
have "?lhs ((topspace X \<times> topspace Y) \<inter> (U \<times> V))" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
431 |
proof (rule relative_to_inc) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
432 |
show "(finite intersection_of (\<lambda>x. x \<in> \<X> \<or> x \<in> \<Y>)) (U \<times> V)" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
433 |
apply (simp add: intersection_of_def \<X>_def \<Y>_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
434 |
apply (rule_tac x="{(U \<times> topspace Y),(topspace X \<times> V)}" in exI) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
435 |
using \<open>openin X U\<close> \<open>openin Y V\<close> openin_subset UV apply (fastforce simp add:) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
436 |
done |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
437 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
438 |
ultimately show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
439 |
using \<open>Z = U \<times> V\<close> by auto |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
440 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
441 |
ultimately show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
442 |
by meson |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
443 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
444 |
then show "topology (arbitrary union_of (finite intersection_of (\<lambda>x. x \<in> \<X> \<union> \<Y>) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
445 |
relative_to (topspace X \<times> topspace Y))) = |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
446 |
prod_topology X Y" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
447 |
by (simp add: prod_topology_def) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
448 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
449 |
ultimately show ?thesis |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
450 |
using False by blast |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
451 |
qed |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
452 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
453 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
454 |
lemma compactin_Times: |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
455 |
"compactin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> compactin X S \<and> compactin Y T" |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
456 |
by (auto simp: compactin_subspace subtopology_Times compact_space_prod_topology) |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
457 |
|
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
458 |
end |
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
459 |