2323 qed |
2323 qed |
2324 |
2324 |
2325 lemma Inf_insert: |
2325 lemma Inf_insert: |
2326 fixes S :: "real set" |
2326 fixes S :: "real set" |
2327 shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" |
2327 shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" |
2328 by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal) |
2328 by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal) |
|
2329 |
2329 lemma Inf_insert_finite: |
2330 lemma Inf_insert_finite: |
2330 fixes S :: "real set" |
2331 fixes S :: "real set" |
2331 shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" |
2332 shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" |
2332 by (rule Inf_insert, rule finite_imp_bounded, simp) |
2333 by (rule Inf_insert, rule finite_imp_bounded, simp) |
2333 |
2334 |
2346 |
2347 |
2347 lemma compactE: |
2348 lemma compactE: |
2348 assumes "compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C" |
2349 assumes "compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C" |
2349 obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'" |
2350 obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'" |
2350 using assms unfolding compact_eq_heine_borel by metis |
2351 using assms unfolding compact_eq_heine_borel by metis |
|
2352 |
|
2353 lemma compactE_image: |
|
2354 assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)" |
|
2355 obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)" |
|
2356 using assms unfolding ball_simps[symmetric] SUP_def |
|
2357 by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s]) |
2351 |
2358 |
2352 subsubsection {* Bolzano-Weierstrass property *} |
2359 subsubsection {* Bolzano-Weierstrass property *} |
2353 |
2360 |
2354 lemma heine_borel_imp_bolzano_weierstrass: |
2361 lemma heine_borel_imp_bolzano_weierstrass: |
2355 assumes "compact s" "infinite t" "t \<subseteq> s" |
2362 assumes "compact s" "infinite t" "t \<subseteq> s" |
2568 by (simp add: eventually_Ball_finite) |
2575 by (simp add: eventually_Ball_finite) |
2569 with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)" |
2576 with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)" |
2570 by (auto elim!: eventually_mono [rotated]) |
2577 by (auto elim!: eventually_mono [rotated]) |
2571 thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s" |
2578 thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s" |
2572 by (simp add: eventually_nhds subset_eq) |
2579 by (simp add: eventually_nhds subset_eq) |
|
2580 qed |
|
2581 |
|
2582 lemma compact_imp_bounded: |
|
2583 assumes "compact U" shows "bounded U" |
|
2584 proof - |
|
2585 have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)" using assms by auto |
|
2586 then obtain D where D: "D \<subseteq> U" "finite D" "U \<subseteq> (\<Union>x\<in>D. ball x 1)" |
|
2587 by (elim compactE_image) |
|
2588 def d \<equiv> "SOME d. d \<in> D" |
|
2589 show "bounded U" |
|
2590 unfolding bounded_def |
|
2591 proof (intro exI, safe) |
|
2592 fix x assume "x \<in> U" |
|
2593 with D obtain d' where "d' \<in> D" "x \<in> ball d' 1" by auto |
|
2594 moreover have "dist d x \<le> dist d d' + dist d' x" |
|
2595 using dist_triangle[of d x d'] by (simp add: dist_commute) |
|
2596 moreover |
|
2597 from `x\<in>U` D have "d \<in> D" |
|
2598 unfolding d_def by (rule_tac someI_ex) auto |
|
2599 ultimately |
|
2600 show "dist d x \<le> Max ((\<lambda>d'. dist d d' + 1) ` D)" |
|
2601 using D by (subst Max_ge_iff) (auto intro!: bexI[of _ d']) |
|
2602 qed |
2573 qed |
2603 qed |
2574 |
2604 |
2575 text{* In particular, some common special cases. *} |
2605 text{* In particular, some common special cases. *} |
2576 |
2606 |
2577 lemma compact_empty[simp]: |
2607 lemma compact_empty[simp]: |
3103 using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto |
3133 using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto |
3104 qed |
3134 qed |
3105 |
3135 |
3106 subsubsection{* Heine-Borel theorem *} |
3136 subsubsection{* Heine-Borel theorem *} |
3107 |
3137 |
3108 text {* Following Burkill \& Burkill vol. 2. *} |
|
3109 |
|
3110 lemma seq_compact_imp_heine_borel: |
3138 lemma seq_compact_imp_heine_borel: |
3111 fixes s :: "'a :: metric_space set" |
3139 fixes s :: "'a :: metric_space set" |
3112 assumes "seq_compact s" shows "compact s" |
3140 assumes "seq_compact s" shows "compact s" |
3113 proof - |
3141 proof - |
3114 from seq_compact_imp_totally_bounded[OF `seq_compact s`] |
3142 from seq_compact_imp_totally_bounded[OF `seq_compact s`] |
3148 lemma compact_def: |
3176 lemma compact_def: |
3149 "compact (S :: 'a::metric_space set) \<longleftrightarrow> |
3177 "compact (S :: 'a::metric_space set) \<longleftrightarrow> |
3150 (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f o r) ----> l))" |
3178 (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f o r) ----> l))" |
3151 unfolding compact_eq_seq_compact_metric seq_compact_def by auto |
3179 unfolding compact_eq_seq_compact_metric seq_compact_def by auto |
3152 |
3180 |
|
3181 subsubsection {* Complete the chain of compactness variants *} |
|
3182 |
|
3183 lemma compact_eq_bolzano_weierstrass: |
|
3184 fixes s :: "'a::metric_space set" |
|
3185 shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs") |
|
3186 proof |
|
3187 assume ?lhs thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto |
|
3188 next |
|
3189 assume ?rhs thus ?lhs |
|
3190 unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact) |
|
3191 qed |
|
3192 |
|
3193 lemma bolzano_weierstrass_imp_bounded: |
|
3194 "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s" |
|
3195 using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass . |
|
3196 |
3153 text {* |
3197 text {* |
3154 A metric space (or topological vector space) is said to have the |
3198 A metric space (or topological vector space) is said to have the |
3155 Heine-Borel property if every closed and bounded subset is compact. |
3199 Heine-Borel property if every closed and bounded subset is compact. |
3156 *} |
3200 *} |
3157 |
3201 |
3170 from f have fr: "\<forall>n. (f \<circ> r) n \<in> s" by simp |
3214 from f have fr: "\<forall>n. (f \<circ> r) n \<in> s" by simp |
3171 have "l \<in> s" using `closed s` fr l |
3215 have "l \<in> s" using `closed s` fr l |
3172 unfolding closed_sequential_limits by blast |
3216 unfolding closed_sequential_limits by blast |
3173 show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" |
3217 show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" |
3174 using `l \<in> s` r l by blast |
3218 using `l \<in> s` r l by blast |
|
3219 qed |
|
3220 |
|
3221 lemma compact_eq_bounded_closed: |
|
3222 fixes s :: "'a::heine_borel set" |
|
3223 shows "compact s \<longleftrightarrow> bounded s \<and> closed s" (is "?lhs = ?rhs") |
|
3224 proof |
|
3225 assume ?lhs thus ?rhs |
|
3226 using compact_imp_closed compact_imp_bounded by blast |
|
3227 next |
|
3228 assume ?rhs thus ?lhs |
|
3229 using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto |
3175 qed |
3230 qed |
3176 |
3231 |
3177 lemma lim_subseq: |
3232 lemma lim_subseq: |
3178 "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially" |
3233 "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially" |
3179 unfolding tendsto_def eventually_sequentially o_def |
3234 unfolding tendsto_def eventually_sequentially o_def |
3495 |
3550 |
3496 lemma convergent_imp_bounded: |
3551 lemma convergent_imp_bounded: |
3497 fixes s :: "nat \<Rightarrow> 'a::metric_space" |
3552 fixes s :: "nat \<Rightarrow> 'a::metric_space" |
3498 shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)" |
3553 shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)" |
3499 by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy) |
3554 by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy) |
3500 |
|
3501 subsubsection {* Complete the chain of compactness variants *} |
|
3502 |
|
3503 primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where |
|
3504 "helper_2 beyond 0 = beyond 0" | |
|
3505 "helper_2 beyond (Suc n) = beyond (dist undefined (helper_2 beyond n) + 1 )" |
|
3506 |
|
3507 lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::metric_space set" |
|
3508 assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)" |
|
3509 shows "bounded s" |
|
3510 proof(rule ccontr) |
|
3511 assume "\<not> bounded s" |
|
3512 then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> dist undefined (beyond a) \<le> a" |
|
3513 unfolding bounded_any_center [where a=undefined] |
|
3514 apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> dist undefined x \<le> a"] by auto |
|
3515 hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. dist undefined (beyond a) > a" |
|
3516 unfolding linorder_not_le by auto |
|
3517 def x \<equiv> "helper_2 beyond" |
|
3518 |
|
3519 { fix m n ::nat assume "m<n" |
|
3520 hence "dist undefined (x m) + 1 < dist undefined (x n)" |
|
3521 proof(induct n) |
|
3522 case 0 thus ?case by auto |
|
3523 next |
|
3524 case (Suc n) |
|
3525 have *:"dist undefined (x n) + 1 < dist undefined (x (Suc n))" |
|
3526 unfolding x_def and helper_2.simps |
|
3527 using beyond(2)[of "dist undefined (helper_2 beyond n) + 1"] by auto |
|
3528 thus ?case proof(cases "m < n") |
|
3529 case True thus ?thesis using Suc and * by auto |
|
3530 next |
|
3531 case False hence "m = n" using Suc(2) by auto |
|
3532 thus ?thesis using * by auto |
|
3533 qed |
|
3534 qed } note * = this |
|
3535 { fix m n ::nat assume "m\<noteq>n" |
|
3536 have "1 < dist (x m) (x n)" |
|
3537 proof(cases "m<n") |
|
3538 case True |
|
3539 hence "1 < dist undefined (x n) - dist undefined (x m)" using *[of m n] by auto |
|
3540 thus ?thesis using dist_triangle [of undefined "x n" "x m"] by arith |
|
3541 next |
|
3542 case False hence "n<m" using `m\<noteq>n` by auto |
|
3543 hence "1 < dist undefined (x m) - dist undefined (x n)" using *[of n m] by auto |
|
3544 thus ?thesis using dist_triangle2 [of undefined "x m" "x n"] by arith |
|
3545 qed } note ** = this |
|
3546 { fix a b assume "x a = x b" "a \<noteq> b" |
|
3547 hence False using **[of a b] by auto } |
|
3548 hence "inj x" unfolding inj_on_def by auto |
|
3549 moreover |
|
3550 { fix n::nat |
|
3551 have "x n \<in> s" |
|
3552 proof(cases "n = 0") |
|
3553 case True thus ?thesis unfolding x_def using beyond by auto |
|
3554 next |
|
3555 case False then obtain z where "n = Suc z" using not0_implies_Suc by auto |
|
3556 thus ?thesis unfolding x_def using beyond by auto |
|
3557 qed } |
|
3558 ultimately have "infinite (range x) \<and> range x \<subseteq> s" unfolding x_def using range_inj_infinite[of "helper_2 beyond"] using beyond(1) by auto |
|
3559 |
|
3560 then obtain l where "l\<in>s" and l:"l islimpt range x" using assms[THEN spec[where x="range x"]] by auto |
|
3561 then obtain y where "x y \<noteq> l" and y:"dist (x y) l < 1/2" unfolding islimpt_approachable apply(erule_tac x="1/2" in allE) by auto |
|
3562 then obtain z where "x z \<noteq> l" and z:"dist (x z) l < dist (x y) l" using l[unfolded islimpt_approachable, THEN spec[where x="dist (x y) l"]] |
|
3563 unfolding dist_nz by auto |
|
3564 show False using y and z and dist_triangle_half_l[of "x y" l 1 "x z"] and **[of y z] by auto |
|
3565 qed |
|
3566 |
|
3567 text {* Hence express everything as an equivalence. *} |
|
3568 |
|
3569 lemma compact_eq_bolzano_weierstrass: |
|
3570 fixes s :: "'a::metric_space set" |
|
3571 shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs") |
|
3572 proof |
|
3573 assume ?lhs thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto |
|
3574 next |
|
3575 assume ?rhs thus ?lhs |
|
3576 unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact) |
|
3577 qed |
|
3578 |
3555 |
3579 lemma nat_approx_posE: |
3556 lemma nat_approx_posE: |
3580 fixes e::real |
3557 fixes e::real |
3581 assumes "0 < e" |
3558 assumes "0 < e" |
3582 obtains n::nat where "1 / (Suc n) < e" |
3559 obtains n::nat where "1 / (Suc n) < e" |
3722 thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l" using subseq_diagseq by auto |
3699 thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l" using subseq_diagseq by auto |
3723 qed |
3700 qed |
3724 qed |
3701 qed |
3725 qed |
3702 qed |
3726 |
3703 |
3727 lemma compact_eq_bounded_closed: |
|
3728 fixes s :: "'a::heine_borel set" |
|
3729 shows "compact s \<longleftrightarrow> bounded s \<and> closed s" (is "?lhs = ?rhs") |
|
3730 proof |
|
3731 assume ?lhs thus ?rhs |
|
3732 unfolding compact_eq_bolzano_weierstrass using bolzano_weierstrass_imp_bounded bolzano_weierstrass_imp_closed by auto |
|
3733 next |
|
3734 assume ?rhs thus ?lhs |
|
3735 using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto |
|
3736 qed |
|
3737 |
|
3738 lemma compact_imp_bounded: |
|
3739 fixes s :: "'a::metric_space set" |
|
3740 shows "compact s \<Longrightarrow> bounded s" |
|
3741 proof - |
|
3742 assume "compact s" |
|
3743 hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t)" |
|
3744 using heine_borel_imp_bolzano_weierstrass[of s] by auto |
|
3745 thus "bounded s" |
|
3746 by (rule bolzano_weierstrass_imp_bounded) |
|
3747 qed |
|
3748 |
|
3749 lemma compact_cball[simp]: |
3704 lemma compact_cball[simp]: |
3750 fixes x :: "'a::heine_borel" |
3705 fixes x :: "'a::heine_borel" |
3751 shows "compact(cball x e)" |
3706 shows "compact(cball x e)" |
3752 using compact_eq_bounded_closed bounded_cball closed_cball |
3707 using compact_eq_bounded_closed bounded_cball closed_cball |
3753 by blast |
3708 by blast |
4936 shows "uniformly_continuous_on s f" |
4891 shows "uniformly_continuous_on s f" |
4937 unfolding uniformly_continuous_on_def |
4892 unfolding uniformly_continuous_on_def |
4938 proof (cases, safe) |
4893 proof (cases, safe) |
4939 fix e :: real assume "0 < e" "s \<noteq> {}" |
4894 fix e :: real assume "0 < e" "s \<noteq> {}" |
4940 def [simp]: R \<equiv> "{(y, d). y \<in> s \<and> 0 < d \<and> ball y d \<inter> s \<subseteq> {x \<in> s. f x \<in> ball (f y) (e/2) } }" |
4895 def [simp]: R \<equiv> "{(y, d). y \<in> s \<and> 0 < d \<and> ball y d \<inter> s \<subseteq> {x \<in> s. f x \<in> ball (f y) (e/2) } }" |
4941 let ?C = "(\<lambda>(y, d). ball y (d/2)) ` R" |
4896 let ?b = "(\<lambda>(y, d). ball y (d/2))" |
4942 have "(\<forall>r\<in>?C. open r) \<and> s \<subseteq> \<Union>?C" |
4897 have "(\<forall>r\<in>R. open (?b r))" "s \<subseteq> (\<Union>r\<in>R. ?b r)" |
4943 proof safe |
4898 proof safe |
4944 fix y assume "y \<in> s" |
4899 fix y assume "y \<in> s" |
4945 from continuous_open_in_preimage[OF f open_ball] |
4900 from continuous_open_in_preimage[OF f open_ball] |
4946 obtain T where "open T" and T: "{x \<in> s. f x \<in> ball (f y) (e/2)} = T \<inter> s" |
4901 obtain T where "open T" and T: "{x \<in> s. f x \<in> ball (f y) (e/2)} = T \<inter> s" |
4947 unfolding openin_subtopology open_openin by metis |
4902 unfolding openin_subtopology open_openin by metis |
4948 then obtain d where "ball y d \<subseteq> T" "0 < d" |
4903 then obtain d where "ball y d \<subseteq> T" "0 < d" |
4949 using `0 < e` `y \<in> s` by (auto elim!: openE) |
4904 using `0 < e` `y \<in> s` by (auto elim!: openE) |
4950 with T `y \<in> s` show "y \<in> \<Union>(\<lambda>(y, d). ball y (d/2)) ` R" |
4905 with T `y \<in> s` show "y \<in> (\<Union>r\<in>R. ?b r)" |
4951 by (intro UnionI[where X="ball y (d/2)"]) auto |
4906 by (intro UN_I[of "(y, d)"]) auto |
4952 qed auto |
4907 qed auto |
4953 then obtain D where D: "finite D" "D \<subseteq> R" "s \<subseteq> (\<Union>(y, d)\<in>D. ball y (d/2))" |
4908 with s obtain D where D: "finite D" "D \<subseteq> R" "s \<subseteq> (\<Union>(y, d)\<in>D. ball y (d/2))" |
4954 by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s] s Union_image_eq) |
4909 by (rule compactE_image) |
4955 with `s \<noteq> {}` have [simp]: "\<And>x. x < Min (snd ` D) \<longleftrightarrow> (\<forall>(y, d)\<in>D. x < d)" |
4910 with `s \<noteq> {}` have [simp]: "\<And>x. x < Min (snd ` D) \<longleftrightarrow> (\<forall>(y, d)\<in>D. x < d)" |
4956 by (subst Min_gr_iff) auto |
4911 by (subst Min_gr_iff) auto |
4957 show "\<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" |
4912 show "\<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" |
4958 proof (rule, safe) |
4913 proof (rule, safe) |
4959 fix x x' assume in_s: "x' \<in> s" "x \<in> s" |
4914 fix x x' assume in_s: "x' \<in> s" "x \<in> s" |