15 |
15 |
16 subsection \<open>TODO: move?\<close> |
16 subsection \<open>TODO: move?\<close> |
17 |
17 |
18 lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)" |
18 lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)" |
19 using openI by auto |
19 using openI by auto |
|
20 |
|
21 |
|
22 subsubsection%unimportant \<open>Archimedean properties and useful consequences\<close> |
|
23 |
|
24 text\<open>Bernoulli's inequality\<close> |
|
25 proposition Bernoulli_inequality: |
|
26 fixes x :: real |
|
27 assumes "-1 \<le> x" |
|
28 shows "1 + n * x \<le> (1 + x) ^ n" |
|
29 proof (induct n) |
|
30 case 0 |
|
31 then show ?case by simp |
|
32 next |
|
33 case (Suc n) |
|
34 have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2" |
|
35 by (simp add: algebra_simps) |
|
36 also have "... = (1 + x) * (1 + n*x)" |
|
37 by (auto simp: power2_eq_square algebra_simps of_nat_Suc) |
|
38 also have "... \<le> (1 + x) ^ Suc n" |
|
39 using Suc.hyps assms mult_left_mono by fastforce |
|
40 finally show ?case . |
|
41 qed |
|
42 |
|
43 corollary Bernoulli_inequality_even: |
|
44 fixes x :: real |
|
45 assumes "even n" |
|
46 shows "1 + n * x \<le> (1 + x) ^ n" |
|
47 proof (cases "-1 \<le> x \<or> n=0") |
|
48 case True |
|
49 then show ?thesis |
|
50 by (auto simp: Bernoulli_inequality) |
|
51 next |
|
52 case False |
|
53 then have "real n \<ge> 1" |
|
54 by simp |
|
55 with False have "n * x \<le> -1" |
|
56 by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one) |
|
57 then have "1 + n * x \<le> 0" |
|
58 by auto |
|
59 also have "... \<le> (1 + x) ^ n" |
|
60 using assms |
|
61 using zero_le_even_power by blast |
|
62 finally show ?thesis . |
|
63 qed |
|
64 |
|
65 corollary real_arch_pow: |
|
66 fixes x :: real |
|
67 assumes x: "1 < x" |
|
68 shows "\<exists>n. y < x^n" |
|
69 proof - |
|
70 from x have x0: "x - 1 > 0" |
|
71 by arith |
|
72 from reals_Archimedean3[OF x0, rule_format, of y] |
|
73 obtain n :: nat where n: "y < real n * (x - 1)" by metis |
|
74 from x0 have x00: "x- 1 \<ge> -1" by arith |
|
75 from Bernoulli_inequality[OF x00, of n] n |
|
76 have "y < x^n" by auto |
|
77 then show ?thesis by metis |
|
78 qed |
|
79 |
|
80 corollary real_arch_pow_inv: |
|
81 fixes x y :: real |
|
82 assumes y: "y > 0" |
|
83 and x1: "x < 1" |
|
84 shows "\<exists>n. x^n < y" |
|
85 proof (cases "x > 0") |
|
86 case True |
|
87 with x1 have ix: "1 < 1/x" by (simp add: field_simps) |
|
88 from real_arch_pow[OF ix, of "1/y"] |
|
89 obtain n where n: "1/y < (1/x)^n" by blast |
|
90 then show ?thesis using y \<open>x > 0\<close> |
|
91 by (auto simp add: field_simps) |
|
92 next |
|
93 case False |
|
94 with y x1 show ?thesis |
|
95 by (metis less_le_trans not_less power_one_right) |
|
96 qed |
|
97 |
|
98 lemma forall_pos_mono: |
|
99 "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow> |
|
100 (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)" |
|
101 by (metis real_arch_inverse) |
|
102 |
|
103 lemma forall_pos_mono_1: |
|
104 "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow> |
|
105 (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e" |
|
106 apply (rule forall_pos_mono) |
|
107 apply auto |
|
108 apply (metis Suc_pred of_nat_Suc) |
|
109 done |
|
110 |
|
111 subsubsection%unimportant \<open>Affine transformations of intervals\<close> |
|
112 |
|
113 lemma real_affinity_le: "0 < m \<Longrightarrow> m * x + c \<le> y \<longleftrightarrow> x \<le> inverse m * y + - (c / m)" |
|
114 for m :: "'a::linordered_field" |
|
115 by (simp add: field_simps) |
|
116 |
|
117 lemma real_le_affinity: "0 < m \<Longrightarrow> y \<le> m * x + c \<longleftrightarrow> inverse m * y + - (c / m) \<le> x" |
|
118 for m :: "'a::linordered_field" |
|
119 by (simp add: field_simps) |
|
120 |
|
121 lemma real_affinity_lt: "0 < m \<Longrightarrow> m * x + c < y \<longleftrightarrow> x < inverse m * y + - (c / m)" |
|
122 for m :: "'a::linordered_field" |
|
123 by (simp add: field_simps) |
|
124 |
|
125 lemma real_lt_affinity: "0 < m \<Longrightarrow> y < m * x + c \<longleftrightarrow> inverse m * y + - (c / m) < x" |
|
126 for m :: "'a::linordered_field" |
|
127 by (simp add: field_simps) |
|
128 |
|
129 lemma real_affinity_eq: "m \<noteq> 0 \<Longrightarrow> m * x + c = y \<longleftrightarrow> x = inverse m * y + - (c / m)" |
|
130 for m :: "'a::linordered_field" |
|
131 by (simp add: field_simps) |
|
132 |
|
133 lemma real_eq_affinity: "m \<noteq> 0 \<Longrightarrow> y = m * x + c \<longleftrightarrow> inverse m * y + - (c / m) = x" |
|
134 for m :: "'a::linordered_field" |
|
135 by (simp add: field_simps) |
|
136 |
20 |
137 |
21 |
138 |
22 subsection \<open>Topological Basis\<close> |
139 subsection \<open>Topological Basis\<close> |
23 |
140 |
24 context topological_space |
141 context topological_space |
1969 fixes s :: "'a::{t1_space, first_countable_topology} set" |
2103 fixes s :: "'a::{t1_space, first_countable_topology} set" |
1970 shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s" |
2104 shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s" |
1971 by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point) |
2105 by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point) |
1972 |
2106 |
1973 |
2107 |
|
2108 subsection%unimportant \<open>Cartesian products\<close> |
|
2109 |
|
2110 lemma seq_compact_Times: "seq_compact s \<Longrightarrow> seq_compact t \<Longrightarrow> seq_compact (s \<times> t)" |
|
2111 unfolding seq_compact_def |
|
2112 apply clarify |
|
2113 apply (drule_tac x="fst \<circ> f" in spec) |
|
2114 apply (drule mp, simp add: mem_Times_iff) |
|
2115 apply (clarify, rename_tac l1 r1) |
|
2116 apply (drule_tac x="snd \<circ> f \<circ> r1" in spec) |
|
2117 apply (drule mp, simp add: mem_Times_iff) |
|
2118 apply (clarify, rename_tac l2 r2) |
|
2119 apply (rule_tac x="(l1, l2)" in rev_bexI, simp) |
|
2120 apply (rule_tac x="r1 \<circ> r2" in exI) |
|
2121 apply (rule conjI, simp add: strict_mono_def) |
|
2122 apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption) |
|
2123 apply (drule (1) tendsto_Pair) back |
|
2124 apply (simp add: o_def) |
|
2125 done |
|
2126 |
|
2127 lemma compact_Times: |
|
2128 assumes "compact s" "compact t" |
|
2129 shows "compact (s \<times> t)" |
|
2130 proof (rule compactI) |
|
2131 fix C |
|
2132 assume C: "\<forall>t\<in>C. open t" "s \<times> t \<subseteq> \<Union>C" |
|
2133 have "\<forall>x\<in>s. \<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)" |
|
2134 proof |
|
2135 fix x |
|
2136 assume "x \<in> s" |
|
2137 have "\<forall>y\<in>t. \<exists>a b c. c \<in> C \<and> open a \<and> open b \<and> x \<in> a \<and> y \<in> b \<and> a \<times> b \<subseteq> c" (is "\<forall>y\<in>t. ?P y") |
|
2138 proof |
|
2139 fix y |
|
2140 assume "y \<in> t" |
|
2141 with \<open>x \<in> s\<close> C obtain c where "c \<in> C" "(x, y) \<in> c" "open c" by auto |
|
2142 then show "?P y" by (auto elim!: open_prod_elim) |
|
2143 qed |
|
2144 then obtain a b c where b: "\<And>y. y \<in> t \<Longrightarrow> open (b y)" |
|
2145 and c: "\<And>y. y \<in> t \<Longrightarrow> c y \<in> C \<and> open (a y) \<and> open (b y) \<and> x \<in> a y \<and> y \<in> b y \<and> a y \<times> b y \<subseteq> c y" |
|
2146 by metis |
|
2147 then have "\<forall>y\<in>t. open (b y)" "t \<subseteq> (\<Union>y\<in>t. b y)" by auto |
|
2148 with compactE_image[OF \<open>compact t\<close>] obtain D where D: "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)" |
|
2149 by metis |
|
2150 moreover from D c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)" |
|
2151 by (fastforce simp: subset_eq) |
|
2152 ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)" |
|
2153 using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT) |
|
2154 qed |
|
2155 then obtain a d where a: "\<And>x. x\<in>s \<Longrightarrow> open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)" |
|
2156 and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>d x" |
|
2157 unfolding subset_eq UN_iff by metis |
|
2158 moreover |
|
2159 from compactE_image[OF \<open>compact s\<close> a] |
|
2160 obtain e where e: "e \<subseteq> s" "finite e" and s: "s \<subseteq> (\<Union>x\<in>e. a x)" |
|
2161 by auto |
|
2162 moreover |
|
2163 { |
|
2164 from s have "s \<times> t \<subseteq> (\<Union>x\<in>e. a x \<times> t)" |
|
2165 by auto |
|
2166 also have "\<dots> \<subseteq> (\<Union>x\<in>e. \<Union>d x)" |
|
2167 using d \<open>e \<subseteq> s\<close> by (intro UN_mono) auto |
|
2168 finally have "s \<times> t \<subseteq> (\<Union>x\<in>e. \<Union>d x)" . |
|
2169 } |
|
2170 ultimately show "\<exists>C'\<subseteq>C. finite C' \<and> s \<times> t \<subseteq> \<Union>C'" |
|
2171 by (intro exI[of _ "(\<Union>x\<in>e. d x)"]) (auto simp: subset_eq) |
|
2172 qed |
|
2173 |
|
2174 |
1974 subsection \<open>Continuity\<close> |
2175 subsection \<open>Continuity\<close> |
1975 |
2176 |
1976 lemma continuous_at_imp_continuous_within: |
2177 lemma continuous_at_imp_continuous_within: |
1977 "continuous (at x) f \<Longrightarrow> continuous (at x within s) f" |
2178 "continuous (at x) f \<Longrightarrow> continuous (at x within s) f" |
1978 unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto |
2179 unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto |
2094 using assms T_def by (auto simp: tendsto_def) |
2295 using assms T_def by (auto simp: tendsto_def) |
2095 then show "eventually (\<lambda>n. (f \<circ> x) n \<in> S) sequentially" |
2296 then show "eventually (\<lambda>n. (f \<circ> x) n \<in> S) sequentially" |
2096 using T_def by (auto elim!: eventually_mono) |
2297 using T_def by (auto elim!: eventually_mono) |
2097 qed |
2298 qed |
2098 |
2299 |
|
2300 subsection \<open>Homeomorphisms\<close> |
|
2301 |
|
2302 definition%important "homeomorphism s t f g \<longleftrightarrow> |
|
2303 (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and> |
|
2304 (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g" |
|
2305 |
|
2306 lemma homeomorphismI [intro?]: |
|
2307 assumes "continuous_on S f" "continuous_on T g" |
|
2308 "f ` S \<subseteq> T" "g ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y" |
|
2309 shows "homeomorphism S T f g" |
|
2310 using assms by (force simp: homeomorphism_def) |
|
2311 |
|
2312 lemma homeomorphism_translation: |
|
2313 fixes a :: "'a :: real_normed_vector" |
|
2314 shows "homeomorphism ((+) a ` S) S ((+) (- a)) ((+) a)" |
|
2315 unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros) |
|
2316 |
|
2317 lemma homeomorphism_ident: "homeomorphism T T (\<lambda>a. a) (\<lambda>a. a)" |
|
2318 by (rule homeomorphismI) (auto simp: continuous_on_id) |
|
2319 |
|
2320 lemma homeomorphism_compose: |
|
2321 assumes "homeomorphism S T f g" "homeomorphism T U h k" |
|
2322 shows "homeomorphism S U (h o f) (g o k)" |
|
2323 using assms |
|
2324 unfolding homeomorphism_def |
|
2325 by (intro conjI ballI continuous_on_compose) (auto simp: image_comp [symmetric]) |
|
2326 |
|
2327 lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f" |
|
2328 by (simp add: homeomorphism_def) |
|
2329 |
|
2330 lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f" |
|
2331 by (force simp: homeomorphism_def) |
|
2332 |
|
2333 definition%important homeomorphic :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool" |
|
2334 (infixr "homeomorphic" 60) |
|
2335 where "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)" |
|
2336 |
|
2337 lemma homeomorphic_empty [iff]: |
|
2338 "S homeomorphic {} \<longleftrightarrow> S = {}" "{} homeomorphic S \<longleftrightarrow> S = {}" |
|
2339 by (auto simp: homeomorphic_def homeomorphism_def) |
|
2340 |
|
2341 lemma homeomorphic_refl: "s homeomorphic s" |
|
2342 unfolding homeomorphic_def homeomorphism_def |
|
2343 using continuous_on_id |
|
2344 apply (rule_tac x = "(\<lambda>x. x)" in exI) |
|
2345 apply (rule_tac x = "(\<lambda>x. x)" in exI) |
|
2346 apply blast |
|
2347 done |
|
2348 |
|
2349 lemma homeomorphic_sym: "s homeomorphic t \<longleftrightarrow> t homeomorphic s" |
|
2350 unfolding homeomorphic_def homeomorphism_def |
|
2351 by blast |
|
2352 |
|
2353 lemma homeomorphic_trans [trans]: |
|
2354 assumes "S homeomorphic T" |
|
2355 and "T homeomorphic U" |
|
2356 shows "S homeomorphic U" |
|
2357 using assms |
|
2358 unfolding homeomorphic_def |
|
2359 by (metis homeomorphism_compose) |
|
2360 |
|
2361 lemma homeomorphic_minimal: |
|
2362 "s homeomorphic t \<longleftrightarrow> |
|
2363 (\<exists>f g. (\<forall>x\<in>s. f(x) \<in> t \<and> (g(f(x)) = x)) \<and> |
|
2364 (\<forall>y\<in>t. g(y) \<in> s \<and> (f(g(y)) = y)) \<and> |
|
2365 continuous_on s f \<and> continuous_on t g)" |
|
2366 (is "?lhs = ?rhs") |
|
2367 proof |
|
2368 assume ?lhs |
|
2369 then show ?rhs |
|
2370 by (fastforce simp: homeomorphic_def homeomorphism_def) |
|
2371 next |
|
2372 assume ?rhs |
|
2373 then show ?lhs |
|
2374 apply clarify |
|
2375 unfolding homeomorphic_def homeomorphism_def |
|
2376 by (metis equalityI image_subset_iff subsetI) |
|
2377 qed |
|
2378 |
|
2379 lemma homeomorphicI [intro?]: |
|
2380 "\<lbrakk>f ` S = T; g ` T = S; |
|
2381 continuous_on S f; continuous_on T g; |
|
2382 \<And>x. x \<in> S \<Longrightarrow> g(f(x)) = x; |
|
2383 \<And>y. y \<in> T \<Longrightarrow> f(g(y)) = y\<rbrakk> \<Longrightarrow> S homeomorphic T" |
|
2384 unfolding homeomorphic_def homeomorphism_def by metis |
|
2385 |
|
2386 lemma homeomorphism_of_subsets: |
|
2387 "\<lbrakk>homeomorphism S T f g; S' \<subseteq> S; T'' \<subseteq> T; f ` S' = T'\<rbrakk> |
|
2388 \<Longrightarrow> homeomorphism S' T' f g" |
|
2389 apply (auto simp: homeomorphism_def elim!: continuous_on_subset) |
|
2390 by (metis subsetD imageI) |
|
2391 |
|
2392 lemma homeomorphism_apply1: "\<lbrakk>homeomorphism S T f g; x \<in> S\<rbrakk> \<Longrightarrow> g(f x) = x" |
|
2393 by (simp add: homeomorphism_def) |
|
2394 |
|
2395 lemma homeomorphism_apply2: "\<lbrakk>homeomorphism S T f g; x \<in> T\<rbrakk> \<Longrightarrow> f(g x) = x" |
|
2396 by (simp add: homeomorphism_def) |
|
2397 |
|
2398 lemma homeomorphism_image1: "homeomorphism S T f g \<Longrightarrow> f ` S = T" |
|
2399 by (simp add: homeomorphism_def) |
|
2400 |
|
2401 lemma homeomorphism_image2: "homeomorphism S T f g \<Longrightarrow> g ` T = S" |
|
2402 by (simp add: homeomorphism_def) |
|
2403 |
|
2404 lemma homeomorphism_cont1: "homeomorphism S T f g \<Longrightarrow> continuous_on S f" |
|
2405 by (simp add: homeomorphism_def) |
|
2406 |
|
2407 lemma homeomorphism_cont2: "homeomorphism S T f g \<Longrightarrow> continuous_on T g" |
|
2408 by (simp add: homeomorphism_def) |
|
2409 |
|
2410 lemma continuous_on_no_limpt: |
|
2411 "(\<And>x. \<not> x islimpt S) \<Longrightarrow> continuous_on S f" |
|
2412 unfolding continuous_on_def |
|
2413 by (metis UNIV_I empty_iff eventually_at_topological islimptE open_UNIV tendsto_def trivial_limit_within) |
|
2414 |
|
2415 lemma continuous_on_finite: |
|
2416 fixes S :: "'a::t1_space set" |
|
2417 shows "finite S \<Longrightarrow> continuous_on S f" |
|
2418 by (metis continuous_on_no_limpt islimpt_finite) |
|
2419 |
|
2420 lemma homeomorphic_finite: |
|
2421 fixes S :: "'a::t1_space set" and T :: "'b::t1_space set" |
|
2422 assumes "finite T" |
|
2423 shows "S homeomorphic T \<longleftrightarrow> finite S \<and> finite T \<and> card S = card T" (is "?lhs = ?rhs") |
|
2424 proof |
|
2425 assume "S homeomorphic T" |
|
2426 with assms show ?rhs |
|
2427 apply (auto simp: homeomorphic_def homeomorphism_def) |
|
2428 apply (metis finite_imageI) |
|
2429 by (metis card_image_le finite_imageI le_antisym) |
|
2430 next |
|
2431 assume R: ?rhs |
|
2432 with finite_same_card_bij obtain h where "bij_betw h S T" |
|
2433 by auto |
|
2434 with R show ?lhs |
|
2435 apply (auto simp: homeomorphic_def homeomorphism_def continuous_on_finite) |
|
2436 apply (rule_tac x=h in exI) |
|
2437 apply (rule_tac x="inv_into S h" in exI) |
|
2438 apply (auto simp: bij_betw_inv_into_left bij_betw_inv_into_right bij_betw_imp_surj_on inv_into_into bij_betwE) |
|
2439 apply (metis bij_betw_def bij_betw_inv_into) |
|
2440 done |
|
2441 qed |
|
2442 |
|
2443 text \<open>Relatively weak hypotheses if a set is compact.\<close> |
|
2444 |
|
2445 lemma homeomorphism_compact: |
|
2446 fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space" |
|
2447 assumes "compact s" "continuous_on s f" "f ` s = t" "inj_on f s" |
|
2448 shows "\<exists>g. homeomorphism s t f g" |
|
2449 proof - |
|
2450 define g where "g x = (SOME y. y\<in>s \<and> f y = x)" for x |
|
2451 have g: "\<forall>x\<in>s. g (f x) = x" |
|
2452 using assms(3) assms(4)[unfolded inj_on_def] unfolding g_def by auto |
|
2453 { |
|
2454 fix y |
|
2455 assume "y \<in> t" |
|
2456 then obtain x where x:"f x = y" "x\<in>s" |
|
2457 using assms(3) by auto |
|
2458 then have "g (f x) = x" using g by auto |
|
2459 then have "f (g y) = y" unfolding x(1)[symmetric] by auto |
|
2460 } |
|
2461 then have g':"\<forall>x\<in>t. f (g x) = x" by auto |
|
2462 moreover |
|
2463 { |
|
2464 fix x |
|
2465 have "x\<in>s \<Longrightarrow> x \<in> g ` t" |
|
2466 using g[THEN bspec[where x=x]] |
|
2467 unfolding image_iff |
|
2468 using assms(3) |
|
2469 by (auto intro!: bexI[where x="f x"]) |
|
2470 moreover |
|
2471 { |
|
2472 assume "x\<in>g ` t" |
|
2473 then obtain y where y:"y\<in>t" "g y = x" by auto |
|
2474 then obtain x' where x':"x'\<in>s" "f x' = y" |
|
2475 using assms(3) by auto |
|
2476 then have "x \<in> s" |
|
2477 unfolding g_def |
|
2478 using someI2[of "\<lambda>b. b\<in>s \<and> f b = y" x' "\<lambda>x. x\<in>s"] |
|
2479 unfolding y(2)[symmetric] and g_def |
|
2480 by auto |
|
2481 } |
|
2482 ultimately have "x\<in>s \<longleftrightarrow> x \<in> g ` t" .. |
|
2483 } |
|
2484 then have "g ` t = s" by auto |
|
2485 ultimately show ?thesis |
|
2486 unfolding homeomorphism_def homeomorphic_def |
|
2487 apply (rule_tac x=g in exI) |
|
2488 using g and assms(3) and continuous_on_inv[OF assms(2,1), of g, unfolded assms(3)] and assms(2) |
|
2489 apply auto |
|
2490 done |
|
2491 qed |
|
2492 |
|
2493 lemma homeomorphic_compact: |
|
2494 fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space" |
|
2495 shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s \<Longrightarrow> s homeomorphic t" |
|
2496 unfolding homeomorphic_def by (metis homeomorphism_compact) |
|
2497 |
|
2498 text\<open>Preservation of topological properties.\<close> |
|
2499 |
|
2500 lemma homeomorphic_compactness: "s homeomorphic t \<Longrightarrow> (compact s \<longleftrightarrow> compact t)" |
|
2501 unfolding homeomorphic_def homeomorphism_def |
|
2502 by (metis compact_continuous_image) |
|
2503 |
|
2504 |
|
2505 subsection%unimportant \<open>On Linorder Topologies\<close> |
|
2506 |
|
2507 lemma islimpt_greaterThanLessThan1: |
|
2508 fixes a b::"'a::{linorder_topology, dense_order}" |
|
2509 assumes "a < b" |
|
2510 shows "a islimpt {a<..<b}" |
|
2511 proof (rule islimptI) |
|
2512 fix T |
|
2513 assume "open T" "a \<in> T" |
|
2514 from open_right[OF this \<open>a < b\<close>] |
|
2515 obtain c where c: "a < c" "{a..<c} \<subseteq> T" by auto |
|
2516 with assms dense[of a "min c b"] |
|
2517 show "\<exists>y\<in>{a<..<b}. y \<in> T \<and> y \<noteq> a" |
|
2518 by (metis atLeastLessThan_iff greaterThanLessThan_iff min_less_iff_conj |
|
2519 not_le order.strict_implies_order subset_eq) |
|
2520 qed |
|
2521 |
|
2522 lemma islimpt_greaterThanLessThan2: |
|
2523 fixes a b::"'a::{linorder_topology, dense_order}" |
|
2524 assumes "a < b" |
|
2525 shows "b islimpt {a<..<b}" |
|
2526 proof (rule islimptI) |
|
2527 fix T |
|
2528 assume "open T" "b \<in> T" |
|
2529 from open_left[OF this \<open>a < b\<close>] |
|
2530 obtain c where c: "c < b" "{c<..b} \<subseteq> T" by auto |
|
2531 with assms dense[of "max a c" b] |
|
2532 show "\<exists>y\<in>{a<..<b}. y \<in> T \<and> y \<noteq> b" |
|
2533 by (metis greaterThanAtMost_iff greaterThanLessThan_iff max_less_iff_conj |
|
2534 not_le order.strict_implies_order subset_eq) |
|
2535 qed |
|
2536 |
|
2537 lemma closure_greaterThanLessThan[simp]: |
|
2538 fixes a b::"'a::{linorder_topology, dense_order}" |
|
2539 shows "a < b \<Longrightarrow> closure {a <..< b} = {a .. b}" (is "_ \<Longrightarrow> ?l = ?r") |
|
2540 proof |
|
2541 have "?l \<subseteq> closure ?r" |
|
2542 by (rule closure_mono) auto |
|
2543 thus "closure {a<..<b} \<subseteq> {a..b}" by simp |
|
2544 qed (auto simp: closure_def order.order_iff_strict islimpt_greaterThanLessThan1 |
|
2545 islimpt_greaterThanLessThan2) |
|
2546 |
|
2547 lemma closure_greaterThan[simp]: |
|
2548 fixes a b::"'a::{no_top, linorder_topology, dense_order}" |
|
2549 shows "closure {a<..} = {a..}" |
|
2550 proof - |
|
2551 from gt_ex obtain b where "a < b" by auto |
|
2552 hence "{a<..} = {a<..<b} \<union> {b..}" by auto |
|
2553 also have "closure \<dots> = {a..}" using \<open>a < b\<close> unfolding closure_Un |
|
2554 by auto |
|
2555 finally show ?thesis . |
|
2556 qed |
|
2557 |
|
2558 lemma closure_lessThan[simp]: |
|
2559 fixes b::"'a::{no_bot, linorder_topology, dense_order}" |
|
2560 shows "closure {..<b} = {..b}" |
|
2561 proof - |
|
2562 from lt_ex obtain a where "a < b" by auto |
|
2563 hence "{..<b} = {a<..<b} \<union> {..a}" by auto |
|
2564 also have "closure \<dots> = {..b}" using \<open>a < b\<close> unfolding closure_Un |
|
2565 by auto |
|
2566 finally show ?thesis . |
|
2567 qed |
|
2568 |
|
2569 lemma closure_atLeastLessThan[simp]: |
|
2570 fixes a b::"'a::{linorder_topology, dense_order}" |
|
2571 assumes "a < b" |
|
2572 shows "closure {a ..< b} = {a .. b}" |
|
2573 proof - |
|
2574 from assms have "{a ..< b} = {a} \<union> {a <..< b}" by auto |
|
2575 also have "closure \<dots> = {a .. b}" unfolding closure_Un |
|
2576 by (auto simp: assms less_imp_le) |
|
2577 finally show ?thesis . |
|
2578 qed |
|
2579 |
|
2580 lemma closure_greaterThanAtMost[simp]: |
|
2581 fixes a b::"'a::{linorder_topology, dense_order}" |
|
2582 assumes "a < b" |
|
2583 shows "closure {a <.. b} = {a .. b}" |
|
2584 proof - |
|
2585 from assms have "{a <.. b} = {b} \<union> {a <..< b}" by auto |
|
2586 also have "closure \<dots> = {a .. b}" unfolding closure_Un |
|
2587 by (auto simp: assms less_imp_le) |
|
2588 finally show ?thesis . |
|
2589 qed |
|
2590 |
2099 |
2591 |
2100 end |
2592 end |