# HG changeset patch # User immler # Date 1546111929 -3600 # Node ID 5aa5a8d6e5b57ae8b0fa92b0bbf48d1958e1bc4f # Parent c2d5575d9da5825ac7c93624e0cd2b5de048af7c split off theorems involving classes below metric_space and real_normed_vector diff -r c2d5575d9da5 -r 5aa5a8d6e5b5 src/HOL/Analysis/Abstract_Topology.thy --- a/src/HOL/Analysis/Abstract_Topology.thy Sat Dec 29 18:40:29 2018 +0000 +++ b/src/HOL/Analysis/Abstract_Topology.thy Sat Dec 29 20:32:09 2018 +0100 @@ -4,9 +4,588 @@ section \Operators involving abstract topology\ theory Abstract_Topology - imports Topology_Euclidean_Space Path_Connected + imports + Complex_Main + "HOL-Library.Set_Idioms" + "HOL-Library.FuncSet" + (* Path_Connected *) begin +subsection \General notion of a topology as a value\ + +definition%important "istopology L \ + L {} \ (\S T. L S \ L T \ L (S \ T)) \ (\K. Ball K L \ L (\K))" + +typedef%important 'a topology = "{L::('a set) \ bool. istopology L}" + morphisms "openin" "topology" + unfolding istopology_def by blast + +lemma istopology_openin[intro]: "istopology(openin U)" + using openin[of U] by blast + +lemma topology_inverse': "istopology U \ openin (topology U) = U" + using topology_inverse[unfolded mem_Collect_eq] . + +lemma topology_inverse_iff: "istopology U \ openin (topology U) = U" + using topology_inverse[of U] istopology_openin[of "topology U"] by auto + +lemma topology_eq: "T1 = T2 \ (\S. openin T1 S \ openin T2 S)" +proof + assume "T1 = T2" + then show "\S. openin T1 S \ openin T2 S" by simp +next + assume H: "\S. openin T1 S \ openin T2 S" + then have "openin T1 = openin T2" by (simp add: fun_eq_iff) + then have "topology (openin T1) = topology (openin T2)" by simp + then show "T1 = T2" unfolding openin_inverse . +qed + + +text\The "universe": the union of all sets in the topology.\ +definition "topspace T = \{S. openin T S}" + +subsubsection \Main properties of open sets\ + +proposition openin_clauses: + fixes U :: "'a topology" + shows + "openin U {}" + "\S T. openin U S \ openin U T \ openin U (S\T)" + "\K. (\S \ K. openin U S) \ openin U (\K)" + using openin[of U] unfolding istopology_def mem_Collect_eq by fast+ + +lemma openin_subset[intro]: "openin U S \ S \ topspace U" + unfolding topspace_def by blast + +lemma openin_empty[simp]: "openin U {}" + by (rule openin_clauses) + +lemma openin_Int[intro]: "openin U S \ openin U T \ openin U (S \ T)" + by (rule openin_clauses) + +lemma openin_Union[intro]: "(\S. S \ K \ openin U S) \ openin U (\K)" + using openin_clauses by blast + +lemma openin_Un[intro]: "openin U S \ openin U T \ openin U (S \ T)" + using openin_Union[of "{S,T}" U] by auto + +lemma openin_topspace[intro, simp]: "openin U (topspace U)" + by (force simp: openin_Union topspace_def) + +lemma openin_subopen: "openin U S \ (\x \ S. \T. openin U T \ x \ T \ T \ S)" + (is "?lhs \ ?rhs") +proof + assume ?lhs + then show ?rhs by auto +next + assume H: ?rhs + let ?t = "\{T. openin U T \ T \ S}" + have "openin U ?t" by (force simp: openin_Union) + also have "?t = S" using H by auto + finally show "openin U S" . +qed + +lemma openin_INT [intro]: + assumes "finite I" + "\i. i \ I \ openin T (U i)" + shows "openin T ((\i \ I. U i) \ topspace T)" +using assms by (induct, auto simp: inf_sup_aci(2) openin_Int) + +lemma openin_INT2 [intro]: + assumes "finite I" "I \ {}" + "\i. i \ I \ openin T (U i)" + shows "openin T (\i \ I. U i)" +proof - + have "(\i \ I. U i) \ topspace T" + using \I \ {}\ openin_subset[OF assms(3)] by auto + then show ?thesis + using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute) +qed + +lemma openin_Inter [intro]: + assumes "finite \" "\ \ {}" "\X. X \ \ \ openin T X" shows "openin T (\\)" + by (metis (full_types) assms openin_INT2 image_ident) + +lemma openin_Int_Inter: + assumes "finite \" "openin T U" "\X. X \ \ \ openin T X" shows "openin T (U \ \\)" + using openin_Inter [of "insert U \"] assms by auto + + +subsubsection \Closed sets\ + +definition%important "closedin U S \ S \ topspace U \ openin U (topspace U - S)" + +lemma closedin_subset: "closedin U S \ S \ topspace U" + by (metis closedin_def) + +lemma closedin_empty[simp]: "closedin U {}" + by (simp add: closedin_def) + +lemma closedin_topspace[intro, simp]: "closedin U (topspace U)" + by (simp add: closedin_def) + +lemma closedin_Un[intro]: "closedin U S \ closedin U T \ closedin U (S \ T)" + by (auto simp: Diff_Un closedin_def) + +lemma Diff_Inter[intro]: "A - \S = \{A - s|s. s\S}" + by auto + +lemma closedin_Union: + assumes "finite S" "\T. T \ S \ closedin U T" + shows "closedin U (\S)" + using assms by induction auto + +lemma closedin_Inter[intro]: + assumes Ke: "K \ {}" + and Kc: "\S. S \K \ closedin U S" + shows "closedin U (\K)" + using Ke Kc unfolding closedin_def Diff_Inter by auto + +lemma closedin_INT[intro]: + assumes "A \ {}" "\x. x \ A \ closedin U (B x)" + shows "closedin U (\x\A. B x)" + apply (rule closedin_Inter) + using assms + apply auto + done + +lemma closedin_Int[intro]: "closedin U S \ closedin U T \ closedin U (S \ T)" + using closedin_Inter[of "{S,T}" U] by auto + +lemma openin_closedin_eq: "openin U S \ S \ topspace U \ closedin U (topspace U - S)" + apply (auto simp: closedin_def Diff_Diff_Int inf_absorb2) + apply (metis openin_subset subset_eq) + done + +lemma openin_closedin: "S \ topspace U \ (openin U S \ closedin U (topspace U - S))" + by (simp add: openin_closedin_eq) + +lemma openin_diff[intro]: + assumes oS: "openin U S" + and cT: "closedin U T" + shows "openin U (S - T)" +proof - + have "S - T = S \ (topspace U - T)" using openin_subset[of U S] oS cT + by (auto simp: topspace_def openin_subset) + then show ?thesis using oS cT + by (auto simp: closedin_def) +qed + +lemma closedin_diff[intro]: + assumes oS: "closedin U S" + and cT: "openin U T" + shows "closedin U (S - T)" +proof - + have "S - T = S \ (topspace U - T)" + using closedin_subset[of U S] oS cT by (auto simp: topspace_def) + then show ?thesis + using oS cT by (auto simp: openin_closedin_eq) +qed + + +subsection\The discrete topology\ + +definition discrete_topology where "discrete_topology U \ topology (\S. S \ U)" + +lemma openin_discrete_topology [simp]: "openin (discrete_topology U) S \ S \ U" +proof - + have "istopology (\S. S \ U)" + by (auto simp: istopology_def) + then show ?thesis + by (simp add: discrete_topology_def topology_inverse') +qed + +lemma topspace_discrete_topology [simp]: "topspace(discrete_topology U) = U" + by (meson openin_discrete_topology openin_subset openin_topspace order_refl subset_antisym) + +lemma closedin_discrete_topology [simp]: "closedin (discrete_topology U) S \ S \ U" + by (simp add: closedin_def) + +lemma discrete_topology_unique: + "discrete_topology U = X \ topspace X = U \ (\x \ U. openin X {x})" (is "?lhs = ?rhs") +proof + assume R: ?rhs + then have "openin X S" if "S \ U" for S + using openin_subopen subsetD that by fastforce + moreover have "x \ topspace X" if "openin X S" and "x \ S" for x S + using openin_subset that by blast + ultimately + show ?lhs + using R by (auto simp: topology_eq) +qed auto + +lemma discrete_topology_unique_alt: + "discrete_topology U = X \ topspace X \ U \ (\x \ U. openin X {x})" + using openin_subset + by (auto simp: discrete_topology_unique) + +lemma subtopology_eq_discrete_topology_empty: + "X = discrete_topology {} \ topspace X = {}" + using discrete_topology_unique [of "{}" X] by auto + +lemma subtopology_eq_discrete_topology_sing: + "X = discrete_topology {a} \ topspace X = {a}" + by (metis discrete_topology_unique openin_topspace singletonD) + + +subsection \Subspace topology\ + +definition%important "subtopology U V = topology (\T. \S. T = S \ V \ openin U S)" + +lemma istopology_subtopology: "istopology (\T. \S. T = S \ V \ openin U S)" + (is "istopology ?L") +proof - + have "?L {}" by blast + { + fix A B + assume A: "?L A" and B: "?L B" + from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \ V" and Sb: "openin U Sb" "B = Sb \ V" + by blast + have "A \ B = (Sa \ Sb) \ V" "openin U (Sa \ Sb)" + using Sa Sb by blast+ + then have "?L (A \ B)" by blast + } + moreover + { + fix K + assume K: "K \ Collect ?L" + have th0: "Collect ?L = (\S. S \ V) ` Collect (openin U)" + by blast + from K[unfolded th0 subset_image_iff] + obtain Sk where Sk: "Sk \ Collect (openin U)" "K = (\S. S \ V) ` Sk" + by blast + have "\K = (\Sk) \ V" + using Sk by auto + moreover have "openin U (\Sk)" + using Sk by (auto simp: subset_eq) + ultimately have "?L (\K)" by blast + } + ultimately show ?thesis + unfolding subset_eq mem_Collect_eq istopology_def by auto +qed + +lemma openin_subtopology: "openin (subtopology U V) S \ (\T. openin U T \ S = T \ V)" + unfolding subtopology_def topology_inverse'[OF istopology_subtopology] + by auto + +lemma openin_subtopology_Int: + "openin X S \ openin (subtopology X T) (S \ T)" + using openin_subtopology by auto + +lemma openin_subtopology_Int2: + "openin X T \ openin (subtopology X S) (S \ T)" + using openin_subtopology by auto + +lemma openin_subtopology_diff_closed: + "\S \ topspace X; closedin X T\ \ openin (subtopology X S) (S - T)" + unfolding closedin_def openin_subtopology + by (rule_tac x="topspace X - T" in exI) auto + +lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)" + by (force simp: relative_to_def openin_subtopology) + +lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \ V" + by (auto simp: topspace_def openin_subtopology) + +lemma closedin_subtopology: "closedin (subtopology U V) S \ (\T. closedin U T \ S = T \ V)" + unfolding closedin_def topspace_subtopology + by (auto simp: openin_subtopology) + +lemma openin_subtopology_refl: "openin (subtopology U V) V \ V \ topspace U" + unfolding openin_subtopology + by auto (metis IntD1 in_mono openin_subset) + +lemma subtopology_subtopology: + "subtopology (subtopology X S) T = subtopology X (S \ T)" +proof - + have eq: "\T'. (\S'. T' = S' \ T \ (\T. openin X T \ S' = T \ S)) = (\Sa. T' = Sa \ (S \ T) \ openin X Sa)" + by (metis inf_assoc) + have "subtopology (subtopology X S) T = topology (\Ta. \Sa. Ta = Sa \ T \ openin (subtopology X S) Sa)" + by (simp add: subtopology_def) + also have "\ = subtopology X (S \ T)" + by (simp add: openin_subtopology eq) (simp add: subtopology_def) + finally show ?thesis . +qed + +lemma openin_subtopology_alt: + "openin (subtopology X U) S \ S \ (\T. U \ T) ` Collect (openin X)" + by (simp add: image_iff inf_commute openin_subtopology) + +lemma closedin_subtopology_alt: + "closedin (subtopology X U) S \ S \ (\T. U \ T) ` Collect (closedin X)" + by (simp add: image_iff inf_commute closedin_subtopology) + +lemma subtopology_superset: + assumes UV: "topspace U \ V" + shows "subtopology U V = U" +proof - + { + fix S + { + fix T + assume T: "openin U T" "S = T \ V" + from T openin_subset[OF T(1)] UV have eq: "S = T" + by blast + have "openin U S" + unfolding eq using T by blast + } + moreover + { + assume S: "openin U S" + then have "\T. openin U T \ S = T \ V" + using openin_subset[OF S] UV by auto + } + ultimately have "(\T. openin U T \ S = T \ V) \ openin U S" + by blast + } + then show ?thesis + unfolding topology_eq openin_subtopology by blast +qed + +lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" + by (simp add: subtopology_superset) + +lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" + by (simp add: subtopology_superset) + +lemma openin_subtopology_empty: + "openin (subtopology U {}) S \ S = {}" +by (metis Int_empty_right openin_empty openin_subtopology) + +lemma closedin_subtopology_empty: + "closedin (subtopology U {}) S \ S = {}" +by (metis Int_empty_right closedin_empty closedin_subtopology) + +lemma closedin_subtopology_refl [simp]: + "closedin (subtopology U X) X \ X \ topspace U" +by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology) + +lemma closedin_topspace_empty: "topspace T = {} \ (closedin T S \ S = {})" + by (simp add: closedin_def) + +lemma openin_imp_subset: + "openin (subtopology U S) T \ T \ S" +by (metis Int_iff openin_subtopology subsetI) + +lemma closedin_imp_subset: + "closedin (subtopology U S) T \ T \ S" +by (simp add: closedin_def topspace_subtopology) + +lemma openin_open_subtopology: + "openin X S \ openin (subtopology X S) T \ openin X T \ T \ S" + by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology) + +lemma closedin_closed_subtopology: + "closedin X S \ (closedin (subtopology X S) T \ closedin X T \ T \ S)" + by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE) + +lemma openin_subtopology_Un: + "\openin (subtopology X T) S; openin (subtopology X U) S\ + \ openin (subtopology X (T \ U)) S" +by (simp add: openin_subtopology) blast + +lemma closedin_subtopology_Un: + "\closedin (subtopology X T) S; closedin (subtopology X U) S\ + \ closedin (subtopology X (T \ U)) S" +by (simp add: closedin_subtopology) blast + + +subsection \The standard Euclidean topology\ + +definition%important euclidean :: "'a::topological_space topology" + where "euclidean = topology open" + +lemma open_openin: "open S \ openin euclidean S" + unfolding euclidean_def + apply (rule cong[where x=S and y=S]) + apply (rule topology_inverse[symmetric]) + apply (auto simp: istopology_def) + done + +declare open_openin [symmetric, simp] + +lemma topspace_euclidean [simp]: "topspace euclidean = UNIV" + by (force simp: topspace_def) + +lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S" + by (simp add: topspace_subtopology) + +lemma closed_closedin: "closed S \ closedin euclidean S" + by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV) + +declare closed_closedin [symmetric, simp] + +lemma openin_subtopology_self [simp]: "openin (subtopology euclidean S) S" + by (metis openin_topspace topspace_euclidean_subtopology) + +subsubsection\The most basic facts about the usual topology and metric on R\ + +abbreviation euclideanreal :: "real topology" + where "euclideanreal \ topology open" + +lemma real_openin [simp]: "openin euclideanreal S = open S" + by (simp add: euclidean_def open_openin) + +lemma topspace_euclideanreal [simp]: "topspace euclideanreal = UNIV" + using openin_subset open_UNIV real_openin by blast + +lemma topspace_euclideanreal_subtopology [simp]: + "topspace (subtopology euclideanreal S) = S" + by (simp add: topspace_subtopology) + +lemma real_closedin [simp]: "closedin euclideanreal S = closed S" + by (simp add: closed_closedin euclidean_def) + +subsection \Basic "localization" results are handy for connectedness.\ + +lemma openin_open: "openin (subtopology euclidean U) S \ (\T. open T \ (S = U \ T))" + by (auto simp: openin_subtopology) + +lemma openin_Int_open: + "\openin (subtopology euclidean U) S; open T\ + \ openin (subtopology euclidean U) (S \ T)" +by (metis open_Int Int_assoc openin_open) + +lemma openin_open_Int[intro]: "open S \ openin (subtopology euclidean U) (U \ S)" + by (auto simp: openin_open) + +lemma open_openin_trans[trans]: + "open S \ open T \ T \ S \ openin (subtopology euclidean S) T" + by (metis Int_absorb1 openin_open_Int) + +lemma open_subset: "S \ T \ open S \ openin (subtopology euclidean T) S" + by (auto simp: openin_open) + +lemma closedin_closed: "closedin (subtopology euclidean U) S \ (\T. closed T \ S = U \ T)" + by (simp add: closedin_subtopology Int_ac) + +lemma closedin_closed_Int: "closed S \ closedin (subtopology euclidean U) (U \ S)" + by (metis closedin_closed) + +lemma closed_subset: "S \ T \ closed S \ closedin (subtopology euclidean T) S" + by (auto simp: closedin_closed) + +lemma closedin_closed_subset: + "\closedin (subtopology euclidean U) V; T \ U; S = V \ T\ + \ closedin (subtopology euclidean T) S" + by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE) + +lemma finite_imp_closedin: + fixes S :: "'a::t1_space set" + shows "\finite S; S \ T\ \ closedin (subtopology euclidean T) S" + by (simp add: finite_imp_closed closed_subset) + +lemma closedin_singleton [simp]: + fixes a :: "'a::t1_space" + shows "closedin (subtopology euclidean U) {a} \ a \ U" +using closedin_subset by (force intro: closed_subset) + +lemma openin_euclidean_subtopology_iff: + fixes S U :: "'a::metric_space set" + shows "openin (subtopology euclidean U) S \ + S \ U \ (\x\S. \e>0. \x'\U. dist x' x < e \ x'\ S)" + (is "?lhs \ ?rhs") +proof + assume ?lhs + then show ?rhs + unfolding openin_open open_dist by blast +next + define T where "T = {x. \a\S. \d>0. (\y\U. dist y a < d \ y \ S) \ dist x a < d}" + have 1: "\x\T. \e>0. \y. dist y x < e \ y \ T" + unfolding T_def + apply clarsimp + apply (rule_tac x="d - dist x a" in exI) + apply (clarsimp simp add: less_diff_eq) + by (metis dist_commute dist_triangle_lt) + assume ?rhs then have 2: "S = U \ T" + unfolding T_def + by auto (metis dist_self) + from 1 2 show ?lhs + unfolding openin_open open_dist by fast +qed + +lemma connected_openin: + "connected S \ + \(\E1 E2. openin (subtopology euclidean S) E1 \ + openin (subtopology euclidean S) E2 \ + S \ E1 \ E2 \ E1 \ E2 = {} \ E1 \ {} \ E2 \ {})" + apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe) + by (simp_all, blast+) (* SLOW *) + +lemma connected_openin_eq: + "connected S \ + \(\E1 E2. openin (subtopology euclidean S) E1 \ + openin (subtopology euclidean S) E2 \ + E1 \ E2 = S \ E1 \ E2 = {} \ + E1 \ {} \ E2 \ {})" + apply (simp add: connected_openin, safe, blast) + by (metis Int_lower1 Un_subset_iff openin_open subset_antisym) + +lemma connected_closedin: + "connected S \ + (\E1 E2. + closedin (subtopology euclidean S) E1 \ + closedin (subtopology euclidean S) E2 \ + S \ E1 \ E2 \ E1 \ E2 = {} \ E1 \ {} \ E2 \ {})" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + by (auto simp add: connected_closed closedin_closed) +next + assume R: ?rhs + then show ?lhs + proof (clarsimp simp add: connected_closed closedin_closed) + fix A B + assume s_sub: "S \ A \ B" "B \ S \ {}" + and disj: "A \ B \ S = {}" + and cl: "closed A" "closed B" + have "S \ (A \ B) = S" + using s_sub(1) by auto + have "S - A = B \ S" + using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto + then have "S \ A = {}" + by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int R cl closedin_closed_Int inf_commute order_refl s_sub(2)) + then show "A \ S = {}" + by blast + qed +qed + +lemma connected_closedin_eq: + "connected S \ + \(\E1 E2. + closedin (subtopology euclidean S) E1 \ + closedin (subtopology euclidean S) E2 \ + E1 \ E2 = S \ E1 \ E2 = {} \ + E1 \ {} \ E2 \ {})" + apply (simp add: connected_closedin, safe, blast) + by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym) + +text \These "transitivity" results are handy too\ + +lemma openin_trans[trans]: + "openin (subtopology euclidean T) S \ openin (subtopology euclidean U) T \ + openin (subtopology euclidean U) S" + unfolding open_openin openin_open by blast + +lemma openin_open_trans: "openin (subtopology euclidean T) S \ open T \ open S" + by (auto simp: openin_open intro: openin_trans) + +lemma closedin_trans[trans]: + "closedin (subtopology euclidean T) S \ closedin (subtopology euclidean U) T \ + closedin (subtopology euclidean U) S" + by (auto simp: closedin_closed closed_Inter Int_assoc) + +lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \ closed T \ closed S" + by (auto simp: closedin_closed intro: closedin_trans) + +lemma openin_subtopology_Int_subset: + "\openin (subtopology euclidean u) (u \ S); v \ u\ \ openin (subtopology euclidean v) (v \ S)" + by (auto simp: openin_subtopology) + +lemma openin_open_eq: "open s \ (openin (subtopology euclidean s) t \ open t \ t \ s)" + using open_subset openin_open_trans openin_subset by fastforce + subsection\Derived set (set of limit points)\ @@ -2774,7 +3353,7 @@ obtain \ where \: "finite \" "\ \ \" "S \ \\" proof - have 1: "\U\\. openin X U" - unfolding \_def using \ cont continuous_map by blast + unfolding \_def using \ cont[unfolded continuous_map] by blast have 2: "S \ \\" unfolding \_def using compactin_subset_topspace cpt \ by fastforce show thesis @@ -2881,4 +3460,97 @@ unfolding embedding_map_def using homeomorphic_space by blast +subsection \Continuity\ + +lemma continuous_on_open: + "continuous_on S f \ + (\T. openin (subtopology euclidean (f ` S)) T \ + openin (subtopology euclidean S) (S \ f -` T))" + unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute + by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong) + +lemma continuous_on_closed: + "continuous_on S f \ + (\T. closedin (subtopology euclidean (f ` S)) T \ + closedin (subtopology euclidean S) (S \ f -` T))" + unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute + by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong) + +lemma continuous_on_imp_closedin: + assumes "continuous_on S f" "closedin (subtopology euclidean (f ` S)) T" + shows "closedin (subtopology euclidean S) (S \ f -` T)" + using assms continuous_on_closed by blast + +subsection%unimportant \Half-global and completely global cases\ + +lemma continuous_openin_preimage_gen: + assumes "continuous_on S f" "open T" + shows "openin (subtopology euclidean S) (S \ f -` T)" +proof - + have *: "(S \ f -` T) = (S \ f -` (T \ f ` S))" + by auto + have "openin (subtopology euclidean (f ` S)) (T \ f ` S)" + using openin_open_Int[of T "f ` S", OF assms(2)] unfolding openin_open by auto + then show ?thesis + using assms(1)[unfolded continuous_on_open, THEN spec[where x="T \ f ` S"]] + using * by auto +qed + +lemma continuous_closedin_preimage: + assumes "continuous_on S f" and "closed T" + shows "closedin (subtopology euclidean S) (S \ f -` T)" +proof - + have *: "(S \ f -` T) = (S \ f -` (T \ f ` S))" + by auto + have "closedin (subtopology euclidean (f ` S)) (T \ f ` S)" + using closedin_closed_Int[of T "f ` S", OF assms(2)] + by (simp add: Int_commute) + then show ?thesis + using assms(1)[unfolded continuous_on_closed, THEN spec[where x="T \ f ` S"]] + using * by auto +qed + +lemma continuous_openin_preimage_eq: + "continuous_on S f \ + (\T. open T \ openin (subtopology euclidean S) (S \ f -` T))" +apply safe +apply (simp add: continuous_openin_preimage_gen) +apply (fastforce simp add: continuous_on_open openin_open) +done + +lemma continuous_closedin_preimage_eq: + "continuous_on S f \ + (\T. closed T \ closedin (subtopology euclidean S) (S \ f -` T))" +apply safe +apply (simp add: continuous_closedin_preimage) +apply (fastforce simp add: continuous_on_closed closedin_closed) +done + +lemma continuous_open_preimage: + assumes contf: "continuous_on S f" and "open S" "open T" + shows "open (S \ f -` T)" +proof- + obtain U where "open U" "(S \ f -` T) = S \ U" + using continuous_openin_preimage_gen[OF contf \open T\] + unfolding openin_open by auto + then show ?thesis + using open_Int[of S U, OF \open S\] by auto +qed + +lemma continuous_closed_preimage: + assumes contf: "continuous_on S f" and "closed S" "closed T" + shows "closed (S \ f -` T)" +proof- + obtain U where "closed U" "(S \ f -` T) = S \ U" + using continuous_closedin_preimage[OF contf \closed T\] + unfolding closedin_closed by auto + then show ?thesis using closed_Int[of S U, OF \closed S\] by auto +qed + +lemma continuous_open_vimage: "open S \ (\x. continuous (at x) f) \ open (f -` S)" + by (metis continuous_on_eq_continuous_within open_vimage) + +lemma continuous_closed_vimage: "closed S \ (\x. continuous (at x) f) \ closed (f -` S)" + by (simp add: closed_vimage continuous_on_eq_continuous_within) + end diff -r c2d5575d9da5 -r 5aa5a8d6e5b5 src/HOL/Analysis/Connected.thy --- a/src/HOL/Analysis/Connected.thy Sat Dec 29 18:40:29 2018 +0000 +++ b/src/HOL/Analysis/Connected.thy Sat Dec 29 20:32:09 2018 +0100 @@ -5,7 +5,9 @@ section \Connected Components, Homeomorphisms, Baire property, etc\ theory Connected -imports Topology_Euclidean_Space + imports + "HOL-Library.Indicator_Function" + Topology_Euclidean_Space begin subsection%unimportant \More properties of closed balls, spheres, etc\ diff -r c2d5575d9da5 -r 5aa5a8d6e5b5 src/HOL/Analysis/Elementary_Metric_Spaces.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Sat Dec 29 20:32:09 2018 +0100 @@ -0,0 +1,1840 @@ +(* Author: L C Paulson, University of Cambridge + Author: Amine Chaieb, University of Cambridge + Author: Robert Himmelmann, TU Muenchen + Author: Brian Huffman, Portland State University +*) + +section \Elementary Metric Spaces\ + +theory Elementary_Metric_Spaces + imports + Elementary_Topology + Abstract_Topology +begin + +(* FIXME: move elsewhere *) + +lemma approachable_lt_le: "(\(d::real) > 0. \x. f x < d \ P x) \ (\d>0. \x. f x \ d \ P x)" + apply auto + apply (rule_tac x="d/2" in exI) + apply auto + done + +lemma approachable_lt_le2: \ \like the above, but pushes aside an extra formula\ + "(\(d::real) > 0. \x. Q x \ f x < d \ P x) \ (\d>0. \x. f x \ d \ Q x \ P x)" + apply auto + apply (rule_tac x="d/2" in exI, auto) + done + +lemma triangle_lemma: + fixes x y z :: real + assumes x: "0 \ x" + and y: "0 \ y" + and z: "0 \ z" + and xy: "x\<^sup>2 \ y\<^sup>2 + z\<^sup>2" + shows "x \ y + z" +proof - + have "y\<^sup>2 + z\<^sup>2 \ y\<^sup>2 + 2 * y * z + z\<^sup>2" + using z y by simp + with xy have th: "x\<^sup>2 \ (y + z)\<^sup>2" + by (simp add: power2_eq_square field_simps) + from y z have yz: "y + z \ 0" + by arith + from power2_le_imp_le[OF th yz] show ?thesis . +qed + +subsection \Combination of Elementary and Abstract Topology\ + +lemma closedin_limpt: + "closedin (subtopology euclidean T) S \ S \ T \ (\x. x islimpt S \ x \ T \ x \ S)" + apply (simp add: closedin_closed, safe) + apply (simp add: closed_limpt islimpt_subset) + apply (rule_tac x="closure S" in exI, simp) + apply (force simp: closure_def) + done + +lemma closedin_closed_eq: "closed S \ closedin (subtopology euclidean S) T \ closed T \ T \ S" + by (meson closedin_limpt closed_subset closedin_closed_trans) + +lemma connected_closed_set: + "closed S + \ connected S \ (\A B. closed A \ closed B \ A \ {} \ B \ {} \ A \ B = S \ A \ B = {})" + unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast + +text \If a connnected set is written as the union of two nonempty closed sets, then these sets +have to intersect.\ + +lemma connected_as_closed_union: + assumes "connected C" "C = A \ B" "closed A" "closed B" "A \ {}" "B \ {}" + shows "A \ B \ {}" +by (metis assms closed_Un connected_closed_set) + +lemma closedin_subset_trans: + "closedin (subtopology euclidean U) S \ S \ T \ T \ U \ + closedin (subtopology euclidean T) S" + by (meson closedin_limpt subset_iff) + +lemma openin_subset_trans: + "openin (subtopology euclidean U) S \ S \ T \ T \ U \ + openin (subtopology euclidean T) S" + by (auto simp: openin_open) + +lemma openin_Times: + "openin (subtopology euclidean S) S' \ openin (subtopology euclidean T) T' \ + openin (subtopology euclidean (S \ T)) (S' \ T')" + unfolding openin_open using open_Times by blast + + +subsubsection \Closure\ + +lemma closure_openin_Int_closure: + assumes ope: "openin (subtopology euclidean U) S" and "T \ U" + shows "closure(S \ closure T) = closure(S \ T)" +proof + obtain V where "open V" and S: "S = U \ V" + using ope using openin_open by metis + show "closure (S \ closure T) \ closure (S \ T)" + proof (clarsimp simp: S) + fix x + assume "x \ closure (U \ V \ closure T)" + then have "V \ closure T \ A \ x \ closure A" for A + by (metis closure_mono subsetD inf.coboundedI2 inf_assoc) + then have "x \ closure (T \ V)" + by (metis \open V\ closure_closure inf_commute open_Int_closure_subset) + then show "x \ closure (U \ V \ T)" + by (metis \T \ U\ inf.absorb_iff2 inf_assoc inf_commute) + qed +next + show "closure (S \ T) \ closure (S \ closure T)" + by (meson Int_mono closure_mono closure_subset order_refl) +qed + +corollary infinite_openin: + fixes S :: "'a :: t1_space set" + shows "\openin (subtopology euclidean U) S; x \ S; x islimpt U\ \ infinite S" + by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute) + +subsubsection \Frontier\ + +lemma connected_Int_frontier: + "\connected s; s \ t \ {}; s - t \ {}\ \ (s \ frontier t \ {})" + apply (simp add: frontier_interiors connected_openin, safe) + apply (drule_tac x="s \ interior t" in spec, safe) + apply (drule_tac [2] x="s \ interior (-t)" in spec) + apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD]) + done + +subsubsection \Compactness\ + +lemma openin_delete: + fixes a :: "'a :: t1_space" + shows "openin (subtopology euclidean u) s + \ openin (subtopology euclidean u) (s - {a})" +by (metis Int_Diff open_delete openin_open) + + +subsection \Continuity\ + +lemma interior_image_subset: + assumes "inj f" "\x. continuous (at x) f" + shows "interior (f ` S) \ f ` (interior S)" +proof + fix x assume "x \ interior (f ` S)" + then obtain T where as: "open T" "x \ T" "T \ f ` S" .. + then have "x \ f ` S" by auto + then obtain y where y: "y \ S" "x = f y" by auto + have "open (f -` T)" + using assms \open T\ by (simp add: continuous_at_imp_continuous_on open_vimage) + moreover have "y \ vimage f T" + using \x = f y\ \x \ T\ by simp + moreover have "vimage f T \ S" + using \T \ image f S\ \inj f\ unfolding inj_on_def subset_eq by auto + ultimately have "y \ interior S" .. + with \x = f y\ show "x \ f ` interior S" .. +qed + +subsection \Open and closed balls\ + +definition%important ball :: "'a::metric_space \ real \ 'a set" + where "ball x e = {y. dist x y < e}" + +definition%important cball :: "'a::metric_space \ real \ 'a set" + where "cball x e = {y. dist x y \ e}" + +definition%important sphere :: "'a::metric_space \ real \ 'a set" + where "sphere x e = {y. dist x y = e}" + +lemma mem_ball [simp]: "y \ ball x e \ dist x y < e" + by (simp add: ball_def) + +lemma mem_cball [simp]: "y \ cball x e \ dist x y \ e" + by (simp add: cball_def) + +lemma mem_sphere [simp]: "y \ sphere x e \ dist x y = e" + by (simp add: sphere_def) + +lemma ball_trivial [simp]: "ball x 0 = {}" + by (simp add: ball_def) + +lemma cball_trivial [simp]: "cball x 0 = {x}" + by (simp add: cball_def) + +lemma sphere_trivial [simp]: "sphere x 0 = {x}" + by (simp add: sphere_def) + +lemma mem_ball_0 [simp]: "x \ ball 0 e \ norm x < e" + for x :: "'a::real_normed_vector" + by (simp add: dist_norm) + +lemma mem_cball_0 [simp]: "x \ cball 0 e \ norm x \ e" + for x :: "'a::real_normed_vector" + by (simp add: dist_norm) + +lemma disjoint_ballI: "dist x y \ r+s \ ball x r \ ball y s = {}" + using dist_triangle_less_add not_le by fastforce + +lemma disjoint_cballI: "dist x y > r + s \ cball x r \ cball y s = {}" + by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball) + +lemma mem_sphere_0 [simp]: "x \ sphere 0 e \ norm x = e" + for x :: "'a::real_normed_vector" + by (simp add: dist_norm) + +lemma sphere_empty [simp]: "r < 0 \ sphere a r = {}" + for a :: "'a::metric_space" + by auto + +lemma centre_in_ball [simp]: "x \ ball x e \ 0 < e" + by simp + +lemma centre_in_cball [simp]: "x \ cball x e \ 0 \ e" + by simp + +lemma ball_subset_cball [simp, intro]: "ball x e \ cball x e" + by (simp add: subset_eq) + +lemma mem_ball_imp_mem_cball: "x \ ball y e \ x \ cball y e" + by (auto simp: mem_ball mem_cball) + +lemma sphere_cball [simp,intro]: "sphere z r \ cball z r" + by force + +lemma cball_diff_sphere: "cball a r - sphere a r = ball a r" + by auto + +lemma subset_ball[intro]: "d \ e \ ball x d \ ball x e" + by (simp add: subset_eq) + +lemma subset_cball[intro]: "d \ e \ cball x d \ cball x e" + by (simp add: subset_eq) + +lemma mem_ball_leI: "x \ ball y e \ e \ f \ x \ ball y f" + by (auto simp: mem_ball mem_cball) + +lemma mem_cball_leI: "x \ cball y e \ e \ f \ x \ cball y f" + by (auto simp: mem_ball mem_cball) + +lemma cball_trans: "y \ cball z b \ x \ cball y a \ x \ cball z (b + a)" + unfolding mem_cball +proof - + have "dist z x \ dist z y + dist y x" + by (rule dist_triangle) + also assume "dist z y \ b" + also assume "dist y x \ a" + finally show "dist z x \ b + a" by arith +qed + +lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s" + by (simp add: set_eq_iff) arith + +lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s" + by (simp add: set_eq_iff) + +lemma cball_max_Un: "cball a (max r s) = cball a r \ cball a s" + by (simp add: set_eq_iff) arith + +lemma cball_min_Int: "cball a (min r s) = cball a r \ cball a s" + by (simp add: set_eq_iff) + +lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r" + by (auto simp: cball_def ball_def dist_commute) + +lemma image_add_ball [simp]: + fixes a :: "'a::real_normed_vector" + shows "(+) b ` ball a r = ball (a+b) r" +apply (intro equalityI subsetI) +apply (force simp: dist_norm) +apply (rule_tac x="x-b" in image_eqI) +apply (auto simp: dist_norm algebra_simps) +done + +lemma image_add_cball [simp]: + fixes a :: "'a::real_normed_vector" + shows "(+) b ` cball a r = cball (a+b) r" +apply (intro equalityI subsetI) +apply (force simp: dist_norm) +apply (rule_tac x="x-b" in image_eqI) +apply (auto simp: dist_norm algebra_simps) +done + +lemma open_ball [intro, simp]: "open (ball x e)" +proof - + have "open (dist x -` {.. (\x\S. \e>0. ball x e \ S)" + by (simp add: open_dist subset_eq mem_ball Ball_def dist_commute) + +lemma openI [intro?]: "(\x. x\S \ \e>0. ball x e \ S) \ open S" + by (auto simp: open_contains_ball) + +lemma openE[elim?]: + assumes "open S" "x\S" + obtains e where "e>0" "ball x e \ S" + using assms unfolding open_contains_ball by auto + +lemma open_contains_ball_eq: "open S \ x\S \ (\e>0. ball x e \ S)" + by (metis open_contains_ball subset_eq centre_in_ball) + +lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0" + unfolding mem_ball set_eq_iff + apply (simp add: not_less) + apply (metis zero_le_dist order_trans dist_self) + done + +lemma ball_empty: "e \ 0 \ ball x e = {}" by simp + +lemma closed_cball [iff]: "closed (cball x e)" +proof - + have "closed (dist x -` {..e})" + by (intro closed_vimage closed_atMost continuous_intros) + also have "dist x -` {..e} = cball x e" + by auto + finally show ?thesis . +qed + +lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)" +proof - + { + fix x and e::real + assume "x\S" "e>0" "ball x e \ S" + then have "\d>0. cball x d \ S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto) + } + moreover + { + fix x and e::real + assume "x\S" "e>0" "cball x e \ S" + then have "\d>0. ball x d \ S" + unfolding subset_eq + apply (rule_tac x="e/2" in exI, auto) + done + } + ultimately show ?thesis + unfolding open_contains_ball by auto +qed + +lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\e>0. cball x e \ S))" + by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball) + +lemma eventually_nhds_ball: "d > 0 \ eventually (\x. x \ ball z d) (nhds z)" + by (rule eventually_nhds_in_open) simp_all + +lemma eventually_at_ball: "d > 0 \ eventually (\t. t \ ball z d \ t \ A) (at z within A)" + unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute) + +lemma eventually_at_ball': "d > 0 \ eventually (\t. t \ ball z d \ t \ z \ t \ A) (at z within A)" + unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute) + +lemma at_within_ball: "e > 0 \ dist x y < e \ at y within ball x e = at y" + by (subst at_within_open) auto + +lemma atLeastAtMost_eq_cball: + fixes a b::real + shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)" + by (auto simp: dist_real_def field_simps mem_cball) + +lemma greaterThanLessThan_eq_ball: + fixes a b::real + shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)" + by (auto simp: dist_real_def field_simps mem_ball) + + +subsection \Limit Points\ + +lemma islimpt_approachable: + fixes x :: "'a::metric_space" + shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" + unfolding islimpt_iff_eventually eventually_at by fast + +lemma islimpt_approachable_le: "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)" + for x :: "'a::metric_space" + unfolding islimpt_approachable + using approachable_lt_le [where f="\y. dist y x" and P="\y. y \ S \ y = x", + THEN arg_cong [where f=Not]] + by (simp add: Bex_def conj_commute conj_left_commute) + +lemma perfect_choose_dist: "0 < r \ \a. a \ x \ dist a x < r" + for x :: "'a::{perfect_space,metric_space}" + using islimpt_UNIV [of x] by (simp add: islimpt_approachable) + +lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \ x islimpt S" + for x :: "'a::metric_space" + apply (clarsimp simp add: islimpt_approachable) + apply (drule_tac x="e/2" in spec) + apply (auto simp: simp del: less_divide_eq_numeral1) + apply (drule_tac x="dist x' x" in spec) + apply (auto simp: zero_less_dist_iff simp del: less_divide_eq_numeral1) + apply (erule rev_bexI) + apply (metis dist_commute dist_triangle_half_r less_trans less_irrefl) + done + +lemma closed_limpts: "closed {x::'a::metric_space. x islimpt S}" + using closed_limpt limpt_of_limpts by blast + +lemma limpt_of_closure: "x islimpt closure S \ x islimpt S" + for x :: "'a::metric_space" + by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts) + +lemma islimpt_eq_infinite_ball: "x islimpt S \ (\e>0. infinite(S \ ball x e))" + apply (simp add: islimpt_eq_acc_point, safe) + apply (metis Int_commute open_ball centre_in_ball) + by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl) + +lemma islimpt_eq_infinite_cball: "x islimpt S \ (\e>0. infinite(S \ cball x e))" + apply (simp add: islimpt_eq_infinite_ball, safe) + apply (meson Int_mono ball_subset_cball finite_subset order_refl) + by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq) + + +subsection \?\ + +lemma finite_ball_include: + fixes a :: "'a::metric_space" + assumes "finite S" + shows "\e>0. S \ ball a e" + using assms +proof induction + case (insert x S) + then obtain e0 where "e0>0" and e0:"S \ ball a e0" by auto + define e where "e = max e0 (2 * dist a x)" + have "e>0" unfolding e_def using \e0>0\ by auto + moreover have "insert x S \ ball a e" + using e0 \e>0\ unfolding e_def by auto + ultimately show ?case by auto +qed (auto intro: zero_less_one) + +lemma finite_set_avoid: + fixes a :: "'a::metric_space" + assumes "finite S" + shows "\d>0. \x\S. x \ a \ d \ dist a x" + using assms +proof induction + case (insert x S) + then obtain d where "d > 0" and d: "\x\S. x \ a \ d \ dist a x" + by blast + show ?case + proof (cases "x = a") + case True + with \d > 0 \d show ?thesis by auto + next + case False + let ?d = "min d (dist a x)" + from False \d > 0\ have dp: "?d > 0" + by auto + from d have d': "\x\S. x \ a \ ?d \ dist a x" + by auto + with dp False show ?thesis + by (metis insert_iff le_less min_less_iff_conj not_less) + qed +qed (auto intro: zero_less_one) + +lemma discrete_imp_closed: + fixes S :: "'a::metric_space set" + assumes e: "0 < e" + and d: "\x \ S. \y \ S. dist y x < e \ y = x" + shows "closed S" +proof - + have False if C: "\e. e>0 \ \x'\S. x' \ x \ dist x' x < e" for x + proof - + from e have e2: "e/2 > 0" by arith + from C[rule_format, OF e2] obtain y where y: "y \ S" "y \ x" "dist y x < e/2" + by blast + let ?m = "min (e/2) (dist x y) " + from e2 y(2) have mp: "?m > 0" + by simp + from C[OF mp] obtain z where z: "z \ S" "z \ x" "dist z x < ?m" + by blast + from z y have "dist z y < e" + by (intro dist_triangle_lt [where z=x]) simp + from d[rule_format, OF y(1) z(1) this] y z show ?thesis + by (auto simp: dist_commute) + qed + then show ?thesis + by (metis islimpt_approachable closed_limpt [where 'a='a]) +qed + + +subsection \Interior\ + +lemma mem_interior: "x \ interior S \ (\e>0. ball x e \ S)" + using open_contains_ball_eq [where S="interior S"] + by (simp add: open_subset_interior) + + +subsection \Frontier\ + +lemma frontier_straddle: + fixes a :: "'a::metric_space" + shows "a \ frontier S \ (\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e))" + unfolding frontier_def closure_interior + by (auto simp: mem_interior subset_eq ball_def) + + +subsection \Limits\ + +proposition Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)" + by (auto simp: tendsto_iff trivial_limit_eq) + +text \Show that they yield usual definitions in the various cases.\ + +proposition Lim_within_le: "(f \ l)(at a within S) \ + (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)" + by (auto simp: tendsto_iff eventually_at_le) + +proposition Lim_within: "(f \ l) (at a within S) \ + (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" + by (auto simp: tendsto_iff eventually_at) + +corollary Lim_withinI [intro?]: + assumes "\e. e > 0 \ \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l \ e" + shows "(f \ l) (at a within S)" + apply (simp add: Lim_within, clarify) + apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) + done + +proposition Lim_at: "(f \ l) (at a) \ + (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" + by (auto simp: tendsto_iff eventually_at) + +lemma Lim_transform_within_set: + fixes a :: "'a::metric_space" and l :: "'b::metric_space" + shows "\(f \ l) (at a within S); eventually (\x. x \ S \ x \ T) (at a)\ + \ (f \ l) (at a within T)" +apply (clarsimp simp: eventually_at Lim_within) +apply (drule_tac x=e in spec, clarify) +apply (rename_tac k) +apply (rule_tac x="min d k" in exI, simp) +done + +text \Another limit point characterization.\ + +lemma limpt_sequential_inj: + fixes x :: "'a::metric_space" + shows "x islimpt S \ + (\f. (\n::nat. f n \ S - {x}) \ inj f \ (f \ x) sequentially)" + (is "?lhs = ?rhs") +proof + assume ?lhs + then have "\e>0. \x'\S. x' \ x \ dist x' x < e" + by (force simp: islimpt_approachable) + then obtain y where y: "\e. e>0 \ y e \ S \ y e \ x \ dist (y e) x < e" + by metis + define f where "f \ rec_nat (y 1) (\n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))" + have [simp]: "f 0 = y 1" + "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n + by (simp_all add: f_def) + have f: "f n \ S \ (f n \ x) \ dist (f n) x < inverse(2 ^ n)" for n + proof (induction n) + case 0 show ?case + by (simp add: y) + next + case (Suc n) then show ?case + apply (auto simp: y) + by (metis half_gt_zero_iff inverse_positive_iff_positive less_divide_eq_numeral1(1) min_less_iff_conj y zero_less_dist_iff zero_less_numeral zero_less_power) + qed + show ?rhs + proof (rule_tac x=f in exI, intro conjI allI) + show "\n. f n \ S - {x}" + using f by blast + have "dist (f n) x < dist (f m) x" if "m < n" for m n + using that + proof (induction n) + case 0 then show ?case by simp + next + case (Suc n) + then consider "m < n" | "m = n" using less_Suc_eq by blast + then show ?case + proof cases + assume "m < n" + have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x" + by simp + also have "\ < dist (f n) x" + by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y) + also have "\ < dist (f m) x" + using Suc.IH \m < n\ by blast + finally show ?thesis . + next + assume "m = n" then show ?case + by simp (metis dist_pos_lt f half_gt_zero_iff inverse_positive_iff_positive min_less_iff_conj y zero_less_numeral zero_less_power) + qed + qed + then show "inj f" + by (metis less_irrefl linorder_injI) + show "f \ x" + apply (rule tendstoI) + apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI) + apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]]) + apply (simp add: field_simps) + by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power) + qed +next + assume ?rhs + then show ?lhs + by (fastforce simp add: islimpt_approachable lim_sequentially) +qed + +lemma Lim_dist_ubound: + assumes "\(trivial_limit net)" + and "(f \ l) net" + and "eventually (\x. dist a (f x) \ e) net" + shows "dist a l \ e" + using assms by (fast intro: tendsto_le tendsto_intros) + + +subsection \Closure and Limit Characterization\ + +lemma closure_approachable: + fixes S :: "'a::metric_space set" + shows "x \ closure S \ (\e>0. \y\S. dist y x < e)" + apply (auto simp: closure_def islimpt_approachable) + apply (metis dist_self) + done + +lemma closure_approachable_le: + fixes S :: "'a::metric_space set" + shows "x \ closure S \ (\e>0. \y\S. dist y x \ e)" + unfolding closure_approachable + using dense by force + +lemma closure_approachableD: + assumes "x \ closure S" "e>0" + shows "\y\S. dist x y < e" + using assms unfolding closure_approachable by (auto simp: dist_commute) + +lemma closed_approachable: + fixes S :: "'a::metric_space set" + shows "closed S \ (\e>0. \y\S. dist y x < e) \ x \ S" + by (metis closure_closed closure_approachable) + +lemma closure_contains_Inf: + fixes S :: "real set" + assumes "S \ {}" "bdd_below S" + shows "Inf S \ closure S" +proof - + have *: "\x\S. Inf S \ x" + using cInf_lower[of _ S] assms by metis + { + fix e :: real + assume "e > 0" + then have "Inf S < Inf S + e" by simp + with assms obtain x where "x \ S" "x < Inf S + e" + by (subst (asm) cInf_less_iff) auto + with * have "\x\S. dist x (Inf S) < e" + by (intro bexI[of _ x]) (auto simp: dist_real_def) + } + then show ?thesis unfolding closure_approachable by auto +qed + +lemma not_trivial_limit_within_ball: + "\ trivial_limit (at x within S) \ (\e>0. S \ ball x e - {x} \ {})" + (is "?lhs \ ?rhs") +proof + show ?rhs if ?lhs + proof - + { + fix e :: real + assume "e > 0" + then obtain y where "y \ S - {x}" and "dist y x < e" + using \?lhs\ not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] + by auto + then have "y \ S \ ball x e - {x}" + unfolding ball_def by (simp add: dist_commute) + then have "S \ ball x e - {x} \ {}" by blast + } + then show ?thesis by auto + qed + show ?lhs if ?rhs + proof - + { + fix e :: real + assume "e > 0" + then obtain y where "y \ S \ ball x e - {x}" + using \?rhs\ by blast + then have "y \ S - {x}" and "dist y x < e" + unfolding ball_def by (simp_all add: dist_commute) + then have "\y \ S - {x}. dist y x < e" + by auto + } + then show ?thesis + using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] + by auto + qed +qed + +subsection \Boundedness\ + + (* FIXME: This has to be unified with BSEQ!! *) +definition%important (in metric_space) bounded :: "'a set \ bool" + where "bounded S \ (\x e. \y\S. dist x y \ e)" + +lemma bounded_subset_cball: "bounded S \ (\e x. S \ cball x e \ 0 \ e)" + unfolding bounded_def subset_eq by auto (meson order_trans zero_le_dist) + +lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)" + unfolding bounded_def + by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le) + +lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)" + unfolding bounded_any_center [where a=0] + by (simp add: dist_norm) + +lemma bdd_above_norm: "bdd_above (norm ` X) \ bounded X" + by (simp add: bounded_iff bdd_above_def) + +lemma bounded_norm_comp: "bounded ((\x. norm (f x)) ` S) = bounded (f ` S)" + by (simp add: bounded_iff) + +lemma boundedI: + assumes "\x. x \ S \ norm x \ B" + shows "bounded S" + using assms bounded_iff by blast + +lemma bounded_empty [simp]: "bounded {}" + by (simp add: bounded_def) + +lemma bounded_subset: "bounded T \ S \ T \ bounded S" + by (metis bounded_def subset_eq) + +lemma bounded_interior[intro]: "bounded S \ bounded(interior S)" + by (metis bounded_subset interior_subset) + +lemma bounded_closure[intro]: + assumes "bounded S" + shows "bounded (closure S)" +proof - + from assms obtain x and a where a: "\y\S. dist x y \ a" + unfolding bounded_def by auto + { + fix y + assume "y \ closure S" + then obtain f where f: "\n. f n \ S" "(f \ y) sequentially" + unfolding closure_sequential by auto + have "\n. f n \ S \ dist x (f n) \ a" using a by simp + then have "eventually (\n. dist x (f n) \ a) sequentially" + by (simp add: f(1)) + have "dist x y \ a" + apply (rule Lim_dist_ubound [of sequentially f]) + apply (rule trivial_limit_sequentially) + apply (rule f(2)) + apply fact + done + } + then show ?thesis + unfolding bounded_def by auto +qed + +lemma bounded_closure_image: "bounded (f ` closure S) \ bounded (f ` S)" + by (simp add: bounded_subset closure_subset image_mono) + +lemma bounded_cball[simp,intro]: "bounded (cball x e)" + apply (simp add: bounded_def) + apply (rule_tac x=x in exI) + apply (rule_tac x=e in exI, auto) + done + +lemma bounded_ball[simp,intro]: "bounded (ball x e)" + by (metis ball_subset_cball bounded_cball bounded_subset) + +lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T" + by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj) + +lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)" + by (induct rule: finite_induct[of F]) auto + +lemma bounded_UN [intro]: "finite A \ \x\A. bounded (B x) \ bounded (\x\A. B x)" + by (induct set: finite) auto + +lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S" +proof - + have "\y\{x}. dist x y \ 0" + by simp + then have "bounded {x}" + unfolding bounded_def by fast + then show ?thesis + by (metis insert_is_Un bounded_Un) +qed + +lemma bounded_subset_ballI: "S \ ball x r \ bounded S" + by (meson bounded_ball bounded_subset) + +lemma bounded_subset_ballD: + assumes "bounded S" shows "\r. 0 < r \ S \ ball x r" +proof - + obtain e::real and y where "S \ cball y e" "0 \ e" + using assms by (auto simp: bounded_subset_cball) + then show ?thesis + apply (rule_tac x="dist x y + e + 1" in exI) + apply (simp add: add.commute add_pos_nonneg) + apply (erule subset_trans) + apply (clarsimp simp add: cball_def) + by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one) +qed + +lemma finite_imp_bounded [intro]: "finite S \ bounded S" + by (induct set: finite) simp_all + +lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)" + by (metis Int_lower1 Int_lower2 bounded_subset) + +lemma bounded_diff[intro]: "bounded S \ bounded (S - T)" + by (metis Diff_subset bounded_subset) + +lemma bounded_dist_comp: + assumes "bounded (f ` S)" "bounded (g ` S)" + shows "bounded ((\x. dist (f x) (g x)) ` S)" +proof - + from assms obtain M1 M2 where *: "dist (f x) undefined \ M1" "dist undefined (g x) \ M2" if "x \ S" for x + by (auto simp: bounded_any_center[of _ undefined] dist_commute) + have "dist (f x) (g x) \ M1 + M2" if "x \ S" for x + using *[OF that] + by (rule order_trans[OF dist_triangle add_mono]) + then show ?thesis + by (auto intro!: boundedI) +qed + + +subsection \Consequences for Real Numbers\ + +lemma closed_contains_Inf: + fixes S :: "real set" + shows "S \ {} \ bdd_below S \ closed S \ Inf S \ S" + by (metis closure_contains_Inf closure_closed) + +lemma closed_subset_contains_Inf: + fixes A C :: "real set" + shows "closed C \ A \ C \ A \ {} \ bdd_below A \ Inf A \ C" + by (metis closure_contains_Inf closure_minimal subset_eq) + +lemma atLeastAtMost_subset_contains_Inf: + fixes A :: "real set" and a b :: real + shows "A \ {} \ a \ b \ A \ {a..b} \ Inf A \ {a..b}" + by (rule closed_subset_contains_Inf) + (auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a]) + +subsection \Compactness\ + +lemma compact_imp_bounded: + assumes "compact U" + shows "bounded U" +proof - + have "compact U" "\x\U. open (ball x 1)" "U \ (\x\U. ball x 1)" + using assms by auto + then obtain D where D: "D \ U" "finite D" "U \ (\x\D. ball x 1)" + by (metis compactE_image) + from \finite D\ have "bounded (\x\D. ball x 1)" + by (simp add: bounded_UN) + then show "bounded U" using \U \ (\x\D. ball x 1)\ + by (rule bounded_subset) +qed + +lemma closure_Int_ball_not_empty: + assumes "S \ closure T" "x \ S" "r > 0" + shows "T \ ball x r \ {}" + using assms centre_in_ball closure_iff_nhds_not_empty by blast + +subsubsection\Totally bounded\ + +lemma cauchy_def: "Cauchy s \ (\e>0. \N. \m n. m \ N \ n \ N \ dist (s m) (s n) < e)" + unfolding Cauchy_def by metis + +proposition seq_compact_imp_totally_bounded: + assumes "seq_compact s" + shows "\e>0. \k. finite k \ k \ s \ s \ (\x\k. ball x e)" +proof - + { fix e::real assume "e > 0" assume *: "\k. finite k \ k \ s \ \ s \ (\x\k. ball x e)" + let ?Q = "\x n r. r \ s \ (\m < (n::nat). \ (dist (x m) r < e))" + have "\x. \n::nat. ?Q x n (x n)" + proof (rule dependent_wellorder_choice) + fix n x assume "\y. y < n \ ?Q x y (x y)" + then have "\ s \ (\x\x ` {0..s" "z \ (\x\x ` {0..r. ?Q x n r" + using z by auto + qed simp + then obtain x where "\n::nat. x n \ s" and x:"\n m. m < n \ \ (dist (x m) (x n) < e)" + by blast + then obtain l r where "l \ s" and r:"strict_mono r" and "((x \ r) \ l) sequentially" + using assms by (metis seq_compact_def) + from this(3) have "Cauchy (x \ r)" + using LIMSEQ_imp_Cauchy by auto + then obtain N::nat where "\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < e" + unfolding cauchy_def using \e > 0\ by blast + then have False + using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) } + then show ?thesis + by metis +qed + +subsubsection\Heine-Borel theorem\ + +proposition seq_compact_imp_Heine_Borel: + fixes s :: "'a :: metric_space set" + assumes "seq_compact s" + shows "compact s" +proof - + from seq_compact_imp_totally_bounded[OF \seq_compact s\] + obtain f where f: "\e>0. finite (f e) \ f e \ s \ s \ (\x\f e. ball x e)" + unfolding choice_iff' .. + define K where "K = (\(x, r). ball x r) ` ((\e \ \ \ {0 <..}. f e) \ \)" + have "countably_compact s" + using \seq_compact s\ by (rule seq_compact_imp_countably_compact) + then show "compact s" + proof (rule countably_compact_imp_compact) + show "countable K" + unfolding K_def using f + by (auto intro: countable_finite countable_subset countable_rat + intro!: countable_image countable_SIGMA countable_UN) + show "\b\K. open b" by (auto simp: K_def) + next + fix T x + assume T: "open T" "x \ T" and x: "x \ s" + from openE[OF T] obtain e where "0 < e" "ball x e \ T" + by auto + then have "0 < e / 2" "ball x (e / 2) \ T" + by auto + from Rats_dense_in_real[OF \0 < e / 2\] obtain r where "r \ \" "0 < r" "r < e / 2" + by auto + from f[rule_format, of r] \0 < r\ \x \ s\ obtain k where "k \ f r" "x \ ball k r" + by auto + from \r \ \\ \0 < r\ \k \ f r\ have "ball k r \ K" + by (auto simp: K_def) + then show "\b\K. x \ b \ b \ s \ T" + proof (rule bexI[rotated], safe) + fix y + assume "y \ ball k r" + with \r < e / 2\ \x \ ball k r\ have "dist x y < e" + by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute) + with \ball x e \ T\ show "y \ T" + by auto + next + show "x \ ball k r" by fact + qed + qed +qed + +proposition compact_eq_seq_compact_metric: + "compact (s :: 'a::metric_space set) \ seq_compact s" + using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast + +proposition compact_def: \ \this is the definition of compactness in HOL Light\ + "compact (S :: 'a::metric_space set) \ + (\f. (\n. f n \ S) \ (\l\S. \r::nat\nat. strict_mono r \ (f \ r) \ l))" + unfolding compact_eq_seq_compact_metric seq_compact_def by auto + +subsubsection \Complete the chain of compactness variants\ + +proposition compact_eq_Bolzano_Weierstrass: + fixes s :: "'a::metric_space set" + shows "compact s \ (\t. infinite t \ t \ s --> (\x \ s. x islimpt t))" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + using Heine_Borel_imp_Bolzano_Weierstrass[of s] by auto +next + assume ?rhs + then show ?lhs + unfolding compact_eq_seq_compact_metric by (rule Bolzano_Weierstrass_imp_seq_compact) +qed + +proposition Bolzano_Weierstrass_imp_bounded: + "\t. infinite t \ t \ s \ (\x \ s. x islimpt t) \ bounded s" + using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass . + + +subsection \Metric spaces with the Heine-Borel property\ + +text \ + A metric space (or topological vector space) is said to have the + Heine-Borel property if every closed and bounded subset is compact. +\ + +class heine_borel = metric_space + + assumes bounded_imp_convergent_subsequence: + "bounded (range f) \ \l r. strict_mono (r::nat\nat) \ ((f \ r) \ l) sequentially" + +proposition bounded_closed_imp_seq_compact: + fixes s::"'a::heine_borel set" + assumes "bounded s" + and "closed s" + shows "seq_compact s" +proof (unfold seq_compact_def, clarify) + fix f :: "nat \ 'a" + assume f: "\n. f n \ s" + with \bounded s\ have "bounded (range f)" + by (auto intro: bounded_subset) + obtain l r where r: "strict_mono (r :: nat \ nat)" and l: "((f \ r) \ l) sequentially" + using bounded_imp_convergent_subsequence [OF \bounded (range f)\] by auto + from f have fr: "\n. (f \ r) n \ s" + by simp + have "l \ s" using \closed s\ fr l + by (rule closed_sequentially) + show "\l\s. \r. strict_mono r \ ((f \ r) \ l) sequentially" + using \l \ s\ r l by blast +qed + +lemma compact_eq_bounded_closed: + fixes s :: "'a::heine_borel set" + shows "compact s \ bounded s \ closed s" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + using compact_imp_closed compact_imp_bounded + by blast +next + assume ?rhs + then show ?lhs + using bounded_closed_imp_seq_compact[of s] + unfolding compact_eq_seq_compact_metric + by auto +qed + +lemma compact_Inter: + fixes \ :: "'a :: heine_borel set set" + assumes com: "\S. S \ \ \ compact S" and "\ \ {}" + shows "compact(\ \)" + using assms + by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed) + +lemma compact_closure [simp]: + fixes S :: "'a::heine_borel set" + shows "compact(closure S) \ bounded S" +by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed) + +instance%important real :: heine_borel +proof%unimportant + fix f :: "nat \ real" + assume f: "bounded (range f)" + obtain r :: "nat \ nat" where r: "strict_mono r" "monoseq (f \ r)" + unfolding comp_def by (metis seq_monosub) + then have "Bseq (f \ r)" + unfolding Bseq_eq_bounded using f + by (metis BseqI' bounded_iff comp_apply rangeI) + with r show "\l r. strict_mono r \ (f \ r) \ l" + using Bseq_monoseq_convergent[of "f \ r"] by (auto simp: convergent_def) +qed + +lemma compact_lemma_general: + fixes f :: "nat \ 'a" + fixes proj::"'a \ 'b \ 'c::heine_borel" (infixl "proj" 60) + fixes unproj:: "('b \ 'c) \ 'a" + assumes finite_basis: "finite basis" + assumes bounded_proj: "\k. k \ basis \ bounded ((\x. x proj k) ` range f)" + assumes proj_unproj: "\e k. k \ basis \ (unproj e) proj k = e k" + assumes unproj_proj: "\x. unproj (\k. x proj k) = x" + shows "\d\basis. \l::'a. \ r::nat\nat. + strict_mono r \ (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)" +proof safe + fix d :: "'b set" + assume d: "d \ basis" + with finite_basis have "finite d" + by (blast intro: finite_subset) + from this d show "\l::'a. \r::nat\nat. strict_mono r \ + (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)" + proof (induct d) + case empty + then show ?case + unfolding strict_mono_def by auto + next + case (insert k d) + have k[intro]: "k \ basis" + using insert by auto + have s': "bounded ((\x. x proj k) ` range f)" + using k + by (rule bounded_proj) + obtain l1::"'a" and r1 where r1: "strict_mono r1" + and lr1: "\e > 0. eventually (\n. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially" + using insert(3) using insert(4) by auto + have f': "\n. f (r1 n) proj k \ (\x. x proj k) ` range f" + by simp + have "bounded (range (\i. f (r1 i) proj k))" + by (metis (lifting) bounded_subset f' image_subsetI s') + then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\i. f (r1 (r2 i)) proj k) \ l2) sequentially" + using bounded_imp_convergent_subsequence[of "\i. f (r1 i) proj k"] + by (auto simp: o_def) + define r where "r = r1 \ r2" + have r:"strict_mono r" + using r1 and r2 unfolding r_def o_def strict_mono_def by auto + moreover + define l where "l = unproj (\i. if i = k then l2 else l1 proj i)" + { + fix e::real + assume "e > 0" + from lr1 \e > 0\ have N1: "eventually (\n. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially" + by blast + from lr2 \e > 0\ have N2:"eventually (\n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially" + by (rule tendstoD) + from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially" + by (rule eventually_subseq) + have "eventually (\n. \i\(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially" + using N1' N2 + by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj) + } + ultimately show ?case by auto + qed +qed + +lemma bounded_fst: "bounded s \ bounded (fst ` s)" + unfolding bounded_def + by (metis (erased, hide_lams) dist_fst_le image_iff order_trans) + +lemma bounded_snd: "bounded s \ bounded (snd ` s)" + unfolding bounded_def + by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans) + +instance%important prod :: (heine_borel, heine_borel) heine_borel +proof%unimportant + fix f :: "nat \ 'a \ 'b" + assume f: "bounded (range f)" + then have "bounded (fst ` range f)" + by (rule bounded_fst) + then have s1: "bounded (range (fst \ f))" + by (simp add: image_comp) + obtain l1 r1 where r1: "strict_mono r1" and l1: "(\n. fst (f (r1 n))) \ l1" + using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast + from f have s2: "bounded (range (snd \ f \ r1))" + by (auto simp: image_comp intro: bounded_snd bounded_subset) + obtain l2 r2 where r2: "strict_mono r2" and l2: "((\n. snd (f (r1 (r2 n)))) \ l2) sequentially" + using bounded_imp_convergent_subsequence [OF s2] + unfolding o_def by fast + have l1': "((\n. fst (f (r1 (r2 n)))) \ l1) sequentially" + using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def . + have l: "((f \ (r1 \ r2)) \ (l1, l2)) sequentially" + using tendsto_Pair [OF l1' l2] unfolding o_def by simp + have r: "strict_mono (r1 \ r2)" + using r1 r2 unfolding strict_mono_def by simp + show "\l r. strict_mono r \ ((f \ r) \ l) sequentially" + using l r by fast +qed + +subsubsection \Completeness\ + +proposition (in metric_space) completeI: + assumes "\f. \n. f n \ s \ Cauchy f \ \l\s. f \ l" + shows "complete s" + using assms unfolding complete_def by fast + +proposition (in metric_space) completeE: + assumes "complete s" and "\n. f n \ s" and "Cauchy f" + obtains l where "l \ s" and "f \ l" + using assms unfolding complete_def by fast + +(* TODO: generalize to uniform spaces *) +lemma compact_imp_complete: + fixes s :: "'a::metric_space set" + assumes "compact s" + shows "complete s" +proof - + { + fix f + assume as: "(\n::nat. f n \ s)" "Cauchy f" + from as(1) obtain l r where lr: "l\s" "strict_mono r" "(f \ r) \ l" + using assms unfolding compact_def by blast + + note lr' = seq_suble [OF lr(2)] + { + fix e :: real + assume "e > 0" + from as(2) obtain N where N:"\m n. N \ m \ N \ n \ dist (f m) (f n) < e/2" + unfolding cauchy_def + using \e > 0\ + apply (erule_tac x="e/2" in allE, auto) + done + from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]] + obtain M where M:"\n\M. dist ((f \ r) n) l < e/2" + using \e > 0\ by auto + { + fix n :: nat + assume n: "n \ max N M" + have "dist ((f \ r) n) l < e/2" + using n M by auto + moreover have "r n \ N" + using lr'[of n] n by auto + then have "dist (f n) ((f \ r) n) < e / 2" + using N and n by auto + ultimately have "dist (f n) l < e" + using dist_triangle_half_r[of "f (r n)" "f n" e l] + by (auto simp: dist_commute) + } + then have "\N. \n\N. dist (f n) l < e" by blast + } + then have "\l\s. (f \ l) sequentially" using \l\s\ + unfolding lim_sequentially by auto + } + then show ?thesis unfolding complete_def by auto +qed + +proposition compact_eq_totally_bounded: + "compact s \ complete s \ (\e>0. \k. finite k \ s \ (\x\k. ball x e))" + (is "_ \ ?rhs") +proof + assume assms: "?rhs" + then obtain k where k: "\e. 0 < e \ finite (k e)" "\e. 0 < e \ s \ (\x\k e. ball x e)" + by (auto simp: choice_iff') + + show "compact s" + proof cases + assume "s = {}" + then show "compact s" by (simp add: compact_def) + next + assume "s \ {}" + show ?thesis + unfolding compact_def + proof safe + fix f :: "nat \ 'a" + assume f: "\n. f n \ s" + + define e where "e n = 1 / (2 * Suc n)" for n + then have [simp]: "\n. 0 < e n" by auto + define B where "B n U = (SOME b. infinite {n. f n \ b} \ (\x. b \ ball x (e n) \ U))" for n U + { + fix n U + assume "infinite {n. f n \ U}" + then have "\b\k (e n). infinite {i\{n. f n \ U}. f i \ ball b (e n)}" + using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq) + then obtain a where + "a \ k (e n)" + "infinite {i \ {n. f n \ U}. f i \ ball a (e n)}" .. + then have "\b. infinite {i. f i \ b} \ (\x. b \ ball x (e n) \ U)" + by (intro exI[of _ "ball a (e n) \ U"] exI[of _ a]) (auto simp: ac_simps) + from someI_ex[OF this] + have "infinite {i. f i \ B n U}" "\x. B n U \ ball x (e n) \ U" + unfolding B_def by auto + } + note B = this + + define F where "F = rec_nat (B 0 UNIV) B" + { + fix n + have "infinite {i. f i \ F n}" + by (induct n) (auto simp: F_def B) + } + then have F: "\n. \x. F (Suc n) \ ball x (e n) \ F n" + using B by (simp add: F_def) + then have F_dec: "\m n. m \ n \ F n \ F m" + using decseq_SucI[of F] by (auto simp: decseq_def) + + obtain sel where sel: "\k i. i < sel k i" "\k i. f (sel k i) \ F k" + proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI) + fix k i + have "infinite ({n. f n \ F k} - {.. i})" + using \infinite {n. f n \ F k}\ by auto + from infinite_imp_nonempty[OF this] + show "\x>i. f x \ F k" + by (simp add: set_eq_iff not_le conj_commute) + qed + + define t where "t = rec_nat (sel 0 0) (\n i. sel (Suc n) i)" + have "strict_mono t" + unfolding strict_mono_Suc_iff by (simp add: t_def sel) + moreover have "\i. (f \ t) i \ s" + using f by auto + moreover + { + fix n + have "(f \ t) n \ F n" + by (cases n) (simp_all add: t_def sel) + } + note t = this + + have "Cauchy (f \ t)" + proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE) + fix r :: real and N n m + assume "1 / Suc N < r" "Suc N \ n" "Suc N \ m" + then have "(f \ t) n \ F (Suc N)" "(f \ t) m \ F (Suc N)" "2 * e N < r" + using F_dec t by (auto simp: e_def field_simps of_nat_Suc) + with F[of N] obtain x where "dist x ((f \ t) n) < e N" "dist x ((f \ t) m) < e N" + by (auto simp: subset_eq) + with dist_triangle[of "(f \ t) m" "(f \ t) n" x] \2 * e N < r\ + show "dist ((f \ t) m) ((f \ t) n) < r" + by (simp add: dist_commute) + qed + + ultimately show "\l\s. \r. strict_mono r \ (f \ r) \ l" + using assms unfolding complete_def by blast + qed + qed +qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded) + +lemma cauchy_imp_bounded: + assumes "Cauchy s" + shows "bounded (range s)" +proof - + from assms obtain N :: nat where "\m n. N \ m \ N \ n \ dist (s m) (s n) < 1" + unfolding cauchy_def by force + then have N:"\n. N \ n \ dist (s N) (s n) < 1" by auto + moreover + have "bounded (s ` {0..N})" + using finite_imp_bounded[of "s ` {1..N}"] by auto + then obtain a where a:"\x\s ` {0..N}. dist (s N) x \ a" + unfolding bounded_any_center [where a="s N"] by auto + ultimately show "?thesis" + unfolding bounded_any_center [where a="s N"] + apply (rule_tac x="max a 1" in exI, auto) + apply (erule_tac x=y in allE) + apply (erule_tac x=y in ballE, auto) + done +qed + +instance heine_borel < complete_space +proof + fix f :: "nat \ 'a" assume "Cauchy f" + then have "bounded (range f)" + by (rule cauchy_imp_bounded) + then have "compact (closure (range f))" + unfolding compact_eq_bounded_closed by auto + then have "complete (closure (range f))" + by (rule compact_imp_complete) + moreover have "\n. f n \ closure (range f)" + using closure_subset [of "range f"] by auto + ultimately have "\l\closure (range f). (f \ l) sequentially" + using \Cauchy f\ unfolding complete_def by auto + then show "convergent f" + unfolding convergent_def by auto +qed + +lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)" +proof (rule completeI) + fix f :: "nat \ 'a" assume "Cauchy f" + then have "convergent f" by (rule Cauchy_convergent) + then show "\l\UNIV. f \ l" unfolding convergent_def by simp +qed + +lemma complete_imp_closed: + fixes S :: "'a::metric_space set" + assumes "complete S" + shows "closed S" +proof (unfold closed_sequential_limits, clarify) + fix f x assume "\n. f n \ S" and "f \ x" + from \f \ x\ have "Cauchy f" + by (rule LIMSEQ_imp_Cauchy) + with \complete S\ and \\n. f n \ S\ obtain l where "l \ S" and "f \ l" + by (rule completeE) + from \f \ x\ and \f \ l\ have "x = l" + by (rule LIMSEQ_unique) + with \l \ S\ show "x \ S" + by simp +qed + +lemma complete_Int_closed: + fixes S :: "'a::metric_space set" + assumes "complete S" and "closed t" + shows "complete (S \ t)" +proof (rule completeI) + fix f assume "\n. f n \ S \ t" and "Cauchy f" + then have "\n. f n \ S" and "\n. f n \ t" + by simp_all + from \complete S\ obtain l where "l \ S" and "f \ l" + using \\n. f n \ S\ and \Cauchy f\ by (rule completeE) + from \closed t\ and \\n. f n \ t\ and \f \ l\ have "l \ t" + by (rule closed_sequentially) + with \l \ S\ and \f \ l\ show "\l\S \ t. f \ l" + by fast +qed + +lemma complete_closed_subset: + fixes S :: "'a::metric_space set" + assumes "closed S" and "S \ t" and "complete t" + shows "complete S" + using assms complete_Int_closed [of t S] by (simp add: Int_absorb1) + +lemma complete_eq_closed: + fixes S :: "('a::complete_space) set" + shows "complete S \ closed S" +proof + assume "closed S" then show "complete S" + using subset_UNIV complete_UNIV by (rule complete_closed_subset) +next + assume "complete S" then show "closed S" + by (rule complete_imp_closed) +qed + +lemma convergent_eq_Cauchy: + fixes S :: "nat \ 'a::complete_space" + shows "(\l. (S \ l) sequentially) \ Cauchy S" + unfolding Cauchy_convergent_iff convergent_def .. + +lemma convergent_imp_bounded: + fixes S :: "nat \ 'a::metric_space" + shows "(S \ l) sequentially \ bounded (range S)" + by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy) + +lemma frontier_subset_compact: + fixes S :: "'a::heine_borel set" + shows "compact S \ frontier S \ S" + using frontier_subset_closed compact_eq_bounded_closed + by blast + +subsection \Continuity\ + +text\Derive the epsilon-delta forms, which we often use as "definitions"\ + +proposition continuous_within_eps_delta: + "continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)" + unfolding continuous_within and Lim_within by fastforce + +corollary continuous_at_eps_delta: + "continuous (at x) f \ (\e > 0. \d > 0. \x'. dist x' x < d \ dist (f x') (f x) < e)" + using continuous_within_eps_delta [of x UNIV f] by simp + +lemma continuous_at_right_real_increasing: + fixes f :: "real \ real" + assumes nondecF: "\x y. x \ y \ f x \ f y" + shows "continuous (at_right a) f \ (\e>0. \d>0. f (a + d) - f a < e)" + apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le) + apply (intro all_cong ex_cong, safe) + apply (erule_tac x="a + d" in allE, simp) + apply (simp add: nondecF field_simps) + apply (drule nondecF, simp) + done + +lemma continuous_at_left_real_increasing: + assumes nondecF: "\ x y. x \ y \ f x \ ((f y) :: real)" + shows "(continuous (at_left (a :: real)) f) = (\e > 0. \delta > 0. f a - f (a - delta) < e)" + apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le) + apply (intro all_cong ex_cong, safe) + apply (erule_tac x="a - d" in allE, simp) + apply (simp add: nondecF field_simps) + apply (cut_tac x="a - d" and y=x in nondecF, simp_all) + done + +text\Versions in terms of open balls.\ + +lemma continuous_within_ball: + "continuous (at x within s) f \ + (\e > 0. \d > 0. f ` (ball x d \ s) \ ball (f x) e)" + (is "?lhs = ?rhs") +proof + assume ?lhs + { + fix e :: real + assume "e > 0" + then obtain d where d: "d>0" "\xa\s. 0 < dist xa x \ dist xa x < d \ dist (f xa) (f x) < e" + using \?lhs\[unfolded continuous_within Lim_within] by auto + { + fix y + assume "y \ f ` (ball x d \ s)" + then have "y \ ball (f x) e" + using d(2) + apply (auto simp: dist_commute) + apply (erule_tac x=xa in ballE, auto) + using \e > 0\ + apply auto + done + } + then have "\d>0. f ` (ball x d \ s) \ ball (f x) e" + using \d > 0\ + unfolding subset_eq ball_def by (auto simp: dist_commute) + } + then show ?rhs by auto +next + assume ?rhs + then show ?lhs + unfolding continuous_within Lim_within ball_def subset_eq + apply (auto simp: dist_commute) + apply (erule_tac x=e in allE, auto) + done +qed + +lemma continuous_at_ball: + "continuous (at x) f \ (\e>0. \d>0. f ` (ball x d) \ ball (f x) e)" (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball + apply auto + apply (erule_tac x=e in allE, auto) + apply (rule_tac x=d in exI, auto) + apply (erule_tac x=xa in allE) + apply (auto simp: dist_commute) + done +next + assume ?rhs + then show ?lhs + unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball + apply auto + apply (erule_tac x=e in allE, auto) + apply (rule_tac x=d in exI, auto) + apply (erule_tac x="f xa" in allE) + apply (auto simp: dist_commute) + done +qed + +text\Define setwise continuity in terms of limits within the set.\ + +lemma continuous_on_iff: + "continuous_on s f \ + (\x\s. \e>0. \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) < e)" + unfolding continuous_on_def Lim_within + by (metis dist_pos_lt dist_self) + +lemma continuous_within_E: + assumes "continuous (at x within s) f" "e>0" + obtains d where "d>0" "\x'. \x'\ s; dist x' x \ d\ \ dist (f x') (f x) < e" + using assms apply (simp add: continuous_within_eps_delta) + apply (drule spec [of _ e], clarify) + apply (rule_tac d="d/2" in that, auto) + done + +lemma continuous_onI [intro?]: + assumes "\x e. \e > 0; x \ s\ \ \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) \ e" + shows "continuous_on s f" +apply (simp add: continuous_on_iff, clarify) +apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) +done + +text\Some simple consequential lemmas.\ + +lemma continuous_onE: + assumes "continuous_on s f" "x\s" "e>0" + obtains d where "d>0" "\x'. \x' \ s; dist x' x \ d\ \ dist (f x') (f x) < e" + using assms + apply (simp add: continuous_on_iff) + apply (elim ballE allE) + apply (auto intro: that [where d="d/2" for d]) + done + +lemma uniformly_continuous_onE: + assumes "uniformly_continuous_on s f" "0 < e" + obtains d where "d>0" "\x x'. \x\s; x'\s; dist x' x < d\ \ dist (f x') (f x) < e" +using assms +by (auto simp: uniformly_continuous_on_def) + +lemma uniformly_continuous_on_sequentially: + "uniformly_continuous_on s f \ (\x y. (\n. x n \ s) \ (\n. y n \ s) \ + (\n. dist (x n) (y n)) \ 0 \ (\n. dist (f(x n)) (f(y n))) \ 0)" (is "?lhs = ?rhs") +proof + assume ?lhs + { + fix x y + assume x: "\n. x n \ s" + and y: "\n. y n \ s" + and xy: "((\n. dist (x n) (y n)) \ 0) sequentially" + { + fix e :: real + assume "e > 0" + then obtain d where "d > 0" and d: "\x\s. \x'\s. dist x' x < d \ dist (f x') (f x) < e" + using \?lhs\[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto + obtain N where N: "\n\N. dist (x n) (y n) < d" + using xy[unfolded lim_sequentially dist_norm] and \d>0\ by auto + { + fix n + assume "n\N" + then have "dist (f (x n)) (f (y n)) < e" + using N[THEN spec[where x=n]] + using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] + using x and y + by (simp add: dist_commute) + } + then have "\N. \n\N. dist (f (x n)) (f (y n)) < e" + by auto + } + then have "((\n. dist (f(x n)) (f(y n))) \ 0) sequentially" + unfolding lim_sequentially and dist_real_def by auto + } + then show ?rhs by auto +next + assume ?rhs + { + assume "\ ?lhs" + then obtain e where "e > 0" "\d>0. \x\s. \x'\s. dist x' x < d \ \ dist (f x') (f x) < e" + unfolding uniformly_continuous_on_def by auto + then obtain fa where fa: + "\x. 0 < x \ fst (fa x) \ s \ snd (fa x) \ s \ dist (fst (fa x)) (snd (fa x)) < x \ \ dist (f (fst (fa x))) (f (snd (fa x))) < e" + using choice[of "\d x. d>0 \ fst x \ s \ snd x \ s \ dist (snd x) (fst x) < d \ \ dist (f (snd x)) (f (fst x)) < e"] + unfolding Bex_def + by (auto simp: dist_commute) + define x where "x n = fst (fa (inverse (real n + 1)))" for n + define y where "y n = snd (fa (inverse (real n + 1)))" for n + have xyn: "\n. x n \ s \ y n \ s" + and xy0: "\n. dist (x n) (y n) < inverse (real n + 1)" + and fxy:"\n. \ dist (f (x n)) (f (y n)) < e" + unfolding x_def and y_def using fa + by auto + { + fix e :: real + assume "e > 0" + then obtain N :: nat where "N \ 0" and N: "0 < inverse (real N) \ inverse (real N) < e" + unfolding real_arch_inverse[of e] by auto + { + fix n :: nat + assume "n \ N" + then have "inverse (real n + 1) < inverse (real N)" + using of_nat_0_le_iff and \N\0\ by auto + also have "\ < e" using N by auto + finally have "inverse (real n + 1) < e" by auto + then have "dist (x n) (y n) < e" + using xy0[THEN spec[where x=n]] by auto + } + then have "\N. \n\N. dist (x n) (y n) < e" by auto + } + then have "\e>0. \N. \n\N. dist (f (x n)) (f (y n)) < e" + using \?rhs\[THEN spec[where x=x], THEN spec[where x=y]] and xyn + unfolding lim_sequentially dist_real_def by auto + then have False using fxy and \e>0\ by auto + } + then show ?lhs + unfolding uniformly_continuous_on_def by blast +qed + +lemma continuous_closed_imp_Cauchy_continuous: + fixes S :: "('a::complete_space) set" + shows "\continuous_on S f; closed S; Cauchy \; \n. (\ n) \ S\ \ Cauchy(f \ \)" + apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially) + by (meson LIMSEQ_imp_Cauchy complete_def) + +text\The usual transformation theorems.\ + +lemma continuous_transform_within: + fixes f g :: "'a::metric_space \ 'b::topological_space" + assumes "continuous (at x within s) f" + and "0 < d" + and "x \ s" + and "\x'. \x' \ s; dist x' x < d\ \ f x' = g x'" + shows "continuous (at x within s) g" + using assms + unfolding continuous_within + by (force intro: Lim_transform_within) + +subsubsection%unimportant \Structural rules for uniform continuity\ + +lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]: + fixes g :: "_::metric_space \ _" + assumes "uniformly_continuous_on s g" + shows "uniformly_continuous_on s (\x. f (g x))" + using assms unfolding uniformly_continuous_on_sequentially + unfolding dist_norm tendsto_norm_zero_iff diff[symmetric] + by (auto intro: tendsto_zero) + + +subsection \With Abstract Topology (TODO: move and remove dependency?)\ + +lemma openin_contains_ball: + "openin (subtopology euclidean t) s \ + s \ t \ (\x \ s. \e. 0 < e \ ball x e \ t \ s)" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + apply (simp add: openin_open) + apply (metis Int_commute Int_mono inf.cobounded2 open_contains_ball order_refl subsetCE) + done +next + assume ?rhs + then show ?lhs + apply (simp add: openin_euclidean_subtopology_iff) + by (metis (no_types) Int_iff dist_commute inf.absorb_iff2 mem_ball) +qed + +lemma openin_contains_cball: + "openin (subtopology euclidean t) s \ + s \ t \ + (\x \ s. \e. 0 < e \ cball x e \ t \ s)" +apply (simp add: openin_contains_ball) +apply (rule iffI) +apply (auto dest!: bspec) +apply (rule_tac x="e/2" in exI, force+) + done + +subsection \With abstract Topology\ + +lemma Times_in_interior_subtopology: + fixes U :: "('a::metric_space \ 'b::metric_space) set" + assumes "(x, y) \ U" "openin (subtopology euclidean (S \ T)) U" + obtains V W where "openin (subtopology euclidean S) V" "x \ V" + "openin (subtopology euclidean T) W" "y \ W" "(V \ W) \ U" +proof - + from assms obtain e where "e > 0" and "U \ S \ T" + and e: "\x' y'. \x'\S; y'\T; dist (x', y') (x, y) < e\ \ (x', y') \ U" + by (force simp: openin_euclidean_subtopology_iff) + with assms have "x \ S" "y \ T" + by auto + show ?thesis + proof + show "openin (subtopology euclidean S) (ball x (e/2) \ S)" + by (simp add: Int_commute openin_open_Int) + show "x \ ball x (e / 2) \ S" + by (simp add: \0 < e\ \x \ S\) + show "openin (subtopology euclidean T) (ball y (e/2) \ T)" + by (simp add: Int_commute openin_open_Int) + show "y \ ball y (e / 2) \ T" + by (simp add: \0 < e\ \y \ T\) + show "(ball x (e / 2) \ S) \ (ball y (e / 2) \ T) \ U" + by clarify (simp add: e dist_Pair_Pair \0 < e\ dist_commute sqrt_sum_squares_half_less) + qed +qed + +lemma openin_Times_eq: + fixes S :: "'a::metric_space set" and T :: "'b::metric_space set" + shows + "openin (subtopology euclidean (S \ T)) (S' \ T') \ + S' = {} \ T' = {} \ openin (subtopology euclidean S) S' \ openin (subtopology euclidean T) T'" + (is "?lhs = ?rhs") +proof (cases "S' = {} \ T' = {}") + case True + then show ?thesis by auto +next + case False + then obtain x y where "x \ S'" "y \ T'" + by blast + show ?thesis + proof + assume ?lhs + have "openin (subtopology euclidean S) S'" + apply (subst openin_subopen, clarify) + apply (rule Times_in_interior_subtopology [OF _ \?lhs\]) + using \y \ T'\ + apply auto + done + moreover have "openin (subtopology euclidean T) T'" + apply (subst openin_subopen, clarify) + apply (rule Times_in_interior_subtopology [OF _ \?lhs\]) + using \x \ S'\ + apply auto + done + ultimately show ?rhs + by simp + next + assume ?rhs + with False show ?lhs + by (simp add: openin_Times) + qed +qed + +lemma closedin_Times: + "closedin (subtopology euclidean S) S' \ closedin (subtopology euclidean T) T' \ + closedin (subtopology euclidean (S \ T)) (S' \ T')" + unfolding closedin_closed using closed_Times by blast + +lemma Lim_transform_within_openin: + fixes a :: "'a::metric_space" + assumes f: "(f \ l) (at a within T)" + and "openin (subtopology euclidean T) S" "a \ S" + and eq: "\x. \x \ S; x \ a\ \ f x = g x" + shows "(g \ l) (at a within T)" +proof - + obtain \ where "0 < \" and \: "ball a \ \ T \ S" + using assms by (force simp: openin_contains_ball) + then have "a \ ball a \" + by simp + show ?thesis + by (rule Lim_transform_within [OF f \0 < \\ eq]) (use \ in \auto simp: dist_commute subset_iff\) +qed + +lemma closure_Int_ballI: + fixes S :: "'a :: metric_space set" + assumes "\U. \openin (subtopology euclidean S) U; U \ {}\ \ T \ U \ {}" + shows "S \ closure T" +proof (clarsimp simp: closure_approachable dist_commute) + fix x and e::real + assume "x \ S" "0 < e" + with assms [of "S \ ball x e"] show "\y\T. dist x y < e" + by force +qed + +lemma continuous_on_open_gen: + fixes f :: "'a::metric_space \ 'b::metric_space" + assumes "f ` S \ T" + shows "continuous_on S f \ + (\U. openin (subtopology euclidean T) U + \ openin (subtopology euclidean S) (S \ f -` U))" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + apply (clarsimp simp: openin_euclidean_subtopology_iff continuous_on_iff) + by (metis assms image_subset_iff) +next + have ope: "openin (subtopology euclidean T) (ball y e \ T)" for y e + by (simp add: Int_commute openin_open_Int) + assume R [rule_format]: ?rhs + show ?lhs + proof (clarsimp simp add: continuous_on_iff) + fix x and e::real + assume "x \ S" and "0 < e" + then have x: "x \ S \ (f -` ball (f x) e \ f -` T)" + using assms by auto + show "\d>0. \x'\S. dist x' x < d \ dist (f x') (f x) < e" + using R [of "ball (f x) e \ T"] x + by (fastforce simp add: ope openin_euclidean_subtopology_iff [of S] dist_commute) + qed +qed + +lemma continuous_openin_preimage: + fixes f :: "'a::metric_space \ 'b::metric_space" + shows + "\continuous_on S f; f ` S \ T; openin (subtopology euclidean T) U\ + \ openin (subtopology euclidean S) (S \ f -` U)" +by (simp add: continuous_on_open_gen) + +lemma continuous_on_closed_gen: + fixes f :: "'a::metric_space \ 'b::metric_space" + assumes "f ` S \ T" + shows "continuous_on S f \ + (\U. closedin (subtopology euclidean T) U + \ closedin (subtopology euclidean S) (S \ f -` U))" + (is "?lhs = ?rhs") +proof - + have *: "U \ T \ S \ f -` (T - U) = S - (S \ f -` U)" for U + using assms by blast + show ?thesis + proof + assume L: ?lhs + show ?rhs + proof clarify + fix U + assume "closedin (subtopology euclidean T) U" + then show "closedin (subtopology euclidean S) (S \ f -` U)" + using L unfolding continuous_on_open_gen [OF assms] + by (metis * closedin_def inf_le1 topspace_euclidean_subtopology) + qed + next + assume R [rule_format]: ?rhs + show ?lhs + unfolding continuous_on_open_gen [OF assms] + by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology) + qed +qed + +lemma continuous_closedin_preimage_gen: + fixes f :: "'a::metric_space \ 'b::metric_space" + assumes "continuous_on S f" "f ` S \ T" "closedin (subtopology euclidean T) U" + shows "closedin (subtopology euclidean S) (S \ f -` U)" +using assms continuous_on_closed_gen by blast + +lemma continuous_transform_within_openin: + fixes a :: "'a::metric_space" + assumes "continuous (at a within T) f" + and "openin (subtopology euclidean T) S" "a \ S" + and eq: "\x. x \ S \ f x = g x" + shows "continuous (at a within T) g" + using assms by (simp add: Lim_transform_within_openin continuous_within) + +end \ No newline at end of file diff -r c2d5575d9da5 -r 5aa5a8d6e5b5 src/HOL/Analysis/Elementary_Normed_Spaces.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Sat Dec 29 20:32:09 2018 +0100 @@ -0,0 +1,597 @@ +(* Author: L C Paulson, University of Cambridge + Author: Amine Chaieb, University of Cambridge + Author: Robert Himmelmann, TU Muenchen + Author: Brian Huffman, Portland State University +*) + +section \Elementary Normed Vector Spaces\ + +theory Elementary_Normed_Spaces + imports + "HOL-Library.FuncSet" + Elementary_Metric_Spaces +begin + +subsection%unimportant \Various Lemmas Combining Imports\ + +lemma countable_PiE: + "finite I \ (\i. i \ I \ countable (F i)) \ countable (Pi\<^sub>E I F)" + by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) + + +lemma open_sums: + fixes T :: "('b::real_normed_vector) set" + assumes "open S \ open T" + shows "open (\x\ S. \y \ T. {x + y})" + using assms +proof + assume S: "open S" + show ?thesis + proof (clarsimp simp: open_dist) + fix x y + assume "x \ S" "y \ T" + with S obtain e where "e > 0" and e: "\x'. dist x' x < e \ x' \ S" + by (auto simp: open_dist) + then have "\z. dist z (x + y) < e \ \x\S. \y\T. z = x + y" + by (metis \y \ T\ diff_add_cancel dist_add_cancel2) + then show "\e>0. \z. dist z (x + y) < e \ (\x\S. \y\T. z = x + y)" + using \0 < e\ \x \ S\ by blast + qed +next + assume T: "open T" + show ?thesis + proof (clarsimp simp: open_dist) + fix x y + assume "x \ S" "y \ T" + with T obtain e where "e > 0" and e: "\x'. dist x' y < e \ x' \ T" + by (auto simp: open_dist) + then have "\z. dist z (x + y) < e \ \x\S. \y\T. z = x + y" + by (metis \x \ S\ add_diff_cancel_left' add_diff_eq diff_diff_add dist_norm) + then show "\e>0. \z. dist z (x + y) < e \ (\x\S. \y\T. z = x + y)" + using \0 < e\ \y \ T\ by blast + qed +qed + + +subsection \Support\ + +definition (in monoid_add) support_on :: "'b set \ ('b \ 'a) \ 'b set" + where "support_on s f = {x\s. f x \ 0}" + +lemma in_support_on: "x \ support_on s f \ x \ s \ f x \ 0" + by (simp add: support_on_def) + +lemma support_on_simps[simp]: + "support_on {} f = {}" + "support_on (insert x s) f = + (if f x = 0 then support_on s f else insert x (support_on s f))" + "support_on (s \ t) f = support_on s f \ support_on t f" + "support_on (s \ t) f = support_on s f \ support_on t f" + "support_on (s - t) f = support_on s f - support_on t f" + "support_on (f ` s) g = f ` (support_on s (g \ f))" + unfolding support_on_def by auto + +lemma support_on_cong: + "(\x. x \ s \ f x = 0 \ g x = 0) \ support_on s f = support_on s g" + by (auto simp: support_on_def) + +lemma support_on_if: "a \ 0 \ support_on A (\x. if P x then a else 0) = {x\A. P x}" + by (auto simp: support_on_def) + +lemma support_on_if_subset: "support_on A (\x. if P x then a else 0) \ {x \ A. P x}" + by (auto simp: support_on_def) + +lemma finite_support[intro]: "finite S \ finite (support_on S f)" + unfolding support_on_def by auto + +(* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *) +definition (in comm_monoid_add) supp_sum :: "('b \ 'a) \ 'b set \ 'a" + where "supp_sum f S = (\x\support_on S f. f x)" + +lemma supp_sum_empty[simp]: "supp_sum f {} = 0" + unfolding supp_sum_def by auto + +lemma supp_sum_insert[simp]: + "finite (support_on S f) \ + supp_sum f (insert x S) = (if x \ S then supp_sum f S else f x + supp_sum f S)" + by (simp add: supp_sum_def in_support_on insert_absorb) + +lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (\n. f n / r) A" + by (cases "r = 0") + (auto simp: supp_sum_def sum_divide_distrib intro!: sum.cong support_on_cong) + + +subsection \Intervals\ + +lemma image_affinity_interval: + fixes c :: "'a::ordered_real_vector" + shows "((\x. m *\<^sub>R x + c) ` {a..b}) = + (if {a..b}={} then {} + else if 0 \ m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} + else {m *\<^sub>R b + c .. m *\<^sub>R a + c})" + (is "?lhs = ?rhs") +proof (cases "m=0") + case True + then show ?thesis + by force +next + case False + show ?thesis + proof + show "?lhs \ ?rhs" + by (auto simp: scaleR_left_mono scaleR_left_mono_neg) + show "?rhs \ ?lhs" + proof (clarsimp, intro conjI impI subsetI) + show "\0 \ m; a \ b; x \ {m *\<^sub>R a + c..m *\<^sub>R b + c}\ + \ x \ (\x. m *\<^sub>R x + c) ` {a..b}" for x + apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI) + using False apply (auto simp: le_diff_eq pos_le_divideRI) + using diff_le_eq pos_le_divideR_eq by force + show "\\ 0 \ m; a \ b; x \ {m *\<^sub>R b + c..m *\<^sub>R a + c}\ + \ x \ (\x. m *\<^sub>R x + c) ` {a..b}" for x + apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI) + apply (auto simp: diff_le_eq neg_le_divideR_eq) + using diff_eq_diff_less_eq linordered_field_class.sign_simps(11) minus_diff_eq not_less scaleR_le_cancel_left_neg by fastforce + qed + qed +qed + + +subsection%unimportant \Various Lemmas on Normed Algebras\ + + +lemma closed_of_nat_image: "closed (of_nat ` A :: 'a::real_normed_algebra_1 set)" + by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_nat) + +lemma closed_of_int_image: "closed (of_int ` A :: 'a::real_normed_algebra_1 set)" + by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_int) + +lemma closed_Nats [simp]: "closed (\ :: 'a :: real_normed_algebra_1 set)" + unfolding Nats_def by (rule closed_of_nat_image) + +lemma closed_Ints [simp]: "closed (\ :: 'a :: real_normed_algebra_1 set)" + unfolding Ints_def by (rule closed_of_int_image) + +lemma closed_subset_Ints: + fixes A :: "'a :: real_normed_algebra_1 set" + assumes "A \ \" + shows "closed A" +proof (intro discrete_imp_closed[OF zero_less_one] ballI impI, goal_cases) + case (1 x y) + with assms have "x \ \" and "y \ \" by auto + with \dist y x < 1\ show "y = x" + by (auto elim!: Ints_cases simp: dist_of_int) +qed + +subsection \Filters\ + +definition indirection :: "'a::real_normed_vector \ 'a \ 'a filter" (infixr "indirection" 70) + where "a indirection v = at a within {b. \c\0. b - a = scaleR c v}" + + +subsection \Trivial Limits\ + +lemma trivial_limit_at_infinity: + "\ trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) filter)" + unfolding trivial_limit_def eventually_at_infinity + apply clarsimp + apply (subgoal_tac "\x::'a. x \ 0", clarify) + apply (rule_tac x="scaleR (b / norm x) x" in exI, simp) + apply (cut_tac islimpt_UNIV [of "0::'a", unfolded islimpt_def]) + apply (drule_tac x=UNIV in spec, simp) + done + +subsection \Limits\ + +proposition Lim_at_infinity: "(f \ l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" + by (auto simp: tendsto_iff eventually_at_infinity) + +corollary Lim_at_infinityI [intro?]: + assumes "\e. e > 0 \ \B. \x. norm x \ B \ dist (f x) l \ e" + shows "(f \ l) at_infinity" + apply (simp add: Lim_at_infinity, clarify) + apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) + done + +lemma Lim_transform_within_set_eq: + fixes a l :: "'a::real_normed_vector" + shows "eventually (\x. x \ s \ x \ t) (at a) + \ ((f \ l) (at a within s) \ (f \ l) (at a within t))" + by (force intro: Lim_transform_within_set elim: eventually_mono) + +lemma Lim_null: + fixes f :: "'a \ 'b::real_normed_vector" + shows "(f \ l) net \ ((\x. f(x) - l) \ 0) net" + by (simp add: Lim dist_norm) + +lemma Lim_null_comparison: + fixes f :: "'a \ 'b::real_normed_vector" + assumes "eventually (\x. norm (f x) \ g x) net" "(g \ 0) net" + shows "(f \ 0) net" + using assms(2) +proof (rule metric_tendsto_imp_tendsto) + show "eventually (\x. dist (f x) 0 \ dist (g x) 0) net" + using assms(1) by (rule eventually_mono) (simp add: dist_norm) +qed + +lemma Lim_transform_bound: + fixes f :: "'a \ 'b::real_normed_vector" + and g :: "'a \ 'c::real_normed_vector" + assumes "eventually (\n. norm (f n) \ norm (g n)) net" + and "(g \ 0) net" + shows "(f \ 0) net" + using assms(1) tendsto_norm_zero [OF assms(2)] + by (rule Lim_null_comparison) + +lemma lim_null_mult_right_bounded: + fixes f :: "'a \ 'b::real_normed_div_algebra" + assumes f: "(f \ 0) F" and g: "eventually (\x. norm(g x) \ B) F" + shows "((\z. f z * g z) \ 0) F" +proof - + have *: "((\x. norm (f x) * B) \ 0) F" + by (simp add: f tendsto_mult_left_zero tendsto_norm_zero) + have "((\x. norm (f x) * norm (g x)) \ 0) F" + apply (rule Lim_null_comparison [OF _ *]) + apply (simp add: eventually_mono [OF g] mult_left_mono) + done + then show ?thesis + by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) +qed + +lemma lim_null_mult_left_bounded: + fixes f :: "'a \ 'b::real_normed_div_algebra" + assumes g: "eventually (\x. norm(g x) \ B) F" and f: "(f \ 0) F" + shows "((\z. g z * f z) \ 0) F" +proof - + have *: "((\x. B * norm (f x)) \ 0) F" + by (simp add: f tendsto_mult_right_zero tendsto_norm_zero) + have "((\x. norm (g x) * norm (f x)) \ 0) F" + apply (rule Lim_null_comparison [OF _ *]) + apply (simp add: eventually_mono [OF g] mult_right_mono) + done + then show ?thesis + by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) +qed + +lemma lim_null_scaleR_bounded: + assumes f: "(f \ 0) net" and gB: "eventually (\a. f a = 0 \ norm(g a) \ B) net" + shows "((\n. f n *\<^sub>R g n) \ 0) net" +proof + fix \::real + assume "0 < \" + then have B: "0 < \ / (abs B + 1)" by simp + have *: "\f x\ * norm (g x) < \" if f: "\f x\ * (\B\ + 1) < \" and g: "norm (g x) \ B" for x + proof - + have "\f x\ * norm (g x) \ \f x\ * B" + by (simp add: mult_left_mono g) + also have "\ \ \f x\ * (\B\ + 1)" + by (simp add: mult_left_mono) + also have "\ < \" + by (rule f) + finally show ?thesis . + qed + show "\\<^sub>F x in net. dist (f x *\<^sub>R g x) 0 < \" + apply (rule eventually_mono [OF eventually_conj [OF tendstoD [OF f B] gB] ]) + apply (auto simp: \0 < \\ divide_simps * split: if_split_asm) + done +qed + +lemma Lim_norm_ubound: + fixes f :: "'a \ 'b::real_normed_vector" + assumes "\(trivial_limit net)" "(f \ l) net" "eventually (\x. norm(f x) \ e) net" + shows "norm(l) \ e" + using assms by (fast intro: tendsto_le tendsto_intros) + +lemma Lim_norm_lbound: + fixes f :: "'a \ 'b::real_normed_vector" + assumes "\ trivial_limit net" + and "(f \ l) net" + and "eventually (\x. e \ norm (f x)) net" + shows "e \ norm l" + using assms by (fast intro: tendsto_le tendsto_intros) + +text\Limit under bilinear function\ + +lemma Lim_bilinear: + assumes "(f \ l) net" + and "(g \ m) net" + and "bounded_bilinear h" + shows "((\x. h (f x) (g x)) \ (h l m)) net" + using \bounded_bilinear h\ \(f \ l) net\ \(g \ m) net\ + by (rule bounded_bilinear.tendsto) + +lemma Lim_at_zero: + fixes a :: "'a::real_normed_vector" + and l :: "'b::topological_space" + shows "(f \ l) (at a) \ ((\x. f(a + x)) \ l) (at 0)" + using LIM_offset_zero LIM_offset_zero_cancel .. + + +subsection%unimportant \Limit Point of Filter\ + +lemma netlimit_at_vector: + fixes a :: "'a::real_normed_vector" + shows "netlimit (at a) = a" +proof (cases "\x. x \ a") + case True then obtain x where x: "x \ a" .. + have "\ trivial_limit (at a)" + unfolding trivial_limit_def eventually_at dist_norm + apply clarsimp + apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI) + apply (simp add: norm_sgn sgn_zero_iff x) + done + then show ?thesis + by (rule netlimit_within [of a UNIV]) +qed simp + +subsection \Boundedness\ + +lemma bounded_pos: "bounded S \ (\b>0. \x\ S. norm x \ b)" + apply (simp add: bounded_iff) + apply (subgoal_tac "\x (y::real). 0 < 1 + \y\ \ (x \ y \ x \ 1 + \y\)") + apply metis + apply arith + done + +lemma bounded_pos_less: "bounded S \ (\b>0. \x\ S. norm x < b)" + apply (simp add: bounded_pos) + apply (safe; rule_tac x="b+1" in exI; force) + done + +lemma Bseq_eq_bounded: + fixes f :: "nat \ 'a::real_normed_vector" + shows "Bseq f \ bounded (range f)" + unfolding Bseq_def bounded_pos by auto + +lemma bounded_linear_image: + assumes "bounded S" + and "bounded_linear f" + shows "bounded (f ` S)" +proof - + from assms(1) obtain b where "b > 0" and b: "\x\S. norm x \ b" + unfolding bounded_pos by auto + from assms(2) obtain B where B: "B > 0" "\x. norm (f x) \ B * norm x" + using bounded_linear.pos_bounded by (auto simp: ac_simps) + show ?thesis + unfolding bounded_pos + proof (intro exI, safe) + show "norm (f x) \ B * b" if "x \ S" for x + by (meson B b less_imp_le mult_left_mono order_trans that) + qed (use \b > 0\ \B > 0\ in auto) +qed + +lemma bounded_scaling: + fixes S :: "'a::real_normed_vector set" + shows "bounded S \ bounded ((\x. c *\<^sub>R x) ` S)" + apply (rule bounded_linear_image, assumption) + apply (rule bounded_linear_scaleR_right) + done + +lemma bounded_scaleR_comp: + fixes f :: "'a \ 'b::real_normed_vector" + assumes "bounded (f ` S)" + shows "bounded ((\x. r *\<^sub>R f x) ` S)" + using bounded_scaling[of "f ` S" r] assms + by (auto simp: image_image) + +lemma bounded_translation: + fixes S :: "'a::real_normed_vector set" + assumes "bounded S" + shows "bounded ((\x. a + x) ` S)" +proof - + from assms obtain b where b: "b > 0" "\x\S. norm x \ b" + unfolding bounded_pos by auto + { + fix x + assume "x \ S" + then have "norm (a + x) \ b + norm a" + using norm_triangle_ineq[of a x] b by auto + } + then show ?thesis + unfolding bounded_pos + using norm_ge_zero[of a] b(1) and add_strict_increasing[of b 0 "norm a"] + by (auto intro!: exI[of _ "b + norm a"]) +qed + +lemma bounded_translation_minus: + fixes S :: "'a::real_normed_vector set" + shows "bounded S \ bounded ((\x. x - a) ` S)" +using bounded_translation [of S "-a"] by simp + +lemma bounded_uminus [simp]: + fixes X :: "'a::real_normed_vector set" + shows "bounded (uminus ` X) \ bounded X" +by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp: add.commute norm_minus_commute) + +lemma uminus_bounded_comp [simp]: + fixes f :: "'a \ 'b::real_normed_vector" + shows "bounded ((\x. - f x) ` S) \ bounded (f ` S)" + using bounded_uminus[of "f ` S"] + by (auto simp: image_image) + +lemma bounded_plus_comp: + fixes f g::"'a \ 'b::real_normed_vector" + assumes "bounded (f ` S)" + assumes "bounded (g ` S)" + shows "bounded ((\x. f x + g x) ` S)" +proof - + { + fix B C + assume "\x. x\S \ norm (f x) \ B" "\x. x\S \ norm (g x) \ C" + then have "\x. x \ S \ norm (f x + g x) \ B + C" + by (auto intro!: norm_triangle_le add_mono) + } then show ?thesis + using assms by (fastforce simp: bounded_iff) +qed + +lemma bounded_plus: + fixes S ::"'a::real_normed_vector set" + assumes "bounded S" "bounded T" + shows "bounded ((\(x,y). x + y) ` (S \ T))" + using bounded_plus_comp [of fst "S \ T" snd] assms + by (auto simp: split_def split: if_split_asm) + +lemma bounded_minus_comp: + "bounded (f ` S) \ bounded (g ` S) \ bounded ((\x. f x - g x) ` S)" + for f g::"'a \ 'b::real_normed_vector" + using bounded_plus_comp[of "f" S "\x. - g x"] + by auto + +lemma bounded_minus: + fixes S ::"'a::real_normed_vector set" + assumes "bounded S" "bounded T" + shows "bounded ((\(x,y). x - y) ` (S \ T))" + using bounded_minus_comp [of fst "S \ T" snd] assms + by (auto simp: split_def split: if_split_asm) + +lemma not_bounded_UNIV[simp]: + "\ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)" +proof (auto simp: bounded_pos not_le) + obtain x :: 'a where "x \ 0" + using perfect_choose_dist [OF zero_less_one] by fast + fix b :: real + assume b: "b >0" + have b1: "b +1 \ 0" + using b by simp + with \x \ 0\ have "b < norm (scaleR (b + 1) (sgn x))" + by (simp add: norm_sgn) + then show "\x::'a. b < norm x" .. +qed + +corollary cobounded_imp_unbounded: + fixes S :: "'a::{real_normed_vector, perfect_space} set" + shows "bounded (- S) \ \ bounded S" + using bounded_Un [of S "-S"] by (simp add: sup_compl_top) + + +subsection \Normed spaces with the Heine-Borel property\ + +lemma not_compact_UNIV[simp]: + fixes s :: "'a::{real_normed_vector,perfect_space,heine_borel} set" + shows "\ compact (UNIV::'a set)" + by (simp add: compact_eq_bounded_closed) + +text\Representing sets as the union of a chain of compact sets.\ +lemma closed_Union_compact_subsets: + fixes S :: "'a::{heine_borel,real_normed_vector} set" + assumes "closed S" + obtains F where "\n. compact(F n)" "\n. F n \ S" "\n. F n \ F(Suc n)" + "(\n. F n) = S" "\K. \compact K; K \ S\ \ \N. \n \ N. K \ F n" +proof + show "compact (S \ cball 0 (of_nat n))" for n + using assms compact_eq_bounded_closed by auto +next + show "(\n. S \ cball 0 (real n)) = S" + by (auto simp: real_arch_simple) +next + fix K :: "'a set" + assume "compact K" "K \ S" + then obtain N where "K \ cball 0 N" + by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI) + then show "\N. \n\N. K \ S \ cball 0 (real n)" + by (metis of_nat_le_iff Int_subset_iff \K \ S\ real_arch_simple subset_cball subset_trans) +qed auto + + +subsection \Continuity\ + +subsubsection%unimportant \Structural rules for uniform continuity\ + +lemma uniformly_continuous_on_dist[continuous_intros]: + fixes f g :: "'a::metric_space \ 'b::metric_space" + assumes "uniformly_continuous_on s f" + and "uniformly_continuous_on s g" + shows "uniformly_continuous_on s (\x. dist (f x) (g x))" +proof - + { + fix a b c d :: 'b + have "\dist a b - dist c d\ \ dist a c + dist b d" + using dist_triangle2 [of a b c] dist_triangle2 [of b c d] + using dist_triangle3 [of c d a] dist_triangle [of a d b] + by arith + } note le = this + { + fix x y + assume f: "(\n. dist (f (x n)) (f (y n))) \ 0" + assume g: "(\n. dist (g (x n)) (g (y n))) \ 0" + have "(\n. \dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))\) \ 0" + by (rule Lim_transform_bound [OF _ tendsto_add_zero [OF f g]], + simp add: le) + } + then show ?thesis + using assms unfolding uniformly_continuous_on_sequentially + unfolding dist_real_def by simp +qed + +lemma uniformly_continuous_on_norm[continuous_intros]: + fixes f :: "'a :: metric_space \ 'b :: real_normed_vector" + assumes "uniformly_continuous_on s f" + shows "uniformly_continuous_on s (\x. norm (f x))" + unfolding norm_conv_dist using assms + by (intro uniformly_continuous_on_dist uniformly_continuous_on_const) + +lemma uniformly_continuous_on_cmul[continuous_intros]: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + assumes "uniformly_continuous_on s f" + shows "uniformly_continuous_on s (\x. c *\<^sub>R f(x))" + using bounded_linear_scaleR_right assms + by (rule bounded_linear.uniformly_continuous_on) + +lemma dist_minus: + fixes x y :: "'a::real_normed_vector" + shows "dist (- x) (- y) = dist x y" + unfolding dist_norm minus_diff_minus norm_minus_cancel .. + +lemma uniformly_continuous_on_minus[continuous_intros]: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\x. - f x)" + unfolding uniformly_continuous_on_def dist_minus . + +lemma uniformly_continuous_on_add[continuous_intros]: + fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + assumes "uniformly_continuous_on s f" + and "uniformly_continuous_on s g" + shows "uniformly_continuous_on s (\x. f x + g x)" + using assms + unfolding uniformly_continuous_on_sequentially + unfolding dist_norm tendsto_norm_zero_iff add_diff_add + by (auto intro: tendsto_add_zero) + +lemma uniformly_continuous_on_diff[continuous_intros]: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + assumes "uniformly_continuous_on s f" + and "uniformly_continuous_on s g" + shows "uniformly_continuous_on s (\x. f x - g x)" + using assms uniformly_continuous_on_add [of s f "- g"] + by (simp add: fun_Compl_def uniformly_continuous_on_minus) + + +subsection%unimportant \Topological properties of linear functions\ + +lemma linear_lim_0: + assumes "bounded_linear f" + shows "(f \ 0) (at (0))" +proof - + interpret f: bounded_linear f by fact + have "(f \ f 0) (at 0)" + using tendsto_ident_at by (rule f.tendsto) + then show ?thesis unfolding f.zero . +qed + +lemma linear_continuous_at: + assumes "bounded_linear f" + shows "continuous (at a) f" + unfolding continuous_at using assms + apply (rule bounded_linear.tendsto) + apply (rule tendsto_ident_at) + done + +lemma linear_continuous_within: + "bounded_linear f \ continuous (at x within s) f" + using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto + +lemma linear_continuous_on: + "bounded_linear f \ continuous_on s f" + using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto + +end \ No newline at end of file diff -r c2d5575d9da5 -r 5aa5a8d6e5b5 src/HOL/Analysis/Elementary_Topology.thy --- a/src/HOL/Analysis/Elementary_Topology.thy Sat Dec 29 18:40:29 2018 +0000 +++ b/src/HOL/Analysis/Elementary_Topology.thy Sat Dec 29 20:32:09 2018 +0100 @@ -8,161 +8,15 @@ theory Elementary_Topology imports - "HOL-Library.Indicator_Function" - "HOL-Library.Countable_Set" - "HOL-Library.FuncSet" "HOL-Library.Set_Idioms" - "HOL-Library.Infinite_Set" Product_Vector begin -(* FIXME: move elsewhere *) -lemma approachable_lt_le: "(\(d::real) > 0. \x. f x < d \ P x) \ (\d>0. \x. f x \ d \ P x)" - apply auto - apply (rule_tac x="d/2" in exI) - apply auto - done - -lemma approachable_lt_le2: \ \like the above, but pushes aside an extra formula\ - "(\(d::real) > 0. \x. Q x \ f x < d \ P x) \ (\d>0. \x. f x \ d \ Q x \ P x)" - apply auto - apply (rule_tac x="d/2" in exI, auto) - done - -lemma triangle_lemma: - fixes x y z :: real - assumes x: "0 \ x" - and y: "0 \ y" - and z: "0 \ z" - and xy: "x\<^sup>2 \ y\<^sup>2 + z\<^sup>2" - shows "x \ y + z" -proof - - have "y\<^sup>2 + z\<^sup>2 \ y\<^sup>2 + 2 * y * z + z\<^sup>2" - using z y by simp - with xy have th: "x\<^sup>2 \ (y + z)\<^sup>2" - by (simp add: power2_eq_square field_simps) - from y z have yz: "y + z \ 0" - by arith - from power2_le_imp_le[OF th yz] show ?thesis . -qed - -definition (in monoid_add) support_on :: "'b set \ ('b \ 'a) \ 'b set" - where "support_on s f = {x\s. f x \ 0}" - -lemma in_support_on: "x \ support_on s f \ x \ s \ f x \ 0" - by (simp add: support_on_def) - -lemma support_on_simps[simp]: - "support_on {} f = {}" - "support_on (insert x s) f = - (if f x = 0 then support_on s f else insert x (support_on s f))" - "support_on (s \ t) f = support_on s f \ support_on t f" - "support_on (s \ t) f = support_on s f \ support_on t f" - "support_on (s - t) f = support_on s f - support_on t f" - "support_on (f ` s) g = f ` (support_on s (g \ f))" - unfolding support_on_def by auto - -lemma support_on_cong: - "(\x. x \ s \ f x = 0 \ g x = 0) \ support_on s f = support_on s g" - by (auto simp: support_on_def) - -lemma support_on_if: "a \ 0 \ support_on A (\x. if P x then a else 0) = {x\A. P x}" - by (auto simp: support_on_def) - -lemma support_on_if_subset: "support_on A (\x. if P x then a else 0) \ {x \ A. P x}" - by (auto simp: support_on_def) - -lemma finite_support[intro]: "finite S \ finite (support_on S f)" - unfolding support_on_def by auto - -(* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *) -definition (in comm_monoid_add) supp_sum :: "('b \ 'a) \ 'b set \ 'a" - where "supp_sum f S = (\x\support_on S f. f x)" - -lemma supp_sum_empty[simp]: "supp_sum f {} = 0" - unfolding supp_sum_def by auto - -lemma supp_sum_insert[simp]: - "finite (support_on S f) \ - supp_sum f (insert x S) = (if x \ S then supp_sum f S else f x + supp_sum f S)" - by (simp add: supp_sum_def in_support_on insert_absorb) +subsection \TODO: move?\ -lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (\n. f n / r) A" - by (cases "r = 0") - (auto simp: supp_sum_def sum_divide_distrib intro!: sum.cong support_on_cong) - -(*END OF SUPPORT, ETC.*) - -lemma image_affinity_interval: - fixes c :: "'a::ordered_real_vector" - shows "((\x. m *\<^sub>R x + c) ` {a..b}) = - (if {a..b}={} then {} - else if 0 \ m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} - else {m *\<^sub>R b + c .. m *\<^sub>R a + c})" - (is "?lhs = ?rhs") -proof (cases "m=0") - case True - then show ?thesis - by force -next - case False - show ?thesis - proof - show "?lhs \ ?rhs" - by (auto simp: scaleR_left_mono scaleR_left_mono_neg) - show "?rhs \ ?lhs" - proof (clarsimp, intro conjI impI subsetI) - show "\0 \ m; a \ b; x \ {m *\<^sub>R a + c..m *\<^sub>R b + c}\ - \ x \ (\x. m *\<^sub>R x + c) ` {a..b}" for x - apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI) - using False apply (auto simp: le_diff_eq pos_le_divideRI) - using diff_le_eq pos_le_divideR_eq by force - show "\\ 0 \ m; a \ b; x \ {m *\<^sub>R b + c..m *\<^sub>R a + c}\ - \ x \ (\x. m *\<^sub>R x + c) ` {a..b}" for x - apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI) - apply (auto simp: diff_le_eq neg_le_divideR_eq) - using diff_eq_diff_less_eq linordered_field_class.sign_simps(11) minus_diff_eq not_less scaleR_le_cancel_left_neg by fastforce - qed - qed -qed - -lemma countable_PiE: - "finite I \ (\i. i \ I \ countable (F i)) \ countable (Pi\<^sub>E I F)" - by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) - -lemma open_sums: - fixes T :: "('b::real_normed_vector) set" - assumes "open S \ open T" - shows "open (\x\ S. \y \ T. {x + y})" - using assms -proof - assume S: "open S" - show ?thesis - proof (clarsimp simp: open_dist) - fix x y - assume "x \ S" "y \ T" - with S obtain e where "e > 0" and e: "\x'. dist x' x < e \ x' \ S" - by (auto simp: open_dist) - then have "\z. dist z (x + y) < e \ \x\S. \y\T. z = x + y" - by (metis \y \ T\ diff_add_cancel dist_add_cancel2) - then show "\e>0. \z. dist z (x + y) < e \ (\x\S. \y\T. z = x + y)" - using \0 < e\ \x \ S\ by blast - qed -next - assume T: "open T" - show ?thesis - proof (clarsimp simp: open_dist) - fix x y - assume "x \ S" "y \ T" - with T obtain e where "e > 0" and e: "\x'. dist x' y < e \ x' \ T" - by (auto simp: open_dist) - then have "\z. dist z (x + y) < e \ \x\S. \y\T. z = x + y" - by (metis \x \ S\ add_diff_cancel_left' add_diff_eq diff_diff_add dist_norm) - then show "\e>0. \z. dist z (x + y) < e \ (\x\S. \y\T. z = x + y)" - using \0 < e\ \y \ T\ by blast - qed -qed +lemma open_subopen: "open S \ (\x\S. \T. open T \ x \ T \ T \ S)" + using openI by auto subsection \Topological Basis\ @@ -630,824 +484,8 @@ class polish_space = complete_space + second_countable_topology -subsection \General notion of a topology as a value\ -definition%important "istopology L \ - L {} \ (\S T. L S \ L T \ L (S \ T)) \ (\K. Ball K L \ L (\K))" - -typedef%important 'a topology = "{L::('a set) \ bool. istopology L}" - morphisms "openin" "topology" - unfolding istopology_def by blast - -lemma istopology_openin[intro]: "istopology(openin U)" - using openin[of U] by blast - -lemma topology_inverse': "istopology U \ openin (topology U) = U" - using topology_inverse[unfolded mem_Collect_eq] . - -lemma topology_inverse_iff: "istopology U \ openin (topology U) = U" - using topology_inverse[of U] istopology_openin[of "topology U"] by auto - -lemma topology_eq: "T1 = T2 \ (\S. openin T1 S \ openin T2 S)" -proof - assume "T1 = T2" - then show "\S. openin T1 S \ openin T2 S" by simp -next - assume H: "\S. openin T1 S \ openin T2 S" - then have "openin T1 = openin T2" by (simp add: fun_eq_iff) - then have "topology (openin T1) = topology (openin T2)" by simp - then show "T1 = T2" unfolding openin_inverse . -qed - - -text\The "universe": the union of all sets in the topology.\ -definition "topspace T = \{S. openin T S}" - -subsubsection \Main properties of open sets\ - -proposition openin_clauses: - fixes U :: "'a topology" - shows - "openin U {}" - "\S T. openin U S \ openin U T \ openin U (S\T)" - "\K. (\S \ K. openin U S) \ openin U (\K)" - using openin[of U] unfolding istopology_def mem_Collect_eq by fast+ - -lemma openin_subset[intro]: "openin U S \ S \ topspace U" - unfolding topspace_def by blast - -lemma openin_empty[simp]: "openin U {}" - by (rule openin_clauses) - -lemma openin_Int[intro]: "openin U S \ openin U T \ openin U (S \ T)" - by (rule openin_clauses) - -lemma openin_Union[intro]: "(\S. S \ K \ openin U S) \ openin U (\K)" - using openin_clauses by blast - -lemma openin_Un[intro]: "openin U S \ openin U T \ openin U (S \ T)" - using openin_Union[of "{S,T}" U] by auto - -lemma openin_topspace[intro, simp]: "openin U (topspace U)" - by (force simp: openin_Union topspace_def) - -lemma openin_subopen: "openin U S \ (\x \ S. \T. openin U T \ x \ T \ T \ S)" - (is "?lhs \ ?rhs") -proof - assume ?lhs - then show ?rhs by auto -next - assume H: ?rhs - let ?t = "\{T. openin U T \ T \ S}" - have "openin U ?t" by (force simp: openin_Union) - also have "?t = S" using H by auto - finally show "openin U S" . -qed - -lemma openin_INT [intro]: - assumes "finite I" - "\i. i \ I \ openin T (U i)" - shows "openin T ((\i \ I. U i) \ topspace T)" -using assms by (induct, auto simp: inf_sup_aci(2) openin_Int) - -lemma openin_INT2 [intro]: - assumes "finite I" "I \ {}" - "\i. i \ I \ openin T (U i)" - shows "openin T (\i \ I. U i)" -proof - - have "(\i \ I. U i) \ topspace T" - using \I \ {}\ openin_subset[OF assms(3)] by auto - then show ?thesis - using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute) -qed - -lemma openin_Inter [intro]: - assumes "finite \" "\ \ {}" "\X. X \ \ \ openin T X" shows "openin T (\\)" - by (metis (full_types) assms openin_INT2 image_ident) - -lemma openin_Int_Inter: - assumes "finite \" "openin T U" "\X. X \ \ \ openin T X" shows "openin T (U \ \\)" - using openin_Inter [of "insert U \"] assms by auto - - -subsubsection \Closed sets\ - -definition%important "closedin U S \ S \ topspace U \ openin U (topspace U - S)" - -lemma closedin_subset: "closedin U S \ S \ topspace U" - by (metis closedin_def) - -lemma closedin_empty[simp]: "closedin U {}" - by (simp add: closedin_def) - -lemma closedin_topspace[intro, simp]: "closedin U (topspace U)" - by (simp add: closedin_def) - -lemma closedin_Un[intro]: "closedin U S \ closedin U T \ closedin U (S \ T)" - by (auto simp: Diff_Un closedin_def) - -lemma Diff_Inter[intro]: "A - \S = \{A - s|s. s\S}" - by auto - -lemma closedin_Union: - assumes "finite S" "\T. T \ S \ closedin U T" - shows "closedin U (\S)" - using assms by induction auto - -lemma closedin_Inter[intro]: - assumes Ke: "K \ {}" - and Kc: "\S. S \K \ closedin U S" - shows "closedin U (\K)" - using Ke Kc unfolding closedin_def Diff_Inter by auto - -lemma closedin_INT[intro]: - assumes "A \ {}" "\x. x \ A \ closedin U (B x)" - shows "closedin U (\x\A. B x)" - apply (rule closedin_Inter) - using assms - apply auto - done - -lemma closedin_Int[intro]: "closedin U S \ closedin U T \ closedin U (S \ T)" - using closedin_Inter[of "{S,T}" U] by auto - -lemma openin_closedin_eq: "openin U S \ S \ topspace U \ closedin U (topspace U - S)" - apply (auto simp: closedin_def Diff_Diff_Int inf_absorb2) - apply (metis openin_subset subset_eq) - done - -lemma openin_closedin: "S \ topspace U \ (openin U S \ closedin U (topspace U - S))" - by (simp add: openin_closedin_eq) - -lemma openin_diff[intro]: - assumes oS: "openin U S" - and cT: "closedin U T" - shows "openin U (S - T)" -proof - - have "S - T = S \ (topspace U - T)" using openin_subset[of U S] oS cT - by (auto simp: topspace_def openin_subset) - then show ?thesis using oS cT - by (auto simp: closedin_def) -qed - -lemma closedin_diff[intro]: - assumes oS: "closedin U S" - and cT: "openin U T" - shows "closedin U (S - T)" -proof - - have "S - T = S \ (topspace U - T)" - using closedin_subset[of U S] oS cT by (auto simp: topspace_def) - then show ?thesis - using oS cT by (auto simp: openin_closedin_eq) -qed - - -subsection\The discrete topology\ - -definition discrete_topology where "discrete_topology U \ topology (\S. S \ U)" - -lemma openin_discrete_topology [simp]: "openin (discrete_topology U) S \ S \ U" -proof - - have "istopology (\S. S \ U)" - by (auto simp: istopology_def) - then show ?thesis - by (simp add: discrete_topology_def topology_inverse') -qed - -lemma topspace_discrete_topology [simp]: "topspace(discrete_topology U) = U" - by (meson openin_discrete_topology openin_subset openin_topspace order_refl subset_antisym) - -lemma closedin_discrete_topology [simp]: "closedin (discrete_topology U) S \ S \ U" - by (simp add: closedin_def) - -lemma discrete_topology_unique: - "discrete_topology U = X \ topspace X = U \ (\x \ U. openin X {x})" (is "?lhs = ?rhs") -proof - assume R: ?rhs - then have "openin X S" if "S \ U" for S - using openin_subopen subsetD that by fastforce - moreover have "x \ topspace X" if "openin X S" and "x \ S" for x S - using openin_subset that by blast - ultimately - show ?lhs - using R by (auto simp: topology_eq) -qed auto - -lemma discrete_topology_unique_alt: - "discrete_topology U = X \ topspace X \ U \ (\x \ U. openin X {x})" - using openin_subset - by (auto simp: discrete_topology_unique) - -lemma subtopology_eq_discrete_topology_empty: - "X = discrete_topology {} \ topspace X = {}" - using discrete_topology_unique [of "{}" X] by auto - -lemma subtopology_eq_discrete_topology_sing: - "X = discrete_topology {a} \ topspace X = {a}" - by (metis discrete_topology_unique openin_topspace singletonD) - - -subsection \Subspace topology\ - -definition%important "subtopology U V = topology (\T. \S. T = S \ V \ openin U S)" - -lemma istopology_subtopology: "istopology (\T. \S. T = S \ V \ openin U S)" - (is "istopology ?L") -proof - - have "?L {}" by blast - { - fix A B - assume A: "?L A" and B: "?L B" - from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \ V" and Sb: "openin U Sb" "B = Sb \ V" - by blast - have "A \ B = (Sa \ Sb) \ V" "openin U (Sa \ Sb)" - using Sa Sb by blast+ - then have "?L (A \ B)" by blast - } - moreover - { - fix K - assume K: "K \ Collect ?L" - have th0: "Collect ?L = (\S. S \ V) ` Collect (openin U)" - by blast - from K[unfolded th0 subset_image_iff] - obtain Sk where Sk: "Sk \ Collect (openin U)" "K = (\S. S \ V) ` Sk" - by blast - have "\K = (\Sk) \ V" - using Sk by auto - moreover have "openin U (\Sk)" - using Sk by (auto simp: subset_eq) - ultimately have "?L (\K)" by blast - } - ultimately show ?thesis - unfolding subset_eq mem_Collect_eq istopology_def by auto -qed - -lemma openin_subtopology: "openin (subtopology U V) S \ (\T. openin U T \ S = T \ V)" - unfolding subtopology_def topology_inverse'[OF istopology_subtopology] - by auto - -lemma openin_subtopology_Int: - "openin X S \ openin (subtopology X T) (S \ T)" - using openin_subtopology by auto - -lemma openin_subtopology_Int2: - "openin X T \ openin (subtopology X S) (S \ T)" - using openin_subtopology by auto - -lemma openin_subtopology_diff_closed: - "\S \ topspace X; closedin X T\ \ openin (subtopology X S) (S - T)" - unfolding closedin_def openin_subtopology - by (rule_tac x="topspace X - T" in exI) auto - -lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)" - by (force simp: relative_to_def openin_subtopology) - -lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \ V" - by (auto simp: topspace_def openin_subtopology) - -lemma closedin_subtopology: "closedin (subtopology U V) S \ (\T. closedin U T \ S = T \ V)" - unfolding closedin_def topspace_subtopology - by (auto simp: openin_subtopology) - -lemma openin_subtopology_refl: "openin (subtopology U V) V \ V \ topspace U" - unfolding openin_subtopology - by auto (metis IntD1 in_mono openin_subset) - -lemma subtopology_subtopology: - "subtopology (subtopology X S) T = subtopology X (S \ T)" -proof - - have eq: "\T'. (\S'. T' = S' \ T \ (\T. openin X T \ S' = T \ S)) = (\Sa. T' = Sa \ (S \ T) \ openin X Sa)" - by (metis inf_assoc) - have "subtopology (subtopology X S) T = topology (\Ta. \Sa. Ta = Sa \ T \ openin (subtopology X S) Sa)" - by (simp add: subtopology_def) - also have "\ = subtopology X (S \ T)" - by (simp add: openin_subtopology eq) (simp add: subtopology_def) - finally show ?thesis . -qed - -lemma openin_subtopology_alt: - "openin (subtopology X U) S \ S \ (\T. U \ T) ` Collect (openin X)" - by (simp add: image_iff inf_commute openin_subtopology) - -lemma closedin_subtopology_alt: - "closedin (subtopology X U) S \ S \ (\T. U \ T) ` Collect (closedin X)" - by (simp add: image_iff inf_commute closedin_subtopology) - -lemma subtopology_superset: - assumes UV: "topspace U \ V" - shows "subtopology U V = U" -proof - - { - fix S - { - fix T - assume T: "openin U T" "S = T \ V" - from T openin_subset[OF T(1)] UV have eq: "S = T" - by blast - have "openin U S" - unfolding eq using T by blast - } - moreover - { - assume S: "openin U S" - then have "\T. openin U T \ S = T \ V" - using openin_subset[OF S] UV by auto - } - ultimately have "(\T. openin U T \ S = T \ V) \ openin U S" - by blast - } - then show ?thesis - unfolding topology_eq openin_subtopology by blast -qed - -lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" - by (simp add: subtopology_superset) - -lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" - by (simp add: subtopology_superset) - -lemma openin_subtopology_empty: - "openin (subtopology U {}) S \ S = {}" -by (metis Int_empty_right openin_empty openin_subtopology) - -lemma closedin_subtopology_empty: - "closedin (subtopology U {}) S \ S = {}" -by (metis Int_empty_right closedin_empty closedin_subtopology) - -lemma closedin_subtopology_refl [simp]: - "closedin (subtopology U X) X \ X \ topspace U" -by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology) - -lemma closedin_topspace_empty: "topspace T = {} \ (closedin T S \ S = {})" - by (simp add: closedin_def) - -lemma openin_imp_subset: - "openin (subtopology U S) T \ T \ S" -by (metis Int_iff openin_subtopology subsetI) - -lemma closedin_imp_subset: - "closedin (subtopology U S) T \ T \ S" -by (simp add: closedin_def topspace_subtopology) - -lemma openin_open_subtopology: - "openin X S \ openin (subtopology X S) T \ openin X T \ T \ S" - by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology) - -lemma closedin_closed_subtopology: - "closedin X S \ (closedin (subtopology X S) T \ closedin X T \ T \ S)" - by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE) - -lemma openin_subtopology_Un: - "\openin (subtopology X T) S; openin (subtopology X U) S\ - \ openin (subtopology X (T \ U)) S" -by (simp add: openin_subtopology) blast - -lemma closedin_subtopology_Un: - "\closedin (subtopology X T) S; closedin (subtopology X U) S\ - \ closedin (subtopology X (T \ U)) S" -by (simp add: closedin_subtopology) blast - - -subsection \The standard Euclidean topology\ - -definition%important euclidean :: "'a::topological_space topology" - where "euclidean = topology open" - -lemma open_openin: "open S \ openin euclidean S" - unfolding euclidean_def - apply (rule cong[where x=S and y=S]) - apply (rule topology_inverse[symmetric]) - apply (auto simp: istopology_def) - done - -declare open_openin [symmetric, simp] - -lemma topspace_euclidean [simp]: "topspace euclidean = UNIV" - by (force simp: topspace_def) - -lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S" - by (simp add: topspace_subtopology) - -lemma closed_closedin: "closed S \ closedin euclidean S" - by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV) - -declare closed_closedin [symmetric, simp] - -lemma open_subopen: "open S \ (\x\S. \T. open T \ x \ T \ T \ S)" - using openI by auto - -lemma openin_subtopology_self [simp]: "openin (subtopology euclidean S) S" - by (metis openin_topspace topspace_euclidean_subtopology) - -subsubsection\The most basic facts about the usual topology and metric on R\ - -abbreviation euclideanreal :: "real topology" - where "euclideanreal \ topology open" - -lemma real_openin [simp]: "openin euclideanreal S = open S" - by (simp add: euclidean_def open_openin) - -lemma topspace_euclideanreal [simp]: "topspace euclideanreal = UNIV" - using openin_subset open_UNIV real_openin by blast - -lemma topspace_euclideanreal_subtopology [simp]: - "topspace (subtopology euclideanreal S) = S" - by (simp add: topspace_subtopology) - -lemma real_closedin [simp]: "closedin euclideanreal S = closed S" - by (simp add: closed_closedin euclidean_def) - -subsection \Basic "localization" results are handy for connectedness.\ - -lemma openin_open: "openin (subtopology euclidean U) S \ (\T. open T \ (S = U \ T))" - by (auto simp: openin_subtopology) - -lemma openin_Int_open: - "\openin (subtopology euclidean U) S; open T\ - \ openin (subtopology euclidean U) (S \ T)" -by (metis open_Int Int_assoc openin_open) - -lemma openin_open_Int[intro]: "open S \ openin (subtopology euclidean U) (U \ S)" - by (auto simp: openin_open) - -lemma open_openin_trans[trans]: - "open S \ open T \ T \ S \ openin (subtopology euclidean S) T" - by (metis Int_absorb1 openin_open_Int) - -lemma open_subset: "S \ T \ open S \ openin (subtopology euclidean T) S" - by (auto simp: openin_open) - -lemma closedin_closed: "closedin (subtopology euclidean U) S \ (\T. closed T \ S = U \ T)" - by (simp add: closedin_subtopology Int_ac) - -lemma closedin_closed_Int: "closed S \ closedin (subtopology euclidean U) (U \ S)" - by (metis closedin_closed) - -lemma closed_subset: "S \ T \ closed S \ closedin (subtopology euclidean T) S" - by (auto simp: closedin_closed) - -lemma closedin_closed_subset: - "\closedin (subtopology euclidean U) V; T \ U; S = V \ T\ - \ closedin (subtopology euclidean T) S" - by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE) - -lemma finite_imp_closedin: - fixes S :: "'a::t1_space set" - shows "\finite S; S \ T\ \ closedin (subtopology euclidean T) S" - by (simp add: finite_imp_closed closed_subset) - -lemma closedin_singleton [simp]: - fixes a :: "'a::t1_space" - shows "closedin (subtopology euclidean U) {a} \ a \ U" -using closedin_subset by (force intro: closed_subset) - -lemma openin_euclidean_subtopology_iff: - fixes S U :: "'a::metric_space set" - shows "openin (subtopology euclidean U) S \ - S \ U \ (\x\S. \e>0. \x'\U. dist x' x < e \ x'\ S)" - (is "?lhs \ ?rhs") -proof - assume ?lhs - then show ?rhs - unfolding openin_open open_dist by blast -next - define T where "T = {x. \a\S. \d>0. (\y\U. dist y a < d \ y \ S) \ dist x a < d}" - have 1: "\x\T. \e>0. \y. dist y x < e \ y \ T" - unfolding T_def - apply clarsimp - apply (rule_tac x="d - dist x a" in exI) - apply (clarsimp simp add: less_diff_eq) - by (metis dist_commute dist_triangle_lt) - assume ?rhs then have 2: "S = U \ T" - unfolding T_def - by auto (metis dist_self) - from 1 2 show ?lhs - unfolding openin_open open_dist by fast -qed - -lemma connected_openin: - "connected S \ - \(\E1 E2. openin (subtopology euclidean S) E1 \ - openin (subtopology euclidean S) E2 \ - S \ E1 \ E2 \ E1 \ E2 = {} \ E1 \ {} \ E2 \ {})" - apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe) - apply (simp_all, blast+) (* SLOW *) - done - -lemma connected_openin_eq: - "connected S \ - \(\E1 E2. openin (subtopology euclidean S) E1 \ - openin (subtopology euclidean S) E2 \ - E1 \ E2 = S \ E1 \ E2 = {} \ - E1 \ {} \ E2 \ {})" - apply (simp add: connected_openin, safe, blast) - by (metis Int_lower1 Un_subset_iff openin_open subset_antisym) - -lemma connected_closedin: - "connected S \ - (\E1 E2. - closedin (subtopology euclidean S) E1 \ - closedin (subtopology euclidean S) E2 \ - S \ E1 \ E2 \ E1 \ E2 = {} \ E1 \ {} \ E2 \ {})" - (is "?lhs = ?rhs") -proof - assume ?lhs - then show ?rhs - by (auto simp add: connected_closed closedin_closed) -next - assume R: ?rhs - then show ?lhs - proof (clarsimp simp add: connected_closed closedin_closed) - fix A B - assume s_sub: "S \ A \ B" "B \ S \ {}" - and disj: "A \ B \ S = {}" - and cl: "closed A" "closed B" - have "S \ (A \ B) = S" - using s_sub(1) by auto - have "S - A = B \ S" - using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto - then have "S \ A = {}" - by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int R cl closedin_closed_Int inf_commute order_refl s_sub(2)) - then show "A \ S = {}" - by blast - qed -qed - -lemma connected_closedin_eq: - "connected S \ - \(\E1 E2. - closedin (subtopology euclidean S) E1 \ - closedin (subtopology euclidean S) E2 \ - E1 \ E2 = S \ E1 \ E2 = {} \ - E1 \ {} \ E2 \ {})" - apply (simp add: connected_closedin, safe, blast) - by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym) - -text \These "transitivity" results are handy too\ - -lemma openin_trans[trans]: - "openin (subtopology euclidean T) S \ openin (subtopology euclidean U) T \ - openin (subtopology euclidean U) S" - unfolding open_openin openin_open by blast - -lemma openin_open_trans: "openin (subtopology euclidean T) S \ open T \ open S" - by (auto simp: openin_open intro: openin_trans) - -lemma closedin_trans[trans]: - "closedin (subtopology euclidean T) S \ closedin (subtopology euclidean U) T \ - closedin (subtopology euclidean U) S" - by (auto simp: closedin_closed closed_Inter Int_assoc) - -lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \ closed T \ closed S" - by (auto simp: closedin_closed intro: closedin_trans) - -lemma openin_subtopology_Int_subset: - "\openin (subtopology euclidean u) (u \ S); v \ u\ \ openin (subtopology euclidean v) (v \ S)" - by (auto simp: openin_subtopology) - -lemma openin_open_eq: "open s \ (openin (subtopology euclidean s) t \ open t \ t \ s)" - using open_subset openin_open_trans openin_subset by fastforce - - -subsection \Open and closed balls\ - -definition%important ball :: "'a::metric_space \ real \ 'a set" - where "ball x e = {y. dist x y < e}" - -definition%important cball :: "'a::metric_space \ real \ 'a set" - where "cball x e = {y. dist x y \ e}" - -definition%important sphere :: "'a::metric_space \ real \ 'a set" - where "sphere x e = {y. dist x y = e}" - -lemma mem_ball [simp]: "y \ ball x e \ dist x y < e" - by (simp add: ball_def) - -lemma mem_cball [simp]: "y \ cball x e \ dist x y \ e" - by (simp add: cball_def) - -lemma mem_sphere [simp]: "y \ sphere x e \ dist x y = e" - by (simp add: sphere_def) - -lemma ball_trivial [simp]: "ball x 0 = {}" - by (simp add: ball_def) - -lemma cball_trivial [simp]: "cball x 0 = {x}" - by (simp add: cball_def) - -lemma sphere_trivial [simp]: "sphere x 0 = {x}" - by (simp add: sphere_def) - -lemma mem_ball_0 [simp]: "x \ ball 0 e \ norm x < e" - for x :: "'a::real_normed_vector" - by (simp add: dist_norm) - -lemma mem_cball_0 [simp]: "x \ cball 0 e \ norm x \ e" - for x :: "'a::real_normed_vector" - by (simp add: dist_norm) - -lemma disjoint_ballI: "dist x y \ r+s \ ball x r \ ball y s = {}" - using dist_triangle_less_add not_le by fastforce - -lemma disjoint_cballI: "dist x y > r + s \ cball x r \ cball y s = {}" - by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball) - -lemma mem_sphere_0 [simp]: "x \ sphere 0 e \ norm x = e" - for x :: "'a::real_normed_vector" - by (simp add: dist_norm) - -lemma sphere_empty [simp]: "r < 0 \ sphere a r = {}" - for a :: "'a::metric_space" - by auto - -lemma centre_in_ball [simp]: "x \ ball x e \ 0 < e" - by simp - -lemma centre_in_cball [simp]: "x \ cball x e \ 0 \ e" - by simp - -lemma ball_subset_cball [simp, intro]: "ball x e \ cball x e" - by (simp add: subset_eq) - -lemma mem_ball_imp_mem_cball: "x \ ball y e \ x \ cball y e" - by (auto simp: mem_ball mem_cball) - -lemma sphere_cball [simp,intro]: "sphere z r \ cball z r" - by force - -lemma cball_diff_sphere: "cball a r - sphere a r = ball a r" - by auto - -lemma subset_ball[intro]: "d \ e \ ball x d \ ball x e" - by (simp add: subset_eq) - -lemma subset_cball[intro]: "d \ e \ cball x d \ cball x e" - by (simp add: subset_eq) - -lemma mem_ball_leI: "x \ ball y e \ e \ f \ x \ ball y f" - by (auto simp: mem_ball mem_cball) - -lemma mem_cball_leI: "x \ cball y e \ e \ f \ x \ cball y f" - by (auto simp: mem_ball mem_cball) - -lemma cball_trans: "y \ cball z b \ x \ cball y a \ x \ cball z (b + a)" - unfolding mem_cball -proof - - have "dist z x \ dist z y + dist y x" - by (rule dist_triangle) - also assume "dist z y \ b" - also assume "dist y x \ a" - finally show "dist z x \ b + a" by arith -qed - -lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s" - by (simp add: set_eq_iff) arith - -lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s" - by (simp add: set_eq_iff) - -lemma cball_max_Un: "cball a (max r s) = cball a r \ cball a s" - by (simp add: set_eq_iff) arith - -lemma cball_min_Int: "cball a (min r s) = cball a r \ cball a s" - by (simp add: set_eq_iff) - -lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r" - by (auto simp: cball_def ball_def dist_commute) - -lemma image_add_ball [simp]: - fixes a :: "'a::real_normed_vector" - shows "(+) b ` ball a r = ball (a+b) r" -apply (intro equalityI subsetI) -apply (force simp: dist_norm) -apply (rule_tac x="x-b" in image_eqI) -apply (auto simp: dist_norm algebra_simps) -done - -lemma image_add_cball [simp]: - fixes a :: "'a::real_normed_vector" - shows "(+) b ` cball a r = cball (a+b) r" -apply (intro equalityI subsetI) -apply (force simp: dist_norm) -apply (rule_tac x="x-b" in image_eqI) -apply (auto simp: dist_norm algebra_simps) -done - -lemma open_ball [intro, simp]: "open (ball x e)" -proof - - have "open (dist x -` {.. (\x\S. \e>0. ball x e \ S)" - by (simp add: open_dist subset_eq mem_ball Ball_def dist_commute) - -lemma openI [intro?]: "(\x. x\S \ \e>0. ball x e \ S) \ open S" - by (auto simp: open_contains_ball) - -lemma openE[elim?]: - assumes "open S" "x\S" - obtains e where "e>0" "ball x e \ S" - using assms unfolding open_contains_ball by auto - -lemma open_contains_ball_eq: "open S \ x\S \ (\e>0. ball x e \ S)" - by (metis open_contains_ball subset_eq centre_in_ball) - -lemma openin_contains_ball: - "openin (subtopology euclidean t) s \ - s \ t \ (\x \ s. \e. 0 < e \ ball x e \ t \ s)" - (is "?lhs = ?rhs") -proof - assume ?lhs - then show ?rhs - apply (simp add: openin_open) - apply (metis Int_commute Int_mono inf.cobounded2 open_contains_ball order_refl subsetCE) - done -next - assume ?rhs - then show ?lhs - apply (simp add: openin_euclidean_subtopology_iff) - by (metis (no_types) Int_iff dist_commute inf.absorb_iff2 mem_ball) -qed - -lemma openin_contains_cball: - "openin (subtopology euclidean t) s \ - s \ t \ - (\x \ s. \e. 0 < e \ cball x e \ t \ s)" -apply (simp add: openin_contains_ball) -apply (rule iffI) -apply (auto dest!: bspec) -apply (rule_tac x="e/2" in exI, force+) -done - -lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0" - unfolding mem_ball set_eq_iff - apply (simp add: not_less) - apply (metis zero_le_dist order_trans dist_self) - done - -lemma ball_empty: "e \ 0 \ ball x e = {}" by simp - -lemma closed_cball [iff]: "closed (cball x e)" -proof - - have "closed (dist x -` {..e})" - by (intro closed_vimage closed_atMost continuous_intros) - also have "dist x -` {..e} = cball x e" - by auto - finally show ?thesis . -qed - -lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)" -proof - - { - fix x and e::real - assume "x\S" "e>0" "ball x e \ S" - then have "\d>0. cball x d \ S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto) - } - moreover - { - fix x and e::real - assume "x\S" "e>0" "cball x e \ S" - then have "\d>0. ball x d \ S" - unfolding subset_eq - apply (rule_tac x="e/2" in exI, auto) - done - } - ultimately show ?thesis - unfolding open_contains_ball by auto -qed - -lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\e>0. cball x e \ S))" - by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball) - -lemma eventually_nhds_ball: "d > 0 \ eventually (\x. x \ ball z d) (nhds z)" - by (rule eventually_nhds_in_open) simp_all - -lemma eventually_at_ball: "d > 0 \ eventually (\t. t \ ball z d \ t \ A) (at z within A)" - unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute) - -lemma eventually_at_ball': "d > 0 \ eventually (\t. t \ ball z d \ t \ z \ t \ A) (at z within A)" - unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute) - -lemma at_within_ball: "e > 0 \ dist x y < e \ at y within ball x e = at y" - by (subst at_within_open) auto - -lemma atLeastAtMost_eq_cball: - fixes a b::real - shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)" - by (auto simp: dist_real_def field_simps mem_cball) - -lemma greaterThanLessThan_eq_ball: - fixes a b::real - shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)" - by (auto simp: dist_real_def field_simps mem_ball) - - -subsection \Limit points\ +subsection \Limit Points\ definition%important (in topological_space) islimpt:: "'a \ 'a set \ bool" (infixr "islimpt" 60) where "x islimpt S \ (\T. x\T \ open T \ (\y\S. y\T \ y\x))" @@ -1468,18 +506,6 @@ lemma islimpt_subset: "x islimpt S \ S \ T \ x islimpt T" unfolding islimpt_def by fast -lemma islimpt_approachable: - fixes x :: "'a::metric_space" - shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" - unfolding islimpt_iff_eventually eventually_at by fast - -lemma islimpt_approachable_le: "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)" - for x :: "'a::metric_space" - unfolding islimpt_approachable - using approachable_lt_le [where f="\y. dist y x" and P="\y. y \ S \ y = x", - THEN arg_cong [where f=Not]] - by (simp add: Bex_def conj_commute conj_left_commute) - lemma islimpt_UNIV_iff: "x islimpt UNIV \ \ open {x}" unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast) @@ -1492,10 +518,6 @@ for x :: "'a::perfect_space" unfolding islimpt_UNIV_iff by (rule not_open_singleton) -lemma perfect_choose_dist: "0 < r \ \a. a \ x \ dist a x < r" - for x :: "'a::{perfect_space,metric_space}" - using islimpt_UNIV [of x] by (simp add: islimpt_approachable) - lemma closed_limpt: "closed S \ (\x. x islimpt S \ x \ S)" unfolding closed_def apply (subst open_subopen) @@ -1506,95 +528,160 @@ lemma islimpt_EMPTY[simp]: "\ x islimpt {}" by (auto simp: islimpt_def) -lemma finite_ball_include: - fixes a :: "'a::metric_space" - assumes "finite S" - shows "\e>0. S \ ball a e" - using assms -proof induction - case (insert x S) - then obtain e0 where "e0>0" and e0:"S \ ball a e0" by auto - define e where "e = max e0 (2 * dist a x)" - have "e>0" unfolding e_def using \e0>0\ by auto - moreover have "insert x S \ ball a e" - using e0 \e>0\ unfolding e_def by auto - ultimately show ?case by auto -qed (auto intro: zero_less_one) - -lemma finite_set_avoid: - fixes a :: "'a::metric_space" - assumes "finite S" - shows "\d>0. \x\S. x \ a \ d \ dist a x" - using assms -proof induction - case (insert x S) - then obtain d where "d > 0" and d: "\x\S. x \ a \ d \ dist a x" - by blast - show ?case - proof (cases "x = a") - case True - with \d > 0 \d show ?thesis by auto - next - case False - let ?d = "min d (dist a x)" - from False \d > 0\ have dp: "?d > 0" - by auto - from d have d': "\x\S. x \ a \ ?d \ dist a x" - by auto - with dp False show ?thesis - by (metis insert_iff le_less min_less_iff_conj not_less) - qed -qed (auto intro: zero_less_one) - lemma islimpt_Un: "x islimpt (S \ T) \ x islimpt S \ x islimpt T" by (simp add: islimpt_iff_eventually eventually_conj_iff) -lemma discrete_imp_closed: - fixes S :: "'a::metric_space set" - assumes e: "0 < e" - and d: "\x \ S. \y \ S. dist y x < e \ y = x" - shows "closed S" -proof - - have False if C: "\e. e>0 \ \x'\S. x' \ x \ dist x' x < e" for x - proof - - from e have e2: "e/2 > 0" by arith - from C[rule_format, OF e2] obtain y where y: "y \ S" "y \ x" "dist y x < e/2" - by blast - let ?m = "min (e/2) (dist x y) " - from e2 y(2) have mp: "?m > 0" - by simp - from C[OF mp] obtain z where z: "z \ S" "z \ x" "dist z x < ?m" - by blast - from z y have "dist z y < e" - by (intro dist_triangle_lt [where z=x]) simp - from d[rule_format, OF y(1) z(1) this] y z show ?thesis - by (auto simp: dist_commute) + +lemma islimpt_insert: + fixes x :: "'a::t1_space" + shows "x islimpt (insert a s) \ x islimpt s" +proof + assume *: "x islimpt (insert a s)" + show "x islimpt s" + proof (rule islimptI) + fix t + assume t: "x \ t" "open t" + show "\y\s. y \ t \ y \ x" + proof (cases "x = a") + case True + obtain y where "y \ insert a s" "y \ t" "y \ x" + using * t by (rule islimptE) + with \x = a\ show ?thesis by auto + next + case False + with t have t': "x \ t - {a}" "open (t - {a})" + by (simp_all add: open_Diff) + obtain y where "y \ insert a s" "y \ t - {a}" "y \ x" + using * t' by (rule islimptE) + then show ?thesis by auto + qed qed - then show ?thesis - by (metis islimpt_approachable closed_limpt [where 'a='a]) +next + assume "x islimpt s" + then show "x islimpt (insert a s)" + by (rule islimpt_subset) auto +qed + +lemma islimpt_finite: + fixes x :: "'a::t1_space" + shows "finite s \ \ x islimpt s" + by (induct set: finite) (simp_all add: islimpt_insert) + +lemma islimpt_Un_finite: + fixes x :: "'a::t1_space" + shows "finite s \ x islimpt (s \ t) \ x islimpt t" + by (simp add: islimpt_Un islimpt_finite) + +lemma islimpt_eq_acc_point: + fixes l :: "'a :: t1_space" + shows "l islimpt S \ (\U. l\U \ open U \ infinite (U \ S))" +proof (safe intro!: islimptI) + fix U + assume "l islimpt S" "l \ U" "open U" "finite (U \ S)" + then have "l islimpt S" "l \ (U - (U \ S - {l}))" "open (U - (U \ S - {l}))" + by (auto intro: finite_imp_closed) + then show False + by (rule islimptE) auto +next + fix T + assume *: "\U. l\U \ open U \ infinite (U \ S)" "l \ T" "open T" + then have "infinite (T \ S - {l})" + by auto + then have "\x. x \ (T \ S - {l})" + unfolding ex_in_conv by (intro notI) simp + then show "\y\S. y \ T \ y \ l" + by auto qed -lemma closed_of_nat_image: "closed (of_nat ` A :: 'a::real_normed_algebra_1 set)" - by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_nat) - -lemma closed_of_int_image: "closed (of_int ` A :: 'a::real_normed_algebra_1 set)" - by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_int) - -lemma closed_Nats [simp]: "closed (\ :: 'a :: real_normed_algebra_1 set)" - unfolding Nats_def by (rule closed_of_nat_image) +lemma acc_point_range_imp_convergent_subsequence: + fixes l :: "'a :: first_countable_topology" + assumes l: "\U. l\U \ open U \ infinite (U \ range f)" + shows "\r::nat\nat. strict_mono r \ (f \ r) \ l" +proof - + from countable_basis_at_decseq[of l] + obtain A where A: + "\i. open (A i)" + "\i. l \ A i" + "\S. open S \ l \ S \ eventually (\i. A i \ S) sequentially" + by blast + define s where "s n i = (SOME j. i < j \ f j \ A (Suc n))" for n i + { + fix n i + have "infinite (A (Suc n) \ range f - f`{.. i})" + using l A by auto + then have "\x. x \ A (Suc n) \ range f - f`{.. i}" + unfolding ex_in_conv by (intro notI) simp + then have "\j. f j \ A (Suc n) \ j \ {.. i}" + by auto + then have "\a. i < a \ f a \ A (Suc n)" + by (auto simp: not_le) + then have "i < s n i" "f (s n i) \ A (Suc n)" + unfolding s_def by (auto intro: someI2_ex) + } + note s = this + define r where "r = rec_nat (s 0 0) s" + have "strict_mono r" + by (auto simp: r_def s strict_mono_Suc_iff) + moreover + have "(\n. f (r n)) \ l" + proof (rule topological_tendstoI) + fix S + assume "open S" "l \ S" + with A(3) have "eventually (\i. A i \ S) sequentially" + by auto + moreover + { + fix i + assume "Suc 0 \ i" + then have "f (r i) \ A i" + by (cases i) (simp_all add: r_def s) + } + then have "eventually (\i. f (r i) \ A i) sequentially" + by (auto simp: eventually_sequentially) + ultimately show "eventually (\i. f (r i) \ S) sequentially" + by eventually_elim auto + qed + ultimately show "\r::nat\nat. strict_mono r \ (f \ r) \ l" + by (auto simp: convergent_def comp_def) +qed -lemma closed_Ints [simp]: "closed (\ :: 'a :: real_normed_algebra_1 set)" - unfolding Ints_def by (rule closed_of_int_image) +lemma islimpt_range_imp_convergent_subsequence: + fixes l :: "'a :: {t1_space, first_countable_topology}" + assumes l: "l islimpt (range f)" + shows "\r::nat\nat. strict_mono r \ (f \ r) \ l" + using l unfolding islimpt_eq_acc_point + by (rule acc_point_range_imp_convergent_subsequence) -lemma closed_subset_Ints: - fixes A :: "'a :: real_normed_algebra_1 set" - assumes "A \ \" - shows "closed A" -proof (intro discrete_imp_closed[OF zero_less_one] ballI impI, goal_cases) - case (1 x y) - with assms have "x \ \" and "y \ \" by auto - with \dist y x < 1\ show "y = x" - by (auto elim!: Ints_cases simp: dist_of_int) +lemma sequence_unique_limpt: + fixes f :: "nat \ 'a::t2_space" + assumes "(f \ l) sequentially" + and "l' islimpt (range f)" + shows "l' = l" +proof (rule ccontr) + assume "l' \ l" + obtain s t where "open s" "open t" "l' \ s" "l \ t" "s \ t = {}" + using hausdorff [OF \l' \ l\] by auto + have "eventually (\n. f n \ t) sequentially" + using assms(1) \open t\ \l \ t\ by (rule topological_tendstoD) + then obtain N where "\n\N. f n \ t" + unfolding eventually_sequentially by auto + + have "UNIV = {.. {N..}" + by auto + then have "l' islimpt (f ` ({.. {N..}))" + using assms(2) by simp + then have "l' islimpt (f ` {.. f ` {N..})" + by (simp add: image_Un) + then have "l' islimpt (f ` {N..})" + by (simp add: islimpt_Un_finite) + then obtain y where "y \ f ` {N..}" "y \ s" "y \ l'" + using \l' \ s\ \open s\ by (rule islimptE) + then obtain n where "N \ n" "f n \ s" "f n \ l'" + by auto + with \\n\N. f n \ t\ have "f n \ s \ t" + by simp + with \s \ t = {}\ show False + by simp qed @@ -1659,10 +746,6 @@ by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1 Int_lower2 interior_maximal interior_subset open_Int open_interior) -lemma mem_interior: "x \ interior S \ (\e>0. ball x e \ S)" - using open_contains_ball_eq [where S="interior S"] - by (simp add: open_subset_interior) - lemma eventually_nhds_in_nhd: "x \ interior s \ eventually (\y. y \ s) (nhds x)" using interior_subset[of s] by (subst eventually_nhds) blast @@ -1874,159 +957,12 @@ done qed -lemma closure_openin_Int_closure: - assumes ope: "openin (subtopology euclidean U) S" and "T \ U" - shows "closure(S \ closure T) = closure(S \ T)" -proof - obtain V where "open V" and S: "S = U \ V" - using ope using openin_open by metis - show "closure (S \ closure T) \ closure (S \ T)" - proof (clarsimp simp: S) - fix x - assume "x \ closure (U \ V \ closure T)" - then have "V \ closure T \ A \ x \ closure A" for A - by (metis closure_mono subsetD inf.coboundedI2 inf_assoc) - then have "x \ closure (T \ V)" - by (metis \open V\ closure_closure inf_commute open_Int_closure_subset) - then show "x \ closure (U \ V \ T)" - by (metis \T \ U\ inf.absorb_iff2 inf_assoc inf_commute) - qed -next - show "closure (S \ T) \ closure (S \ closure T)" - by (meson Int_mono closure_mono closure_subset order_refl) -qed - lemma islimpt_in_closure: "(x islimpt S) = (x\closure(S-{x}))" unfolding closure_def using islimpt_punctured by blast lemma connected_imp_connected_closure: "connected S \ connected (closure S)" by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD) -lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \ x islimpt S" - for x :: "'a::metric_space" - apply (clarsimp simp add: islimpt_approachable) - apply (drule_tac x="e/2" in spec) - apply (auto simp: simp del: less_divide_eq_numeral1) - apply (drule_tac x="dist x' x" in spec) - apply (auto simp: zero_less_dist_iff simp del: less_divide_eq_numeral1) - apply (erule rev_bexI) - apply (metis dist_commute dist_triangle_half_r less_trans less_irrefl) - done - -lemma closed_limpts: "closed {x::'a::metric_space. x islimpt S}" - using closed_limpt limpt_of_limpts by blast - -lemma limpt_of_closure: "x islimpt closure S \ x islimpt S" - for x :: "'a::metric_space" - by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts) - -lemma closedin_limpt: - "closedin (subtopology euclidean T) S \ S \ T \ (\x. x islimpt S \ x \ T \ x \ S)" - apply (simp add: closedin_closed, safe) - apply (simp add: closed_limpt islimpt_subset) - apply (rule_tac x="closure S" in exI, simp) - apply (force simp: closure_def) - done - -lemma closedin_closed_eq: "closed S \ closedin (subtopology euclidean S) T \ closed T \ T \ S" - by (meson closedin_limpt closed_subset closedin_closed_trans) - -lemma connected_closed_set: - "closed S - \ connected S \ (\A B. closed A \ closed B \ A \ {} \ B \ {} \ A \ B = S \ A \ B = {})" - unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast - -text \If a connnected set is written as the union of two nonempty closed sets, then these sets -have to intersect.\ - -lemma connected_as_closed_union: - assumes "connected C" "C = A \ B" "closed A" "closed B" "A \ {}" "B \ {}" - shows "A \ B \ {}" -by (metis assms closed_Un connected_closed_set) - -lemma closedin_subset_trans: - "closedin (subtopology euclidean U) S \ S \ T \ T \ U \ - closedin (subtopology euclidean T) S" - by (meson closedin_limpt subset_iff) - -lemma openin_subset_trans: - "openin (subtopology euclidean U) S \ S \ T \ T \ U \ - openin (subtopology euclidean T) S" - by (auto simp: openin_open) - -lemma openin_Times: - "openin (subtopology euclidean S) S' \ openin (subtopology euclidean T) T' \ - openin (subtopology euclidean (S \ T)) (S' \ T')" - unfolding openin_open using open_Times by blast - -lemma Times_in_interior_subtopology: - fixes U :: "('a::metric_space \ 'b::metric_space) set" - assumes "(x, y) \ U" "openin (subtopology euclidean (S \ T)) U" - obtains V W where "openin (subtopology euclidean S) V" "x \ V" - "openin (subtopology euclidean T) W" "y \ W" "(V \ W) \ U" -proof - - from assms obtain e where "e > 0" and "U \ S \ T" - and e: "\x' y'. \x'\S; y'\T; dist (x', y') (x, y) < e\ \ (x', y') \ U" - by (force simp: openin_euclidean_subtopology_iff) - with assms have "x \ S" "y \ T" - by auto - show ?thesis - proof - show "openin (subtopology euclidean S) (ball x (e/2) \ S)" - by (simp add: Int_commute openin_open_Int) - show "x \ ball x (e / 2) \ S" - by (simp add: \0 < e\ \x \ S\) - show "openin (subtopology euclidean T) (ball y (e/2) \ T)" - by (simp add: Int_commute openin_open_Int) - show "y \ ball y (e / 2) \ T" - by (simp add: \0 < e\ \y \ T\) - show "(ball x (e / 2) \ S) \ (ball y (e / 2) \ T) \ U" - by clarify (simp add: e dist_Pair_Pair \0 < e\ dist_commute sqrt_sum_squares_half_less) - qed -qed - -lemma openin_Times_eq: - fixes S :: "'a::metric_space set" and T :: "'b::metric_space set" - shows - "openin (subtopology euclidean (S \ T)) (S' \ T') \ - S' = {} \ T' = {} \ openin (subtopology euclidean S) S' \ openin (subtopology euclidean T) T'" - (is "?lhs = ?rhs") -proof (cases "S' = {} \ T' = {}") - case True - then show ?thesis by auto -next - case False - then obtain x y where "x \ S'" "y \ T'" - by blast - show ?thesis - proof - assume ?lhs - have "openin (subtopology euclidean S) S'" - apply (subst openin_subopen, clarify) - apply (rule Times_in_interior_subtopology [OF _ \?lhs\]) - using \y \ T'\ - apply auto - done - moreover have "openin (subtopology euclidean T) T'" - apply (subst openin_subopen, clarify) - apply (rule Times_in_interior_subtopology [OF _ \?lhs\]) - using \x \ S'\ - apply auto - done - ultimately show ?rhs - by simp - next - assume ?rhs - with False show ?lhs - by (simp add: openin_Times) - qed -qed - -lemma closedin_Times: - "closedin (subtopology euclidean S) S' \ closedin (subtopology euclidean T) T' \ - closedin (subtopology euclidean (S \ T)) (S' \ T')" - unfolding closedin_closed using closed_Times by blast - lemma bdd_below_closure: fixes A :: "real set" assumes "bdd_below A" @@ -2075,12 +1011,6 @@ by (simp add: Int_Un_distrib Int_assoc Int_left_commute assms frontier_closures) qed -lemma frontier_straddle: - fixes a :: "'a::metric_space" - shows "a \ frontier S \ (\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e))" - unfolding frontier_def closure_interior - by (auto simp: mem_interior subset_eq ball_def) - lemma frontier_subset_closed: "closed S \ frontier S \ S" by (metis frontier_def closure_closed Diff_subset) @@ -2118,14 +1048,6 @@ lemma frontier_interior_subset: "frontier(interior S) \ frontier S" by (simp add: Diff_mono frontier_interiors interior_mono interior_subset) -lemma connected_Int_frontier: - "\connected s; s \ t \ {}; s - t \ {}\ \ (s \ frontier t \ {})" - apply (simp add: frontier_interiors connected_openin, safe) - apply (drule_tac x="s \ interior t" in spec, safe) - apply (drule_tac [2] x="s \ interior (-t)" in spec) - apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD]) - done - lemma closure_Un_frontier: "closure S = S \ frontier S" proof - have "S \ interior S = S" @@ -2137,9 +1059,6 @@ subsection%unimportant \Filters and the ``eventually true'' quantifier\ -definition indirection :: "'a::real_normed_vector \ 'a \ 'a filter" (infixr "indirection" 70) - where "a indirection v = at a within {b. \c\0. b - a = scaleR c v}" - text \Identify Trivial limits, where we can't approach arbitrarily closely.\ lemma trivial_limit_within: "trivial_limit (at a within S) \ \ a islimpt S" @@ -2167,16 +1086,6 @@ for a :: "'a::perfect_space" by (rule at_neq_bot) -lemma trivial_limit_at_infinity: - "\ trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) filter)" - unfolding trivial_limit_def eventually_at_infinity - apply clarsimp - apply (subgoal_tac "\x::'a. x \ 0", clarify) - apply (rule_tac x="scaleR (b / norm x) x" in exI, simp) - apply (cut_tac islimpt_UNIV [of "0::'a", unfolded islimpt_def]) - apply (drule_tac x=UNIV in spec, simp) - done - lemma not_trivial_limit_within: "\ trivial_limit (at x within S) = (x \ closure (S - {x}))" using islimpt_in_closure by (metis trivial_limit_within) @@ -2203,82 +1112,9 @@ subsection \Limits\ -proposition Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)" - by (auto simp: tendsto_iff trivial_limit_eq) - -text \Show that they yield usual definitions in the various cases.\ - -proposition Lim_within_le: "(f \ l)(at a within S) \ - (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)" - by (auto simp: tendsto_iff eventually_at_le) - -proposition Lim_within: "(f \ l) (at a within S) \ - (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" - by (auto simp: tendsto_iff eventually_at) - -corollary Lim_withinI [intro?]: - assumes "\e. e > 0 \ \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l \ e" - shows "(f \ l) (at a within S)" - apply (simp add: Lim_within, clarify) - apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) - done - -proposition Lim_at: "(f \ l) (at a) \ - (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" - by (auto simp: tendsto_iff eventually_at) - -proposition Lim_at_infinity: "(f \ l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" - by (auto simp: tendsto_iff eventually_at_infinity) - -corollary Lim_at_infinityI [intro?]: - assumes "\e. e > 0 \ \B. \x. norm x \ B \ dist (f x) l \ e" - shows "(f \ l) at_infinity" - apply (simp add: Lim_at_infinity, clarify) - apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) - done - lemma Lim_eventually: "eventually (\x. f x = l) net \ (f \ l) net" by (rule topological_tendstoI) (auto elim: eventually_mono) -lemma Lim_transform_within_set: - fixes a :: "'a::metric_space" and l :: "'b::metric_space" - shows "\(f \ l) (at a within S); eventually (\x. x \ S \ x \ T) (at a)\ - \ (f \ l) (at a within T)" -apply (clarsimp simp: eventually_at Lim_within) -apply (drule_tac x=e in spec, clarify) -apply (rename_tac k) -apply (rule_tac x="min d k" in exI, simp) -done - -lemma Lim_transform_within_set_eq: - fixes a l :: "'a::real_normed_vector" - shows "eventually (\x. x \ s \ x \ t) (at a) - \ ((f \ l) (at a within s) \ (f \ l) (at a within t))" - by (force intro: Lim_transform_within_set elim: eventually_mono) - -lemma Lim_transform_within_openin: - fixes a :: "'a::metric_space" - assumes f: "(f \ l) (at a within T)" - and "openin (subtopology euclidean T) S" "a \ S" - and eq: "\x. \x \ S; x \ a\ \ f x = g x" - shows "(g \ l) (at a within T)" -proof - - obtain \ where "0 < \" and \: "ball a \ \ T \ S" - using assms by (force simp: openin_contains_ball) - then have "a \ ball a \" - by simp - show ?thesis - by (rule Lim_transform_within [OF f \0 < \\ eq]) (use \ in \auto simp: dist_commute subset_iff\) -qed - -lemma continuous_transform_within_openin: - fixes a :: "'a::metric_space" - assumes "continuous (at a within T) f" - and "openin (subtopology euclidean T) S" "a \ S" - and eq: "\x. x \ S \ f x = g x" - shows "continuous (at a within T) g" - using assms by (simp add: Lim_transform_within_openin continuous_within) - text \The expected monotonicity property.\ lemma Lim_Un: @@ -2364,73 +1200,6 @@ qed qed -text \Another limit point characterization.\ - -lemma limpt_sequential_inj: - fixes x :: "'a::metric_space" - shows "x islimpt S \ - (\f. (\n::nat. f n \ S - {x}) \ inj f \ (f \ x) sequentially)" - (is "?lhs = ?rhs") -proof - assume ?lhs - then have "\e>0. \x'\S. x' \ x \ dist x' x < e" - by (force simp: islimpt_approachable) - then obtain y where y: "\e. e>0 \ y e \ S \ y e \ x \ dist (y e) x < e" - by metis - define f where "f \ rec_nat (y 1) (\n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))" - have [simp]: "f 0 = y 1" - "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n - by (simp_all add: f_def) - have f: "f n \ S \ (f n \ x) \ dist (f n) x < inverse(2 ^ n)" for n - proof (induction n) - case 0 show ?case - by (simp add: y) - next - case (Suc n) then show ?case - apply (auto simp: y) - by (metis half_gt_zero_iff inverse_positive_iff_positive less_divide_eq_numeral1(1) min_less_iff_conj y zero_less_dist_iff zero_less_numeral zero_less_power) - qed - show ?rhs - proof (rule_tac x=f in exI, intro conjI allI) - show "\n. f n \ S - {x}" - using f by blast - have "dist (f n) x < dist (f m) x" if "m < n" for m n - using that - proof (induction n) - case 0 then show ?case by simp - next - case (Suc n) - then consider "m < n" | "m = n" using less_Suc_eq by blast - then show ?case - proof cases - assume "m < n" - have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x" - by simp - also have "\ < dist (f n) x" - by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y) - also have "\ < dist (f m) x" - using Suc.IH \m < n\ by blast - finally show ?thesis . - next - assume "m = n" then show ?case - by simp (metis dist_pos_lt f half_gt_zero_iff inverse_positive_iff_positive min_less_iff_conj y zero_less_numeral zero_less_power) - qed - qed - then show "inj f" - by (metis less_irrefl linorder_injI) - show "f \ x" - apply (rule tendstoI) - apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI) - apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]]) - apply (simp add: field_simps) - by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power) - qed -next - assume ?rhs - then show ?lhs - by (fastforce simp add: islimpt_approachable lim_sequentially) -qed - (*could prove directly from islimpt_sequential_inj, but only for metric spaces*) lemma islimpt_sequential: fixes x :: "'a::first_countable_topology" @@ -2477,83 +1246,6 @@ qed qed -lemma Lim_null: - fixes f :: "'a \ 'b::real_normed_vector" - shows "(f \ l) net \ ((\x. f(x) - l) \ 0) net" - by (simp add: Lim dist_norm) - -lemma Lim_null_comparison: - fixes f :: "'a \ 'b::real_normed_vector" - assumes "eventually (\x. norm (f x) \ g x) net" "(g \ 0) net" - shows "(f \ 0) net" - using assms(2) -proof (rule metric_tendsto_imp_tendsto) - show "eventually (\x. dist (f x) 0 \ dist (g x) 0) net" - using assms(1) by (rule eventually_mono) (simp add: dist_norm) -qed - -lemma Lim_transform_bound: - fixes f :: "'a \ 'b::real_normed_vector" - and g :: "'a \ 'c::real_normed_vector" - assumes "eventually (\n. norm (f n) \ norm (g n)) net" - and "(g \ 0) net" - shows "(f \ 0) net" - using assms(1) tendsto_norm_zero [OF assms(2)] - by (rule Lim_null_comparison) - -lemma lim_null_mult_right_bounded: - fixes f :: "'a \ 'b::real_normed_div_algebra" - assumes f: "(f \ 0) F" and g: "eventually (\x. norm(g x) \ B) F" - shows "((\z. f z * g z) \ 0) F" -proof - - have *: "((\x. norm (f x) * B) \ 0) F" - by (simp add: f tendsto_mult_left_zero tendsto_norm_zero) - have "((\x. norm (f x) * norm (g x)) \ 0) F" - apply (rule Lim_null_comparison [OF _ *]) - apply (simp add: eventually_mono [OF g] mult_left_mono) - done - then show ?thesis - by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) -qed - -lemma lim_null_mult_left_bounded: - fixes f :: "'a \ 'b::real_normed_div_algebra" - assumes g: "eventually (\x. norm(g x) \ B) F" and f: "(f \ 0) F" - shows "((\z. g z * f z) \ 0) F" -proof - - have *: "((\x. B * norm (f x)) \ 0) F" - by (simp add: f tendsto_mult_right_zero tendsto_norm_zero) - have "((\x. norm (g x) * norm (f x)) \ 0) F" - apply (rule Lim_null_comparison [OF _ *]) - apply (simp add: eventually_mono [OF g] mult_right_mono) - done - then show ?thesis - by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) -qed - -lemma lim_null_scaleR_bounded: - assumes f: "(f \ 0) net" and gB: "eventually (\a. f a = 0 \ norm(g a) \ B) net" - shows "((\n. f n *\<^sub>R g n) \ 0) net" -proof - fix \::real - assume "0 < \" - then have B: "0 < \ / (abs B + 1)" by simp - have *: "\f x\ * norm (g x) < \" if f: "\f x\ * (\B\ + 1) < \" and g: "norm (g x) \ B" for x - proof - - have "\f x\ * norm (g x) \ \f x\ * B" - by (simp add: mult_left_mono g) - also have "\ \ \f x\ * (\B\ + 1)" - by (simp add: mult_left_mono) - also have "\ < \" - by (rule f) - finally show ?thesis . - qed - show "\\<^sub>F x in net. dist (f x *\<^sub>R g x) 0 < \" - apply (rule eventually_mono [OF eventually_conj [OF tendstoD [OF f B] gB] ]) - apply (auto simp: \0 < \\ divide_simps * split: if_split_asm) - done -qed - text\Deducing things about the limit from the elements.\ lemma Lim_in_closed_set: @@ -2573,40 +1265,7 @@ by (simp add: eventually_False) qed -text\Need to prove closed(cball(x,e)) before deducing this as a corollary.\ - -lemma Lim_dist_ubound: - assumes "\(trivial_limit net)" - and "(f \ l) net" - and "eventually (\x. dist a (f x) \ e) net" - shows "dist a l \ e" - using assms by (fast intro: tendsto_le tendsto_intros) - -lemma Lim_norm_ubound: - fixes f :: "'a \ 'b::real_normed_vector" - assumes "\(trivial_limit net)" "(f \ l) net" "eventually (\x. norm(f x) \ e) net" - shows "norm(l) \ e" - using assms by (fast intro: tendsto_le tendsto_intros) - -lemma Lim_norm_lbound: - fixes f :: "'a \ 'b::real_normed_vector" - assumes "\ trivial_limit net" - and "(f \ l) net" - and "eventually (\x. e \ norm (f x)) net" - shows "e \ norm l" - using assms by (fast intro: tendsto_le tendsto_intros) - -text\Limit under bilinear function\ - -lemma Lim_bilinear: - assumes "(f \ l) net" - and "(g \ m) net" - and "bounded_bilinear h" - shows "((\x. h (f x) (g x)) \ (h l m)) net" - using \bounded_bilinear h\ \(f \ l) net\ \(g \ m) net\ - by (rule bounded_bilinear.tendsto) - -text\These are special for limits out of the same vector space.\ +text\These are special for limits out of the same topological space.\ lemma Lim_within_id: "(id \ a) (at a within s)" unfolding id_def by (rule tendsto_ident_at) @@ -2614,12 +1273,6 @@ lemma Lim_at_id: "(id \ a) (at a)" unfolding id_def by (rule tendsto_ident_at) -lemma Lim_at_zero: - fixes a :: "'a::real_normed_vector" - and l :: "'b::topological_space" - shows "(f \ l) (at a) \ ((\x. f(a + x)) \ l) (at 0)" - using LIM_offset_zero LIM_offset_zero_cancel .. - text\It's also sometimes useful to extract the limit point from the filter.\ abbreviation netlimit :: "'a::t2_space filter \ 'a" @@ -2643,22 +1296,6 @@ shows "netlimit (at x within S) = x" using assms by (metis at_within_interior netlimit_at) -lemma netlimit_at_vector: - fixes a :: "'a::real_normed_vector" - shows "netlimit (at a) = a" -proof (cases "\x. x \ a") - case True then obtain x where x: "x \ a" .. - have "\ trivial_limit (at a)" - unfolding trivial_limit_def eventually_at dist_norm - apply clarsimp - apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI) - apply (simp add: norm_sgn sgn_zero_iff x) - done - then show ?thesis - by (rule netlimit_within [of a UNIV]) -qed simp - - text\Useful lemmas on closure and set of possible sequential limits.\ lemma closure_sequential: @@ -2689,111 +1326,6 @@ shows "closed S \ (\x l. (\n. x n \ S) \ (x \ l) sequentially \ l \ S)" by (metis closure_sequential closure_subset_eq subset_iff) -lemma closure_approachable: - fixes S :: "'a::metric_space set" - shows "x \ closure S \ (\e>0. \y\S. dist y x < e)" - apply (auto simp: closure_def islimpt_approachable) - apply (metis dist_self) - done - -lemma closure_approachable_le: - fixes S :: "'a::metric_space set" - shows "x \ closure S \ (\e>0. \y\S. dist y x \ e)" - unfolding closure_approachable - using dense by force - -lemma closure_approachableD: - assumes "x \ closure S" "e>0" - shows "\y\S. dist x y < e" - using assms unfolding closure_approachable by (auto simp: dist_commute) - -lemma closed_approachable: - fixes S :: "'a::metric_space set" - shows "closed S \ (\e>0. \y\S. dist y x < e) \ x \ S" - by (metis closure_closed closure_approachable) - -lemma closure_contains_Inf: - fixes S :: "real set" - assumes "S \ {}" "bdd_below S" - shows "Inf S \ closure S" -proof - - have *: "\x\S. Inf S \ x" - using cInf_lower[of _ S] assms by metis - { - fix e :: real - assume "e > 0" - then have "Inf S < Inf S + e" by simp - with assms obtain x where "x \ S" "x < Inf S + e" - by (subst (asm) cInf_less_iff) auto - with * have "\x\S. dist x (Inf S) < e" - by (intro bexI[of _ x]) (auto simp: dist_real_def) - } - then show ?thesis unfolding closure_approachable by auto -qed - -lemma closure_Int_ballI: - fixes S :: "'a :: metric_space set" - assumes "\U. \openin (subtopology euclidean S) U; U \ {}\ \ T \ U \ {}" - shows "S \ closure T" -proof (clarsimp simp: closure_approachable dist_commute) - fix x and e::real - assume "x \ S" "0 < e" - with assms [of "S \ ball x e"] show "\y\T. dist x y < e" - by force -qed - -lemma closed_contains_Inf: - fixes S :: "real set" - shows "S \ {} \ bdd_below S \ closed S \ Inf S \ S" - by (metis closure_contains_Inf closure_closed) - -lemma closed_subset_contains_Inf: - fixes A C :: "real set" - shows "closed C \ A \ C \ A \ {} \ bdd_below A \ Inf A \ C" - by (metis closure_contains_Inf closure_minimal subset_eq) - -lemma atLeastAtMost_subset_contains_Inf: - fixes A :: "real set" and a b :: real - shows "A \ {} \ a \ b \ A \ {a..b} \ Inf A \ {a..b}" - by (rule closed_subset_contains_Inf) - (auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a]) - -lemma not_trivial_limit_within_ball: - "\ trivial_limit (at x within S) \ (\e>0. S \ ball x e - {x} \ {})" - (is "?lhs \ ?rhs") -proof - show ?rhs if ?lhs - proof - - { - fix e :: real - assume "e > 0" - then obtain y where "y \ S - {x}" and "dist y x < e" - using \?lhs\ not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] - by auto - then have "y \ S \ ball x e - {x}" - unfolding ball_def by (simp add: dist_commute) - then have "S \ ball x e - {x} \ {}" by blast - } - then show ?thesis by auto - qed - show ?lhs if ?rhs - proof - - { - fix e :: real - assume "e > 0" - then obtain y where "y \ S \ ball x e - {x}" - using \?rhs\ by blast - then have "y \ S - {x}" and "dist y x < e" - unfolding ball_def by (simp_all add: dist_commute) - then have "\y \ S - {x}. dist y x < e" - by auto - } - then show ?thesis - using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] - by auto - qed -qed - lemma tendsto_If_within_closures: assumes f: "x \ s \ (closure s \ closure t) \ (f \ l x) (at x within s \ (closure s \ closure t))" @@ -2817,275 +1349,6 @@ qed -subsection \Boundedness\ - - (* FIXME: This has to be unified with BSEQ!! *) -definition%important (in metric_space) bounded :: "'a set \ bool" - where "bounded S \ (\x e. \y\S. dist x y \ e)" - -lemma bounded_subset_cball: "bounded S \ (\e x. S \ cball x e \ 0 \ e)" - unfolding bounded_def subset_eq by auto (meson order_trans zero_le_dist) - -lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)" - unfolding bounded_def - by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le) - -lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)" - unfolding bounded_any_center [where a=0] - by (simp add: dist_norm) - -lemma bdd_above_norm: "bdd_above (norm ` X) \ bounded X" - by (simp add: bounded_iff bdd_above_def) - -lemma bounded_norm_comp: "bounded ((\x. norm (f x)) ` S) = bounded (f ` S)" - by (simp add: bounded_iff) - -lemma boundedI: - assumes "\x. x \ S \ norm x \ B" - shows "bounded S" - using assms bounded_iff by blast - -lemma bounded_empty [simp]: "bounded {}" - by (simp add: bounded_def) - -lemma bounded_subset: "bounded T \ S \ T \ bounded S" - by (metis bounded_def subset_eq) - -lemma bounded_interior[intro]: "bounded S \ bounded(interior S)" - by (metis bounded_subset interior_subset) - -lemma bounded_closure[intro]: - assumes "bounded S" - shows "bounded (closure S)" -proof - - from assms obtain x and a where a: "\y\S. dist x y \ a" - unfolding bounded_def by auto - { - fix y - assume "y \ closure S" - then obtain f where f: "\n. f n \ S" "(f \ y) sequentially" - unfolding closure_sequential by auto - have "\n. f n \ S \ dist x (f n) \ a" using a by simp - then have "eventually (\n. dist x (f n) \ a) sequentially" - by (simp add: f(1)) - have "dist x y \ a" - apply (rule Lim_dist_ubound [of sequentially f]) - apply (rule trivial_limit_sequentially) - apply (rule f(2)) - apply fact - done - } - then show ?thesis - unfolding bounded_def by auto -qed - -lemma bounded_closure_image: "bounded (f ` closure S) \ bounded (f ` S)" - by (simp add: bounded_subset closure_subset image_mono) - -lemma bounded_cball[simp,intro]: "bounded (cball x e)" - apply (simp add: bounded_def) - apply (rule_tac x=x in exI) - apply (rule_tac x=e in exI, auto) - done - -lemma bounded_ball[simp,intro]: "bounded (ball x e)" - by (metis ball_subset_cball bounded_cball bounded_subset) - -lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T" - by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj) - -lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)" - by (induct rule: finite_induct[of F]) auto - -lemma bounded_UN [intro]: "finite A \ \x\A. bounded (B x) \ bounded (\x\A. B x)" - by (induct set: finite) auto - -lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S" -proof - - have "\y\{x}. dist x y \ 0" - by simp - then have "bounded {x}" - unfolding bounded_def by fast - then show ?thesis - by (metis insert_is_Un bounded_Un) -qed - -lemma bounded_subset_ballI: "S \ ball x r \ bounded S" - by (meson bounded_ball bounded_subset) - -lemma bounded_subset_ballD: - assumes "bounded S" shows "\r. 0 < r \ S \ ball x r" -proof - - obtain e::real and y where "S \ cball y e" "0 \ e" - using assms by (auto simp: bounded_subset_cball) - then show ?thesis - apply (rule_tac x="dist x y + e + 1" in exI) - apply (simp add: add.commute add_pos_nonneg) - apply (erule subset_trans) - apply (clarsimp simp add: cball_def) - by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one) -qed - -lemma finite_imp_bounded [intro]: "finite S \ bounded S" - by (induct set: finite) simp_all - -lemma bounded_pos: "bounded S \ (\b>0. \x\ S. norm x \ b)" - apply (simp add: bounded_iff) - apply (subgoal_tac "\x (y::real). 0 < 1 + \y\ \ (x \ y \ x \ 1 + \y\)") - apply metis - apply arith - done - -lemma bounded_pos_less: "bounded S \ (\b>0. \x\ S. norm x < b)" - apply (simp add: bounded_pos) - apply (safe; rule_tac x="b+1" in exI; force) - done - -lemma Bseq_eq_bounded: - fixes f :: "nat \ 'a::real_normed_vector" - shows "Bseq f \ bounded (range f)" - unfolding Bseq_def bounded_pos by auto - -lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)" - by (metis Int_lower1 Int_lower2 bounded_subset) - -lemma bounded_diff[intro]: "bounded S \ bounded (S - T)" - by (metis Diff_subset bounded_subset) - -lemma not_bounded_UNIV[simp]: - "\ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)" -proof (auto simp: bounded_pos not_le) - obtain x :: 'a where "x \ 0" - using perfect_choose_dist [OF zero_less_one] by fast - fix b :: real - assume b: "b >0" - have b1: "b +1 \ 0" - using b by simp - with \x \ 0\ have "b < norm (scaleR (b + 1) (sgn x))" - by (simp add: norm_sgn) - then show "\x::'a. b < norm x" .. -qed - -corollary cobounded_imp_unbounded: - fixes S :: "'a::{real_normed_vector, perfect_space} set" - shows "bounded (- S) \ \ bounded S" - using bounded_Un [of S "-S"] by (simp add: sup_compl_top) - -lemma bounded_dist_comp: - assumes "bounded (f ` S)" "bounded (g ` S)" - shows "bounded ((\x. dist (f x) (g x)) ` S)" -proof - - from assms obtain M1 M2 where *: "dist (f x) undefined \ M1" "dist undefined (g x) \ M2" if "x \ S" for x - by (auto simp: bounded_any_center[of _ undefined] dist_commute) - have "dist (f x) (g x) \ M1 + M2" if "x \ S" for x - using *[OF that] - by (rule order_trans[OF dist_triangle add_mono]) - then show ?thesis - by (auto intro!: boundedI) -qed - -lemma bounded_linear_image: - assumes "bounded S" - and "bounded_linear f" - shows "bounded (f ` S)" -proof - - from assms(1) obtain b where "b > 0" and b: "\x\S. norm x \ b" - unfolding bounded_pos by auto - from assms(2) obtain B where B: "B > 0" "\x. norm (f x) \ B * norm x" - using bounded_linear.pos_bounded by (auto simp: ac_simps) - show ?thesis - unfolding bounded_pos - proof (intro exI, safe) - show "norm (f x) \ B * b" if "x \ S" for x - by (meson B b less_imp_le mult_left_mono order_trans that) - qed (use \b > 0\ \B > 0\ in auto) -qed - -lemma bounded_scaling: - fixes S :: "'a::real_normed_vector set" - shows "bounded S \ bounded ((\x. c *\<^sub>R x) ` S)" - apply (rule bounded_linear_image, assumption) - apply (rule bounded_linear_scaleR_right) - done - -lemma bounded_scaleR_comp: - fixes f :: "'a \ 'b::real_normed_vector" - assumes "bounded (f ` S)" - shows "bounded ((\x. r *\<^sub>R f x) ` S)" - using bounded_scaling[of "f ` S" r] assms - by (auto simp: image_image) - -lemma bounded_translation: - fixes S :: "'a::real_normed_vector set" - assumes "bounded S" - shows "bounded ((\x. a + x) ` S)" -proof - - from assms obtain b where b: "b > 0" "\x\S. norm x \ b" - unfolding bounded_pos by auto - { - fix x - assume "x \ S" - then have "norm (a + x) \ b + norm a" - using norm_triangle_ineq[of a x] b by auto - } - then show ?thesis - unfolding bounded_pos - using norm_ge_zero[of a] b(1) and add_strict_increasing[of b 0 "norm a"] - by (auto intro!: exI[of _ "b + norm a"]) -qed - -lemma bounded_translation_minus: - fixes S :: "'a::real_normed_vector set" - shows "bounded S \ bounded ((\x. x - a) ` S)" -using bounded_translation [of S "-a"] by simp - -lemma bounded_uminus [simp]: - fixes X :: "'a::real_normed_vector set" - shows "bounded (uminus ` X) \ bounded X" -by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp: add.commute norm_minus_commute) - -lemma uminus_bounded_comp [simp]: - fixes f :: "'a \ 'b::real_normed_vector" - shows "bounded ((\x. - f x) ` S) \ bounded (f ` S)" - using bounded_uminus[of "f ` S"] - by (auto simp: image_image) - -lemma bounded_plus_comp: - fixes f g::"'a \ 'b::real_normed_vector" - assumes "bounded (f ` S)" - assumes "bounded (g ` S)" - shows "bounded ((\x. f x + g x) ` S)" -proof - - { - fix B C - assume "\x. x\S \ norm (f x) \ B" "\x. x\S \ norm (g x) \ C" - then have "\x. x \ S \ norm (f x + g x) \ B + C" - by (auto intro!: norm_triangle_le add_mono) - } then show ?thesis - using assms by (fastforce simp: bounded_iff) -qed - -lemma bounded_plus: - fixes S ::"'a::real_normed_vector set" - assumes "bounded S" "bounded T" - shows "bounded ((\(x,y). x + y) ` (S \ T))" - using bounded_plus_comp [of fst "S \ T" snd] assms - by (auto simp: split_def split: if_split_asm) - -lemma bounded_minus_comp: - "bounded (f ` S) \ bounded (g ` S) \ bounded ((\x. f x - g x) ` S)" - for f g::"'a \ 'b::real_normed_vector" - using bounded_plus_comp[of "f" S "\x. - g x"] - by auto - -lemma bounded_minus: - fixes S ::"'a::real_normed_vector set" - assumes "bounded S" "bounded T" - shows "bounded ((\(x,y). x - y) ` (S \ T))" - using bounded_minus_comp [of fst "S \ T" snd] assms - by (auto simp: split_def split: if_split_asm) - - subsection \Compactness\ subsubsection \Bolzano-Weierstrass property\ @@ -3139,58 +1402,6 @@ using g(2) using finite_subset by auto qed -lemma acc_point_range_imp_convergent_subsequence: - fixes l :: "'a :: first_countable_topology" - assumes l: "\U. l\U \ open U \ infinite (U \ range f)" - shows "\r::nat\nat. strict_mono r \ (f \ r) \ l" -proof - - from countable_basis_at_decseq[of l] - obtain A where A: - "\i. open (A i)" - "\i. l \ A i" - "\S. open S \ l \ S \ eventually (\i. A i \ S) sequentially" - by blast - define s where "s n i = (SOME j. i < j \ f j \ A (Suc n))" for n i - { - fix n i - have "infinite (A (Suc n) \ range f - f`{.. i})" - using l A by auto - then have "\x. x \ A (Suc n) \ range f - f`{.. i}" - unfolding ex_in_conv by (intro notI) simp - then have "\j. f j \ A (Suc n) \ j \ {.. i}" - by auto - then have "\a. i < a \ f a \ A (Suc n)" - by (auto simp: not_le) - then have "i < s n i" "f (s n i) \ A (Suc n)" - unfolding s_def by (auto intro: someI2_ex) - } - note s = this - define r where "r = rec_nat (s 0 0) s" - have "strict_mono r" - by (auto simp: r_def s strict_mono_Suc_iff) - moreover - have "(\n. f (r n)) \ l" - proof (rule topological_tendstoI) - fix S - assume "open S" "l \ S" - with A(3) have "eventually (\i. A i \ S) sequentially" - by auto - moreover - { - fix i - assume "Suc 0 \ i" - then have "f (r i) \ A i" - by (cases i) (simp_all add: r_def s) - } - then have "eventually (\i. f (r i) \ A i) sequentially" - by (auto simp: eventually_sequentially) - ultimately show "eventually (\i. f (r i) \ S) sequentially" - by eventually_elim auto - qed - ultimately show "\r::nat\nat. strict_mono r \ (f \ r) \ l" - by (auto simp: convergent_def comp_def) -qed - lemma sequence_infinite_lemma: fixes f :: "nat \ 'a::t1_space" assumes "\n. f n \ l" @@ -3212,130 +1423,6 @@ by auto qed -lemma closure_insert: - fixes x :: "'a::t1_space" - shows "closure (insert x s) = insert x (closure s)" - apply (rule closure_unique) - apply (rule insert_mono [OF closure_subset]) - apply (rule closed_insert [OF closed_closure]) - apply (simp add: closure_minimal) - done - -lemma islimpt_insert: - fixes x :: "'a::t1_space" - shows "x islimpt (insert a s) \ x islimpt s" -proof - assume *: "x islimpt (insert a s)" - show "x islimpt s" - proof (rule islimptI) - fix t - assume t: "x \ t" "open t" - show "\y\s. y \ t \ y \ x" - proof (cases "x = a") - case True - obtain y where "y \ insert a s" "y \ t" "y \ x" - using * t by (rule islimptE) - with \x = a\ show ?thesis by auto - next - case False - with t have t': "x \ t - {a}" "open (t - {a})" - by (simp_all add: open_Diff) - obtain y where "y \ insert a s" "y \ t - {a}" "y \ x" - using * t' by (rule islimptE) - then show ?thesis by auto - qed - qed -next - assume "x islimpt s" - then show "x islimpt (insert a s)" - by (rule islimpt_subset) auto -qed - -lemma islimpt_finite: - fixes x :: "'a::t1_space" - shows "finite s \ \ x islimpt s" - by (induct set: finite) (simp_all add: islimpt_insert) - -lemma islimpt_Un_finite: - fixes x :: "'a::t1_space" - shows "finite s \ x islimpt (s \ t) \ x islimpt t" - by (simp add: islimpt_Un islimpt_finite) - -lemma islimpt_eq_acc_point: - fixes l :: "'a :: t1_space" - shows "l islimpt S \ (\U. l\U \ open U \ infinite (U \ S))" -proof (safe intro!: islimptI) - fix U - assume "l islimpt S" "l \ U" "open U" "finite (U \ S)" - then have "l islimpt S" "l \ (U - (U \ S - {l}))" "open (U - (U \ S - {l}))" - by (auto intro: finite_imp_closed) - then show False - by (rule islimptE) auto -next - fix T - assume *: "\U. l\U \ open U \ infinite (U \ S)" "l \ T" "open T" - then have "infinite (T \ S - {l})" - by auto - then have "\x. x \ (T \ S - {l})" - unfolding ex_in_conv by (intro notI) simp - then show "\y\S. y \ T \ y \ l" - by auto -qed - -corollary infinite_openin: - fixes S :: "'a :: t1_space set" - shows "\openin (subtopology euclidean U) S; x \ S; x islimpt U\ \ infinite S" - by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute) - -lemma islimpt_range_imp_convergent_subsequence: - fixes l :: "'a :: {t1_space, first_countable_topology}" - assumes l: "l islimpt (range f)" - shows "\r::nat\nat. strict_mono r \ (f \ r) \ l" - using l unfolding islimpt_eq_acc_point - by (rule acc_point_range_imp_convergent_subsequence) - -lemma islimpt_eq_infinite_ball: "x islimpt S \ (\e>0. infinite(S \ ball x e))" - apply (simp add: islimpt_eq_acc_point, safe) - apply (metis Int_commute open_ball centre_in_ball) - by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl) - -lemma islimpt_eq_infinite_cball: "x islimpt S \ (\e>0. infinite(S \ cball x e))" - apply (simp add: islimpt_eq_infinite_ball, safe) - apply (meson Int_mono ball_subset_cball finite_subset order_refl) - by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq) - -lemma sequence_unique_limpt: - fixes f :: "nat \ 'a::t2_space" - assumes "(f \ l) sequentially" - and "l' islimpt (range f)" - shows "l' = l" -proof (rule ccontr) - assume "l' \ l" - obtain s t where "open s" "open t" "l' \ s" "l \ t" "s \ t = {}" - using hausdorff [OF \l' \ l\] by auto - have "eventually (\n. f n \ t) sequentially" - using assms(1) \open t\ \l \ t\ by (rule topological_tendstoD) - then obtain N where "\n\N. f n \ t" - unfolding eventually_sequentially by auto - - have "UNIV = {.. {N..}" - by auto - then have "l' islimpt (f ` ({.. {N..}))" - using assms(2) by simp - then have "l' islimpt (f ` {.. f ` {N..})" - by (simp add: image_Un) - then have "l' islimpt (f ` {N..})" - by (simp add: islimpt_Un_finite) - then obtain y where "y \ f ` {N..}" "y \ s" "y \ l'" - using \l' \ s\ \open s\ by (rule islimptE) - then obtain n where "N \ n" "f n \ s" "f n \ l'" - by auto - with \\n\N. f n \ t\ have "f n \ s \ t" - by simp - with \s \ t = {}\ show False - by simp -qed - lemma Bolzano_Weierstrass_imp_closed: fixes s :: "'a::{first_countable_topology,t2_space} set" assumes "\t. infinite t \ t \ s --> (\x \ s. x islimpt t)" @@ -3362,19 +1449,15 @@ unfolding closed_sequential_limits by fast qed -lemma compact_imp_bounded: - assumes "compact U" - shows "bounded U" -proof - - have "compact U" "\x\U. open (ball x 1)" "U \ (\x\U. ball x 1)" - using assms by auto - then obtain D where D: "D \ U" "finite D" "U \ (\x\D. ball x 1)" - by (metis compactE_image) - from \finite D\ have "bounded (\x\D. ball x 1)" - by (simp add: bounded_UN) - then show "bounded U" using \U \ (\x\D. ball x 1)\ - by (rule bounded_subset) -qed +lemma closure_insert: + fixes x :: "'a::t1_space" + shows "closure (insert x s) = insert x (closure s)" + apply (rule closure_unique) + apply (rule insert_mono [OF closure_subset]) + apply (rule closed_insert [OF closed_closure]) + apply (simp add: closure_minimal) + done + text\In particular, some common special cases.\ @@ -3435,11 +1518,6 @@ shows "open s \ open (s - {x})" by (simp add: open_Diff) -lemma openin_delete: - fixes a :: "'a :: t1_space" - shows "openin (subtopology euclidean u) s - \ openin (subtopology euclidean u) (s - {a})" -by (metis Int_Diff open_delete openin_open) text\Compactness expressed with filters\ @@ -3464,11 +1542,6 @@ by (simp add: closure_subset open_Compl) qed -corollary closure_Int_ball_not_empty: - assumes "S \ closure T" "x \ S" "r > 0" - shows "T \ ball x r \ {}" - using assms centre_in_ball closure_iff_nhds_not_empty by blast - lemma compact_filter: "compact U \ (\F. F \ bot \ eventually (\x. x \ U) F \ (\x\U. inf (nhds x) F \ bot))" proof (intro allI iffI impI compact_fip[THEN iffD2] notI) @@ -3892,702 +1965,8 @@ by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point) -subsubsection\Totally bounded\ - -lemma cauchy_def: "Cauchy s \ (\e>0. \N. \m n. m \ N \ n \ N \ dist (s m) (s n) < e)" - unfolding Cauchy_def by metis - -proposition seq_compact_imp_totally_bounded: - assumes "seq_compact s" - shows "\e>0. \k. finite k \ k \ s \ s \ (\x\k. ball x e)" -proof - - { fix e::real assume "e > 0" assume *: "\k. finite k \ k \ s \ \ s \ (\x\k. ball x e)" - let ?Q = "\x n r. r \ s \ (\m < (n::nat). \ (dist (x m) r < e))" - have "\x. \n::nat. ?Q x n (x n)" - proof (rule dependent_wellorder_choice) - fix n x assume "\y. y < n \ ?Q x y (x y)" - then have "\ s \ (\x\x ` {0..s" "z \ (\x\x ` {0..r. ?Q x n r" - using z by auto - qed simp - then obtain x where "\n::nat. x n \ s" and x:"\n m. m < n \ \ (dist (x m) (x n) < e)" - by blast - then obtain l r where "l \ s" and r:"strict_mono r" and "((x \ r) \ l) sequentially" - using assms by (metis seq_compact_def) - from this(3) have "Cauchy (x \ r)" - using LIMSEQ_imp_Cauchy by auto - then obtain N::nat where "\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < e" - unfolding cauchy_def using \e > 0\ by blast - then have False - using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) } - then show ?thesis - by metis -qed - -subsubsection\Heine-Borel theorem\ - -proposition seq_compact_imp_Heine_Borel: - fixes s :: "'a :: metric_space set" - assumes "seq_compact s" - shows "compact s" -proof - - from seq_compact_imp_totally_bounded[OF \seq_compact s\] - obtain f where f: "\e>0. finite (f e) \ f e \ s \ s \ (\x\f e. ball x e)" - unfolding choice_iff' .. - define K where "K = (\(x, r). ball x r) ` ((\e \ \ \ {0 <..}. f e) \ \)" - have "countably_compact s" - using \seq_compact s\ by (rule seq_compact_imp_countably_compact) - then show "compact s" - proof (rule countably_compact_imp_compact) - show "countable K" - unfolding K_def using f - by (auto intro: countable_finite countable_subset countable_rat - intro!: countable_image countable_SIGMA countable_UN) - show "\b\K. open b" by (auto simp: K_def) - next - fix T x - assume T: "open T" "x \ T" and x: "x \ s" - from openE[OF T] obtain e where "0 < e" "ball x e \ T" - by auto - then have "0 < e / 2" "ball x (e / 2) \ T" - by auto - from Rats_dense_in_real[OF \0 < e / 2\] obtain r where "r \ \" "0 < r" "r < e / 2" - by auto - from f[rule_format, of r] \0 < r\ \x \ s\ obtain k where "k \ f r" "x \ ball k r" - by auto - from \r \ \\ \0 < r\ \k \ f r\ have "ball k r \ K" - by (auto simp: K_def) - then show "\b\K. x \ b \ b \ s \ T" - proof (rule bexI[rotated], safe) - fix y - assume "y \ ball k r" - with \r < e / 2\ \x \ ball k r\ have "dist x y < e" - by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute) - with \ball x e \ T\ show "y \ T" - by auto - next - show "x \ ball k r" by fact - qed - qed -qed - -proposition compact_eq_seq_compact_metric: - "compact (s :: 'a::metric_space set) \ seq_compact s" - using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast - -proposition compact_def: \ \this is the definition of compactness in HOL Light\ - "compact (S :: 'a::metric_space set) \ - (\f. (\n. f n \ S) \ (\l\S. \r::nat\nat. strict_mono r \ (f \ r) \ l))" - unfolding compact_eq_seq_compact_metric seq_compact_def by auto - -subsubsection \Complete the chain of compactness variants\ - -proposition compact_eq_Bolzano_Weierstrass: - fixes s :: "'a::metric_space set" - shows "compact s \ (\t. infinite t \ t \ s --> (\x \ s. x islimpt t))" - (is "?lhs = ?rhs") -proof - assume ?lhs - then show ?rhs - using Heine_Borel_imp_Bolzano_Weierstrass[of s] by auto -next - assume ?rhs - then show ?lhs - unfolding compact_eq_seq_compact_metric by (rule Bolzano_Weierstrass_imp_seq_compact) -qed - -proposition Bolzano_Weierstrass_imp_bounded: - "\t. infinite t \ t \ s \ (\x \ s. x islimpt t) \ bounded s" - using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass . - - -subsection \Metric spaces with the Heine-Borel property\ - -text \ - A metric space (or topological vector space) is said to have the - Heine-Borel property if every closed and bounded subset is compact. -\ - -class heine_borel = metric_space + - assumes bounded_imp_convergent_subsequence: - "bounded (range f) \ \l r. strict_mono (r::nat\nat) \ ((f \ r) \ l) sequentially" - -proposition bounded_closed_imp_seq_compact: - fixes s::"'a::heine_borel set" - assumes "bounded s" - and "closed s" - shows "seq_compact s" -proof (unfold seq_compact_def, clarify) - fix f :: "nat \ 'a" - assume f: "\n. f n \ s" - with \bounded s\ have "bounded (range f)" - by (auto intro: bounded_subset) - obtain l r where r: "strict_mono (r :: nat \ nat)" and l: "((f \ r) \ l) sequentially" - using bounded_imp_convergent_subsequence [OF \bounded (range f)\] by auto - from f have fr: "\n. (f \ r) n \ s" - by simp - have "l \ s" using \closed s\ fr l - by (rule closed_sequentially) - show "\l\s. \r. strict_mono r \ ((f \ r) \ l) sequentially" - using \l \ s\ r l by blast -qed - -lemma compact_eq_bounded_closed: - fixes s :: "'a::heine_borel set" - shows "compact s \ bounded s \ closed s" - (is "?lhs = ?rhs") -proof - assume ?lhs - then show ?rhs - using compact_imp_closed compact_imp_bounded - by blast -next - assume ?rhs - then show ?lhs - using bounded_closed_imp_seq_compact[of s] - unfolding compact_eq_seq_compact_metric - by auto -qed - -lemma compact_Inter: - fixes \ :: "'a :: heine_borel set set" - assumes com: "\S. S \ \ \ compact S" and "\ \ {}" - shows "compact(\ \)" - using assms - by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed) - -lemma compact_closure [simp]: - fixes S :: "'a::heine_borel set" - shows "compact(closure S) \ bounded S" -by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed) - -lemma not_compact_UNIV[simp]: - fixes s :: "'a::{real_normed_vector,perfect_space,heine_borel} set" - shows "\ compact (UNIV::'a set)" - by (simp add: compact_eq_bounded_closed) - -text\Representing sets as the union of a chain of compact sets.\ -lemma closed_Union_compact_subsets: - fixes S :: "'a::{heine_borel,real_normed_vector} set" - assumes "closed S" - obtains F where "\n. compact(F n)" "\n. F n \ S" "\n. F n \ F(Suc n)" - "(\n. F n) = S" "\K. \compact K; K \ S\ \ \N. \n \ N. K \ F n" -proof - show "compact (S \ cball 0 (of_nat n))" for n - using assms compact_eq_bounded_closed by auto -next - show "(\n. S \ cball 0 (real n)) = S" - by (auto simp: real_arch_simple) -next - fix K :: "'a set" - assume "compact K" "K \ S" - then obtain N where "K \ cball 0 N" - by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI) - then show "\N. \n\N. K \ S \ cball 0 (real n)" - by (metis of_nat_le_iff Int_subset_iff \K \ S\ real_arch_simple subset_cball subset_trans) -qed auto - -instance%important real :: heine_borel -proof%unimportant - fix f :: "nat \ real" - assume f: "bounded (range f)" - obtain r :: "nat \ nat" where r: "strict_mono r" "monoseq (f \ r)" - unfolding comp_def by (metis seq_monosub) - then have "Bseq (f \ r)" - unfolding Bseq_eq_bounded using f by (force intro: bounded_subset) - with r show "\l r. strict_mono r \ (f \ r) \ l" - using Bseq_monoseq_convergent[of "f \ r"] by (auto simp: convergent_def) -qed - -lemma compact_lemma_general: - fixes f :: "nat \ 'a" - fixes proj::"'a \ 'b \ 'c::heine_borel" (infixl "proj" 60) - fixes unproj:: "('b \ 'c) \ 'a" - assumes finite_basis: "finite basis" - assumes bounded_proj: "\k. k \ basis \ bounded ((\x. x proj k) ` range f)" - assumes proj_unproj: "\e k. k \ basis \ (unproj e) proj k = e k" - assumes unproj_proj: "\x. unproj (\k. x proj k) = x" - shows "\d\basis. \l::'a. \ r::nat\nat. - strict_mono r \ (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)" -proof safe - fix d :: "'b set" - assume d: "d \ basis" - with finite_basis have "finite d" - by (blast intro: finite_subset) - from this d show "\l::'a. \r::nat\nat. strict_mono r \ - (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)" - proof (induct d) - case empty - then show ?case - unfolding strict_mono_def by auto - next - case (insert k d) - have k[intro]: "k \ basis" - using insert by auto - have s': "bounded ((\x. x proj k) ` range f)" - using k - by (rule bounded_proj) - obtain l1::"'a" and r1 where r1: "strict_mono r1" - and lr1: "\e > 0. eventually (\n. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially" - using insert(3) using insert(4) by auto - have f': "\n. f (r1 n) proj k \ (\x. x proj k) ` range f" - by simp - have "bounded (range (\i. f (r1 i) proj k))" - by (metis (lifting) bounded_subset f' image_subsetI s') - then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\i. f (r1 (r2 i)) proj k) \ l2) sequentially" - using bounded_imp_convergent_subsequence[of "\i. f (r1 i) proj k"] - by (auto simp: o_def) - define r where "r = r1 \ r2" - have r:"strict_mono r" - using r1 and r2 unfolding r_def o_def strict_mono_def by auto - moreover - define l where "l = unproj (\i. if i = k then l2 else l1 proj i)" - { - fix e::real - assume "e > 0" - from lr1 \e > 0\ have N1: "eventually (\n. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially" - by blast - from lr2 \e > 0\ have N2:"eventually (\n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially" - by (rule tendstoD) - from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially" - by (rule eventually_subseq) - have "eventually (\n. \i\(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially" - using N1' N2 - by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj) - } - ultimately show ?case by auto - qed -qed - -lemma bounded_fst: "bounded s \ bounded (fst ` s)" - unfolding bounded_def - by (metis (erased, hide_lams) dist_fst_le image_iff order_trans) - -lemma bounded_snd: "bounded s \ bounded (snd ` s)" - unfolding bounded_def - by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans) - -instance%important prod :: (heine_borel, heine_borel) heine_borel -proof%unimportant - fix f :: "nat \ 'a \ 'b" - assume f: "bounded (range f)" - then have "bounded (fst ` range f)" - by (rule bounded_fst) - then have s1: "bounded (range (fst \ f))" - by (simp add: image_comp) - obtain l1 r1 where r1: "strict_mono r1" and l1: "(\n. fst (f (r1 n))) \ l1" - using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast - from f have s2: "bounded (range (snd \ f \ r1))" - by (auto simp: image_comp intro: bounded_snd bounded_subset) - obtain l2 r2 where r2: "strict_mono r2" and l2: "((\n. snd (f (r1 (r2 n)))) \ l2) sequentially" - using bounded_imp_convergent_subsequence [OF s2] - unfolding o_def by fast - have l1': "((\n. fst (f (r1 (r2 n)))) \ l1) sequentially" - using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def . - have l: "((f \ (r1 \ r2)) \ (l1, l2)) sequentially" - using tendsto_Pair [OF l1' l2] unfolding o_def by simp - have r: "strict_mono (r1 \ r2)" - using r1 r2 unfolding strict_mono_def by simp - show "\l r. strict_mono r \ ((f \ r) \ l) sequentially" - using l r by fast -qed - -subsubsection \Completeness\ - -proposition (in metric_space) completeI: - assumes "\f. \n. f n \ s \ Cauchy f \ \l\s. f \ l" - shows "complete s" - using assms unfolding complete_def by fast - -proposition (in metric_space) completeE: - assumes "complete s" and "\n. f n \ s" and "Cauchy f" - obtains l where "l \ s" and "f \ l" - using assms unfolding complete_def by fast - -(* TODO: generalize to uniform spaces *) -lemma compact_imp_complete: - fixes s :: "'a::metric_space set" - assumes "compact s" - shows "complete s" -proof - - { - fix f - assume as: "(\n::nat. f n \ s)" "Cauchy f" - from as(1) obtain l r where lr: "l\s" "strict_mono r" "(f \ r) \ l" - using assms unfolding compact_def by blast - - note lr' = seq_suble [OF lr(2)] - { - fix e :: real - assume "e > 0" - from as(2) obtain N where N:"\m n. N \ m \ N \ n \ dist (f m) (f n) < e/2" - unfolding cauchy_def - using \e > 0\ - apply (erule_tac x="e/2" in allE, auto) - done - from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]] - obtain M where M:"\n\M. dist ((f \ r) n) l < e/2" - using \e > 0\ by auto - { - fix n :: nat - assume n: "n \ max N M" - have "dist ((f \ r) n) l < e/2" - using n M by auto - moreover have "r n \ N" - using lr'[of n] n by auto - then have "dist (f n) ((f \ r) n) < e / 2" - using N and n by auto - ultimately have "dist (f n) l < e" - using dist_triangle_half_r[of "f (r n)" "f n" e l] - by (auto simp: dist_commute) - } - then have "\N. \n\N. dist (f n) l < e" by blast - } - then have "\l\s. (f \ l) sequentially" using \l\s\ - unfolding lim_sequentially by auto - } - then show ?thesis unfolding complete_def by auto -qed - -proposition compact_eq_totally_bounded: - "compact s \ complete s \ (\e>0. \k. finite k \ s \ (\x\k. ball x e))" - (is "_ \ ?rhs") -proof - assume assms: "?rhs" - then obtain k where k: "\e. 0 < e \ finite (k e)" "\e. 0 < e \ s \ (\x\k e. ball x e)" - by (auto simp: choice_iff') - - show "compact s" - proof cases - assume "s = {}" - then show "compact s" by (simp add: compact_def) - next - assume "s \ {}" - show ?thesis - unfolding compact_def - proof safe - fix f :: "nat \ 'a" - assume f: "\n. f n \ s" - - define e where "e n = 1 / (2 * Suc n)" for n - then have [simp]: "\n. 0 < e n" by auto - define B where "B n U = (SOME b. infinite {n. f n \ b} \ (\x. b \ ball x (e n) \ U))" for n U - { - fix n U - assume "infinite {n. f n \ U}" - then have "\b\k (e n). infinite {i\{n. f n \ U}. f i \ ball b (e n)}" - using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq) - then obtain a where - "a \ k (e n)" - "infinite {i \ {n. f n \ U}. f i \ ball a (e n)}" .. - then have "\b. infinite {i. f i \ b} \ (\x. b \ ball x (e n) \ U)" - by (intro exI[of _ "ball a (e n) \ U"] exI[of _ a]) (auto simp: ac_simps) - from someI_ex[OF this] - have "infinite {i. f i \ B n U}" "\x. B n U \ ball x (e n) \ U" - unfolding B_def by auto - } - note B = this - - define F where "F = rec_nat (B 0 UNIV) B" - { - fix n - have "infinite {i. f i \ F n}" - by (induct n) (auto simp: F_def B) - } - then have F: "\n. \x. F (Suc n) \ ball x (e n) \ F n" - using B by (simp add: F_def) - then have F_dec: "\m n. m \ n \ F n \ F m" - using decseq_SucI[of F] by (auto simp: decseq_def) - - obtain sel where sel: "\k i. i < sel k i" "\k i. f (sel k i) \ F k" - proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI) - fix k i - have "infinite ({n. f n \ F k} - {.. i})" - using \infinite {n. f n \ F k}\ by auto - from infinite_imp_nonempty[OF this] - show "\x>i. f x \ F k" - by (simp add: set_eq_iff not_le conj_commute) - qed - - define t where "t = rec_nat (sel 0 0) (\n i. sel (Suc n) i)" - have "strict_mono t" - unfolding strict_mono_Suc_iff by (simp add: t_def sel) - moreover have "\i. (f \ t) i \ s" - using f by auto - moreover - { - fix n - have "(f \ t) n \ F n" - by (cases n) (simp_all add: t_def sel) - } - note t = this - - have "Cauchy (f \ t)" - proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE) - fix r :: real and N n m - assume "1 / Suc N < r" "Suc N \ n" "Suc N \ m" - then have "(f \ t) n \ F (Suc N)" "(f \ t) m \ F (Suc N)" "2 * e N < r" - using F_dec t by (auto simp: e_def field_simps of_nat_Suc) - with F[of N] obtain x where "dist x ((f \ t) n) < e N" "dist x ((f \ t) m) < e N" - by (auto simp: subset_eq) - with dist_triangle[of "(f \ t) m" "(f \ t) n" x] \2 * e N < r\ - show "dist ((f \ t) m) ((f \ t) n) < r" - by (simp add: dist_commute) - qed - - ultimately show "\l\s. \r. strict_mono r \ (f \ r) \ l" - using assms unfolding complete_def by blast - qed - qed -qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded) - -lemma cauchy_imp_bounded: - assumes "Cauchy s" - shows "bounded (range s)" -proof - - from assms obtain N :: nat where "\m n. N \ m \ N \ n \ dist (s m) (s n) < 1" - unfolding cauchy_def by force - then have N:"\n. N \ n \ dist (s N) (s n) < 1" by auto - moreover - have "bounded (s ` {0..N})" - using finite_imp_bounded[of "s ` {1..N}"] by auto - then obtain a where a:"\x\s ` {0..N}. dist (s N) x \ a" - unfolding bounded_any_center [where a="s N"] by auto - ultimately show "?thesis" - unfolding bounded_any_center [where a="s N"] - apply (rule_tac x="max a 1" in exI, auto) - apply (erule_tac x=y in allE) - apply (erule_tac x=y in ballE, auto) - done -qed - -instance heine_borel < complete_space -proof - fix f :: "nat \ 'a" assume "Cauchy f" - then have "bounded (range f)" - by (rule cauchy_imp_bounded) - then have "compact (closure (range f))" - unfolding compact_eq_bounded_closed by auto - then have "complete (closure (range f))" - by (rule compact_imp_complete) - moreover have "\n. f n \ closure (range f)" - using closure_subset [of "range f"] by auto - ultimately have "\l\closure (range f). (f \ l) sequentially" - using \Cauchy f\ unfolding complete_def by auto - then show "convergent f" - unfolding convergent_def by auto -qed - -lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)" -proof (rule completeI) - fix f :: "nat \ 'a" assume "Cauchy f" - then have "convergent f" by (rule Cauchy_convergent) - then show "\l\UNIV. f \ l" unfolding convergent_def by simp -qed - -lemma complete_imp_closed: - fixes S :: "'a::metric_space set" - assumes "complete S" - shows "closed S" -proof (unfold closed_sequential_limits, clarify) - fix f x assume "\n. f n \ S" and "f \ x" - from \f \ x\ have "Cauchy f" - by (rule LIMSEQ_imp_Cauchy) - with \complete S\ and \\n. f n \ S\ obtain l where "l \ S" and "f \ l" - by (rule completeE) - from \f \ x\ and \f \ l\ have "x = l" - by (rule LIMSEQ_unique) - with \l \ S\ show "x \ S" - by simp -qed - -lemma complete_Int_closed: - fixes S :: "'a::metric_space set" - assumes "complete S" and "closed t" - shows "complete (S \ t)" -proof (rule completeI) - fix f assume "\n. f n \ S \ t" and "Cauchy f" - then have "\n. f n \ S" and "\n. f n \ t" - by simp_all - from \complete S\ obtain l where "l \ S" and "f \ l" - using \\n. f n \ S\ and \Cauchy f\ by (rule completeE) - from \closed t\ and \\n. f n \ t\ and \f \ l\ have "l \ t" - by (rule closed_sequentially) - with \l \ S\ and \f \ l\ show "\l\S \ t. f \ l" - by fast -qed - -lemma complete_closed_subset: - fixes S :: "'a::metric_space set" - assumes "closed S" and "S \ t" and "complete t" - shows "complete S" - using assms complete_Int_closed [of t S] by (simp add: Int_absorb1) - -lemma complete_eq_closed: - fixes S :: "('a::complete_space) set" - shows "complete S \ closed S" -proof - assume "closed S" then show "complete S" - using subset_UNIV complete_UNIV by (rule complete_closed_subset) -next - assume "complete S" then show "closed S" - by (rule complete_imp_closed) -qed - -lemma convergent_eq_Cauchy: - fixes S :: "nat \ 'a::complete_space" - shows "(\l. (S \ l) sequentially) \ Cauchy S" - unfolding Cauchy_convergent_iff convergent_def .. - -lemma convergent_imp_bounded: - fixes S :: "nat \ 'a::metric_space" - shows "(S \ l) sequentially \ bounded (range S)" - by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy) - -lemma frontier_subset_compact: - fixes S :: "'a::heine_borel set" - shows "compact S \ frontier S \ S" - using frontier_subset_closed compact_eq_bounded_closed - by blast - subsection \Continuity\ -text\Derive the epsilon-delta forms, which we often use as "definitions"\ - -proposition continuous_within_eps_delta: - "continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)" - unfolding continuous_within and Lim_within by fastforce - -corollary continuous_at_eps_delta: - "continuous (at x) f \ (\e > 0. \d > 0. \x'. dist x' x < d \ dist (f x') (f x) < e)" - using continuous_within_eps_delta [of x UNIV f] by simp - -lemma continuous_at_right_real_increasing: - fixes f :: "real \ real" - assumes nondecF: "\x y. x \ y \ f x \ f y" - shows "continuous (at_right a) f \ (\e>0. \d>0. f (a + d) - f a < e)" - apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le) - apply (intro all_cong ex_cong, safe) - apply (erule_tac x="a + d" in allE, simp) - apply (simp add: nondecF field_simps) - apply (drule nondecF, simp) - done - -lemma continuous_at_left_real_increasing: - assumes nondecF: "\ x y. x \ y \ f x \ ((f y) :: real)" - shows "(continuous (at_left (a :: real)) f) = (\e > 0. \delta > 0. f a - f (a - delta) < e)" - apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le) - apply (intro all_cong ex_cong, safe) - apply (erule_tac x="a - d" in allE, simp) - apply (simp add: nondecF field_simps) - apply (cut_tac x="a - d" and y=x in nondecF, simp_all) - done - -text\Versions in terms of open balls.\ - -lemma continuous_within_ball: - "continuous (at x within s) f \ - (\e > 0. \d > 0. f ` (ball x d \ s) \ ball (f x) e)" - (is "?lhs = ?rhs") -proof - assume ?lhs - { - fix e :: real - assume "e > 0" - then obtain d where d: "d>0" "\xa\s. 0 < dist xa x \ dist xa x < d \ dist (f xa) (f x) < e" - using \?lhs\[unfolded continuous_within Lim_within] by auto - { - fix y - assume "y \ f ` (ball x d \ s)" - then have "y \ ball (f x) e" - using d(2) - apply (auto simp: dist_commute) - apply (erule_tac x=xa in ballE, auto) - using \e > 0\ - apply auto - done - } - then have "\d>0. f ` (ball x d \ s) \ ball (f x) e" - using \d > 0\ - unfolding subset_eq ball_def by (auto simp: dist_commute) - } - then show ?rhs by auto -next - assume ?rhs - then show ?lhs - unfolding continuous_within Lim_within ball_def subset_eq - apply (auto simp: dist_commute) - apply (erule_tac x=e in allE, auto) - done -qed - -lemma continuous_at_ball: - "continuous (at x) f \ (\e>0. \d>0. f ` (ball x d) \ ball (f x) e)" (is "?lhs = ?rhs") -proof - assume ?lhs - then show ?rhs - unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball - apply auto - apply (erule_tac x=e in allE, auto) - apply (rule_tac x=d in exI, auto) - apply (erule_tac x=xa in allE) - apply (auto simp: dist_commute) - done -next - assume ?rhs - then show ?lhs - unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball - apply auto - apply (erule_tac x=e in allE, auto) - apply (rule_tac x=d in exI, auto) - apply (erule_tac x="f xa" in allE) - apply (auto simp: dist_commute) - done -qed - -text\Define setwise continuity in terms of limits within the set.\ - -lemma continuous_on_iff: - "continuous_on s f \ - (\x\s. \e>0. \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) < e)" - unfolding continuous_on_def Lim_within - by (metis dist_pos_lt dist_self) - -lemma continuous_within_E: - assumes "continuous (at x within s) f" "e>0" - obtains d where "d>0" "\x'. \x'\ s; dist x' x \ d\ \ dist (f x') (f x) < e" - using assms apply (simp add: continuous_within_eps_delta) - apply (drule spec [of _ e], clarify) - apply (rule_tac d="d/2" in that, auto) - done - -lemma continuous_onI [intro?]: - assumes "\x e. \e > 0; x \ s\ \ \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) \ e" - shows "continuous_on s f" -apply (simp add: continuous_on_iff, clarify) -apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) -done - -text\Some simple consequential lemmas.\ - -lemma continuous_onE: - assumes "continuous_on s f" "x\s" "e>0" - obtains d where "d>0" "\x'. \x' \ s; dist x' x \ d\ \ dist (f x') (f x) < e" - using assms - apply (simp add: continuous_on_iff) - apply (elim ballE allE) - apply (auto intro: that [where d="d/2" for d]) - done - -lemma uniformly_continuous_onE: - assumes "uniformly_continuous_on s f" "0 < e" - obtains d where "d>0" "\x x'. \x\s; x'\s; dist x' x < d\ \ dist (f x') (f x) < e" -using assms -by (auto simp: uniformly_continuous_on_def) - lemma continuous_at_imp_continuous_within: "continuous (at x) f \ continuous (at x within s) f" unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto @@ -4669,7 +2048,7 @@ using continuous_within_sequentiallyI[of _ s f] by auto lemma continuous_on_sequentially: - fixes f :: "'a::metric_space \ 'b::topological_space" + fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" shows "continuous_on s f \ (\x. \a \ s. (\n. x(n) \ s) \ (x \ a) sequentially --> ((f \ x) \ f a) sequentially)" @@ -4688,181 +2067,6 @@ by auto qed -lemma uniformly_continuous_on_sequentially: - "uniformly_continuous_on s f \ (\x y. (\n. x n \ s) \ (\n. y n \ s) \ - (\n. dist (x n) (y n)) \ 0 \ (\n. dist (f(x n)) (f(y n))) \ 0)" (is "?lhs = ?rhs") -proof - assume ?lhs - { - fix x y - assume x: "\n. x n \ s" - and y: "\n. y n \ s" - and xy: "((\n. dist (x n) (y n)) \ 0) sequentially" - { - fix e :: real - assume "e > 0" - then obtain d where "d > 0" and d: "\x\s. \x'\s. dist x' x < d \ dist (f x') (f x) < e" - using \?lhs\[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto - obtain N where N: "\n\N. dist (x n) (y n) < d" - using xy[unfolded lim_sequentially dist_norm] and \d>0\ by auto - { - fix n - assume "n\N" - then have "dist (f (x n)) (f (y n)) < e" - using N[THEN spec[where x=n]] - using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] - using x and y - by (simp add: dist_commute) - } - then have "\N. \n\N. dist (f (x n)) (f (y n)) < e" - by auto - } - then have "((\n. dist (f(x n)) (f(y n))) \ 0) sequentially" - unfolding lim_sequentially and dist_real_def by auto - } - then show ?rhs by auto -next - assume ?rhs - { - assume "\ ?lhs" - then obtain e where "e > 0" "\d>0. \x\s. \x'\s. dist x' x < d \ \ dist (f x') (f x) < e" - unfolding uniformly_continuous_on_def by auto - then obtain fa where fa: - "\x. 0 < x \ fst (fa x) \ s \ snd (fa x) \ s \ dist (fst (fa x)) (snd (fa x)) < x \ \ dist (f (fst (fa x))) (f (snd (fa x))) < e" - using choice[of "\d x. d>0 \ fst x \ s \ snd x \ s \ dist (snd x) (fst x) < d \ \ dist (f (snd x)) (f (fst x)) < e"] - unfolding Bex_def - by (auto simp: dist_commute) - define x where "x n = fst (fa (inverse (real n + 1)))" for n - define y where "y n = snd (fa (inverse (real n + 1)))" for n - have xyn: "\n. x n \ s \ y n \ s" - and xy0: "\n. dist (x n) (y n) < inverse (real n + 1)" - and fxy:"\n. \ dist (f (x n)) (f (y n)) < e" - unfolding x_def and y_def using fa - by auto - { - fix e :: real - assume "e > 0" - then obtain N :: nat where "N \ 0" and N: "0 < inverse (real N) \ inverse (real N) < e" - unfolding real_arch_inverse[of e] by auto - { - fix n :: nat - assume "n \ N" - then have "inverse (real n + 1) < inverse (real N)" - using of_nat_0_le_iff and \N\0\ by auto - also have "\ < e" using N by auto - finally have "inverse (real n + 1) < e" by auto - then have "dist (x n) (y n) < e" - using xy0[THEN spec[where x=n]] by auto - } - then have "\N. \n\N. dist (x n) (y n) < e" by auto - } - then have "\e>0. \N. \n\N. dist (f (x n)) (f (y n)) < e" - using \?rhs\[THEN spec[where x=x], THEN spec[where x=y]] and xyn - unfolding lim_sequentially dist_real_def by auto - then have False using fxy and \e>0\ by auto - } - then show ?lhs - unfolding uniformly_continuous_on_def by blast -qed - -lemma continuous_closed_imp_Cauchy_continuous: - fixes S :: "('a::complete_space) set" - shows "\continuous_on S f; closed S; Cauchy \; \n. (\ n) \ S\ \ Cauchy(f \ \)" - apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially) - by (meson LIMSEQ_imp_Cauchy complete_def) - -text\The usual transformation theorems.\ - -lemma continuous_transform_within: - fixes f g :: "'a::metric_space \ 'b::topological_space" - assumes "continuous (at x within s) f" - and "0 < d" - and "x \ s" - and "\x'. \x' \ s; dist x' x < d\ \ f x' = g x'" - shows "continuous (at x within s) g" - using assms - unfolding continuous_within - by (force intro: Lim_transform_within) - - -subsubsection%unimportant \Structural rules for uniform continuity\ - -lemma uniformly_continuous_on_dist[continuous_intros]: - fixes f g :: "'a::metric_space \ 'b::metric_space" - assumes "uniformly_continuous_on s f" - and "uniformly_continuous_on s g" - shows "uniformly_continuous_on s (\x. dist (f x) (g x))" -proof - - { - fix a b c d :: 'b - have "\dist a b - dist c d\ \ dist a c + dist b d" - using dist_triangle2 [of a b c] dist_triangle2 [of b c d] - using dist_triangle3 [of c d a] dist_triangle [of a d b] - by arith - } note le = this - { - fix x y - assume f: "(\n. dist (f (x n)) (f (y n))) \ 0" - assume g: "(\n. dist (g (x n)) (g (y n))) \ 0" - have "(\n. \dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))\) \ 0" - by (rule Lim_transform_bound [OF _ tendsto_add_zero [OF f g]], - simp add: le) - } - then show ?thesis - using assms unfolding uniformly_continuous_on_sequentially - unfolding dist_real_def by simp -qed - -lemma uniformly_continuous_on_norm[continuous_intros]: - fixes f :: "'a :: metric_space \ 'b :: real_normed_vector" - assumes "uniformly_continuous_on s f" - shows "uniformly_continuous_on s (\x. norm (f x))" - unfolding norm_conv_dist using assms - by (intro uniformly_continuous_on_dist uniformly_continuous_on_const) - -lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]: - fixes g :: "_::metric_space \ _" - assumes "uniformly_continuous_on s g" - shows "uniformly_continuous_on s (\x. f (g x))" - using assms unfolding uniformly_continuous_on_sequentially - unfolding dist_norm tendsto_norm_zero_iff diff[symmetric] - by (auto intro: tendsto_zero) - -lemma uniformly_continuous_on_cmul[continuous_intros]: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" - assumes "uniformly_continuous_on s f" - shows "uniformly_continuous_on s (\x. c *\<^sub>R f(x))" - using bounded_linear_scaleR_right assms - by (rule bounded_linear.uniformly_continuous_on) - -lemma dist_minus: - fixes x y :: "'a::real_normed_vector" - shows "dist (- x) (- y) = dist x y" - unfolding dist_norm minus_diff_minus norm_minus_cancel .. - -lemma uniformly_continuous_on_minus[continuous_intros]: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" - shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\x. - f x)" - unfolding uniformly_continuous_on_def dist_minus . - -lemma uniformly_continuous_on_add[continuous_intros]: - fixes f g :: "'a::metric_space \ 'b::real_normed_vector" - assumes "uniformly_continuous_on s f" - and "uniformly_continuous_on s g" - shows "uniformly_continuous_on s (\x. f x + g x)" - using assms - unfolding uniformly_continuous_on_sequentially - unfolding dist_norm tendsto_norm_zero_iff add_diff_add - by (auto intro: tendsto_add_zero) - -lemma uniformly_continuous_on_diff[continuous_intros]: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" - assumes "uniformly_continuous_on s f" - and "uniformly_continuous_on s g" - shows "uniformly_continuous_on s (\x. f x - g x)" - using assms uniformly_continuous_on_add [of s f "- g"] - by (simp add: fun_Compl_def uniformly_continuous_on_minus) - text \Continuity in terms of open preimages.\ lemma continuous_at_open: @@ -4886,213 +2090,4 @@ using T_def by (auto elim!: eventually_mono) qed -lemma continuous_on_open: - "continuous_on S f \ - (\T. openin (subtopology euclidean (f ` S)) T \ - openin (subtopology euclidean S) (S \ f -` T))" - unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute - by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong) - -lemma continuous_on_open_gen: - fixes f :: "'a::metric_space \ 'b::metric_space" - assumes "f ` S \ T" - shows "continuous_on S f \ - (\U. openin (subtopology euclidean T) U - \ openin (subtopology euclidean S) (S \ f -` U))" - (is "?lhs = ?rhs") -proof - assume ?lhs - then show ?rhs - apply (clarsimp simp: openin_euclidean_subtopology_iff continuous_on_iff) - by (metis assms image_subset_iff) -next - have ope: "openin (subtopology euclidean T) (ball y e \ T)" for y e - by (simp add: Int_commute openin_open_Int) - assume R [rule_format]: ?rhs - show ?lhs - proof (clarsimp simp add: continuous_on_iff) - fix x and e::real - assume "x \ S" and "0 < e" - then have x: "x \ S \ (f -` ball (f x) e \ f -` T)" - using assms by auto - show "\d>0. \x'\S. dist x' x < d \ dist (f x') (f x) < e" - using R [of "ball (f x) e \ T"] x - by (fastforce simp add: ope openin_euclidean_subtopology_iff [of S] dist_commute) - qed -qed - -lemma continuous_openin_preimage: - fixes f :: "'a::metric_space \ 'b::metric_space" - shows - "\continuous_on S f; f ` S \ T; openin (subtopology euclidean T) U\ - \ openin (subtopology euclidean S) (S \ f -` U)" -by (simp add: continuous_on_open_gen) - -text \Similarly in terms of closed sets.\ - -lemma continuous_on_closed: - "continuous_on S f \ - (\T. closedin (subtopology euclidean (f ` S)) T \ - closedin (subtopology euclidean S) (S \ f -` T))" - unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute - by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong) - -lemma continuous_on_closed_gen: - fixes f :: "'a::metric_space \ 'b::metric_space" - assumes "f ` S \ T" - shows "continuous_on S f \ - (\U. closedin (subtopology euclidean T) U - \ closedin (subtopology euclidean S) (S \ f -` U))" - (is "?lhs = ?rhs") -proof - - have *: "U \ T \ S \ f -` (T - U) = S - (S \ f -` U)" for U - using assms by blast - show ?thesis - proof - assume L: ?lhs - show ?rhs - proof clarify - fix U - assume "closedin (subtopology euclidean T) U" - then show "closedin (subtopology euclidean S) (S \ f -` U)" - using L unfolding continuous_on_open_gen [OF assms] - by (metis * closedin_def inf_le1 topspace_euclidean_subtopology) - qed - next - assume R [rule_format]: ?rhs - show ?lhs - unfolding continuous_on_open_gen [OF assms] - by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology) - qed -qed - -lemma continuous_closedin_preimage_gen: - fixes f :: "'a::metric_space \ 'b::metric_space" - assumes "continuous_on S f" "f ` S \ T" "closedin (subtopology euclidean T) U" - shows "closedin (subtopology euclidean S) (S \ f -` U)" -using assms continuous_on_closed_gen by blast - -lemma continuous_on_imp_closedin: - assumes "continuous_on S f" "closedin (subtopology euclidean (f ` S)) T" - shows "closedin (subtopology euclidean S) (S \ f -` T)" -using assms continuous_on_closed by blast - -subsection%unimportant \Half-global and completely global cases\ - -lemma continuous_openin_preimage_gen: - assumes "continuous_on S f" "open T" - shows "openin (subtopology euclidean S) (S \ f -` T)" -proof - - have *: "(S \ f -` T) = (S \ f -` (T \ f ` S))" - by auto - have "openin (subtopology euclidean (f ` S)) (T \ f ` S)" - using openin_open_Int[of T "f ` S", OF assms(2)] unfolding openin_open by auto - then show ?thesis - using assms(1)[unfolded continuous_on_open, THEN spec[where x="T \ f ` S"]] - using * by auto -qed - -lemma continuous_closedin_preimage: - assumes "continuous_on S f" and "closed T" - shows "closedin (subtopology euclidean S) (S \ f -` T)" -proof - - have *: "(S \ f -` T) = (S \ f -` (T \ f ` S))" - by auto - have "closedin (subtopology euclidean (f ` S)) (T \ f ` S)" - using closedin_closed_Int[of T "f ` S", OF assms(2)] - by (simp add: Int_commute) - then show ?thesis - using assms(1)[unfolded continuous_on_closed, THEN spec[where x="T \ f ` S"]] - using * by auto -qed - -lemma continuous_openin_preimage_eq: - "continuous_on S f \ - (\T. open T \ openin (subtopology euclidean S) (S \ f -` T))" -apply safe -apply (simp add: continuous_openin_preimage_gen) -apply (fastforce simp add: continuous_on_open openin_open) -done - -lemma continuous_closedin_preimage_eq: - "continuous_on S f \ - (\T. closed T \ closedin (subtopology euclidean S) (S \ f -` T))" -apply safe -apply (simp add: continuous_closedin_preimage) -apply (fastforce simp add: continuous_on_closed closedin_closed) -done - -lemma continuous_open_preimage: - assumes contf: "continuous_on S f" and "open S" "open T" - shows "open (S \ f -` T)" -proof- - obtain U where "open U" "(S \ f -` T) = S \ U" - using continuous_openin_preimage_gen[OF contf \open T\] - unfolding openin_open by auto - then show ?thesis - using open_Int[of S U, OF \open S\] by auto -qed - -lemma continuous_closed_preimage: - assumes contf: "continuous_on S f" and "closed S" "closed T" - shows "closed (S \ f -` T)" -proof- - obtain U where "closed U" "(S \ f -` T) = S \ U" - using continuous_closedin_preimage[OF contf \closed T\] - unfolding closedin_closed by auto - then show ?thesis using closed_Int[of S U, OF \closed S\] by auto -qed - -lemma continuous_open_vimage: "open S \ (\x. continuous (at x) f) \ open (f -` S)" - by (metis continuous_on_eq_continuous_within open_vimage) - -lemma continuous_closed_vimage: "closed S \ (\x. continuous (at x) f) \ closed (f -` S)" - by (simp add: closed_vimage continuous_on_eq_continuous_within) - -lemma interior_image_subset: - assumes "inj f" "\x. continuous (at x) f" - shows "interior (f ` S) \ f ` (interior S)" -proof - fix x assume "x \ interior (f ` S)" - then obtain T where as: "open T" "x \ T" "T \ f ` S" .. - then have "x \ f ` S" by auto - then obtain y where y: "y \ S" "x = f y" by auto - have "open (f -` T)" - using assms \open T\ by (simp add: continuous_at_imp_continuous_on open_vimage) - moreover have "y \ vimage f T" - using \x = f y\ \x \ T\ by simp - moreover have "vimage f T \ S" - using \T \ image f S\ \inj f\ unfolding inj_on_def subset_eq by auto - ultimately have "y \ interior S" .. - with \x = f y\ show "x \ f ` interior S" .. -qed - -subsection%unimportant \Topological properties of linear functions\ - -lemma linear_lim_0: - assumes "bounded_linear f" - shows "(f \ 0) (at (0))" -proof - - interpret f: bounded_linear f by fact - have "(f \ f 0) (at 0)" - using tendsto_ident_at by (rule f.tendsto) - then show ?thesis unfolding f.zero . -qed - -lemma linear_continuous_at: - assumes "bounded_linear f" - shows "continuous (at a) f" - unfolding continuous_at using assms - apply (rule bounded_linear.tendsto) - apply (rule tendsto_ident_at) - done - -lemma linear_continuous_within: - "bounded_linear f \ continuous (at x within s) f" - using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto - -lemma linear_continuous_on: - "bounded_linear f \ continuous_on s f" - using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto - end \ No newline at end of file diff -r c2d5575d9da5 -r 5aa5a8d6e5b5 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sat Dec 29 18:40:29 2018 +0000 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sat Dec 29 20:32:09 2018 +0100 @@ -8,7 +8,7 @@ theory Topology_Euclidean_Space imports - Elementary_Topology + Elementary_Normed_Spaces Linear_Algebra Norm_Arith begin