129 subsection \<open>Topological Basis\<close> |
129 subsection \<open>Topological Basis\<close> |
130 |
130 |
131 context topological_space |
131 context topological_space |
132 begin |
132 begin |
133 |
133 |
134 definition "topological_basis B \<longleftrightarrow> |
134 definition%important "topological_basis B \<longleftrightarrow> |
135 (\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" |
135 (\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" |
136 |
136 |
137 lemma topological_basis: |
137 lemma topological_basis: |
138 "topological_basis B \<longleftrightarrow> (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" |
138 "topological_basis B \<longleftrightarrow> (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))" |
139 unfolding topological_basis_def |
139 unfolding topological_basis_def |
576 then show ?thesis using \<open>b \<in> B\<close> by auto |
576 then show ?thesis using \<open>b \<in> B\<close> by auto |
577 qed |
577 qed |
578 then show ?thesis using B(1) by auto |
578 then show ?thesis using B(1) by auto |
579 qed |
579 qed |
580 |
580 |
581 subsection \<open>Polish spaces\<close> |
581 subsection%important \<open>Polish spaces\<close> |
582 |
582 |
583 text \<open>Textbooks define Polish spaces as completely metrizable. |
583 text \<open>Textbooks define Polish spaces as completely metrizable. |
584 We assume the topology to be complete for a given metric.\<close> |
584 We assume the topology to be complete for a given metric.\<close> |
585 |
585 |
586 class polish_space = complete_space + second_countable_topology |
586 class%important polish_space = complete_space + second_countable_topology |
587 |
587 |
588 subsection \<open>General notion of a topology as a value\<close> |
588 subsection \<open>General notion of a topology as a value\<close> |
589 |
589 |
590 definition "istopology L \<longleftrightarrow> |
590 definition%important "istopology L \<longleftrightarrow> |
591 L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))" |
591 L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))" |
592 |
592 |
593 typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}" |
593 typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}" |
594 morphisms "openin" "topology" |
594 morphisms "openin" "topology" |
595 unfolding istopology_def by blast |
595 unfolding istopology_def by blast |
596 |
596 |
597 lemma istopology_openin[intro]: "istopology(openin U)" |
597 lemma istopology_openin[intro]: "istopology(openin U)" |
598 using openin[of U] by blast |
598 using openin[of U] by blast |
618 |
618 |
619 definition "topspace T = \<Union>{S. openin T S}" |
619 definition "topspace T = \<Union>{S. openin T S}" |
620 |
620 |
621 subsubsection \<open>Main properties of open sets\<close> |
621 subsubsection \<open>Main properties of open sets\<close> |
622 |
622 |
623 lemma openin_clauses: |
623 lemma%important openin_clauses: |
624 fixes U :: "'a topology" |
624 fixes U :: "'a topology" |
625 shows |
625 shows |
626 "openin U {}" |
626 "openin U {}" |
627 "\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)" |
627 "\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)" |
628 "\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)" |
628 "\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)" |
681 by (metis (full_types) assms openin_INT2 image_ident) |
681 by (metis (full_types) assms openin_INT2 image_ident) |
682 |
682 |
683 |
683 |
684 subsubsection \<open>Closed sets\<close> |
684 subsubsection \<open>Closed sets\<close> |
685 |
685 |
686 definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)" |
686 definition%important "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)" |
687 |
687 |
688 lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" |
688 lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" |
689 by (metis closedin_def) |
689 by (metis closedin_def) |
690 |
690 |
691 lemma closedin_empty[simp]: "closedin U {}" |
691 lemma closedin_empty[simp]: "closedin U {}" |
868 by (simp add: closedin_subtopology) blast |
868 by (simp add: closedin_subtopology) blast |
869 |
869 |
870 |
870 |
871 subsubsection \<open>The standard Euclidean topology\<close> |
871 subsubsection \<open>The standard Euclidean topology\<close> |
872 |
872 |
873 definition euclidean :: "'a::topological_space topology" |
873 definition%important euclidean :: "'a::topological_space topology" |
874 where "euclidean = topology open" |
874 where "euclidean = topology open" |
875 |
875 |
876 lemma open_openin: "open S \<longleftrightarrow> openin euclidean S" |
876 lemma open_openin: "open S \<longleftrightarrow> openin euclidean S" |
877 unfolding euclidean_def |
877 unfolding euclidean_def |
878 apply (rule cong[where x=S and y=S]) |
878 apply (rule cong[where x=S and y=S]) |
1052 using open_subset openin_open_trans openin_subset by fastforce |
1052 using open_subset openin_open_trans openin_subset by fastforce |
1053 |
1053 |
1054 |
1054 |
1055 subsection \<open>Open and closed balls\<close> |
1055 subsection \<open>Open and closed balls\<close> |
1056 |
1056 |
1057 definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" |
1057 definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" |
1058 where "ball x e = {y. dist x y < e}" |
1058 where "ball x e = {y. dist x y < e}" |
1059 |
1059 |
1060 definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" |
1060 definition%important cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" |
1061 where "cball x e = {y. dist x y \<le> e}" |
1061 where "cball x e = {y. dist x y \<le> e}" |
1062 |
1062 |
1063 definition sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" |
1063 definition%important sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" |
1064 where "sphere x e = {y. dist x y = e}" |
1064 where "sphere x e = {y. dist x y = e}" |
1065 |
1065 |
1066 lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" |
1066 lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" |
1067 by (simp add: ball_def) |
1067 by (simp add: ball_def) |
1068 |
1068 |
1325 by (metis One_non_0) |
1325 by (metis One_non_0) |
1326 |
1326 |
1327 corollary Zero_neq_One[iff]: "0 \<noteq> One" |
1327 corollary Zero_neq_One[iff]: "0 \<noteq> One" |
1328 by (metis One_non_0) |
1328 by (metis One_non_0) |
1329 |
1329 |
1330 definition (in euclidean_space) eucl_less (infix "<e" 50) |
1330 definition%important (in euclidean_space) eucl_less (infix "<e" 50) |
1331 where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)" |
1331 where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)" |
1332 |
1332 |
1333 definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}" |
1333 definition%important box_eucl_less: "box a b = {x. a <e x \<and> x <e b}" |
1334 definition "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}" |
1334 definition%important "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}" |
1335 |
1335 |
1336 lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}" |
1336 lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}" |
1337 and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b" |
1337 and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b" |
1338 and mem_box: "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i)" |
1338 and mem_box: "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i)" |
1339 "x \<in> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)" |
1339 "x \<in> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)" |
1871 by auto |
1871 by auto |
1872 ultimately show ?thesis |
1872 ultimately show ?thesis |
1873 by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases) |
1873 by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases) |
1874 qed |
1874 qed |
1875 |
1875 |
1876 text \<open>Intervals in general, including infinite and mixtures of open and closed.\<close> |
1876 subsection \<open>Intervals in general, including infinite and mixtures of open and closed.\<close> |
1877 |
1877 |
1878 definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow> |
1878 definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow> |
1879 (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)" |
1879 (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)" |
1880 |
1880 |
1881 lemma is_interval_1: |
1881 lemma is_interval_1: |
1882 "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)" |
1882 "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)" |
1883 unfolding is_interval_def by auto |
1883 unfolding is_interval_def by auto |
2051 by (metis image_cong uminus_add_conv_diff) |
2051 by (metis image_cong uminus_add_conv_diff) |
2052 |
2052 |
2053 |
2053 |
2054 subsection \<open>Limit points\<close> |
2054 subsection \<open>Limit points\<close> |
2055 |
2055 |
2056 definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) |
2056 definition%important (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) |
2057 where "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))" |
2057 where "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))" |
2058 |
2058 |
2059 lemma islimptI: |
2059 lemma islimptI: |
2060 assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x" |
2060 assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x" |
2061 shows "x islimpt S" |
2061 shows "x islimpt S" |
2724 then show ?thesis |
2724 then show ?thesis |
2725 using closure_subset by (auto simp: frontier_def) |
2725 using closure_subset by (auto simp: frontier_def) |
2726 qed |
2726 qed |
2727 |
2727 |
2728 |
2728 |
2729 subsection \<open>Filters and the ``eventually true'' quantifier\<close> |
2729 subsection%unimportant \<open>Filters and the ``eventually true'' quantifier\<close> |
2730 |
2730 |
2731 definition indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter" (infixr "indirection" 70) |
2731 definition indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter" (infixr "indirection" 70) |
2732 where "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}" |
2732 where "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}" |
2733 |
2733 |
2734 text \<open>Identify Trivial limits, where we can't approach arbitrarily closely.\<close> |
2734 text \<open>Identify Trivial limits, where we can't approach arbitrarily closely.\<close> |
2792 by (simp add: filter_eq_iff) |
2792 by (simp add: filter_eq_iff) |
2793 |
2793 |
2794 |
2794 |
2795 subsection \<open>Limits\<close> |
2795 subsection \<open>Limits\<close> |
2796 |
2796 |
2797 lemma Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" |
2797 lemma%important Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" |
2798 by (auto simp: tendsto_iff trivial_limit_eq) |
2798 by (auto simp: tendsto_iff trivial_limit_eq) |
2799 |
2799 |
2800 text \<open>Show that they yield usual definitions in the various cases.\<close> |
2800 text \<open>Show that they yield usual definitions in the various cases.\<close> |
2801 |
2801 |
2802 lemma Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> |
2802 lemma%important Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> |
2803 (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)" |
2803 (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)" |
2804 by (auto simp: tendsto_iff eventually_at_le) |
2804 by (auto simp: tendsto_iff eventually_at_le) |
2805 |
2805 |
2806 lemma Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> |
2806 lemma%important Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> |
2807 (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" |
2807 (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" |
2808 by (auto simp: tendsto_iff eventually_at) |
2808 by (auto simp: tendsto_iff eventually_at) |
2809 |
2809 |
2810 corollary Lim_withinI [intro?]: |
2810 corollary Lim_withinI [intro?]: |
2811 assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l \<le> e" |
2811 assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l \<le> e" |
2812 shows "(f \<longlongrightarrow> l) (at a within S)" |
2812 shows "(f \<longlongrightarrow> l) (at a within S)" |
2813 apply (simp add: Lim_within, clarify) |
2813 apply (simp add: Lim_within, clarify) |
2814 apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) |
2814 apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) |
2815 done |
2815 done |
2816 |
2816 |
2817 lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow> |
2817 lemma%important Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow> |
2818 (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" |
2818 (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" |
2819 by (auto simp: tendsto_iff eventually_at) |
2819 by (auto simp: tendsto_iff eventually_at) |
2820 |
2820 |
2821 lemma Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)" |
2821 lemma%important Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)" |
2822 by (auto simp: tendsto_iff eventually_at_infinity) |
2822 by (auto simp: tendsto_iff eventually_at_infinity) |
2823 |
2823 |
2824 corollary Lim_at_infinityI [intro?]: |
2824 corollary Lim_at_infinityI [intro?]: |
2825 assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>B. \<forall>x. norm x \<ge> B \<longrightarrow> dist (f x) l \<le> e" |
2825 assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>B. \<forall>x. norm x \<ge> B \<longrightarrow> dist (f x) l \<le> e" |
2826 shows "(f \<longlongrightarrow> l) at_infinity" |
2826 shows "(f \<longlongrightarrow> l) at_infinity" |
3409 |
3409 |
3410 |
3410 |
3411 subsection \<open>Boundedness\<close> |
3411 subsection \<open>Boundedness\<close> |
3412 |
3412 |
3413 (* FIXME: This has to be unified with BSEQ!! *) |
3413 (* FIXME: This has to be unified with BSEQ!! *) |
3414 definition (in metric_space) bounded :: "'a set \<Rightarrow> bool" |
3414 definition%important (in metric_space) bounded :: "'a set \<Rightarrow> bool" |
3415 where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)" |
3415 where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)" |
3416 |
3416 |
3417 lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)" |
3417 lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)" |
3418 unfolding bounded_def subset_eq by auto (meson order_trans zero_le_dist) |
3418 unfolding bounded_def subset_eq by auto (meson order_trans zero_le_dist) |
3419 |
3419 |
3688 |
3688 |
3689 subsection \<open>Compactness\<close> |
3689 subsection \<open>Compactness\<close> |
3690 |
3690 |
3691 subsubsection \<open>Bolzano-Weierstrass property\<close> |
3691 subsubsection \<open>Bolzano-Weierstrass property\<close> |
3692 |
3692 |
3693 lemma heine_borel_imp_bolzano_weierstrass: |
3693 lemma%important heine_borel_imp_bolzano_weierstrass: |
3694 assumes "compact s" |
3694 assumes "compact s" |
3695 and "infinite t" |
3695 and "infinite t" |
3696 and "t \<subseteq> s" |
3696 and "t \<subseteq> s" |
3697 shows "\<exists>x \<in> s. x islimpt t" |
3697 shows "\<exists>x \<in> s. x islimpt t" |
3698 proof (rule ccontr) |
3698 proof%unimportant (rule ccontr) |
3699 assume "\<not> (\<exists>x \<in> s. x islimpt t)" |
3699 assume "\<not> (\<exists>x \<in> s. x islimpt t)" |
3700 then obtain f where f: "\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)" |
3700 then obtain f where f: "\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)" |
3701 unfolding islimpt_def |
3701 unfolding islimpt_def |
3702 using bchoice[of s "\<lambda> x T. x \<in> T \<and> open T \<and> (\<forall>y\<in>t. y \<in> T \<longrightarrow> y = x)"] |
3702 using bchoice[of s "\<lambda> x T. x \<in> T \<and> open T \<and> (\<forall>y\<in>t. y \<in> T \<longrightarrow> y = x)"] |
3703 by auto |
3703 by auto |
4155 } |
4155 } |
4156 with \<open>x\<in>U\<close> have "x \<in> U \<inter> \<Inter>A" by auto |
4156 with \<open>x\<in>U\<close> have "x \<in> U \<inter> \<Inter>A" by auto |
4157 with \<open>U \<inter> \<Inter>A = {}\<close> show False by auto |
4157 with \<open>U \<inter> \<Inter>A = {}\<close> show False by auto |
4158 qed |
4158 qed |
4159 |
4159 |
4160 definition "countably_compact U \<longleftrightarrow> |
4160 definition%important "countably_compact U \<longleftrightarrow> |
4161 (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))" |
4161 (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))" |
4162 |
4162 |
4163 lemma countably_compactE: |
4163 lemma countably_compactE: |
4164 assumes "countably_compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C" "countable C" |
4164 assumes "countably_compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C" "countable C" |
4165 obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'" |
4165 obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'" |
4206 unfolding bchoice_iff Bex_def .. |
4206 unfolding bchoice_iff Bex_def .. |
4207 with T show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T" |
4207 with T show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T" |
4208 unfolding C_def by (intro exI[of _ "f`T"]) fastforce |
4208 unfolding C_def by (intro exI[of _ "f`T"]) fastforce |
4209 qed |
4209 qed |
4210 |
4210 |
4211 lemma countably_compact_imp_compact_second_countable: |
4211 lemma%important countably_compact_imp_compact_second_countable: |
4212 "countably_compact U \<Longrightarrow> compact (U :: 'a :: second_countable_topology set)" |
4212 "countably_compact U \<Longrightarrow> compact (U :: 'a :: second_countable_topology set)" |
4213 proof (rule countably_compact_imp_compact) |
4213 proof%unimportant (rule countably_compact_imp_compact) |
4214 fix T and x :: 'a |
4214 fix T and x :: 'a |
4215 assume "open T" "x \<in> T" |
4215 assume "open T" "x \<in> T" |
4216 from topological_basisE[OF is_basis this] obtain b where |
4216 from topological_basisE[OF is_basis this] obtain b where |
4217 "b \<in> (SOME B. countable B \<and> topological_basis B)" "x \<in> b" "b \<subseteq> T" . |
4217 "b \<in> (SOME B. countable B \<and> topological_basis B)" "x \<in> b" "b \<subseteq> T" . |
4218 then show "\<exists>b\<in>SOME B. countable B \<and> topological_basis B. x \<in> b \<and> b \<inter> U \<subseteq> T" |
4218 then show "\<exists>b\<in>SOME B. countable B \<and> topological_basis B. x \<in> b \<and> b \<inter> U \<subseteq> T" |
4223 "countably_compact U \<longleftrightarrow> compact (U :: 'a :: second_countable_topology set)" |
4223 "countably_compact U \<longleftrightarrow> compact (U :: 'a :: second_countable_topology set)" |
4224 using countably_compact_imp_compact_second_countable compact_imp_countably_compact by blast |
4224 using countably_compact_imp_compact_second_countable compact_imp_countably_compact by blast |
4225 |
4225 |
4226 subsubsection\<open>Sequential compactness\<close> |
4226 subsubsection\<open>Sequential compactness\<close> |
4227 |
4227 |
4228 definition seq_compact :: "'a::topological_space set \<Rightarrow> bool" |
4228 definition%important seq_compact :: "'a::topological_space set \<Rightarrow> bool" |
4229 where "seq_compact S \<longleftrightarrow> |
4229 where "seq_compact S \<longleftrightarrow> |
4230 (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))" |
4230 (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))" |
4231 |
4231 |
4232 lemma seq_compactI: |
4232 lemma seq_compactI: |
4233 assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" |
4233 assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" |
4484 lemma seq_compact_eq_compact: |
4484 lemma seq_compact_eq_compact: |
4485 fixes U :: "'a :: second_countable_topology set" |
4485 fixes U :: "'a :: second_countable_topology set" |
4486 shows "seq_compact U \<longleftrightarrow> compact U" |
4486 shows "seq_compact U \<longleftrightarrow> compact U" |
4487 using seq_compact_eq_countably_compact countably_compact_eq_compact by blast |
4487 using seq_compact_eq_countably_compact countably_compact_eq_compact by blast |
4488 |
4488 |
4489 lemma bolzano_weierstrass_imp_seq_compact: |
4489 lemma%important bolzano_weierstrass_imp_seq_compact: |
4490 fixes s :: "'a::{t1_space, first_countable_topology} set" |
4490 fixes s :: "'a::{t1_space, first_countable_topology} set" |
4491 shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s" |
4491 shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s" |
4492 by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point) |
4492 by%unimportant (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point) |
4493 |
4493 |
4494 |
4494 |
4495 subsubsection\<open>Totally bounded\<close> |
4495 subsubsection\<open>Totally bounded\<close> |
4496 |
4496 |
4497 lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (s m) (s n) < e)" |
4497 lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (s m) (s n) < e)" |
4498 unfolding Cauchy_def by metis |
4498 unfolding Cauchy_def by metis |
4499 |
4499 |
4500 lemma seq_compact_imp_totally_bounded: |
4500 lemma%important seq_compact_imp_totally_bounded: |
4501 assumes "seq_compact s" |
4501 assumes "seq_compact s" |
4502 shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)" |
4502 shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)" |
4503 proof - |
4503 proof%unimportant - |
4504 { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)" |
4504 { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)" |
4505 let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))" |
4505 let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))" |
4506 have "\<exists>x. \<forall>n::nat. ?Q x n (x n)" |
4506 have "\<exists>x. \<forall>n::nat. ?Q x n (x n)" |
4507 proof (rule dependent_wellorder_choice) |
4507 proof (rule dependent_wellorder_choice) |
4508 fix n x assume "\<And>y. y < n \<Longrightarrow> ?Q x y (x y)" |
4508 fix n x assume "\<And>y. y < n \<Longrightarrow> ?Q x y (x y)" |
4527 by metis |
4527 by metis |
4528 qed |
4528 qed |
4529 |
4529 |
4530 subsubsection\<open>Heine-Borel theorem\<close> |
4530 subsubsection\<open>Heine-Borel theorem\<close> |
4531 |
4531 |
4532 lemma seq_compact_imp_heine_borel: |
4532 lemma%important seq_compact_imp_heine_borel: |
4533 fixes s :: "'a :: metric_space set" |
4533 fixes s :: "'a :: metric_space set" |
4534 assumes "seq_compact s" |
4534 assumes "seq_compact s" |
4535 shows "compact s" |
4535 shows "compact s" |
4536 proof - |
4536 proof%unimportant - |
4537 from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>] |
4537 from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>] |
4538 obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)" |
4538 obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)" |
4539 unfolding choice_iff' .. |
4539 unfolding choice_iff' .. |
4540 define K where "K = (\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)" |
4540 define K where "K = (\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)" |
4541 have "countably_compact s" |
4541 have "countably_compact s" |
4572 show "x \<in> ball k r" by fact |
4572 show "x \<in> ball k r" by fact |
4573 qed |
4573 qed |
4574 qed |
4574 qed |
4575 qed |
4575 qed |
4576 |
4576 |
4577 lemma compact_eq_seq_compact_metric: |
4577 lemma%important compact_eq_seq_compact_metric: |
4578 "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s" |
4578 "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s" |
4579 using compact_imp_seq_compact seq_compact_imp_heine_borel by blast |
4579 using compact_imp_seq_compact seq_compact_imp_heine_borel by blast |
4580 |
4580 |
4581 lemma compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close> |
4581 lemma%important compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close> |
4582 "compact (S :: 'a::metric_space set) \<longleftrightarrow> |
4582 "compact (S :: 'a::metric_space set) \<longleftrightarrow> |
4583 (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))" |
4583 (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))" |
4584 unfolding compact_eq_seq_compact_metric seq_compact_def by auto |
4584 unfolding compact_eq_seq_compact_metric seq_compact_def by auto |
4585 |
4585 |
4586 subsubsection \<open>Complete the chain of compactness variants\<close> |
4586 subsubsection \<open>Complete the chain of compactness variants\<close> |
4587 |
4587 |
4588 lemma compact_eq_bolzano_weierstrass: |
4588 lemma%important compact_eq_bolzano_weierstrass: |
4589 fixes s :: "'a::metric_space set" |
4589 fixes s :: "'a::metric_space set" |
4590 shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" |
4590 shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" |
4591 (is "?lhs = ?rhs") |
4591 (is "?lhs = ?rhs") |
4592 proof |
4592 proof%unimportant |
4593 assume ?lhs |
4593 assume ?lhs |
4594 then show ?rhs |
4594 then show ?rhs |
4595 using heine_borel_imp_bolzano_weierstrass[of s] by auto |
4595 using heine_borel_imp_bolzano_weierstrass[of s] by auto |
4596 next |
4596 next |
4597 assume ?rhs |
4597 assume ?rhs |
4598 then show ?lhs |
4598 then show ?lhs |
4599 unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact) |
4599 unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact) |
4600 qed |
4600 qed |
4601 |
4601 |
4602 lemma bolzano_weierstrass_imp_bounded: |
4602 lemma%important bolzano_weierstrass_imp_bounded: |
4603 "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s" |
4603 "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s" |
4604 using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass . |
4604 using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass . |
4605 |
4605 |
4606 |
4606 |
4607 subsection \<open>Metric spaces with the Heine-Borel property\<close> |
4607 subsection \<open>Metric spaces with the Heine-Borel property\<close> |
4609 text \<open> |
4609 text \<open> |
4610 A metric space (or topological vector space) is said to have the |
4610 A metric space (or topological vector space) is said to have the |
4611 Heine-Borel property if every closed and bounded subset is compact. |
4611 Heine-Borel property if every closed and bounded subset is compact. |
4612 \<close> |
4612 \<close> |
4613 |
4613 |
4614 class heine_borel = metric_space + |
4614 class%important heine_borel = metric_space + |
4615 assumes bounded_imp_convergent_subsequence: |
4615 assumes bounded_imp_convergent_subsequence: |
4616 "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" |
4616 "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" |
4617 |
4617 |
4618 lemma bounded_closed_imp_seq_compact: |
4618 lemma%important bounded_closed_imp_seq_compact: |
4619 fixes s::"'a::heine_borel set" |
4619 fixes s::"'a::heine_borel set" |
4620 assumes "bounded s" |
4620 assumes "bounded s" |
4621 and "closed s" |
4621 and "closed s" |
4622 shows "seq_compact s" |
4622 shows "seq_compact s" |
4623 proof (unfold seq_compact_def, clarify) |
4623 proof%unimportant (unfold seq_compact_def, clarify) |
4624 fix f :: "nat \<Rightarrow> 'a" |
4624 fix f :: "nat \<Rightarrow> 'a" |
4625 assume f: "\<forall>n. f n \<in> s" |
4625 assume f: "\<forall>n. f n \<in> s" |
4626 with \<open>bounded s\<close> have "bounded (range f)" |
4626 with \<open>bounded s\<close> have "bounded (range f)" |
4627 by (auto intro: bounded_subset) |
4627 by (auto intro: bounded_subset) |
4628 obtain l r where r: "strict_mono (r :: nat \<Rightarrow> nat)" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially" |
4628 obtain l r where r: "strict_mono (r :: nat \<Rightarrow> nat)" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially" |
4688 by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI) |
4688 by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI) |
4689 then show "\<exists>N. \<forall>n\<ge>N. K \<subseteq> S \<inter> cball 0 (real n)" |
4689 then show "\<exists>N. \<forall>n\<ge>N. K \<subseteq> S \<inter> cball 0 (real n)" |
4690 by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans) |
4690 by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans) |
4691 qed auto |
4691 qed auto |
4692 |
4692 |
4693 instance real :: heine_borel |
4693 instance%important real :: heine_borel |
4694 proof |
4694 proof%unimportant |
4695 fix f :: "nat \<Rightarrow> real" |
4695 fix f :: "nat \<Rightarrow> real" |
4696 assume f: "bounded (range f)" |
4696 assume f: "bounded (range f)" |
4697 obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)" |
4697 obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)" |
4698 unfolding comp_def by (metis seq_monosub) |
4698 unfolding comp_def by (metis seq_monosub) |
4699 then have "Bseq (f \<circ> r)" |
4699 then have "Bseq (f \<circ> r)" |
4769 strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)" |
4769 strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)" |
4770 by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"]) |
4770 by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"]) |
4771 (auto intro!: assms bounded_linear_inner_left bounded_linear_image |
4771 (auto intro!: assms bounded_linear_inner_left bounded_linear_image |
4772 simp: euclidean_representation) |
4772 simp: euclidean_representation) |
4773 |
4773 |
4774 instance euclidean_space \<subseteq> heine_borel |
4774 instance%important euclidean_space \<subseteq> heine_borel |
4775 proof |
4775 proof%unimportant |
4776 fix f :: "nat \<Rightarrow> 'a" |
4776 fix f :: "nat \<Rightarrow> 'a" |
4777 assume f: "bounded (range f)" |
4777 assume f: "bounded (range f)" |
4778 then obtain l::'a and r where r: "strict_mono r" |
4778 then obtain l::'a and r where r: "strict_mono r" |
4779 and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially" |
4779 and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially" |
4780 using compact_lemma [OF f] by blast |
4780 using compact_lemma [OF f] by blast |
4816 |
4816 |
4817 lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)" |
4817 lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)" |
4818 unfolding bounded_def |
4818 unfolding bounded_def |
4819 by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans) |
4819 by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans) |
4820 |
4820 |
4821 instance prod :: (heine_borel, heine_borel) heine_borel |
4821 instance%important prod :: (heine_borel, heine_borel) heine_borel |
4822 proof |
4822 proof%unimportant |
4823 fix f :: "nat \<Rightarrow> 'a \<times> 'b" |
4823 fix f :: "nat \<Rightarrow> 'a \<times> 'b" |
4824 assume f: "bounded (range f)" |
4824 assume f: "bounded (range f)" |
4825 then have "bounded (fst ` range f)" |
4825 then have "bounded (fst ` range f)" |
4826 by (rule bounded_fst) |
4826 by (rule bounded_fst) |
4827 then have s1: "bounded (range (fst \<circ> f))" |
4827 then have s1: "bounded (range (fst \<circ> f))" |
4843 using l r by fast |
4843 using l r by fast |
4844 qed |
4844 qed |
4845 |
4845 |
4846 subsubsection \<open>Completeness\<close> |
4846 subsubsection \<open>Completeness\<close> |
4847 |
4847 |
4848 lemma (in metric_space) completeI: |
4848 lemma%important (in metric_space) completeI: |
4849 assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l" |
4849 assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l" |
4850 shows "complete s" |
4850 shows "complete s" |
4851 using assms unfolding complete_def by fast |
4851 using assms unfolding complete_def by fast |
4852 |
4852 |
4853 lemma (in metric_space) completeE: |
4853 lemma%important (in metric_space) completeE: |
4854 assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f" |
4854 assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f" |
4855 obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l" |
4855 obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l" |
4856 using assms unfolding complete_def by fast |
4856 using assms unfolding complete_def by fast |
4857 |
4857 |
4858 (* TODO: generalize to uniform spaces *) |
4858 (* TODO: generalize to uniform spaces *) |
4898 unfolding lim_sequentially by auto |
4898 unfolding lim_sequentially by auto |
4899 } |
4899 } |
4900 then show ?thesis unfolding complete_def by auto |
4900 then show ?thesis unfolding complete_def by auto |
4901 qed |
4901 qed |
4902 |
4902 |
4903 lemma compact_eq_totally_bounded: |
4903 lemma%important compact_eq_totally_bounded: |
4904 "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))" |
4904 "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))" |
4905 (is "_ \<longleftrightarrow> ?rhs") |
4905 (is "_ \<longleftrightarrow> ?rhs") |
4906 proof |
4906 proof%unimportant |
4907 assume assms: "?rhs" |
4907 assume assms: "?rhs" |
4908 then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)" |
4908 then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)" |
4909 by (auto simp: choice_iff') |
4909 by (auto simp: choice_iff') |
4910 |
4910 |
4911 show "compact s" |
4911 show "compact s" |
5105 |
5105 |
5106 subsection \<open>Continuity\<close> |
5106 subsection \<open>Continuity\<close> |
5107 |
5107 |
5108 text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close> |
5108 text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close> |
5109 |
5109 |
5110 lemma continuous_within_eps_delta: |
5110 lemma%important continuous_within_eps_delta: |
5111 "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s. dist x' x < d --> dist (f x') (f x) < e)" |
5111 "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s. dist x' x < d --> dist (f x') (f x) < e)" |
5112 unfolding continuous_within and Lim_within by fastforce |
5112 unfolding continuous_within and Lim_within by fastforce |
5113 |
5113 |
5114 corollary continuous_at_eps_delta: |
5114 corollary continuous_at_eps_delta: |
5115 "continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)" |
5115 "continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)" |
5433 using assms |
5433 using assms |
5434 unfolding continuous_within |
5434 unfolding continuous_within |
5435 by (force intro: Lim_transform_within) |
5435 by (force intro: Lim_transform_within) |
5436 |
5436 |
5437 |
5437 |
5438 subsubsection \<open>Structural rules for pointwise continuity\<close> |
5438 subsubsection%unimportant \<open>Structural rules for pointwise continuity\<close> |
5439 |
5439 |
5440 lemma continuous_infnorm[continuous_intros]: |
5440 lemma continuous_infnorm[continuous_intros]: |
5441 "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))" |
5441 "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))" |
5442 unfolding continuous_def by (rule tendsto_infnorm) |
5442 unfolding continuous_def by (rule tendsto_infnorm) |
5443 |
5443 |
5445 assumes "continuous F f" |
5445 assumes "continuous F f" |
5446 and "continuous F g" |
5446 and "continuous F g" |
5447 shows "continuous F (\<lambda>x. inner (f x) (g x))" |
5447 shows "continuous F (\<lambda>x. inner (f x) (g x))" |
5448 using assms unfolding continuous_def by (rule tendsto_inner) |
5448 using assms unfolding continuous_def by (rule tendsto_inner) |
5449 |
5449 |
5450 subsubsection \<open>Structural rules for setwise continuity\<close> |
5450 subsubsection%unimportant \<open>Structural rules for setwise continuity\<close> |
5451 |
5451 |
5452 lemma continuous_on_infnorm[continuous_intros]: |
5452 lemma continuous_on_infnorm[continuous_intros]: |
5453 "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))" |
5453 "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))" |
5454 unfolding continuous_on by (fast intro: tendsto_infnorm) |
5454 unfolding continuous_on by (fast intro: tendsto_infnorm) |
5455 |
5455 |
5459 and "continuous_on s g" |
5459 and "continuous_on s g" |
5460 shows "continuous_on s (\<lambda>x. inner (f x) (g x))" |
5460 shows "continuous_on s (\<lambda>x. inner (f x) (g x))" |
5461 using bounded_bilinear_inner assms |
5461 using bounded_bilinear_inner assms |
5462 by (rule bounded_bilinear.continuous_on) |
5462 by (rule bounded_bilinear.continuous_on) |
5463 |
5463 |
5464 subsubsection \<open>Structural rules for uniform continuity\<close> |
5464 subsubsection%unimportant \<open>Structural rules for uniform continuity\<close> |
5465 |
5465 |
5466 lemma uniformly_continuous_on_dist[continuous_intros]: |
5466 lemma uniformly_continuous_on_dist[continuous_intros]: |
5467 fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" |
5467 fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" |
5468 assumes "uniformly_continuous_on s f" |
5468 assumes "uniformly_continuous_on s f" |
5469 and "uniformly_continuous_on s g" |
5469 and "uniformly_continuous_on s g" |
5651 lemma continuous_on_imp_closedin: |
5651 lemma continuous_on_imp_closedin: |
5652 assumes "continuous_on S f" "closedin (subtopology euclidean (f ` S)) T" |
5652 assumes "continuous_on S f" "closedin (subtopology euclidean (f ` S)) T" |
5653 shows "closedin (subtopology euclidean S) (S \<inter> f -` T)" |
5653 shows "closedin (subtopology euclidean S) (S \<inter> f -` T)" |
5654 using assms continuous_on_closed by blast |
5654 using assms continuous_on_closed by blast |
5655 |
5655 |
5656 subsection \<open>Half-global and completely global cases.\<close> |
5656 subsection%unimportant \<open>Half-global and completely global cases.\<close> |
5657 |
5657 |
5658 lemma continuous_openin_preimage_gen: |
5658 lemma continuous_openin_preimage_gen: |
5659 assumes "continuous_on S f" "open T" |
5659 assumes "continuous_on S f" "open T" |
5660 shows "openin (subtopology euclidean S) (S \<inter> f -` T)" |
5660 shows "openin (subtopology euclidean S) (S \<inter> f -` T)" |
5661 proof - |
5661 proof - |
5741 using \<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto |
5741 using \<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto |
5742 ultimately have "y \<in> interior S" .. |
5742 ultimately have "y \<in> interior S" .. |
5743 with \<open>x = f y\<close> show "x \<in> f ` interior S" .. |
5743 with \<open>x = f y\<close> show "x \<in> f ` interior S" .. |
5744 qed |
5744 qed |
5745 |
5745 |
5746 subsection \<open>Topological properties of linear functions.\<close> |
5746 subsection%unimportant \<open>Topological properties of linear functions.\<close> |
5747 |
5747 |
5748 lemma linear_lim_0: |
5748 lemma linear_lim_0: |
5749 assumes "bounded_linear f" |
5749 assumes "bounded_linear f" |
5750 shows "(f \<longlongrightarrow> 0) (at (0))" |
5750 shows "(f \<longlongrightarrow> 0) (at (0))" |
5751 proof - |
5751 proof - |
5769 |
5769 |
5770 lemma linear_continuous_on: |
5770 lemma linear_continuous_on: |
5771 "bounded_linear f \<Longrightarrow> continuous_on s f" |
5771 "bounded_linear f \<Longrightarrow> continuous_on s f" |
5772 using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto |
5772 using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto |
5773 |
5773 |
5774 subsection \<open>Intervals\<close> |
5774 subsection%unimportant \<open>Intervals\<close> |
5775 |
5775 |
5776 text \<open>Openness of halfspaces.\<close> |
5776 text \<open>Openness of halfspaces.\<close> |
5777 |
5777 |
5778 lemma open_halfspace_lt: "open {x. inner a x < b}" |
5778 lemma open_halfspace_lt: "open {x. inner a x < b}" |
5779 by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) |
5779 by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) |