# HG changeset patch # User paulson # Date 1537568092 -3600 # Node ID 30e88eabf1670807aed63e8f0083b97854863a4d # Parent aec64b88e708d5948e3cc4c9ca713cea7b7eba84# Parent 1eb517214deb1acc65bbc3864836f31083fc6f29 merged diff -r aec64b88e708 -r 30e88eabf167 src/HOL/Analysis/Function_Topology.thy --- a/src/HOL/Analysis/Function_Topology.thy Fri Sep 21 22:26:10 2018 +0200 +++ b/src/HOL/Analysis/Function_Topology.thy Fri Sep 21 23:14:52 2018 +0100 @@ -1,9 +1,9 @@ -(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr +(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr with additions from LCP License: BSD *) theory Function_Topology -imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure +imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure begin @@ -94,13 +94,12 @@ using assms(3) apply (induct rule: generate_topology_on.induct) using assms(1) assms(2) unfolding istopology_def by auto -definition%unimportant topology_generated_by::"('a set set) \ ('a topology)" - where "topology_generated_by S = topology (generate_topology_on S)" +abbreviation%unimportant topology_generated_by::"('a set set) \ ('a topology)" + where "topology_generated_by S \ topology (generate_topology_on S)" lemma%unimportant openin_topology_generated_by_iff: "openin (topology_generated_by S) s \ generate_topology_on S s" -using topology_inverse'[OF istopology_generate_topology_on[of S]] -unfolding topology_generated_by_def by simp + using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp lemma%unimportant openin_topology_generated_by: "openin (topology_generated_by S) s \ generate_topology_on S s" @@ -127,6 +126,138 @@ "s \ S \ openin (topology_generated_by S) s" by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis) +lemma generate_topology_on_Inter: + "\finite \; \K. K \ \ \ generate_topology_on \ K; \ \ {}\ \ generate_topology_on \ (\\)" + by (induction \ rule: finite_induct; force intro: generate_topology_on.intros) + +subsection\Topology bases and sub-bases\ + +lemma istopology_base_alt: + "istopology (arbitrary union_of P) \ + (\S T. (arbitrary union_of P) S \ (arbitrary union_of P) T + \ (arbitrary union_of P) (S \ T))" + by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union) + +lemma istopology_base_eq: + "istopology (arbitrary union_of P) \ + (\S T. P S \ P T \ (arbitrary union_of P) (S \ T))" + by (simp add: istopology_base_alt arbitrary_union_of_Int_eq) + +lemma istopology_base: + "(\S T. \P S; P T\ \ P(S \ T)) \ istopology (arbitrary union_of P)" + by (simp add: arbitrary_def istopology_base_eq union_of_inc) + +lemma openin_topology_base_unique: + "openin X = arbitrary union_of P \ + (\V. P V \ openin X V) \ (\U x. openin X U \ x \ U \ (\V. P V \ x \ V \ V \ U))" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + by (auto simp: union_of_def arbitrary_def) +next + assume R: ?rhs + then have *: "\\\Collect P. \\ = S" if "openin X S" for S + using that by (rule_tac x="{V. P V \ V \ S}" in exI) fastforce + from R show ?lhs + by (fastforce simp add: union_of_def arbitrary_def intro: *) +qed + +lemma topology_base_unique: + "\\S. P S \ openin X S; + \U x. \openin X U; x \ U\ \ \B. P B \ x \ B \ B \ U\ + \ topology(arbitrary union_of P) = X" + by (metis openin_topology_base_unique openin_inverse [of X]) + +lemma topology_bases_eq_aux: + "\(arbitrary union_of P) S; + \U x. \P U; x \ U\ \ \V. Q V \ x \ V \ V \ U\ + \ (arbitrary union_of Q) S" + by (metis arbitrary_union_of_alt arbitrary_union_of_idempot) + +lemma topology_bases_eq: + "\\U x. \P U; x \ U\ \ \V. Q V \ x \ V \ V \ U; + \V x. \Q V; x \ V\ \ \U. P U \ x \ U \ U \ V\ + \ topology (arbitrary union_of P) = + topology (arbitrary union_of Q)" + by (fastforce intro: arg_cong [where f=topology] elim: topology_bases_eq_aux) + +lemma istopology_subbase: + "istopology (arbitrary union_of (finite intersection_of P relative_to S))" + by (simp add: finite_intersection_of_Int istopology_base relative_to_Int) + +lemma openin_subbase: + "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S + \ (arbitrary union_of (finite intersection_of B relative_to U)) S" + by (simp add: istopology_subbase topology_inverse') + +lemma topspace_subbase [simp]: + "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _") +proof + show "?lhs \ U" + by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset) + show "U \ ?lhs" + by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase + openin_subset relative_to_inc subset_UNIV topology_inverse') +qed + +lemma minimal_topology_subbase: + "\\S. P S \ openin X S; openin X U; + openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S\ + \ openin X S" + apply (simp add: istopology_subbase topology_inverse) + apply (simp add: union_of_def intersection_of_def relative_to_def) + apply (blast intro: openin_Int_Inter) + done + +lemma istopology_subbase_UNIV: + "istopology (arbitrary union_of (finite intersection_of P))" + by (simp add: istopology_base finite_intersection_of_Int) + + +lemma generate_topology_on_eq: + "generate_topology_on S = arbitrary union_of finite' intersection_of (\x. x \ S)" (is "?lhs = ?rhs") +proof (intro ext iffI) + fix A + assume "?lhs A" + then show "?rhs A" + proof induction + case (Int a b) + then show ?case + by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base) + next + case (UN K) + then show ?case + by (simp add: arbitrary_union_of_Union) + next + case (Basis s) + then show ?case + by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset) + qed auto +next + fix A + assume "?rhs A" + then obtain \ where \: "\T. T \ \ \ \\. finite' \ \ \ \ S \ \\ = T" and eq: "A = \\" + unfolding union_of_def intersection_of_def by auto + show "?lhs A" + unfolding eq + proof (rule generate_topology_on.UN) + fix T + assume "T \ \" + with \ obtain \ where "finite' \" "\ \ S" "\\ = T" + by blast + have "generate_topology_on S (\\)" + proof (rule generate_topology_on_Inter) + show "finite \" "\ \ {}" + by (auto simp: \finite' \\) + show "\K. K \ \ \ generate_topology_on S K" + by (metis \\ \ S\ generate_topology_on.simps subset_iff) + qed + then show "generate_topology_on S T" + using \\\ = T\ by blast + qed +qed + subsubsection%important \Continuity\ text \We will need to deal with continuous maps in terms of topologies and not in terms @@ -315,11 +446,113 @@ text \The total set of the product topology is the product of the total sets along each coordinate.\ -lemma%important product_topology_topspace: +proposition product_topology: + "product_topology X I = + topology + (arbitrary union_of + ((finite intersection_of + (\F. \i U. F = {f. f i \ U} \ i \ I \ openin (X i) U)) + relative_to (\\<^sub>E i\I. topspace (X i))))" + (is "_ = topology (_ union_of ((_ intersection_of ?\) relative_to ?TOP))") +proof - + let ?\ = "(\F. \Y. F = Pi\<^sub>E I Y \ (\i. openin (X i) (Y i)) \ finite {i. Y i \ topspace (X i)})" + have *: "(finite' intersection_of ?\) A = (finite intersection_of ?\ relative_to ?TOP) A" for A + proof - + have 1: "\U. (\\. finite \ \ \ \ Collect ?\ \ \\ = U) \ ?TOP \ U = \\" + if \: "\ \ Collect ?\" and "finite' \" "A = \\" "\ \ {}" for \ + proof - + have "\U \ \. \Y. U = Pi\<^sub>E I Y \ (\i. openin (X i) (Y i)) \ finite {i. Y i \ topspace (X i)}" + using \ by auto + then obtain Y where Y: "\U. U \ \ \ U = Pi\<^sub>E I (Y U) \ (\i. openin (X i) (Y U i)) \ finite {i. (Y U) i \ topspace (X i)}" + by metis + obtain U where "U \ \" + using \\ \ {}\ by blast + let ?F = "\U. (\i. {f. f i \ Y U i}) ` {i \ I. Y U i \ topspace (X i)}" + show ?thesis + proof (intro conjI exI) + show "finite (\U\\. ?F U)" + using Y \finite' \\ by auto + show "?TOP \ \(\U\\. ?F U) = \\" + proof + have *: "f \ U" + if "U \ \" and "\V\\. \i. i \ I \ Y V i \ topspace (X i) \ f i \ Y V i" + and "\i\I. f i \ topspace (X i)" and "f \ extensional I" for f U + proof - + have "Pi\<^sub>E I (Y U) = U" + using Y \U \ \\ by blast + then show "f \ U" + using that unfolding PiE_def Pi_def by blast + qed + show "?TOP \ \(\U\\. ?F U) \ \\" + by (auto simp: PiE_iff *) + show "\\ \ ?TOP \ \(\U\\. ?F U)" + using Y openin_subset \finite' \\ by fastforce + qed + qed (use Y openin_subset in \blast+\) + qed + have 2: "\\'. finite' \' \ \' \ Collect ?\ \ \\' = ?TOP \ \\" + if \: "\ \ Collect ?\" and "finite \" for \ + proof (cases "\={}") + case True + then show ?thesis + apply (rule_tac x="{?TOP}" in exI, simp) + apply (rule_tac x="\i. topspace (X i)" in exI) + apply force + done + next + case False + then obtain U where "U \ \" + by blast + have "\U \ \. \i Y. U = {f. f i \ Y} \ i \ I \ openin (X i) Y" + using \ by auto + then obtain J Y where + Y: "\U. U \ \ \ U = {f. f (J U) \ Y U} \ J U \ I \ openin (X (J U)) (Y U)" + by metis + let ?G = "\U. \\<^sub>E i\I. if i = J U then Y U else topspace (X i)" + show ?thesis + proof (intro conjI exI) + show "finite (?G ` \)" "?G ` \ \ {}" + using \finite \\ \U \ \\ by blast+ + have *: "\U. U \ \ \ openin (X (J U)) (Y U)" + using Y by force + show "?G ` \ \ {Pi\<^sub>E I Y |Y. (\i. openin (X i) (Y i)) \ finite {i. Y i \ topspace (X i)}}" + apply clarsimp + apply (rule_tac x=" (\i. if i = J U then Y U else topspace (X i))" in exI) + apply (auto simp: *) + done + next + show "(\U\\. ?G U) = ?TOP \ \\" + proof + have "(\\<^sub>E i\I. if i = J U then Y U else topspace (X i)) \ (\\<^sub>E i\I. topspace (X i))" + apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm) + using Y \U \ \\ openin_subset by blast+ + then have "(\U\\. ?G U) \ ?TOP" + using \U \ \\ + by fastforce + moreover have "(\U\\. ?G U) \ \\" + using PiE_mem Y by fastforce + ultimately show "(\U\\. ?G U) \ ?TOP \ \\" + by auto + qed (use Y in fastforce) + qed + qed + show ?thesis + unfolding relative_to_def intersection_of_def + by (safe; blast dest!: 1 2) + qed + show ?thesis + unfolding product_topology_def generate_topology_on_eq + apply (rule arg_cong [where f = topology]) + apply (rule arg_cong [where f = "(union_of)arbitrary"]) + apply (force simp: *) + done +qed + +lemma%important topspace_product_topology: "topspace (product_topology T I) = (\\<^sub>E i\I. topspace(T i))" proof%unimportant show "topspace (product_topology T I) \ (\\<^sub>E i\I. topspace (T i))" - unfolding product_topology_def apply (simp only: topology_generated_by_topspace) + unfolding product_topology_def topology_generated_by_topspace unfolding topspace_def by auto have "(\\<^sub>E i\I. topspace (T i)) \ {(\\<^sub>E i\I. X i) |X. (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}}" using openin_topspace not_finite_existsD by auto @@ -330,11 +563,11 @@ lemma%unimportant product_topology_basis: assumes "\i. openin (T i) (X i)" "finite {i. X i \ topspace (T i)}" shows "openin (product_topology T I) (\\<^sub>E i\I. X i)" -unfolding product_topology_def apply (rule topology_generated_by_Basis) using assms by auto + unfolding product_topology_def + by (rule topology_generated_by_Basis) (use assms in auto) lemma%important product_topology_open_contains_basis: - assumes "openin (product_topology T I) U" - "x \ U" + assumes "openin (product_topology T I) U" "x \ U" shows "\X. x \ (\\<^sub>E i\I. X i) \ (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)} \ (\\<^sub>E i\I. X i) \ U" proof%unimportant - have "generate_topology_on {(\\<^sub>E i\I. X i) |X. (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}} U" @@ -375,6 +608,114 @@ qed +lemma openin_product_topology: + "openin (product_topology X I) = + arbitrary union_of + ((finite intersection_of (\F. (\i U. F = {f. f i \ U} \ i \ I \ openin (X i) U))) + relative_to topspace (product_topology X I))" + apply (subst product_topology) + apply (simp add: topspace_product_topology topology_inverse' [OF istopology_subbase]) + done + +lemma subtopology_PiE: + "subtopology (product_topology X I) (\\<^sub>E i\I. (S i)) = product_topology (\i. subtopology (X i) (S i)) I" +proof - + let ?P = "\F. \i U. F = {f. f i \ U} \ i \ I \ openin (X i) U" + let ?X = "\\<^sub>E i\I. topspace (X i)" + have "finite intersection_of ?P relative_to ?X \ Pi\<^sub>E I S = + finite intersection_of (?P relative_to ?X \ Pi\<^sub>E I S) relative_to ?X \ Pi\<^sub>E I S" + by (rule finite_intersection_of_relative_to) + also have "\ = finite intersection_of + ((\F. \i U. F = {f. f i \ U} \ i \ I \ (openin (X i) relative_to S i) U) + relative_to ?X \ Pi\<^sub>E I S) + relative_to ?X \ Pi\<^sub>E I S" + apply (rule arg_cong2 [where f = "(relative_to)"]) + apply (rule arg_cong [where f = "(intersection_of)finite"]) + apply (rule ext) + apply (auto simp: relative_to_def intersection_of_def) + done + finally + have "finite intersection_of ?P relative_to ?X \ Pi\<^sub>E I S = + finite intersection_of + (\F. \i U. F = {f. f i \ U} \ i \ I \ (openin (X i) relative_to S i) U) + relative_to ?X \ Pi\<^sub>E I S" + by (metis finite_intersection_of_relative_to) + then show ?thesis + unfolding topology_eq + apply clarify + apply (simp add: openin_product_topology flip: openin_relative_to) + apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int) + done +qed + + +lemma product_topology_base_alt: + "finite intersection_of (\F. (\i U. F = {f. f i \ U} \ i \ I \ openin (X i) U)) + relative_to topspace(product_topology X I) = + (\F. (\U. F = Pi\<^sub>E I U \ finite {i \ I. U i \ topspace(X i)} \ (\i \ I. openin (X i) (U i))))" + (is "?lhs = ?rhs") +proof - + have "(\F. ?lhs F \ ?rhs F)" + unfolding all_relative_to all_intersection_of topspace_product_topology + proof clarify + fix \ + assume "finite \" and "\ \ {{f. f i \ U} |i U. i \ I \ openin (X i) U}" + then show "\U. (\\<^sub>E i\I. topspace (X i)) \ \\ = Pi\<^sub>E I U \ + finite {i \ I. U i \ topspace (X i)} \ (\i\I. openin (X i) (U i))" + proof (induction) + case (insert F \) + then obtain U where eq: "(\\<^sub>E i\I. topspace (X i)) \ \\ = Pi\<^sub>E I U" + and fin: "finite {i \ I. U i \ topspace (X i)}" + and ope: "\i. i \ I \ openin (X i) (U i)" + by auto + obtain i V where "F = {f. f i \ V}" "i \ I" "openin (X i) V" + using insert by auto + let ?U = "\j. U j \ (if j = i then V else topspace(X j))" + show ?case + proof (intro exI conjI) + show "(\\<^sub>E i\I. topspace (X i)) \ \insert F \ = Pi\<^sub>E I ?U" + using eq PiE_mem \i \ I\ by (auto simp: \F = {f. f i \ V}\) fastforce + next + show "finite {i \ I. ?U i \ topspace (X i)}" + by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto + next + show "\i\I. openin (X i) (?U i)" + by (simp add: \openin (X i) V\ ope openin_Int) + qed + qed (auto intro: dest: not_finite_existsD) + qed + moreover have "(\F. ?rhs F \ ?lhs F)" + proof clarify + fix U :: "'a \ 'b set" + assume fin: "finite {i \ I. U i \ topspace (X i)}" and ope: "\i\I. openin (X i) (U i)" + let ?U = "\i\{i \ I. U i \ topspace (X i)}. {x. x i \ U i}" + show "?lhs (Pi\<^sub>E I U)" + unfolding relative_to_def topspace_product_topology + proof (intro exI conjI) + show "(finite intersection_of (\F. \i U. F = {f. f i \ U} \ i \ I \ openin (X i) U)) ?U" + using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto + show "(\\<^sub>E i\I. topspace (X i)) \ ?U = Pi\<^sub>E I U" + using ope openin_subset by fastforce + qed + qed + ultimately show ?thesis + by meson +qed + + +lemma topspace_product_topology_alt: + "topspace (product_topology Y I) = {f \ extensional I. \k \ I. f k \ topspace(Y k)}" + by (force simp: product_topology PiE_def) + +lemma openin_product_topology_alt: + "openin (product_topology X I) S \ + (\x \ S. \U. finite {i \ I. U i \ topspace(X i)} \ + (\i \ I. openin (X i) (U i)) \ x \ Pi\<^sub>E I U \ Pi\<^sub>E I U \ S)" + apply (simp add: openin_product_topology arbitrary_union_of_alt product_topology_base_alt, auto) + apply (drule bspec; blast) + done + + text \The basic property of the product topology is the continuity of projections:\ lemma%unimportant continuous_on_topo_product_coordinates [simp]: @@ -396,7 +737,7 @@ using ** by auto } then show ?thesis unfolding continuous_on_topo_def - by (auto simp add: assms product_topology_topspace PiE_iff) + by (auto simp add: assms topspace_product_topology PiE_iff) qed lemma%important continuous_on_topo_coordinatewise_then_product [intro]: @@ -427,7 +768,7 @@ show "f `topspace T1 \ \{Pi\<^sub>E I X |X. (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}}" apply (subst topology_generated_by_topspace[symmetric]) apply (subst product_topology_def[symmetric]) - apply (simp only: product_topology_topspace) + apply (simp only: topspace_product_topology) apply (auto simp add: PiE_iff) using assms unfolding continuous_on_topo_def by auto qed @@ -449,7 +790,7 @@ have "f x \ topspace (product_topology T I)" using assms \x \ topspace T1\ unfolding continuous_on_topo_def by auto then have "f x \ (\\<^sub>E i\I. topspace (T i))" - using product_topology_topspace by metis + using topspace_product_topology by metis then show "f x i = undefined" using \i \ I\ by (auto simp add: PiE_iff extensional_def) qed @@ -479,7 +820,7 @@ instance proof%unimportant have "topspace (product_topology (\(i::'a). euclidean::('b topology)) UNIV) = UNIV" - unfolding product_topology_topspace topspace_euclidean by auto + unfolding topspace_product_topology topspace_euclidean by auto then show "open (UNIV::('a \ 'b) set)" unfolding open_fun_def by (metis openin_topspace) qed (auto simp add: open_fun_def) @@ -1233,6 +1574,8 @@ by standard + + subsection%important \Measurability\ (*FIX ME mv *) text \There are two natural sigma-algebras on a product space: the borel sigma algebra, diff -r aec64b88e708 -r 30e88eabf167 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Sep 21 22:26:10 2018 +0200 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Sep 21 23:14:52 2018 +0100 @@ -11,6 +11,7 @@ "HOL-Library.Indicator_Function" "HOL-Library.Countable_Set" "HOL-Library.FuncSet" + "HOL-Library.Set_Idioms" Linear_Algebra Norm_Arith begin @@ -817,6 +818,9 @@ unfolding subtopology_def topology_inverse'[OF istopology_subtopology] by 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)