author | paulson <lp15@cam.ac.uk> |
Thu, 05 Jan 2017 16:37:49 +0000 | |
changeset 64791 | 05a2b3b20664 |
parent 64789 | 6440577e34ee |
child 64792 | 3074080f4f12 |
permissions | -rw-r--r-- |
63627 | 1 |
(* Title: HOL/Analysis/Homeomorphism.thy |
63130 | 2 |
Author: LC Paulson (ported from HOL Light) |
3 |
*) |
|
4 |
||
5 |
section \<open>Homeomorphism Theorems\<close> |
|
6 |
||
7 |
theory Homeomorphism |
|
8 |
imports Path_Connected |
|
9 |
begin |
|
10 |
||
64789
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
11 |
lemma homeomorphic_spheres': |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
12 |
fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space" |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
13 |
assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)" |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
14 |
shows "(sphere a \<delta>) homeomorphic (sphere b \<delta>)" |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
15 |
proof - |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
16 |
obtain f :: "'a\<Rightarrow>'b" and g where "linear f" "linear g" |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
17 |
and fg: "\<And>x. norm(f x) = norm x" "\<And>y. norm(g y) = norm y" "\<And>x. g(f x) = x" "\<And>y. f(g y) = y" |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
18 |
by (blast intro: isomorphisms_UNIV_UNIV [OF dimeq]) |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
19 |
then have "continuous_on UNIV f" "continuous_on UNIV g" |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
20 |
using linear_continuous_on linear_linear by blast+ |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
21 |
then show ?thesis |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
22 |
unfolding homeomorphic_minimal |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
23 |
apply(rule_tac x="\<lambda>x. b + f(x - a)" in exI) |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
24 |
apply(rule_tac x="\<lambda>x. a + g(x - b)" in exI) |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
25 |
using assms |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
26 |
apply (force intro: continuous_intros |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
27 |
continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg) |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
28 |
done |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
29 |
qed |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
30 |
|
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
31 |
lemma homeomorphic_spheres_gen: |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
32 |
fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space" |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
33 |
assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)" |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
34 |
shows "(sphere a r homeomorphic sphere b s)" |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
35 |
apply (rule homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres']) |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
36 |
using assms apply auto |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
37 |
done |
6440577e34ee
connectedness, circles not simply connected , punctured universe
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset
|
38 |
|
63130 | 39 |
subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close> |
40 |
||
41 |
proposition ray_to_rel_frontier: |
|
42 |
fixes a :: "'a::real_inner" |
|
43 |
assumes "bounded S" |
|
44 |
and a: "a \<in> rel_interior S" |
|
45 |
and aff: "(a + l) \<in> affine hull S" |
|
46 |
and "l \<noteq> 0" |
|
47 |
obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S" |
|
48 |
"\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S" |
|
49 |
proof - |
|
50 |
have aaff: "a \<in> affine hull S" |
|
51 |
by (meson a hull_subset rel_interior_subset rev_subsetD) |
|
52 |
let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}" |
|
53 |
obtain B where "B > 0" and B: "S \<subseteq> ball a B" |
|
54 |
using bounded_subset_ballD [OF \<open>bounded S\<close>] by blast |
|
55 |
have "a + (B / norm l) *\<^sub>R l \<notin> ball a B" |
|
56 |
by (simp add: dist_norm \<open>l \<noteq> 0\<close>) |
|
57 |
with B have "a + (B / norm l) *\<^sub>R l \<notin> rel_interior S" |
|
58 |
using rel_interior_subset subsetCE by blast |
|
59 |
with \<open>B > 0\<close> \<open>l \<noteq> 0\<close> have nonMT: "?D \<noteq> {}" |
|
60 |
using divide_pos_pos zero_less_norm_iff by fastforce |
|
61 |
have bdd: "bdd_below ?D" |
|
62 |
by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq) |
|
63 |
have relin_Ex: "\<And>x. x \<in> rel_interior S \<Longrightarrow> |
|
64 |
\<exists>e>0. \<forall>x'\<in>affine hull S. dist x' x < e \<longrightarrow> x' \<in> rel_interior S" |
|
65 |
using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff) |
|
66 |
define d where "d = Inf ?D" |
|
67 |
obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "\<And>\<eta>. \<lbrakk>0 \<le> \<eta>; \<eta> < \<epsilon>\<rbrakk> \<Longrightarrow> (a + \<eta> *\<^sub>R l) \<in> rel_interior S" |
|
68 |
proof - |
|
69 |
obtain e where "e>0" |
|
70 |
and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' a < e \<Longrightarrow> x' \<in> rel_interior S" |
|
71 |
using relin_Ex a by blast |
|
72 |
show thesis |
|
73 |
proof (rule_tac \<epsilon> = "e / norm l" in that) |
|
74 |
show "0 < e / norm l" by (simp add: \<open>0 < e\<close> \<open>l \<noteq> 0\<close>) |
|
75 |
next |
|
76 |
show "a + \<eta> *\<^sub>R l \<in> rel_interior S" if "0 \<le> \<eta>" "\<eta> < e / norm l" for \<eta> |
|
77 |
proof (rule e) |
|
78 |
show "a + \<eta> *\<^sub>R l \<in> affine hull S" |
|
79 |
by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff) |
|
80 |
show "dist (a + \<eta> *\<^sub>R l) a < e" |
|
81 |
using that by (simp add: \<open>l \<noteq> 0\<close> dist_norm pos_less_divide_eq) |
|
82 |
qed |
|
83 |
qed |
|
84 |
qed |
|
85 |
have inint: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> a + e *\<^sub>R l \<in> rel_interior S" |
|
86 |
unfolding d_def using cInf_lower [OF _ bdd] |
|
87 |
by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left) |
|
88 |
have "\<epsilon> \<le> d" |
|
89 |
unfolding d_def |
|
90 |
apply (rule cInf_greatest [OF nonMT]) |
|
91 |
using \<epsilon> dual_order.strict_implies_order le_less_linear by blast |
|
92 |
with \<open>0 < \<epsilon>\<close> have "0 < d" by simp |
|
93 |
have "a + d *\<^sub>R l \<notin> rel_interior S" |
|
94 |
proof |
|
95 |
assume adl: "a + d *\<^sub>R l \<in> rel_interior S" |
|
96 |
obtain e where "e > 0" |
|
97 |
and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' (a + d *\<^sub>R l) < e \<Longrightarrow> x' \<in> rel_interior S" |
|
98 |
using relin_Ex adl by blast |
|
99 |
have "d + e / norm l \<le> Inf {d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}" |
|
100 |
proof (rule cInf_greatest [OF nonMT], clarsimp) |
|
101 |
fix x::real |
|
102 |
assume "0 < x" and nonrel: "a + x *\<^sub>R l \<notin> rel_interior S" |
|
103 |
show "d + e / norm l \<le> x" |
|
104 |
proof (cases "x < d") |
|
105 |
case True with inint nonrel \<open>0 < x\<close> |
|
106 |
show ?thesis by auto |
|
107 |
next |
|
108 |
case False |
|
109 |
then have dle: "x < d + e / norm l \<Longrightarrow> dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e" |
|
110 |
by (simp add: field_simps \<open>l \<noteq> 0\<close>) |
|
111 |
have ain: "a + x *\<^sub>R l \<in> affine hull S" |
|
112 |
by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff) |
|
113 |
show ?thesis |
|
114 |
using e [OF ain] nonrel dle by force |
|
115 |
qed |
|
116 |
qed |
|
117 |
then show False |
|
118 |
using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] divide_simps) |
|
119 |
qed |
|
120 |
moreover have "a + d *\<^sub>R l \<in> closure S" |
|
121 |
proof (clarsimp simp: closure_approachable) |
|
122 |
fix \<eta>::real assume "0 < \<eta>" |
|
123 |
have 1: "a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l \<in> S" |
|
124 |
apply (rule subsetD [OF rel_interior_subset inint]) |
|
125 |
using \<open>l \<noteq> 0\<close> \<open>0 < d\<close> \<open>0 < \<eta>\<close> by auto |
|
126 |
have "norm l * min d (\<eta> / (norm l * 2)) \<le> norm l * (\<eta> / (norm l * 2))" |
|
127 |
by (metis min_def mult_left_mono norm_ge_zero order_refl) |
|
128 |
also have "... < \<eta>" |
|
129 |
using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: divide_simps) |
|
130 |
finally have 2: "norm l * min d (\<eta> / (norm l * 2)) < \<eta>" . |
|
131 |
show "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>" |
|
132 |
apply (rule_tac x="a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l" in bexI) |
|
133 |
using 1 2 \<open>0 < d\<close> \<open>0 < \<eta>\<close> apply (auto simp: algebra_simps) |
|
134 |
done |
|
135 |
qed |
|
136 |
ultimately have infront: "a + d *\<^sub>R l \<in> rel_frontier S" |
|
137 |
by (simp add: rel_frontier_def) |
|
138 |
show ?thesis |
|
139 |
by (rule that [OF \<open>0 < d\<close> infront inint]) |
|
140 |
qed |
|
141 |
||
142 |
corollary ray_to_frontier: |
|
143 |
fixes a :: "'a::euclidean_space" |
|
144 |
assumes "bounded S" |
|
145 |
and a: "a \<in> interior S" |
|
146 |
and "l \<noteq> 0" |
|
147 |
obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S" |
|
148 |
"\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S" |
|
149 |
proof - |
|
150 |
have "interior S = rel_interior S" |
|
151 |
using a rel_interior_nonempty_interior by auto |
|
152 |
then have "a \<in> rel_interior S" |
|
153 |
using a by simp |
|
154 |
then show ?thesis |
|
155 |
apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> _ _ \<open>l \<noteq> 0\<close>]) |
|
156 |
using a affine_hull_nonempty_interior apply blast |
|
157 |
by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that) |
|
158 |
qed |
|
159 |
||
64394 | 160 |
proposition rel_frontier_not_sing: |
161 |
fixes a :: "'a::euclidean_space" |
|
162 |
assumes "bounded S" |
|
163 |
shows "rel_frontier S \<noteq> {a}" |
|
164 |
proof (cases "S = {}") |
|
165 |
case True then show ?thesis by simp |
|
166 |
next |
|
167 |
case False |
|
168 |
then obtain z where "z \<in> S" |
|
169 |
by blast |
|
170 |
then show ?thesis |
|
171 |
proof (cases "S = {z}") |
|
172 |
case True then show ?thesis by simp |
|
173 |
next |
|
174 |
case False |
|
175 |
then obtain w where "w \<in> S" "w \<noteq> z" |
|
176 |
using \<open>z \<in> S\<close> by blast |
|
177 |
show ?thesis |
|
178 |
proof |
|
179 |
assume "rel_frontier S = {a}" |
|
180 |
then consider "w \<notin> rel_frontier S" | "z \<notin> rel_frontier S" |
|
181 |
using \<open>w \<noteq> z\<close> by auto |
|
182 |
then show False |
|
183 |
proof cases |
|
184 |
case 1 |
|
185 |
then have w: "w \<in> rel_interior S" |
|
186 |
using \<open>w \<in> S\<close> closure_subset rel_frontier_def by fastforce |
|
187 |
have "w + (w - z) \<in> affine hull S" |
|
188 |
by (metis \<open>w \<in> S\<close> \<open>z \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one) |
|
189 |
then obtain e where "0 < e" "(w + e *\<^sub>R (w - z)) \<in> rel_frontier S" |
|
190 |
using \<open>w \<noteq> z\<close> \<open>z \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq w) |
|
191 |
moreover obtain d where "0 < d" "(w + d *\<^sub>R (z - w)) \<in> rel_frontier S" |
|
192 |
using ray_to_rel_frontier [OF \<open>bounded S\<close> w, of "1 *\<^sub>R (z - w)"] \<open>w \<noteq> z\<close> \<open>z \<in> S\<close> |
|
193 |
by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one) |
|
194 |
ultimately have "d *\<^sub>R (z - w) = e *\<^sub>R (w - z)" |
|
195 |
using \<open>rel_frontier S = {a}\<close> by force |
|
196 |
moreover have "e \<noteq> -d " |
|
197 |
using \<open>0 < e\<close> \<open>0 < d\<close> by force |
|
198 |
ultimately show False |
|
199 |
by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus) |
|
200 |
next |
|
201 |
case 2 |
|
202 |
then have z: "z \<in> rel_interior S" |
|
203 |
using \<open>z \<in> S\<close> closure_subset rel_frontier_def by fastforce |
|
204 |
have "z + (z - w) \<in> affine hull S" |
|
205 |
by (metis \<open>z \<in> S\<close> \<open>w \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one) |
|
206 |
then obtain e where "0 < e" "(z + e *\<^sub>R (z - w)) \<in> rel_frontier S" |
|
207 |
using \<open>w \<noteq> z\<close> \<open>w \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq z) |
|
208 |
moreover obtain d where "0 < d" "(z + d *\<^sub>R (w - z)) \<in> rel_frontier S" |
|
209 |
using ray_to_rel_frontier [OF \<open>bounded S\<close> z, of "1 *\<^sub>R (w - z)"] \<open>w \<noteq> z\<close> \<open>w \<in> S\<close> |
|
210 |
by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one) |
|
211 |
ultimately have "d *\<^sub>R (w - z) = e *\<^sub>R (z - w)" |
|
212 |
using \<open>rel_frontier S = {a}\<close> by force |
|
213 |
moreover have "e \<noteq> -d " |
|
214 |
using \<open>0 < e\<close> \<open>0 < d\<close> by force |
|
215 |
ultimately show False |
|
216 |
by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus) |
|
217 |
qed |
|
218 |
qed |
|
219 |
qed |
|
220 |
qed |
|
221 |
||
63130 | 222 |
proposition |
223 |
fixes S :: "'a::euclidean_space set" |
|
224 |
assumes "compact S" and 0: "0 \<in> rel_interior S" |
|
225 |
and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment 0 x \<subseteq> rel_interior S" |
|
226 |
shows starlike_compact_projective1_0: |
|
227 |
"S - rel_interior S homeomorphic sphere 0 1 \<inter> affine hull S" |
|
228 |
(is "?SMINUS homeomorphic ?SPHER") |
|
229 |
and starlike_compact_projective2_0: |
|
230 |
"S homeomorphic cball 0 1 \<inter> affine hull S" |
|
231 |
(is "S homeomorphic ?CBALL") |
|
232 |
proof - |
|
233 |
have starI: "(u *\<^sub>R x) \<in> rel_interior S" if "x \<in> S" "0 \<le> u" "u < 1" for x u |
|
234 |
proof (cases "x=0 \<or> u=0") |
|
235 |
case True with 0 show ?thesis by force |
|
236 |
next |
|
237 |
case False with that show ?thesis |
|
238 |
by (auto simp: in_segment intro: star [THEN subsetD]) |
|
239 |
qed |
|
240 |
have "0 \<in> S" using assms rel_interior_subset by auto |
|
241 |
define proj where "proj \<equiv> \<lambda>x::'a. x /\<^sub>R norm x" |
|
242 |
have eqI: "x = y" if "proj x = proj y" "norm x = norm y" for x y |
|
243 |
using that by (force simp: proj_def) |
|
244 |
then have iff_eq: "\<And>x y. (proj x = proj y \<and> norm x = norm y) \<longleftrightarrow> x = y" |
|
245 |
by blast |
|
246 |
have projI: "x \<in> affine hull S \<Longrightarrow> proj x \<in> affine hull S" for x |
|
247 |
by (metis \<open>0 \<in> S\<close> affine_hull_span_0 hull_inc span_mul proj_def) |
|
248 |
have nproj1 [simp]: "x \<noteq> 0 \<Longrightarrow> norm(proj x) = 1" for x |
|
249 |
by (simp add: proj_def) |
|
250 |
have proj0_iff [simp]: "proj x = 0 \<longleftrightarrow> x = 0" for x |
|
251 |
by (simp add: proj_def) |
|
252 |
have cont_proj: "continuous_on (UNIV - {0}) proj" |
|
253 |
unfolding proj_def by (rule continuous_intros | force)+ |
|
254 |
have proj_spherI: "\<And>x. \<lbrakk>x \<in> affine hull S; x \<noteq> 0\<rbrakk> \<Longrightarrow> proj x \<in> ?SPHER" |
|
255 |
by (simp add: projI) |
|
256 |
have "bounded S" "closed S" |
|
257 |
using \<open>compact S\<close> compact_eq_bounded_closed by blast+ |
|
258 |
have inj_on_proj: "inj_on proj (S - rel_interior S)" |
|
259 |
proof |
|
260 |
fix x y |
|
261 |
assume x: "x \<in> S - rel_interior S" |
|
262 |
and y: "y \<in> S - rel_interior S" and eq: "proj x = proj y" |
|
263 |
then have xynot: "x \<noteq> 0" "y \<noteq> 0" "x \<in> S" "y \<in> S" "x \<notin> rel_interior S" "y \<notin> rel_interior S" |
|
264 |
using 0 by auto |
|
265 |
consider "norm x = norm y" | "norm x < norm y" | "norm x > norm y" by linarith |
|
266 |
then show "x = y" |
|
267 |
proof cases |
|
268 |
assume "norm x = norm y" |
|
269 |
with iff_eq eq show "x = y" by blast |
|
270 |
next |
|
271 |
assume *: "norm x < norm y" |
|
272 |
have "x /\<^sub>R norm x = norm x *\<^sub>R (x /\<^sub>R norm x) /\<^sub>R norm (norm x *\<^sub>R (x /\<^sub>R norm x))" |
|
273 |
by force |
|
274 |
then have "proj ((norm x / norm y) *\<^sub>R y) = proj x" |
|
275 |
by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR) |
|
276 |
then have [simp]: "(norm x / norm y) *\<^sub>R y = x" |
|
277 |
by (rule eqI) (simp add: \<open>y \<noteq> 0\<close>) |
|
278 |
have no: "0 \<le> norm x / norm y" "norm x / norm y < 1" |
|
279 |
using * by (auto simp: divide_simps) |
|
280 |
then show "x = y" |
|
281 |
using starI [OF \<open>y \<in> S\<close> no] xynot by auto |
|
282 |
next |
|
283 |
assume *: "norm x > norm y" |
|
284 |
have "y /\<^sub>R norm y = norm y *\<^sub>R (y /\<^sub>R norm y) /\<^sub>R norm (norm y *\<^sub>R (y /\<^sub>R norm y))" |
|
285 |
by force |
|
286 |
then have "proj ((norm y / norm x) *\<^sub>R x) = proj y" |
|
287 |
by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR) |
|
288 |
then have [simp]: "(norm y / norm x) *\<^sub>R x = y" |
|
289 |
by (rule eqI) (simp add: \<open>x \<noteq> 0\<close>) |
|
290 |
have no: "0 \<le> norm y / norm x" "norm y / norm x < 1" |
|
291 |
using * by (auto simp: divide_simps) |
|
292 |
then show "x = y" |
|
293 |
using starI [OF \<open>x \<in> S\<close> no] xynot by auto |
|
294 |
qed |
|
295 |
qed |
|
296 |
have "\<exists>surf. homeomorphism (S - rel_interior S) ?SPHER proj surf" |
|
297 |
proof (rule homeomorphism_compact) |
|
298 |
show "compact (S - rel_interior S)" |
|
299 |
using \<open>compact S\<close> compact_rel_boundary by blast |
|
300 |
show "continuous_on (S - rel_interior S) proj" |
|
301 |
using 0 by (blast intro: continuous_on_subset [OF cont_proj]) |
|
302 |
show "proj ` (S - rel_interior S) = ?SPHER" |
|
303 |
proof |
|
304 |
show "proj ` (S - rel_interior S) \<subseteq> ?SPHER" |
|
305 |
using 0 by (force simp: hull_inc projI intro: nproj1) |
|
306 |
show "?SPHER \<subseteq> proj ` (S - rel_interior S)" |
|
307 |
proof (clarsimp simp: proj_def) |
|
308 |
fix x |
|
309 |
assume "x \<in> affine hull S" and nox: "norm x = 1" |
|
310 |
then have "x \<noteq> 0" by auto |
|
311 |
obtain d where "0 < d" and dx: "(d *\<^sub>R x) \<in> rel_frontier S" |
|
312 |
and ri: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (e *\<^sub>R x) \<in> rel_interior S" |
|
313 |
using ray_to_rel_frontier [OF \<open>bounded S\<close> 0] \<open>x \<in> affine hull S\<close> \<open>x \<noteq> 0\<close> by auto |
|
314 |
show "x \<in> (\<lambda>x. x /\<^sub>R norm x) ` (S - rel_interior S)" |
|
315 |
apply (rule_tac x="d *\<^sub>R x" in image_eqI) |
|
316 |
using \<open>0 < d\<close> |
|
317 |
using dx \<open>closed S\<close> apply (auto simp: rel_frontier_def divide_simps nox) |
|
318 |
done |
|
319 |
qed |
|
320 |
qed |
|
321 |
qed (rule inj_on_proj) |
|
322 |
then obtain surf where surf: "homeomorphism (S - rel_interior S) ?SPHER proj surf" |
|
323 |
by blast |
|
324 |
then have cont_surf: "continuous_on (proj ` (S - rel_interior S)) surf" |
|
325 |
by (auto simp: homeomorphism_def) |
|
326 |
have surf_nz: "\<And>x. x \<in> ?SPHER \<Longrightarrow> surf x \<noteq> 0" |
|
327 |
by (metis "0" DiffE homeomorphism_def imageI surf) |
|
328 |
have cont_nosp: "continuous_on (?SPHER) (\<lambda>x. norm x *\<^sub>R ((surf o proj) x))" |
|
329 |
apply (rule continuous_intros)+ |
|
330 |
apply (rule continuous_on_subset [OF cont_proj], force) |
|
331 |
apply (rule continuous_on_subset [OF cont_surf]) |
|
332 |
apply (force simp: homeomorphism_image1 [OF surf] dest: proj_spherI) |
|
333 |
done |
|
334 |
have surfpS: "\<And>x. \<lbrakk>norm x = 1; x \<in> affine hull S\<rbrakk> \<Longrightarrow> surf (proj x) \<in> S" |
|
335 |
by (metis (full_types) DiffE \<open>0 \<in> S\<close> homeomorphism_def image_eqI norm_zero proj_spherI real_vector.scale_zero_left scaleR_one surf) |
|
336 |
have *: "\<exists>y. norm y = 1 \<and> y \<in> affine hull S \<and> x = surf (proj y)" |
|
337 |
if "x \<in> S" "x \<notin> rel_interior S" for x |
|
338 |
proof - |
|
339 |
have "proj x \<in> ?SPHER" |
|
340 |
by (metis (full_types) "0" hull_inc proj_spherI that) |
|
341 |
moreover have "surf (proj x) = x" |
|
342 |
by (metis Diff_iff homeomorphism_def surf that) |
|
343 |
ultimately show ?thesis |
|
344 |
by (metis \<open>\<And>x. x \<in> ?SPHER \<Longrightarrow> surf x \<noteq> 0\<close> hull_inc inverse_1 local.proj_def norm_sgn projI scaleR_one sgn_div_norm that(1)) |
|
345 |
qed |
|
346 |
have surfp_notin: "\<And>x. \<lbrakk>norm x = 1; x \<in> affine hull S\<rbrakk> \<Longrightarrow> surf (proj x) \<notin> rel_interior S" |
|
347 |
by (metis (full_types) DiffE one_neq_zero homeomorphism_def image_eqI norm_zero proj_spherI surf) |
|
348 |
have no_sp_im: "(\<lambda>x. norm x *\<^sub>R surf (proj x)) ` (?SPHER) = S - rel_interior S" |
|
349 |
by (auto simp: surfpS image_def Bex_def surfp_notin *) |
|
350 |
have inj_spher: "inj_on (\<lambda>x. norm x *\<^sub>R surf (proj x)) ?SPHER" |
|
351 |
proof |
|
352 |
fix x y |
|
353 |
assume xy: "x \<in> ?SPHER" "y \<in> ?SPHER" |
|
354 |
and eq: " norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)" |
|
355 |
then have "norm x = 1" "norm y = 1" "x \<in> affine hull S" "y \<in> affine hull S" |
|
356 |
using 0 by auto |
|
357 |
with eq show "x = y" |
|
358 |
by (simp add: proj_def) (metis surf xy homeomorphism_def) |
|
359 |
qed |
|
360 |
have co01: "compact ?SPHER" |
|
361 |
by (simp add: closed_affine_hull compact_Int_closed) |
|
362 |
show "?SMINUS homeomorphic ?SPHER" |
|
363 |
apply (subst homeomorphic_sym) |
|
364 |
apply (rule homeomorphic_compact [OF co01 cont_nosp [unfolded o_def] no_sp_im inj_spher]) |
|
365 |
done |
|
366 |
have proj_scaleR: "\<And>a x. 0 < a \<Longrightarrow> proj (a *\<^sub>R x) = proj x" |
|
367 |
by (simp add: proj_def) |
|
368 |
have cont_sp0: "continuous_on (affine hull S - {0}) (surf o proj)" |
|
369 |
apply (rule continuous_on_compose [OF continuous_on_subset [OF cont_proj]], force) |
|
370 |
apply (rule continuous_on_subset [OF cont_surf]) |
|
371 |
using homeomorphism_image1 proj_spherI surf by fastforce |
|
372 |
obtain B where "B>0" and B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B" |
|
373 |
by (metis compact_imp_bounded \<open>compact S\<close> bounded_pos_less less_eq_real_def) |
|
374 |
have cont_nosp: "continuous (at x within ?CBALL) (\<lambda>x. norm x *\<^sub>R surf (proj x))" |
|
375 |
if "norm x \<le> 1" "x \<in> affine hull S" for x |
|
376 |
proof (cases "x=0") |
|
377 |
case True |
|
378 |
show ?thesis using True |
|
379 |
apply (simp add: continuous_within) |
|
380 |
apply (rule lim_null_scaleR_bounded [where B=B]) |
|
381 |
apply (simp_all add: tendsto_norm_zero eventually_at) |
|
382 |
apply (rule_tac x=B in exI) |
|
383 |
using B surfpS proj_def projI apply (auto simp: \<open>B > 0\<close>) |
|
384 |
done |
|
385 |
next |
|
386 |
case False |
|
387 |
then have "\<forall>\<^sub>F x in at x. (x \<in> affine hull S - {0}) = (x \<in> affine hull S)" |
|
388 |
apply (simp add: eventually_at) |
|
389 |
apply (rule_tac x="norm x" in exI) |
|
390 |
apply (auto simp: False) |
|
391 |
done |
|
392 |
with cont_sp0 have *: "continuous (at x within affine hull S) (\<lambda>x. surf (proj x))" |
|
393 |
apply (simp add: continuous_on_eq_continuous_within) |
|
394 |
apply (drule_tac x=x in bspec, force simp: False that) |
|
395 |
apply (simp add: continuous_within Lim_transform_within_set) |
|
396 |
done |
|
397 |
show ?thesis |
|
398 |
apply (rule continuous_within_subset [where s = "affine hull S", OF _ Int_lower2]) |
|
399 |
apply (rule continuous_intros *)+ |
|
400 |
done |
|
401 |
qed |
|
402 |
have cont_nosp2: "continuous_on ?CBALL (\<lambda>x. norm x *\<^sub>R ((surf o proj) x))" |
|
403 |
by (simp add: continuous_on_eq_continuous_within cont_nosp) |
|
404 |
have "norm y *\<^sub>R surf (proj y) \<in> S" if "y \<in> cball 0 1" and yaff: "y \<in> affine hull S" for y |
|
405 |
proof (cases "y=0") |
|
406 |
case True then show ?thesis |
|
407 |
by (simp add: \<open>0 \<in> S\<close>) |
|
408 |
next |
|
409 |
case False |
|
410 |
then have "norm y *\<^sub>R surf (proj y) = norm y *\<^sub>R surf (proj (y /\<^sub>R norm y))" |
|
411 |
by (simp add: proj_def) |
|
412 |
have "norm y \<le> 1" using that by simp |
|
413 |
have "surf (proj (y /\<^sub>R norm y)) \<in> S" |
|
414 |
apply (rule surfpS) |
|
415 |
using proj_def projI yaff |
|
416 |
by (auto simp: False) |
|
417 |
then have "surf (proj y) \<in> S" |
|
418 |
by (simp add: False proj_def) |
|
419 |
then show "norm y *\<^sub>R surf (proj y) \<in> S" |
|
420 |
by (metis dual_order.antisym le_less_linear norm_ge_zero rel_interior_subset scaleR_one |
|
421 |
starI subset_eq \<open>norm y \<le> 1\<close>) |
|
422 |
qed |
|
423 |
moreover have "x \<in> (\<lambda>x. norm x *\<^sub>R surf (proj x)) ` (?CBALL)" if "x \<in> S" for x |
|
424 |
proof (cases "x=0") |
|
425 |
case True with that hull_inc show ?thesis by fastforce |
|
426 |
next |
|
427 |
case False |
|
428 |
then have psp: "proj (surf (proj x)) = proj x" |
|
429 |
by (metis homeomorphism_def hull_inc proj_spherI surf that) |
|
430 |
have nxx: "norm x *\<^sub>R proj x = x" |
|
431 |
by (simp add: False local.proj_def) |
|
432 |
have affineI: "(1 / norm (surf (proj x))) *\<^sub>R x \<in> affine hull S" |
|
433 |
by (metis \<open>0 \<in> S\<close> affine_hull_span_0 hull_inc span_clauses(4) that) |
|
434 |
have sproj_nz: "surf (proj x) \<noteq> 0" |
|
435 |
by (metis False proj0_iff psp) |
|
436 |
then have "proj x = proj (proj x)" |
|
437 |
by (metis False nxx proj_scaleR zero_less_norm_iff) |
|
438 |
moreover have scaleproj: "\<And>a r. r *\<^sub>R proj a = (r / norm a) *\<^sub>R a" |
|
439 |
by (simp add: divide_inverse local.proj_def) |
|
440 |
ultimately have "(norm (surf (proj x)) / norm x) *\<^sub>R x \<notin> rel_interior S" |
|
441 |
by (metis (no_types) sproj_nz divide_self_if hull_inc norm_eq_zero nproj1 projI psp scaleR_one surfp_notin that) |
|
442 |
then have "(norm (surf (proj x)) / norm x) \<ge> 1" |
|
443 |
using starI [OF that] by (meson starI [OF that] le_less_linear norm_ge_zero zero_le_divide_iff) |
|
444 |
then have nole: "norm x \<le> norm (surf (proj x))" |
|
445 |
by (simp add: le_divide_eq_1) |
|
446 |
show ?thesis |
|
447 |
apply (rule_tac x="inverse(norm(surf (proj x))) *\<^sub>R x" in image_eqI) |
|
448 |
apply (metis (no_types, hide_lams) mult.commute scaleproj abs_inverse abs_norm_cancel divide_inverse norm_scaleR nxx positive_imp_inverse_positive proj_scaleR psp sproj_nz zero_less_norm_iff) |
|
449 |
apply (auto simp: divide_simps nole affineI) |
|
450 |
done |
|
451 |
qed |
|
452 |
ultimately have im_cball: "(\<lambda>x. norm x *\<^sub>R surf (proj x)) ` ?CBALL = S" |
|
453 |
by blast |
|
454 |
have inj_cball: "inj_on (\<lambda>x. norm x *\<^sub>R surf (proj x)) ?CBALL" |
|
455 |
proof |
|
456 |
fix x y |
|
457 |
assume "x \<in> ?CBALL" "y \<in> ?CBALL" |
|
458 |
and eq: "norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)" |
|
459 |
then have x: "x \<in> affine hull S" and y: "y \<in> affine hull S" |
|
460 |
using 0 by auto |
|
461 |
show "x = y" |
|
462 |
proof (cases "x=0 \<or> y=0") |
|
463 |
case True then show "x = y" using eq proj_spherI surf_nz x y by force |
|
464 |
next |
|
465 |
case False |
|
466 |
with x y have speq: "surf (proj x) = surf (proj y)" |
|
467 |
by (metis eq homeomorphism_apply2 proj_scaleR proj_spherI surf zero_less_norm_iff) |
|
468 |
then have "norm x = norm y" |
|
469 |
by (metis \<open>x \<in> affine hull S\<close> \<open>y \<in> affine hull S\<close> eq proj_spherI real_vector.scale_cancel_right surf_nz) |
|
470 |
moreover have "proj x = proj y" |
|
471 |
by (metis (no_types) False speq homeomorphism_apply2 proj_spherI surf x y) |
|
472 |
ultimately show "x = y" |
|
473 |
using eq eqI by blast |
|
474 |
qed |
|
475 |
qed |
|
476 |
have co01: "compact ?CBALL" |
|
477 |
by (simp add: closed_affine_hull compact_Int_closed) |
|
478 |
show "S homeomorphic ?CBALL" |
|
479 |
apply (subst homeomorphic_sym) |
|
480 |
apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball]) |
|
481 |
done |
|
482 |
qed |
|
483 |
||
484 |
corollary |
|
485 |
fixes S :: "'a::euclidean_space set" |
|
486 |
assumes "compact S" and a: "a \<in> rel_interior S" |
|
487 |
and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S" |
|
488 |
shows starlike_compact_projective1: |
|
489 |
"S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S" |
|
490 |
and starlike_compact_projective2: |
|
491 |
"S homeomorphic cball a 1 \<inter> affine hull S" |
|
492 |
proof - |
|
493 |
have 1: "compact (op+ (-a) ` S)" by (meson assms compact_translation) |
|
494 |
have 2: "0 \<in> rel_interior (op+ (-a) ` S)" |
|
495 |
by (simp add: a rel_interior_translation) |
|
496 |
have 3: "open_segment 0 x \<subseteq> rel_interior (op+ (-a) ` S)" if "x \<in> (op+ (-a) ` S)" for x |
|
497 |
proof - |
|
498 |
have "x+a \<in> S" using that by auto |
|
499 |
then have "open_segment a (x+a) \<subseteq> rel_interior S" by (metis star) |
|
500 |
then show ?thesis using open_segment_translation |
|
501 |
using rel_interior_translation by fastforce |
|
502 |
qed |
|
503 |
have "S - rel_interior S homeomorphic (op+ (-a) ` S) - rel_interior (op+ (-a) ` S)" |
|
504 |
by (metis rel_interior_translation translation_diff homeomorphic_translation) |
|
505 |
also have "... homeomorphic sphere 0 1 \<inter> affine hull (op+ (-a) ` S)" |
|
506 |
by (rule starlike_compact_projective1_0 [OF 1 2 3]) |
|
507 |
also have "... = op+ (-a) ` (sphere a 1 \<inter> affine hull S)" |
|
508 |
by (metis affine_hull_translation left_minus sphere_translation translation_Int) |
|
509 |
also have "... homeomorphic sphere a 1 \<inter> affine hull S" |
|
510 |
using homeomorphic_translation homeomorphic_sym by blast |
|
511 |
finally show "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S" . |
|
512 |
||
513 |
have "S homeomorphic (op+ (-a) ` S)" |
|
514 |
by (metis homeomorphic_translation) |
|
515 |
also have "... homeomorphic cball 0 1 \<inter> affine hull (op+ (-a) ` S)" |
|
516 |
by (rule starlike_compact_projective2_0 [OF 1 2 3]) |
|
517 |
also have "... = op+ (-a) ` (cball a 1 \<inter> affine hull S)" |
|
518 |
by (metis affine_hull_translation left_minus cball_translation translation_Int) |
|
519 |
also have "... homeomorphic cball a 1 \<inter> affine hull S" |
|
520 |
using homeomorphic_translation homeomorphic_sym by blast |
|
521 |
finally show "S homeomorphic cball a 1 \<inter> affine hull S" . |
|
522 |
qed |
|
523 |
||
524 |
corollary starlike_compact_projective_special: |
|
525 |
assumes "compact S" |
|
526 |
and cb01: "cball (0::'a::euclidean_space) 1 \<subseteq> S" |
|
527 |
and scale: "\<And>x u. \<lbrakk>x \<in> S; 0 \<le> u; u < 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x \<in> S - frontier S" |
|
528 |
shows "S homeomorphic (cball (0::'a::euclidean_space) 1)" |
|
529 |
proof - |
|
530 |
have "ball 0 1 \<subseteq> interior S" |
|
531 |
using cb01 interior_cball interior_mono by blast |
|
532 |
then have 0: "0 \<in> rel_interior S" |
|
533 |
by (meson centre_in_ball subsetD interior_subset_rel_interior le_numeral_extra(2) not_le) |
|
534 |
have [simp]: "affine hull S = UNIV" |
|
535 |
using \<open>ball 0 1 \<subseteq> interior S\<close> by (auto intro!: affine_hull_nonempty_interior) |
|
536 |
have star: "open_segment 0 x \<subseteq> rel_interior S" if "x \<in> S" for x |
|
63627 | 537 |
proof |
63130 | 538 |
fix p assume "p \<in> open_segment 0 x" |
539 |
then obtain u where "x \<noteq> 0" and u: "0 \<le> u" "u < 1" and p: "u *\<^sub>R x = p" |
|
63627 | 540 |
by (auto simp: in_segment) |
63130 | 541 |
then show "p \<in> rel_interior S" |
542 |
using scale [OF that u] closure_subset frontier_def interior_subset_rel_interior by fastforce |
|
543 |
qed |
|
544 |
show ?thesis |
|
545 |
using starlike_compact_projective2_0 [OF \<open>compact S\<close> 0 star] by simp |
|
546 |
qed |
|
547 |
||
548 |
lemma homeomorphic_convex_lemma: |
|
549 |
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
550 |
assumes "convex S" "compact S" "convex T" "compact T" |
|
551 |
and affeq: "aff_dim S = aff_dim T" |
|
552 |
shows "(S - rel_interior S) homeomorphic (T - rel_interior T) \<and> |
|
553 |
S homeomorphic T" |
|
554 |
proof (cases "rel_interior S = {} \<or> rel_interior T = {}") |
|
555 |
case True |
|
556 |
then show ?thesis |
|
557 |
by (metis Diff_empty affeq \<open>convex S\<close> \<open>convex T\<close> aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty) |
|
558 |
next |
|
559 |
case False |
|
560 |
then obtain a b where a: "a \<in> rel_interior S" and b: "b \<in> rel_interior T" by auto |
|
561 |
have starS: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S" |
|
562 |
using rel_interior_closure_convex_segment |
|
563 |
a \<open>convex S\<close> closure_subset subsetCE by blast |
|
564 |
have starT: "\<And>x. x \<in> T \<Longrightarrow> open_segment b x \<subseteq> rel_interior T" |
|
565 |
using rel_interior_closure_convex_segment |
|
566 |
b \<open>convex T\<close> closure_subset subsetCE by blast |
|
567 |
let ?aS = "op+ (-a) ` S" and ?bT = "op+ (-b) ` T" |
|
568 |
have 0: "0 \<in> affine hull ?aS" "0 \<in> affine hull ?bT" |
|
569 |
by (metis a b subsetD hull_inc image_eqI left_minus rel_interior_subset)+ |
|
570 |
have subs: "subspace (span ?aS)" "subspace (span ?bT)" |
|
571 |
by (rule subspace_span)+ |
|
572 |
moreover |
|
573 |
have "dim (span (op + (- a) ` S)) = dim (span (op + (- b) ` T))" |
|
574 |
by (metis 0 aff_dim_translation_eq aff_dim_zero affeq dim_span nat_int) |
|
575 |
ultimately obtain f g where "linear f" "linear g" |
|
576 |
and fim: "f ` span ?aS = span ?bT" |
|
577 |
and gim: "g ` span ?bT = span ?aS" |
|
578 |
and fno: "\<And>x. x \<in> span ?aS \<Longrightarrow> norm(f x) = norm x" |
|
579 |
and gno: "\<And>x. x \<in> span ?bT \<Longrightarrow> norm(g x) = norm x" |
|
580 |
and gf: "\<And>x. x \<in> span ?aS \<Longrightarrow> g(f x) = x" |
|
581 |
and fg: "\<And>x. x \<in> span ?bT \<Longrightarrow> f(g x) = x" |
|
582 |
by (rule isometries_subspaces) blast |
|
583 |
have [simp]: "continuous_on A f" for A |
|
584 |
using \<open>linear f\<close> linear_conv_bounded_linear linear_continuous_on by blast |
|
585 |
have [simp]: "continuous_on B g" for B |
|
586 |
using \<open>linear g\<close> linear_conv_bounded_linear linear_continuous_on by blast |
|
587 |
have eqspanS: "affine hull ?aS = span ?aS" |
|
588 |
by (metis a affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset) |
|
589 |
have eqspanT: "affine hull ?bT = span ?bT" |
|
590 |
by (metis b affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset) |
|
591 |
have "S homeomorphic cball a 1 \<inter> affine hull S" |
|
592 |
by (rule starlike_compact_projective2 [OF \<open>compact S\<close> a starS]) |
|
593 |
also have "... homeomorphic op+ (-a) ` (cball a 1 \<inter> affine hull S)" |
|
594 |
by (metis homeomorphic_translation) |
|
595 |
also have "... = cball 0 1 \<inter> op+ (-a) ` (affine hull S)" |
|
596 |
by (auto simp: dist_norm) |
|
597 |
also have "... = cball 0 1 \<inter> span ?aS" |
|
598 |
using eqspanS affine_hull_translation by blast |
|
599 |
also have "... homeomorphic cball 0 1 \<inter> span ?bT" |
|
600 |
proof (rule homeomorphicI [where f=f and g=g]) |
|
601 |
show fim1: "f ` (cball 0 1 \<inter> span ?aS) = cball 0 1 \<inter> span ?bT" |
|
602 |
apply (rule subset_antisym) |
|
603 |
using fim fno apply (force simp:, clarify) |
|
604 |
by (metis IntI fg gim gno image_eqI mem_cball_0) |
|
605 |
show "g ` (cball 0 1 \<inter> span ?bT) = cball 0 1 \<inter> span ?aS" |
|
606 |
apply (rule subset_antisym) |
|
607 |
using gim gno apply (force simp:, clarify) |
|
608 |
by (metis IntI fim1 gf image_eqI) |
|
609 |
qed (auto simp: fg gf) |
|
610 |
also have "... = cball 0 1 \<inter> op+ (-b) ` (affine hull T)" |
|
611 |
using eqspanT affine_hull_translation by blast |
|
612 |
also have "... = op+ (-b) ` (cball b 1 \<inter> affine hull T)" |
|
613 |
by (auto simp: dist_norm) |
|
614 |
also have "... homeomorphic (cball b 1 \<inter> affine hull T)" |
|
615 |
by (metis homeomorphic_translation homeomorphic_sym) |
|
616 |
also have "... homeomorphic T" |
|
617 |
by (metis starlike_compact_projective2 [OF \<open>compact T\<close> b starT] homeomorphic_sym) |
|
618 |
finally have 1: "S homeomorphic T" . |
|
619 |
||
620 |
have "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S" |
|
621 |
by (rule starlike_compact_projective1 [OF \<open>compact S\<close> a starS]) |
|
622 |
also have "... homeomorphic op+ (-a) ` (sphere a 1 \<inter> affine hull S)" |
|
623 |
by (metis homeomorphic_translation) |
|
624 |
also have "... = sphere 0 1 \<inter> op+ (-a) ` (affine hull S)" |
|
625 |
by (auto simp: dist_norm) |
|
626 |
also have "... = sphere 0 1 \<inter> span ?aS" |
|
627 |
using eqspanS affine_hull_translation by blast |
|
628 |
also have "... homeomorphic sphere 0 1 \<inter> span ?bT" |
|
629 |
proof (rule homeomorphicI [where f=f and g=g]) |
|
630 |
show fim1: "f ` (sphere 0 1 \<inter> span ?aS) = sphere 0 1 \<inter> span ?bT" |
|
631 |
apply (rule subset_antisym) |
|
632 |
using fim fno apply (force simp:, clarify) |
|
633 |
by (metis IntI fg gim gno image_eqI mem_sphere_0) |
|
634 |
show "g ` (sphere 0 1 \<inter> span ?bT) = sphere 0 1 \<inter> span ?aS" |
|
635 |
apply (rule subset_antisym) |
|
636 |
using gim gno apply (force simp:, clarify) |
|
637 |
by (metis IntI fim1 gf image_eqI) |
|
638 |
qed (auto simp: fg gf) |
|
639 |
also have "... = sphere 0 1 \<inter> op+ (-b) ` (affine hull T)" |
|
640 |
using eqspanT affine_hull_translation by blast |
|
641 |
also have "... = op+ (-b) ` (sphere b 1 \<inter> affine hull T)" |
|
642 |
by (auto simp: dist_norm) |
|
643 |
also have "... homeomorphic (sphere b 1 \<inter> affine hull T)" |
|
644 |
by (metis homeomorphic_translation homeomorphic_sym) |
|
645 |
also have "... homeomorphic T - rel_interior T" |
|
646 |
by (metis starlike_compact_projective1 [OF \<open>compact T\<close> b starT] homeomorphic_sym) |
|
647 |
finally have 2: "S - rel_interior S homeomorphic T - rel_interior T" . |
|
648 |
show ?thesis |
|
649 |
using 1 2 by blast |
|
650 |
qed |
|
651 |
||
652 |
lemma homeomorphic_convex_compact_sets: |
|
653 |
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
654 |
assumes "convex S" "compact S" "convex T" "compact T" |
|
655 |
and affeq: "aff_dim S = aff_dim T" |
|
656 |
shows "S homeomorphic T" |
|
657 |
using homeomorphic_convex_lemma [OF assms] assms |
|
658 |
by (auto simp: rel_frontier_def) |
|
659 |
||
660 |
lemma homeomorphic_rel_frontiers_convex_bounded_sets: |
|
661 |
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
662 |
assumes "convex S" "bounded S" "convex T" "bounded T" |
|
663 |
and affeq: "aff_dim S = aff_dim T" |
|
664 |
shows "rel_frontier S homeomorphic rel_frontier T" |
|
665 |
using assms homeomorphic_convex_lemma [of "closure S" "closure T"] |
|
666 |
by (simp add: rel_frontier_def convex_rel_interior_closure) |
|
667 |
||
668 |
||
669 |
subsection\<open>Homeomorphisms between punctured spheres and affine sets\<close> |
|
670 |
text\<open>Including the famous stereoscopic projection of the 3-D sphere to the complex plane\<close> |
|
671 |
||
672 |
text\<open>The special case with centre 0 and radius 1\<close> |
|
673 |
lemma homeomorphic_punctured_affine_sphere_affine_01: |
|
674 |
assumes "b \<in> sphere 0 1" "affine T" "0 \<in> T" "b \<in> T" "affine p" |
|
675 |
and affT: "aff_dim T = aff_dim p + 1" |
|
676 |
shows "(sphere 0 1 \<inter> T) - {b} homeomorphic p" |
|
677 |
proof - |
|
678 |
have [simp]: "norm b = 1" "b\<bullet>b = 1" |
|
679 |
using assms by (auto simp: norm_eq_1) |
|
680 |
have [simp]: "T \<inter> {v. b\<bullet>v = 0} \<noteq> {}" |
|
681 |
using \<open>0 \<in> T\<close> by auto |
|
682 |
have [simp]: "\<not> T \<subseteq> {v. b\<bullet>v = 0}" |
|
683 |
using \<open>norm b = 1\<close> \<open>b \<in> T\<close> by auto |
|
684 |
define f where "f \<equiv> \<lambda>x. 2 *\<^sub>R b + (2 / (1 - b\<bullet>x)) *\<^sub>R (x - b)" |
|
685 |
define g where "g \<equiv> \<lambda>y. b + (4 / (norm y ^ 2 + 4)) *\<^sub>R (y - 2 *\<^sub>R b)" |
|
686 |
have [simp]: "\<And>x. \<lbrakk>x \<in> T; b\<bullet>x = 0\<rbrakk> \<Longrightarrow> f (g x) = x" |
|
687 |
unfolding f_def g_def by (simp add: algebra_simps divide_simps add_nonneg_eq_0_iff) |
|
688 |
have no: "\<And>x. \<lbrakk>norm x = 1; b\<bullet>x \<noteq> 1\<rbrakk> \<Longrightarrow> (norm (f x))\<^sup>2 = 4 * (1 + b\<bullet>x) / (1 - b\<bullet>x)" |
|
689 |
apply (simp add: dot_square_norm [symmetric]) |
|
690 |
apply (simp add: f_def vector_add_divide_simps divide_simps norm_eq_1) |
|
691 |
apply (simp add: algebra_simps inner_commute) |
|
692 |
done |
|
693 |
have [simp]: "\<And>u::real. 8 + u * (u * 8) = u * 16 \<longleftrightarrow> u=1" |
|
694 |
by algebra |
|
695 |
have [simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> g (f x) = x" |
|
696 |
unfolding g_def no by (auto simp: f_def divide_simps) |
|
697 |
have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> norm (g x) = 1" |
|
698 |
unfolding g_def |
|
699 |
apply (rule power2_eq_imp_eq) |
|
700 |
apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps) |
|
701 |
apply (simp add: algebra_simps inner_commute) |
|
702 |
done |
|
703 |
have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> b \<bullet> g x \<noteq> 1" |
|
704 |
unfolding g_def |
|
705 |
apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps add_nonneg_eq_0_iff) |
|
706 |
apply (auto simp: algebra_simps) |
|
707 |
done |
|
708 |
have "subspace T" |
|
709 |
by (simp add: assms subspace_affine) |
|
710 |
have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> g x \<in> T" |
|
711 |
unfolding g_def |
|
712 |
by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff) |
|
713 |
have "f ` {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<subseteq> {x. b\<bullet>x = 0}" |
|
714 |
unfolding f_def using \<open>norm b = 1\<close> norm_eq_1 |
|
715 |
by (force simp: field_simps inner_add_right inner_diff_right) |
|
716 |
moreover have "f ` T \<subseteq> T" |
|
717 |
unfolding f_def using assms |
|
718 |
apply (auto simp: field_simps inner_add_right inner_diff_right) |
|
719 |
by (metis add_0 diff_zero mem_affine_3_minus) |
|
720 |
moreover have "{x. b\<bullet>x = 0} \<inter> T \<subseteq> f ` ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T)" |
|
721 |
apply clarify |
|
722 |
apply (rule_tac x = "g x" in image_eqI, auto) |
|
723 |
done |
|
724 |
ultimately have imf: "f ` ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T) = {x. b\<bullet>x = 0} \<inter> T" |
|
725 |
by blast |
|
726 |
have no4: "\<And>y. b\<bullet>y = 0 \<Longrightarrow> norm ((y\<bullet>y + 4) *\<^sub>R b + 4 *\<^sub>R (y - 2 *\<^sub>R b)) = y\<bullet>y + 4" |
|
727 |
apply (rule power2_eq_imp_eq) |
|
728 |
apply (simp_all add: dot_square_norm [symmetric]) |
|
729 |
apply (auto simp: power2_eq_square algebra_simps inner_commute) |
|
730 |
done |
|
731 |
have [simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> b \<bullet> f x = 0" |
|
732 |
by (simp add: f_def algebra_simps divide_simps) |
|
733 |
have [simp]: "\<And>x. \<lbrakk>x \<in> T; norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> f x \<in> T" |
|
734 |
unfolding f_def |
|
735 |
by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff) |
|
736 |
have "g ` {x. b\<bullet>x = 0} \<subseteq> {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1}" |
|
737 |
unfolding g_def |
|
738 |
apply (clarsimp simp: no4 vector_add_divide_simps divide_simps add_nonneg_eq_0_iff dot_square_norm [symmetric]) |
|
739 |
apply (auto simp: algebra_simps) |
|
740 |
done |
|
741 |
moreover have "g ` T \<subseteq> T" |
|
742 |
unfolding g_def |
|
743 |
by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff) |
|
744 |
moreover have "{x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T \<subseteq> g ` ({x. b\<bullet>x = 0} \<inter> T)" |
|
745 |
apply clarify |
|
746 |
apply (rule_tac x = "f x" in image_eqI, auto) |
|
747 |
done |
|
748 |
ultimately have img: "g ` ({x. b\<bullet>x = 0} \<inter> T) = {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T" |
|
749 |
by blast |
|
750 |
have aff: "affine ({x. b\<bullet>x = 0} \<inter> T)" |
|
751 |
by (blast intro: affine_hyperplane assms) |
|
752 |
have contf: "continuous_on ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T) f" |
|
753 |
unfolding f_def by (rule continuous_intros | force)+ |
|
754 |
have contg: "continuous_on ({x. b\<bullet>x = 0} \<inter> T) g" |
|
755 |
unfolding g_def by (rule continuous_intros | force simp: add_nonneg_eq_0_iff)+ |
|
756 |
have "(sphere 0 1 \<inter> T) - {b} = {x. norm x = 1 \<and> (b\<bullet>x \<noteq> 1)} \<inter> T" |
|
757 |
using \<open>norm b = 1\<close> by (auto simp: norm_eq_1) (metis vector_eq \<open>b\<bullet>b = 1\<close>) |
|
758 |
also have "... homeomorphic {x. b\<bullet>x = 0} \<inter> T" |
|
759 |
by (rule homeomorphicI [OF imf img contf contg]) auto |
|
760 |
also have "... homeomorphic p" |
|
761 |
apply (rule homeomorphic_affine_sets [OF aff \<open>affine p\<close>]) |
|
762 |
apply (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF \<open>affine T\<close>] affT) |
|
763 |
done |
|
764 |
finally show ?thesis . |
|
765 |
qed |
|
766 |
||
767 |
theorem homeomorphic_punctured_affine_sphere_affine: |
|
768 |
fixes a :: "'a :: euclidean_space" |
|
769 |
assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p" |
|
770 |
and aff: "aff_dim T = aff_dim p + 1" |
|
771 |
shows "((sphere a r \<inter> T) - {b}) homeomorphic p" |
|
772 |
proof - |
|
773 |
have "a \<noteq> b" using assms by auto |
|
774 |
then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))" |
|
775 |
by (simp add: inj_on_def) |
|
776 |
have "((sphere a r \<inter> T) - {b}) homeomorphic |
|
777 |
op+ (-a) ` ((sphere a r \<inter> T) - {b})" |
|
778 |
by (rule homeomorphic_translation) |
|
779 |
also have "... homeomorphic op *\<^sub>R (inverse r) ` op + (- a) ` (sphere a r \<inter> T - {b})" |
|
780 |
by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl) |
|
781 |
also have "... = sphere 0 1 \<inter> (op *\<^sub>R (inverse r) ` op + (- a) ` T) - {(b - a) /\<^sub>R r}" |
|
782 |
using assms by (auto simp: dist_norm norm_minus_commute divide_simps) |
|
783 |
also have "... homeomorphic p" |
|
784 |
apply (rule homeomorphic_punctured_affine_sphere_affine_01) |
|
785 |
using assms |
|
786 |
apply (auto simp: dist_norm norm_minus_commute affine_scaling affine_translation [symmetric] aff_dim_translation_eq inj) |
|
787 |
done |
|
788 |
finally show ?thesis . |
|
789 |
qed |
|
790 |
||
791 |
proposition homeomorphic_punctured_sphere_affine_gen: |
|
792 |
fixes a :: "'a :: euclidean_space" |
|
793 |
assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S" |
|
794 |
and "affine T" and affS: "aff_dim S = aff_dim T + 1" |
|
795 |
shows "rel_frontier S - {a} homeomorphic T" |
|
796 |
proof - |
|
797 |
have "S \<noteq> {}" using assms by auto |
|
798 |
obtain U :: "'a set" where "affine U" and affdS: "aff_dim U = aff_dim S" |
|
799 |
using choose_affine_subset [OF affine_UNIV aff_dim_geq] |
|
800 |
by (meson aff_dim_affine_hull affine_affine_hull) |
|
801 |
have "convex U" |
|
802 |
by (simp add: affine_imp_convex \<open>affine U\<close>) |
|
803 |
have "U \<noteq> {}" |
|
804 |
by (metis \<open>S \<noteq> {}\<close> \<open>aff_dim U = aff_dim S\<close> aff_dim_empty) |
|
805 |
then obtain z where "z \<in> U" |
|
806 |
by auto |
|
807 |
then have bne: "ball z 1 \<inter> U \<noteq> {}" by force |
|
808 |
have [simp]: "aff_dim(ball z 1 \<inter> U) = aff_dim U" |
|
809 |
using aff_dim_convex_Int_open [OF \<open>convex U\<close> open_ball] bne |
|
810 |
by (fastforce simp add: Int_commute) |
|
811 |
have "rel_frontier S homeomorphic rel_frontier (ball z 1 \<inter> U)" |
|
812 |
apply (rule homeomorphic_rel_frontiers_convex_bounded_sets) |
|
813 |
apply (auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms) |
|
814 |
done |
|
815 |
also have "... = sphere z 1 \<inter> U" |
|
816 |
using convex_affine_rel_frontier_Int [of "ball z 1" U] |
|
817 |
by (simp add: \<open>affine U\<close> bne) |
|
818 |
finally obtain h k where him: "h ` rel_frontier S = sphere z 1 \<inter> U" |
|
819 |
and kim: "k ` (sphere z 1 \<inter> U) = rel_frontier S" |
|
820 |
and hcon: "continuous_on (rel_frontier S) h" |
|
821 |
and kcon: "continuous_on (sphere z 1 \<inter> U) k" |
|
822 |
and kh: "\<And>x. x \<in> rel_frontier S \<Longrightarrow> k(h(x)) = x" |
|
823 |
and hk: "\<And>y. y \<in> sphere z 1 \<inter> U \<Longrightarrow> h(k(y)) = y" |
|
824 |
unfolding homeomorphic_def homeomorphism_def by auto |
|
825 |
have "rel_frontier S - {a} homeomorphic (sphere z 1 \<inter> U) - {h a}" |
|
826 |
proof (rule homeomorphicI [where f=h and g=k]) |
|
827 |
show h: "h ` (rel_frontier S - {a}) = sphere z 1 \<inter> U - {h a}" |
|
828 |
using him a kh by auto metis |
|
829 |
show "k ` (sphere z 1 \<inter> U - {h a}) = rel_frontier S - {a}" |
|
830 |
by (force simp: h [symmetric] image_comp o_def kh) |
|
831 |
qed (auto intro: continuous_on_subset hcon kcon simp: kh hk) |
|
832 |
also have "... homeomorphic T" |
|
833 |
apply (rule homeomorphic_punctured_affine_sphere_affine) |
|
834 |
using a him |
|
835 |
by (auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>) |
|
836 |
finally show ?thesis . |
|
837 |
qed |
|
838 |
||
839 |
||
840 |
lemma homeomorphic_punctured_sphere_affine: |
|
841 |
fixes a :: "'a :: euclidean_space" |
|
842 |
assumes "0 < r" and b: "b \<in> sphere a r" |
|
843 |
and "affine T" and affS: "aff_dim T + 1 = DIM('a)" |
|
844 |
shows "(sphere a r - {b}) homeomorphic T" |
|
845 |
using homeomorphic_punctured_sphere_affine_gen [of "cball a r" b T] |
|
846 |
assms aff_dim_cball by force |
|
847 |
||
848 |
corollary homeomorphic_punctured_sphere_hyperplane: |
|
849 |
fixes a :: "'a :: euclidean_space" |
|
850 |
assumes "0 < r" and b: "b \<in> sphere a r" |
|
851 |
and "c \<noteq> 0" |
|
852 |
shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}" |
|
853 |
apply (rule homeomorphic_punctured_sphere_affine) |
|
854 |
using assms |
|
855 |
apply (auto simp: affine_hyperplane of_nat_diff) |
|
856 |
done |
|
857 |
||
858 |
||
859 |
text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set |
|
860 |
is homeomorphic to a closed subset of a convex set, and |
|
861 |
if the set is locally compact we can take the convex set to be the universe.\<close> |
|
862 |
||
863 |
proposition homeomorphic_closedin_convex: |
|
864 |
fixes S :: "'m::euclidean_space set" |
|
865 |
assumes "aff_dim S < DIM('n)" |
|
866 |
obtains U and T :: "'n::euclidean_space set" |
|
867 |
where "convex U" "U \<noteq> {}" "closedin (subtopology euclidean U) T" |
|
868 |
"S homeomorphic T" |
|
869 |
proof (cases "S = {}") |
|
870 |
case True then show ?thesis |
|
871 |
by (rule_tac U=UNIV and T="{}" in that) auto |
|
872 |
next |
|
873 |
case False |
|
874 |
then obtain a where "a \<in> S" by auto |
|
875 |
obtain i::'n where i: "i \<in> Basis" "i \<noteq> 0" |
|
876 |
using SOME_Basis Basis_zero by force |
|
877 |
have "0 \<in> affine hull (op + (- a) ` S)" |
|
878 |
by (simp add: \<open>a \<in> S\<close> hull_inc) |
|
879 |
then have "dim (op + (- a) ` S) = aff_dim (op + (- a) ` S)" |
|
880 |
by (simp add: aff_dim_zero) |
|
881 |
also have "... < DIM('n)" |
|
882 |
by (simp add: aff_dim_translation_eq assms) |
|
883 |
finally have dd: "dim (op + (- a) ` S) < DIM('n)" |
|
884 |
by linarith |
|
885 |
obtain T where "subspace T" and Tsub: "T \<subseteq> {x. i \<bullet> x = 0}" |
|
886 |
and dimT: "dim T = dim (op + (- a) ` S)" |
|
887 |
apply (rule choose_subspace_of_subspace [of "dim (op + (- a) ` S)" "{x::'n. i \<bullet> x = 0}"]) |
|
888 |
apply (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>]) |
|
889 |
apply (metis DIM_positive Suc_pred dd not_le not_less_eq_eq) |
|
890 |
apply (metis span_eq subspace_hyperplane) |
|
891 |
done |
|
892 |
have "subspace (span (op + (- a) ` S))" |
|
893 |
using subspace_span by blast |
|
894 |
then obtain h k where "linear h" "linear k" |
|
895 |
and heq: "h ` span (op + (- a) ` S) = T" |
|
896 |
and keq:"k ` T = span (op + (- a) ` S)" |
|
897 |
and hinv [simp]: "\<And>x. x \<in> span (op + (- a) ` S) \<Longrightarrow> k(h x) = x" |
|
898 |
and kinv [simp]: "\<And>x. x \<in> T \<Longrightarrow> h(k x) = x" |
|
899 |
apply (rule isometries_subspaces [OF _ \<open>subspace T\<close>]) |
|
900 |
apply (auto simp: dimT) |
|
901 |
done |
|
902 |
have hcont: "continuous_on A h" and kcont: "continuous_on B k" for A B |
|
903 |
using \<open>linear h\<close> \<open>linear k\<close> linear_continuous_on linear_conv_bounded_linear by blast+ |
|
904 |
have ihhhh[simp]: "\<And>x. x \<in> S \<Longrightarrow> i \<bullet> h (x - a) = 0" |
|
905 |
using Tsub [THEN subsetD] heq span_inc by fastforce |
|
906 |
have "sphere 0 1 - {i} homeomorphic {x. i \<bullet> x = 0}" |
|
907 |
apply (rule homeomorphic_punctured_sphere_affine) |
|
908 |
using i |
|
909 |
apply (auto simp: affine_hyperplane) |
|
910 |
by (metis DIM_positive Suc_eq_plus1 add.left_neutral diff_add_cancel not_le not_less_eq_eq of_nat_1 of_nat_diff) |
|
911 |
then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i \<bullet> x = 0} f g" |
|
912 |
by (force simp: homeomorphic_def) |
|
913 |
have "h ` op + (- a) ` S \<subseteq> T" |
|
914 |
using heq span_clauses(1) span_linear_image by blast |
|
915 |
then have "g ` h ` op + (- a) ` S \<subseteq> g ` {x. i \<bullet> x = 0}" |
|
916 |
using Tsub by (simp add: image_mono) |
|
917 |
also have "... \<subseteq> sphere 0 1 - {i}" |
|
918 |
by (simp add: fg [unfolded homeomorphism_def]) |
|
919 |
finally have gh_sub_sph: "(g \<circ> h) ` op + (- a) ` S \<subseteq> sphere 0 1 - {i}" |
|
920 |
by (metis image_comp) |
|
921 |
then have gh_sub_cb: "(g \<circ> h) ` op + (- a) ` S \<subseteq> cball 0 1" |
|
922 |
by (metis Diff_subset order_trans sphere_cball) |
|
923 |
have [simp]: "\<And>u. u \<in> S \<Longrightarrow> norm (g (h (u - a))) = 1" |
|
924 |
using gh_sub_sph [THEN subsetD] by (auto simp: o_def) |
|
925 |
have ghcont: "continuous_on (op + (- a) ` S) (\<lambda>x. g (h x))" |
|
926 |
apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force) |
|
927 |
done |
|
928 |
have kfcont: "continuous_on ((g \<circ> h \<circ> op + (- a)) ` S) (\<lambda>x. k (f x))" |
|
929 |
apply (rule continuous_on_compose2 [OF kcont]) |
|
930 |
using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast) |
|
931 |
done |
|
932 |
have "S homeomorphic op + (- a) ` S" |
|
933 |
by (simp add: homeomorphic_translation) |
|
934 |
also have Shom: "\<dots> homeomorphic (g \<circ> h) ` op + (- a) ` S" |
|
935 |
apply (simp add: homeomorphic_def homeomorphism_def) |
|
936 |
apply (rule_tac x="g \<circ> h" in exI) |
|
937 |
apply (rule_tac x="k \<circ> f" in exI) |
|
938 |
apply (auto simp: ghcont kfcont span_clauses(1) homeomorphism_apply2 [OF fg] image_comp) |
|
939 |
apply (force simp: o_def homeomorphism_apply2 [OF fg] span_clauses(1)) |
|
940 |
done |
|
941 |
finally have Shom: "S homeomorphic (g \<circ> h) ` op + (- a) ` S" . |
|
942 |
show ?thesis |
|
943 |
apply (rule_tac U = "ball 0 1 \<union> image (g o h) (op + (- a) ` S)" |
|
944 |
and T = "image (g o h) (op + (- a) ` S)" |
|
945 |
in that) |
|
946 |
apply (rule convex_intermediate_ball [of 0 1], force) |
|
947 |
using gh_sub_cb apply force |
|
948 |
apply force |
|
949 |
apply (simp add: closedin_closed) |
|
950 |
apply (rule_tac x="sphere 0 1" in exI) |
|
951 |
apply (auto simp: Shom) |
|
952 |
done |
|
953 |
qed |
|
954 |
||
955 |
subsection\<open>Locally compact sets in an open set\<close> |
|
956 |
||
957 |
text\<open> Locally compact sets are closed in an open set and are homeomorphic |
|
958 |
to an absolutely closed set if we have one more dimension to play with.\<close> |
|
959 |
||
960 |
lemma locally_compact_open_Int_closure: |
|
961 |
fixes S :: "'a :: metric_space set" |
|
962 |
assumes "locally compact S" |
|
963 |
obtains T where "open T" "S = T \<inter> closure S" |
|
964 |
proof - |
|
965 |
have "\<forall>x\<in>S. \<exists>T v u. u = S \<inter> T \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<and> open T \<and> compact v" |
|
966 |
by (metis assms locally_compact openin_open) |
|
967 |
then obtain t v where |
|
968 |
tv: "\<And>x. x \<in> S |
|
969 |
\<Longrightarrow> v x \<subseteq> S \<and> open (t x) \<and> compact (v x) \<and> (\<exists>u. x \<in> u \<and> u \<subseteq> v x \<and> u = S \<inter> t x)" |
|
970 |
by metis |
|
971 |
then have o: "open (UNION S t)" |
|
972 |
by blast |
|
973 |
have "S = \<Union> (v ` S)" |
|
974 |
using tv by blast |
|
975 |
also have "... = UNION S t \<inter> closure S" |
|
976 |
proof |
|
977 |
show "UNION S v \<subseteq> UNION S t \<inter> closure S" |
|
978 |
apply safe |
|
979 |
apply (metis Int_iff subsetD UN_iff tv) |
|
980 |
apply (simp add: closure_def rev_subsetD tv) |
|
981 |
done |
|
982 |
have "t x \<inter> closure S \<subseteq> v x" if "x \<in> S" for x |
|
983 |
proof - |
|
984 |
have "t x \<inter> closure S \<subseteq> closure (t x \<inter> S)" |
|
985 |
by (simp add: open_Int_closure_subset that tv) |
|
986 |
also have "... \<subseteq> v x" |
|
987 |
by (metis Int_commute closure_minimal compact_imp_closed that tv) |
|
988 |
finally show ?thesis . |
|
989 |
qed |
|
990 |
then show "UNION S t \<inter> closure S \<subseteq> UNION S v" |
|
991 |
by blast |
|
992 |
qed |
|
993 |
finally have e: "S = UNION S t \<inter> closure S" . |
|
994 |
show ?thesis |
|
995 |
by (rule that [OF o e]) |
|
996 |
qed |
|
997 |
||
998 |
||
999 |
lemma locally_compact_closedin_open: |
|
1000 |
fixes S :: "'a :: metric_space set" |
|
1001 |
assumes "locally compact S" |
|
1002 |
obtains T where "open T" "closedin (subtopology euclidean T) S" |
|
1003 |
by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int) |
|
1004 |
||
1005 |
||
1006 |
lemma locally_compact_homeomorphism_projection_closed: |
|
1007 |
assumes "locally compact S" |
|
1008 |
obtains T and f :: "'a \<Rightarrow> 'a :: euclidean_space \<times> 'b :: euclidean_space" |
|
1009 |
where "closed T" "homeomorphism S T f fst" |
|
1010 |
proof (cases "closed S") |
|
1011 |
case True |
|
1012 |
then show ?thesis |
|
1013 |
apply (rule_tac T = "S \<times> {0}" and f = "\<lambda>x. (x, 0)" in that) |
|
1014 |
apply (auto simp: closed_Times homeomorphism_def continuous_intros) |
|
1015 |
done |
|
1016 |
next |
|
1017 |
case False |
|
1018 |
obtain U where "open U" and US: "U \<inter> closure S = S" |
|
1019 |
by (metis locally_compact_open_Int_closure [OF assms]) |
|
1020 |
with False have Ucomp: "-U \<noteq> {}" |
|
1021 |
using closure_eq by auto |
|
1022 |
have [simp]: "closure (- U) = -U" |
|
1023 |
by (simp add: \<open>open U\<close> closed_Compl) |
|
1024 |
define f :: "'a \<Rightarrow> 'a \<times> 'b" where "f \<equiv> \<lambda>x. (x, One /\<^sub>R setdist {x} (- U))" |
|
1025 |
have "continuous_on U (\<lambda>x. (x, One /\<^sub>R setdist {x} (- U)))" |
|
63301 | 1026 |
apply (intro continuous_intros continuous_on_setdist) |
1027 |
by (simp add: Ucomp setdist_eq_0_sing_1) |
|
63130 | 1028 |
then have homU: "homeomorphism U (f`U) f fst" |
1029 |
by (auto simp: f_def homeomorphism_def image_iff continuous_intros) |
|
1030 |
have cloS: "closedin (subtopology euclidean U) S" |
|
1031 |
by (metis US closed_closure closedin_closed_Int) |
|
1032 |
have cont: "isCont ((\<lambda>x. setdist {x} (- U)) o fst) z" for z :: "'a \<times> 'b" |
|
1033 |
by (rule isCont_o continuous_intros continuous_at_setdist)+ |
|
1034 |
have setdist1D: "setdist {a} (- U) *\<^sub>R b = One \<Longrightarrow> setdist {a} (- U) \<noteq> 0" for a::'a and b::'b |
|
1035 |
by force |
|
1036 |
have *: "r *\<^sub>R b = One \<Longrightarrow> b = (1 / r) *\<^sub>R One" for r and b::'b |
|
1037 |
by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one) |
|
1038 |
have "f ` U = {z. (setdist {fst z} (- U) *\<^sub>R snd z) \<in> {One}}" |
|
63301 | 1039 |
apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp) |
63130 | 1040 |
apply (rule_tac x=a in image_eqI) |
63301 | 1041 |
apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D) |
63130 | 1042 |
done |
1043 |
then have clfU: "closed (f ` U)" |
|
1044 |
apply (rule ssubst) |
|
1045 |
apply (rule continuous_closed_preimage_univ) |
|
1046 |
apply (auto intro: continuous_intros cont [unfolded o_def]) |
|
1047 |
done |
|
1048 |
have "closed (f ` S)" |
|
1049 |
apply (rule closedin_closed_trans [OF _ clfU]) |
|
1050 |
apply (rule homeomorphism_imp_closed_map [OF homU cloS]) |
|
1051 |
done |
|
1052 |
then show ?thesis |
|
1053 |
apply (rule that) |
|
1054 |
apply (rule homeomorphism_of_subsets [OF homU]) |
|
1055 |
using US apply auto |
|
1056 |
done |
|
1057 |
qed |
|
1058 |
||
1059 |
lemma locally_compact_closed_Int_open: |
|
1060 |
fixes S :: "'a :: euclidean_space set" |
|
1061 |
shows |
|
1062 |
"locally compact S \<longleftrightarrow> (\<exists>U u. closed U \<and> open u \<and> S = U \<inter> u)" |
|
1063 |
by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact) |
|
1064 |
||
1065 |
||
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1066 |
lemma lowerdim_embeddings: |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1067 |
assumes "DIM('a) < DIM('b)" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1068 |
obtains f :: "'a::euclidean_space*real \<Rightarrow> 'b::euclidean_space" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1069 |
and g :: "'b \<Rightarrow> 'a*real" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1070 |
and j :: 'b |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1071 |
where "linear f" "linear g" "\<And>z. g (f z) = z" "j \<in> Basis" "\<And>x. f(x,0) \<bullet> j = 0" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1072 |
proof - |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1073 |
let ?B = "Basis :: ('a*real) set" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1074 |
have b01: "(0,1) \<in> ?B" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1075 |
by (simp add: Basis_prod_def) |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1076 |
have "DIM('a * real) \<le> DIM('b)" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1077 |
by (simp add: Suc_leI assms) |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1078 |
then obtain basf :: "'a*real \<Rightarrow> 'b" where sbf: "basf ` ?B \<subseteq> Basis" and injbf: "inj_on basf Basis" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1079 |
by (metis finite_Basis card_le_inj) |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1080 |
define basg:: "'b \<Rightarrow> 'a * real" where |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1081 |
"basg \<equiv> \<lambda>i. if i \<in> basf ` Basis then inv_into Basis basf i else (0,1)" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1082 |
have bgf[simp]: "basg (basf i) = i" if "i \<in> Basis" for i |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1083 |
using inv_into_f_f injbf that by (force simp: basg_def) |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1084 |
have sbg: "basg ` Basis \<subseteq> ?B" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1085 |
by (force simp: basg_def injbf b01) |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1086 |
define f :: "'a*real \<Rightarrow> 'b" where "f \<equiv> \<lambda>u. \<Sum>j\<in>Basis. (u \<bullet> basg j) *\<^sub>R j" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1087 |
define g :: "'b \<Rightarrow> 'a*real" where "g \<equiv> \<lambda>z. (\<Sum>i\<in>Basis. (z \<bullet> basf i) *\<^sub>R i)" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1088 |
show ?thesis |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1089 |
proof |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1090 |
show "linear f" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1091 |
unfolding f_def |
64267 | 1092 |
by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps) |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1093 |
show "linear g" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1094 |
unfolding g_def |
64267 | 1095 |
by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps) |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1096 |
have *: "(\<Sum>a \<in> Basis. a \<bullet> basf b * (x \<bullet> basg a)) = x \<bullet> b" if "b \<in> Basis" for x b |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1097 |
using sbf that by auto |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1098 |
show gf: "g (f x) = x" for x |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1099 |
apply (rule euclidean_eqI) |
64267 | 1100 |
apply (simp add: f_def g_def inner_sum_left scaleR_sum_left algebra_simps) |
1101 |
apply (simp add: Groups_Big.sum_distrib_left [symmetric] *) |
|
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1102 |
done |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1103 |
show "basf(0,1) \<in> Basis" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1104 |
using b01 sbf by auto |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1105 |
then show "f(x,0) \<bullet> basf(0,1) = 0" for x |
64267 | 1106 |
apply (simp add: f_def inner_sum_left) |
1107 |
apply (rule comm_monoid_add_class.sum.neutral) |
|
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1108 |
using b01 inner_not_same_Basis by fastforce |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1109 |
qed |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1110 |
qed |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1111 |
|
63130 | 1112 |
proposition locally_compact_homeomorphic_closed: |
1113 |
fixes S :: "'a::euclidean_space set" |
|
1114 |
assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)" |
|
1115 |
obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T" |
|
1116 |
proof - |
|
1117 |
obtain U:: "('a*real)set" and h |
|
1118 |
where "closed U" and homU: "homeomorphism S U h fst" |
|
1119 |
using locally_compact_homeomorphism_projection_closed assms by metis |
|
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1120 |
obtain f :: "'a*real \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a*real" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1121 |
where "linear f" "linear g" and gf [simp]: "\<And>z. g (f z) = z" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1122 |
using lowerdim_embeddings [OF dimlt] by metis |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1123 |
then have "inj f" |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1124 |
by (metis injI) |
63130 | 1125 |
have gfU: "g ` f ` U = U" |
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1126 |
by (simp add: image_comp o_def) |
63130 | 1127 |
have "S homeomorphic U" |
1128 |
using homU homeomorphic_def by blast |
|
1129 |
also have "... homeomorphic f ` U" |
|
1130 |
apply (rule homeomorphicI [OF refl gfU]) |
|
1131 |
apply (meson \<open>inj f\<close> \<open>linear f\<close> homeomorphism_cont2 linear_homeomorphism_image) |
|
63945
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1132 |
using \<open>linear g\<close> linear_continuous_on linear_conv_bounded_linear apply blast |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1133 |
apply (auto simp: o_def) |
444eafb6e864
a few new theorems and a renaming
paulson <lp15@cam.ac.uk>
parents:
63918
diff
changeset
|
1134 |
done |
63130 | 1135 |
finally show ?thesis |
1136 |
apply (rule_tac T = "f ` U" in that) |
|
1137 |
apply (rule closed_injective_linear_image [OF \<open>closed U\<close> \<open>linear f\<close> \<open>inj f\<close>], assumption) |
|
1138 |
done |
|
1139 |
qed |
|
1140 |
||
1141 |
||
1142 |
lemma homeomorphic_convex_compact_lemma: |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1143 |
fixes S :: "'a::euclidean_space set" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1144 |
assumes "convex S" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1145 |
and "compact S" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1146 |
and "cball 0 1 \<subseteq> S" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1147 |
shows "S homeomorphic (cball (0::'a) 1)" |
63130 | 1148 |
proof (rule starlike_compact_projective_special[OF assms(2-3)]) |
1149 |
fix x u |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1150 |
assume "x \<in> S" and "0 \<le> u" and "u < (1::real)" |
63130 | 1151 |
have "open (ball (u *\<^sub>R x) (1 - u))" |
1152 |
by (rule open_ball) |
|
1153 |
moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)" |
|
1154 |
unfolding centre_in_ball using \<open>u < 1\<close> by simp |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1155 |
moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> S" |
63130 | 1156 |
proof |
1157 |
fix y |
|
1158 |
assume "y \<in> ball (u *\<^sub>R x) (1 - u)" |
|
1159 |
then have "dist (u *\<^sub>R x) y < 1 - u" |
|
1160 |
unfolding mem_ball . |
|
1161 |
with \<open>u < 1\<close> have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1" |
|
1162 |
by (simp add: dist_norm inverse_eq_divide norm_minus_commute) |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1163 |
with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> S" .. |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1164 |
with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> S" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1165 |
using \<open>x \<in> S\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1166 |
then show "y \<in> S" using \<open>u < 1\<close> |
63130 | 1167 |
by simp |
1168 |
qed |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1169 |
ultimately have "u *\<^sub>R x \<in> interior S" .. |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1170 |
then show "u *\<^sub>R x \<in> S - frontier S" |
63130 | 1171 |
using frontier_def and interior_subset by auto |
1172 |
qed |
|
1173 |
||
1174 |
proposition homeomorphic_convex_compact_cball: |
|
1175 |
fixes e :: real |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1176 |
and S :: "'a::euclidean_space set" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1177 |
assumes "convex S" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1178 |
and "compact S" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1179 |
and "interior S \<noteq> {}" |
63130 | 1180 |
and "e > 0" |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1181 |
shows "S homeomorphic (cball (b::'a) e)" |
63130 | 1182 |
proof - |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1183 |
obtain a where "a \<in> interior S" |
63130 | 1184 |
using assms(3) by auto |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1185 |
then obtain d where "d > 0" and d: "cball a d \<subseteq> S" |
63130 | 1186 |
unfolding mem_interior_cball by auto |
1187 |
let ?d = "inverse d" and ?n = "0::'a" |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1188 |
have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` S" |
63130 | 1189 |
apply rule |
1190 |
apply (rule_tac x="d *\<^sub>R x + a" in image_eqI) |
|
1191 |
defer |
|
1192 |
apply (rule d[unfolded subset_eq, rule_format]) |
|
1193 |
using \<open>d > 0\<close> |
|
1194 |
unfolding mem_cball dist_norm |
|
1195 |
apply (auto simp add: mult_right_le_one_le) |
|
1196 |
done |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1197 |
then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` S homeomorphic cball ?n 1" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1198 |
using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` S", |
63130 | 1199 |
OF convex_affinity compact_affinity] |
1200 |
using assms(1,2) |
|
1201 |
by (auto simp add: scaleR_right_diff_distrib) |
|
1202 |
then show ?thesis |
|
1203 |
apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]]) |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1204 |
apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" S "?d *\<^sub>R -a"]]) |
63130 | 1205 |
using \<open>d>0\<close> \<open>e>0\<close> |
1206 |
apply (auto simp add: scaleR_right_diff_distrib) |
|
1207 |
done |
|
1208 |
qed |
|
1209 |
||
1210 |
corollary homeomorphic_convex_compact: |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1211 |
fixes S :: "'a::euclidean_space set" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1212 |
and T :: "'a set" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1213 |
assumes "convex S" "compact S" "interior S \<noteq> {}" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1214 |
and "convex T" "compact T" "interior T \<noteq> {}" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1215 |
shows "S homeomorphic T" |
63130 | 1216 |
using assms |
1217 |
by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym) |
|
1218 |
||
63301 | 1219 |
subsection\<open>Covering spaces and lifting results for them\<close> |
1220 |
||
1221 |
definition covering_space |
|
1222 |
:: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool" |
|
1223 |
where |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1224 |
"covering_space c p S \<equiv> |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1225 |
continuous_on c p \<and> p ` c = S \<and> |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1226 |
(\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (subtopology euclidean S) T \<and> |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1227 |
(\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> T} \<and> |
63301 | 1228 |
(\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and> |
1229 |
pairwise disjnt v \<and> |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1230 |
(\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))" |
63301 | 1231 |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1232 |
lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p" |
63301 | 1233 |
by (simp add: covering_space_def) |
1234 |
||
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1235 |
lemma covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S" |
63301 | 1236 |
by (simp add: covering_space_def) |
1237 |
||
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1238 |
lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T" |
63301 | 1239 |
apply (simp add: homeomorphism_def covering_space_def, clarify) |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1240 |
apply (rule_tac x=T in exI, simp) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1241 |
apply (rule_tac x="{S}" in exI, auto) |
63301 | 1242 |
done |
1243 |
||
1244 |
lemma covering_space_local_homeomorphism: |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1245 |
assumes "covering_space c p S" "x \<in> c" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1246 |
obtains T u q where "x \<in> T" "openin (subtopology euclidean c) T" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1247 |
"p x \<in> u" "openin (subtopology euclidean S) u" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1248 |
"homeomorphism T u p q" |
63301 | 1249 |
using assms |
1250 |
apply (simp add: covering_space_def, clarify) |
|
1251 |
apply (drule_tac x="p x" in bspec, force) |
|
1252 |
by (metis (no_types, lifting) Union_iff mem_Collect_eq) |
|
1253 |
||
1254 |
||
1255 |
lemma covering_space_local_homeomorphism_alt: |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1256 |
assumes p: "covering_space c p S" and "y \<in> S" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1257 |
obtains x T u q where "p x = y" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1258 |
"x \<in> T" "openin (subtopology euclidean c) T" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1259 |
"y \<in> u" "openin (subtopology euclidean S) u" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1260 |
"homeomorphism T u p q" |
63301 | 1261 |
proof - |
1262 |
obtain x where "p x = y" "x \<in> c" |
|
1263 |
using assms covering_space_imp_surjective by blast |
|
1264 |
show ?thesis |
|
1265 |
apply (rule covering_space_local_homeomorphism [OF p \<open>x \<in> c\<close>]) |
|
1266 |
using that \<open>p x = y\<close> by blast |
|
1267 |
qed |
|
1268 |
||
1269 |
proposition covering_space_open_map: |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1270 |
fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1271 |
assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1272 |
shows "openin (subtopology euclidean S) (p ` T)" |
63301 | 1273 |
proof - |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1274 |
have pce: "p ` c = S" |
63301 | 1275 |
and covs: |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1276 |
"\<And>x. x \<in> S \<Longrightarrow> |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1277 |
\<exists>X VS. x \<in> X \<and> openin (subtopology euclidean S) X \<and> |
63301 | 1278 |
\<Union>VS = {x. x \<in> c \<and> p x \<in> X} \<and> |
1279 |
(\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and> |
|
1280 |
pairwise disjnt VS \<and> |
|
1281 |
(\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)" |
|
1282 |
using p by (auto simp: covering_space_def) |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1283 |
have "T \<subseteq> c" by (metis openin_euclidean_subtopology_iff T) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1284 |
have "\<exists>X. openin (subtopology euclidean S) X \<and> y \<in> X \<and> X \<subseteq> p ` T" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1285 |
if "y \<in> p ` T" for y |
63301 | 1286 |
proof - |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1287 |
have "y \<in> S" using \<open>T \<subseteq> c\<close> pce that by blast |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1288 |
obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean S) U" |
63301 | 1289 |
and VS: "\<Union>VS = {x. x \<in> c \<and> p x \<in> U}" |
1290 |
and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V" |
|
1291 |
and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q" |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1292 |
using covs [OF \<open>y \<in> S\<close>] by auto |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1293 |
obtain x where "x \<in> c" "p x \<in> U" "x \<in> T" "p x = y" |
63301 | 1294 |
apply simp |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1295 |
using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast |
63301 | 1296 |
with VS obtain V where "x \<in> V" "V \<in> VS" by auto |
1297 |
then obtain q where q: "homeomorphism V U p q" using homVS by blast |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1298 |
then have ptV: "p ` (T \<inter> V) = U \<inter> {z. q z \<in> (T \<inter> V)}" |
63301 | 1299 |
using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def) |
1300 |
have ocv: "openin (subtopology euclidean c) V" |
|
1301 |
by (simp add: \<open>V \<in> VS\<close> openVS) |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1302 |
have "openin (subtopology euclidean U) {z \<in> U. q z \<in> T \<inter> V}" |
63301 | 1303 |
apply (rule continuous_on_open [THEN iffD1, rule_format]) |
1304 |
using homeomorphism_def q apply blast |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1305 |
using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def |
63301 | 1306 |
by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff) |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1307 |
then have os: "openin (subtopology euclidean S) (U \<inter> {z. q z \<in> T \<inter> V})" |
63301 | 1308 |
using openin_trans [of U] by (simp add: Collect_conj_eq U) |
1309 |
show ?thesis |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1310 |
apply (rule_tac x = "p ` (T \<inter> V)" in exI) |
63301 | 1311 |
apply (rule conjI) |
1312 |
apply (simp only: ptV os) |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1313 |
using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> T\<close> apply blast |
63301 | 1314 |
done |
1315 |
qed |
|
1316 |
with openin_subopen show ?thesis by blast |
|
1317 |
qed |
|
1318 |
||
1319 |
lemma covering_space_lift_unique_gen: |
|
1320 |
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" |
|
1321 |
fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector" |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1322 |
assumes cov: "covering_space c p S" |
63301 | 1323 |
and eq: "g1 a = g2 a" |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1324 |
and f: "continuous_on T f" "f ` T \<subseteq> S" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1325 |
and g1: "continuous_on T g1" "g1 ` T \<subseteq> c" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1326 |
and fg1: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1327 |
and g2: "continuous_on T g2" "g2 ` T \<subseteq> c" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1328 |
and fg2: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1329 |
and u_compt: "U \<in> components T" and "a \<in> U" "x \<in> U" |
63301 | 1330 |
shows "g1 x = g2 x" |
1331 |
proof - |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1332 |
have "U \<subseteq> T" by (rule in_components_subset [OF u_compt]) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1333 |
def G12 \<equiv> "{x \<in> U. g1 x - g2 x = 0}" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1334 |
have "connected U" by (rule in_components_connected [OF u_compt]) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1335 |
have contu: "continuous_on U g1" "continuous_on U g2" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1336 |
using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+ |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1337 |
have o12: "openin (subtopology euclidean U) G12" |
63301 | 1338 |
unfolding G12_def |
1339 |
proof (subst openin_subopen, clarify) |
|
1340 |
fix z |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1341 |
assume z: "z \<in> U" "g1 z - g2 z = 0" |
63301 | 1342 |
obtain v w q where "g1 z \<in> v" and ocv: "openin (subtopology euclidean c) v" |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1343 |
and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean S) w" |
63301 | 1344 |
and hom: "homeomorphism v w p q" |
1345 |
apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov]) |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1346 |
using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+ |
63301 | 1347 |
done |
1348 |
have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1349 |
have gg: "{x \<in> U. g x \<in> v} = {x \<in> U. g x \<in> (v \<inter> g ` U)}" for g |
63301 | 1350 |
by auto |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1351 |
have "openin (subtopology euclidean (g1 ` U)) (v \<inter> g1 ` U)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1352 |
using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1353 |
then have 1: "openin (subtopology euclidean U) {x \<in> U. g1 x \<in> v}" |
63301 | 1354 |
unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format]) |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1355 |
have "openin (subtopology euclidean (g2 ` U)) (v \<inter> g2 ` U)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1356 |
using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1357 |
then have 2: "openin (subtopology euclidean U) {x \<in> U. g2 x \<in> v}" |
63301 | 1358 |
unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format]) |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1359 |
show "\<exists>T. openin (subtopology euclidean U) T \<and> |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1360 |
z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}" |
63301 | 1361 |
using z |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1362 |
apply (rule_tac x = "{x. x \<in> U \<and> g1 x \<in> v} \<inter> {x. x \<in> U \<and> g2 x \<in> v}" in exI) |
63301 | 1363 |
apply (intro conjI) |
1364 |
apply (rule openin_Int [OF 1 2]) |
|
1365 |
using \<open>g1 z \<in> v\<close> \<open>g2 z \<in> v\<close> apply (force simp:, clarify) |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1366 |
apply (metis \<open>U \<subseteq> T\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def) |
63301 | 1367 |
done |
1368 |
qed |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1369 |
have c12: "closedin (subtopology euclidean U) G12" |
63301 | 1370 |
unfolding G12_def |
1371 |
by (intro continuous_intros continuous_closedin_preimage_constant contu) |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1372 |
have "G12 = {} \<or> G12 = U" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1373 |
by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected U\<close> conjI o12 c12) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1374 |
with eq \<open>a \<in> U\<close> have "\<And>x. x \<in> U \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def) |
63301 | 1375 |
then show ?thesis |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1376 |
using \<open>x \<in> U\<close> by force |
63301 | 1377 |
qed |
1378 |
||
1379 |
proposition covering_space_lift_unique: |
|
1380 |
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" |
|
1381 |
fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector" |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1382 |
assumes "covering_space c p S" |
63301 | 1383 |
"g1 a = g2 a" |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1384 |
"continuous_on T f" "f ` T \<subseteq> S" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1385 |
"continuous_on T g1" "g1 ` T \<subseteq> c" "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1386 |
"continuous_on T g2" "g2 ` T \<subseteq> c" "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1387 |
"connected T" "a \<in> T" "x \<in> T" |
63301 | 1388 |
shows "g1 x = g2 x" |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64394
diff
changeset
|
1389 |
using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv by blast |
63301 | 1390 |
|
64791
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1391 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1392 |
lemma covering_space_locally: |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1393 |
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1394 |
assumes loc: "locally \<phi> C" and cov: "covering_space C p S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1395 |
and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1396 |
shows "locally \<psi> S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1397 |
proof - |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1398 |
have "locally \<psi> (p ` C)" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1399 |
apply (rule locally_open_map_image [OF loc]) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1400 |
using cov covering_space_imp_continuous apply blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1401 |
using cov covering_space_imp_surjective covering_space_open_map apply blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1402 |
by (simp add: pim) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1403 |
then show ?thesis |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1404 |
using covering_space_imp_surjective [OF cov] by metis |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1405 |
qed |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1406 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1407 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1408 |
proposition covering_space_locally_eq: |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1409 |
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1410 |
assumes cov: "covering_space C p S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1411 |
and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1412 |
and qim: "\<And>q U. \<lbrakk>U \<subseteq> S; continuous_on U q; \<psi> U\<rbrakk> \<Longrightarrow> \<phi>(q ` U)" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1413 |
shows "locally \<psi> S \<longleftrightarrow> locally \<phi> C" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1414 |
(is "?lhs = ?rhs") |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1415 |
proof |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1416 |
assume L: ?lhs |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1417 |
show ?rhs |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1418 |
proof (rule locallyI) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1419 |
fix V x |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1420 |
assume V: "openin (subtopology euclidean C) V" and "x \<in> V" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1421 |
have "p x \<in> p ` C" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1422 |
by (metis IntE V \<open>x \<in> V\<close> imageI openin_open) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1423 |
then obtain T \<V> where "p x \<in> T" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1424 |
and opeT: "openin (subtopology euclidean S) T" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1425 |
and veq: "\<Union>\<V> = {x \<in> C. p x \<in> T}" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1426 |
and ope: "\<forall>U\<in>\<V>. openin (subtopology euclidean C) U" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1427 |
and hom: "\<forall>U\<in>\<V>. \<exists>q. homeomorphism U T p q" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1428 |
using cov unfolding covering_space_def by (blast intro: that) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1429 |
have "x \<in> \<Union>\<V>" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1430 |
using V veq \<open>p x \<in> T\<close> \<open>x \<in> V\<close> openin_imp_subset by fastforce |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1431 |
then obtain U where "x \<in> U" "U \<in> \<V>" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1432 |
by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1433 |
then obtain q where opeU: "openin (subtopology euclidean C) U" and q: "homeomorphism U T p q" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1434 |
using ope hom by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1435 |
with V have "openin (subtopology euclidean C) (U \<inter> V)" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1436 |
by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1437 |
then have UV: "openin (subtopology euclidean S) (p ` (U \<inter> V))" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1438 |
using cov covering_space_open_map by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1439 |
obtain W W' where opeW: "openin (subtopology euclidean S) W" and "\<psi> W'" "p x \<in> W" "W \<subseteq> W'" and W'sub: "W' \<subseteq> p ` (U \<inter> V)" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1440 |
using locallyE [OF L UV] \<open>x \<in> U\<close> \<open>x \<in> V\<close> by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1441 |
then have "W \<subseteq> T" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1442 |
by (metis Int_lower1 q homeomorphism_image1 image_Int_subset order_trans) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1443 |
show "\<exists>U Z. openin (subtopology euclidean C) U \<and> |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1444 |
\<phi> Z \<and> x \<in> U \<and> U \<subseteq> Z \<and> Z \<subseteq> V" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1445 |
proof (intro exI conjI) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1446 |
have "openin (subtopology euclidean T) W" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1447 |
by (meson opeW opeT openin_imp_subset openin_subset_trans \<open>W \<subseteq> T\<close>) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1448 |
then have "openin (subtopology euclidean U) (q ` W)" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1449 |
by (meson homeomorphism_imp_open_map homeomorphism_symD q) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1450 |
then show "openin (subtopology euclidean C) (q ` W)" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1451 |
using opeU openin_trans by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1452 |
show "\<phi> (q ` W')" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1453 |
by (metis (mono_tags, lifting) Int_subset_iff UV W'sub \<open>\<psi> W'\<close> continuous_on_subset dual_order.trans homeomorphism_def image_Int_subset openin_imp_subset q qim) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1454 |
show "x \<in> q ` W" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1455 |
by (metis \<open>p x \<in> W\<close> \<open>x \<in> U\<close> homeomorphism_def imageI q) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1456 |
show "q ` W \<subseteq> q ` W'" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1457 |
using \<open>W \<subseteq> W'\<close> by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1458 |
have "W' \<subseteq> p ` V" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1459 |
using W'sub by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1460 |
then show "q ` W' \<subseteq> V" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1461 |
using W'sub homeomorphism_apply1 [OF q] by auto |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1462 |
qed |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1463 |
qed |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1464 |
next |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1465 |
assume ?rhs |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1466 |
then show ?lhs |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1467 |
using cov covering_space_locally pim by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1468 |
qed |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1469 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1470 |
lemma covering_space_locally_compact_eq: |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1471 |
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1472 |
assumes "covering_space C p S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1473 |
shows "locally compact S \<longleftrightarrow> locally compact C" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1474 |
apply (rule covering_space_locally_eq [OF assms]) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1475 |
apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1476 |
using compact_continuous_image by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1477 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1478 |
lemma covering_space_locally_connected_eq: |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1479 |
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1480 |
assumes "covering_space C p S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1481 |
shows "locally connected S \<longleftrightarrow> locally connected C" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1482 |
apply (rule covering_space_locally_eq [OF assms]) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1483 |
apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1484 |
using connected_continuous_image by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1485 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1486 |
lemma covering_space_locally_path_connected_eq: |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1487 |
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1488 |
assumes "covering_space C p S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1489 |
shows "locally path_connected S \<longleftrightarrow> locally path_connected C" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1490 |
apply (rule covering_space_locally_eq [OF assms]) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1491 |
apply (meson path_connected_continuous_image assms continuous_on_subset covering_space_imp_continuous) |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1492 |
using path_connected_continuous_image by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1493 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1494 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1495 |
lemma covering_space_locally_compact: |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1496 |
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1497 |
assumes "locally compact C" "covering_space C p S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1498 |
shows "locally compact S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1499 |
using assms covering_space_locally_compact_eq by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1500 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1501 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1502 |
lemma covering_space_locally_connected: |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1503 |
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1504 |
assumes "locally connected C" "covering_space C p S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1505 |
shows "locally connected S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1506 |
using assms covering_space_locally_connected_eq by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1507 |
|
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1508 |
lemma covering_space_locally_path_connected: |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1509 |
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1510 |
assumes "locally path_connected C" "covering_space C p S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1511 |
shows "locally path_connected S" |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1512 |
using assms covering_space_locally_path_connected_eq by blast |
05a2b3b20664
facts about ANRs, ENRs, covering spaces
paulson <lp15@cam.ac.uk>
parents:
64789
diff
changeset
|
1513 |
|
63130 | 1514 |
end |