diff --git a/thys/S_Finite_Measure_Monad/ROOT b/thys/S_Finite_Measure_Monad/ROOT --- a/thys/S_Finite_Measure_Monad/ROOT +++ b/thys/S_Finite_Measure_Monad/ROOT @@ -1,15 +1,17 @@ chapter AFP session "S_Finite_Measure_Monad" = "HOL-Probability" + options [timeout = 600] sessions "Standard_Borel_Spaces" theories "Lemmas_S_Finite_Measure_Monad" "Kernels" - "QuasiBorel" "QBS_Morphism" + "QuasiBorel" + "QBS_Morphism" "Measure_QuasiBorel_Adjunction" "Monad_QuasiBorel" - "Montecarlo" "Query" + "Montecarlo" + "Query" document_files "root.tex" "root.bib" diff --git a/thys/Standard_Borel_Spaces/Abstract_Metrizable_Topology.thy b/thys/Standard_Borel_Spaces/Abstract_Metrizable_Topology.thy --- a/thys/Standard_Borel_Spaces/Abstract_Metrizable_Topology.thy +++ b/thys/Standard_Borel_Spaces/Abstract_Metrizable_Topology.thy @@ -1,2402 +1,2406 @@ (* Title: Abstract_Metrizable_Topology.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) section \Abstract Metrizable Topology\ theory Abstract_Metrizable_Topology imports "Set_Based_Metric_Product" begin subsection \ Metrizable Spaces \ locale metrizable = fixes S :: "'a topology" assumes ex_metric:"\\. metric_set (topspace S) \ \ S = metric_set.mtopology (topspace S) \" begin lemma metric: obtains \ where "metric_set (topspace S) \" "metric_set.mtopology (topspace S) \ = S" using ex_metric by metis lemma bounded_metric: obtains \ where "metric_set (topspace S) \" "metric_set.mtopology (topspace S) \ = S" "\x y. \ x y < 1" proof - obtain \ where "metric_set (topspace S) \" "metric_set.mtopology (topspace S) \ = S" by(rule metric) then have "\\. metric_set (topspace S) \ \ metric_set.mtopology (topspace S) \ = S \ (\x y. \ x y < 1)" using metric_set.bounded_dist_dist(1) metric_set.bounded_dist_dist(2) metric_set.bounded_dist_generate_same_topology by(fastforce intro!: exI[where x="bounded_dist \"]) thus ?thesis using that by auto qed lemma second_countable_if_separable: assumes "separable S" shows "second_countable S" proof - obtain d where hd:"metric_set (topspace S) d" "S = metric_set.mtopology (topspace S) d" using ex_metric by(auto simp: metrizable_def) then interpret m: separable_metric_set "topspace S" d using metric_set.separable_iff_topological_separable[of "topspace S" d] assms by auto show "second_countable S" using m.second_countable \S = m.mtopology\ by simp qed corollary second_countable_iff_separable: "second_countable S \ separable S" using second_countable_if_separable separable_if_second_countable by auto lemma Hausdorff: "Hausdorff_space S" using ex_metric metric_set.mtopology_Hausdorff by fastforce lemma subtopology: "metrizable (subtopology S X)" proof - obtain \ where h:"metric_set (topspace S) \" "metric_set.mtopology (topspace S) \ = S" by(rule metric) then show ?thesis using metric_set.submetric_subtopology[OF h(1),of "topspace S \ X"] by(auto intro!: exI[where x="submetric (topspace S \ X) \"] simp: metrizable_def subtopology_restrict metric_set.mtopology_topspace metric_set.submetric_metric_set) qed lemma g_delta_of_closedin: assumes "closedin S X" shows "g_delta_of S X" using assms ex_metric metric_set.g_delta_of_closed by fastforce lemma closedin_singleton: assumes "s \ topspace S" shows "closedin S {s}" proof - obtain \ where h:"metric_set (topspace S) \" "metric_set.mtopology (topspace S) \ = S" by(rule metric) then show ?thesis using metric_set.closedin_closed_ball[OF h(1),of s 0] by(simp add: metric_set.closed_ball_0[OF h(1) assms]) qed lemma dense_of_infinite: assumes "infinite (topspace S)" "dense_of S U" shows "infinite U" proof - obtain \ where h:"metric_set (topspace S) \" "metric_set.mtopology (topspace S) \ = S" by(rule metric) show ?thesis by(rule metric_set.dense_set_infinite[OF h(1),simplified h(2),OF assms]) qed lemma homeomorphic_metrizable: assumes "S homeomorphic_space S'" shows "metrizable S'" proof(rule metric) fix d assume h: "metric_set (topspace S) d" "metric_set.mtopology (topspace S) d = S" then interpret m: metric_set "topspace S" d by simp from assms obtain f g where fg: "homeomorphic_maps S S' f g" by(auto simp: homeomorphic_space_def) hence g: "g \ topspace S' \ topspace S" "inj_on g (topspace S')" "g ` (topspace S') = topspace S" by (auto simp: homeomorphic_eq_injective_perfect_map homeomorphic_maps_map perfect_map_def) have f: "f \ topspace S \ topspace S'" "inj_on f (topspace S)" "f ` (topspace S) = topspace S'" using fg by (auto simp: homeomorphic_eq_injective_perfect_map homeomorphic_maps_map perfect_map_def) interpret m': metric_set "topspace S'" "m.ed g (topspace S')" by(simp add: m.embed_dist_dist[OF g(1,2)]) show "metrizable S'" unfolding metrizable_def proof(safe intro!: exI[where x="m.ed g (topspace S')"]) have [simp]:"m'.ed f (topspace S) = d" by standard+ (insert f g fg m.dist_notin m.dist_notin',auto simp: m'.embed_dist_on_def m.embed_dist_on_def homeomorphic_maps_def) have [simp]:"((`) f ` {m.open_ball a \ |a \. a \ topspace S \ 0 < \}) = {m'.open_ball a \ |a \. a \ topspace S' \ 0 < \}" proof safe fix a and e :: real assume "a \ topspace S" "0 < e" then show "\b e'. f ` m.open_ball a e = m'.open_ball b e' \ b \ topspace S' \ 0 < e'" using f g fg by(auto simp: m.open_ball_def m'.open_ball_def m.embed_dist_on_def homeomorphic_maps_def intro!: exI[where x="f a"] exI[where x=e]) (metis (no_types, lifting) image_eqI mem_Collect_eq) next fix a and e :: real assume "a \ topspace S'" "0 < e" then show "m'.open_ball a e \ (`) f ` {m.open_ball a \ |a \. a \ topspace S \ 0 < \}" using m'.embed_dist_open_ball[OF f(1,2),simplified,of "g a" e] f g fg m'.open_ballD'(1) by(auto simp: m.embed_dist_on_def homeomorphic_maps_def image_def intro!: exI[where x="g a"] exI[where x=e] exI[where x="m.open_ball (g a) e"]) blast qed show "S' = m'.mtopology" using topology_generated_by_homeomorphic_spaces[OF homeomorphic_maps_imp_map[OF fg] h(2)[symmetric,simplified m.mtopology_def2]] by(simp add: m'.mtopology_def2) qed(rule m'.metric_set_axioms) qed end lemma euclidean_metrizable: "metrizable (euclidean :: ('a ::metric_space) topology)" by (metis euclidean_mtopology metric_class_metric_set metrizable.intro topspace_euclidean) sublocale metric_set \ metrizable "mtopology" using metric_set_axioms metrizable_def mtopology_topspace by fastforce lemma metrizable_prod: assumes "metrizable X" "metrizable Y" shows "metrizable (prod_topology X Y)" proof obtain dx dy where "metric_set (topspace X) dx" "metric_set.mtopology (topspace X) dx = X" "metric_set (topspace Y) dy" "metric_set.mtopology (topspace Y) dy = Y" using metrizable.metric[OF assms(2)] metrizable.metric[OF assms(1)] by metis then show "\\. metric_set (topspace (prod_topology X Y)) \ \ prod_topology X Y = metric_set.mtopology (topspace (prod_topology X Y)) \" by(auto intro!: exI[where x="binary_distance (topspace X) dx (topspace Y) dy"] simp: binary_metric_set binary_distance_mtopology) qed lemma metrizable_product: assumes "countable I" "\i. i \ I \ metrizable (X i)" shows "metrizable (product_topology X I)" proof - obtain d where hd:"\i. i \ I \ metric_set (topspace (X i)) (d i)" "\i. i \ I \ X i = metric_set.mtopology (topspace (X i)) (d i)" using assms(2) by(auto simp: metrizable_def) metis from product_metricI'[of "1/2" _ _ d,OF _ _ assms(1) this(1)] interpret pd: product_metric "1 / 2" I "to_nat_on I" "from_nat_into I" "\i. topspace (X i)" "\i x y. if i \ I then bounded_dist (d i) x y else 0" 1 by simp show ?thesis using hd(2) by(auto simp: metrizable_def pd.product_dist_distance pd.product_dist_mtopology[symmetric] hd(1) metric_set.bounded_dist_generate_same_topology intro!: exI[where x=pd.product_dist] product_topology_cong) qed subsection \ Complete Metrizable Spaces \ locale complete_metrizable = fixes S :: "'a topology" assumes ex_cmetric: "\\. complete_metric_set (topspace S) \ \ S = metric_set.mtopology (topspace S) \" begin lemma cmetric: obtains \ where "complete_metric_set (topspace S) \" "metric_set.mtopology (topspace S) \ = S" using ex_cmetric by metis lemma bounded_cmetric: obtains \ where "complete_metric_set (topspace S) \" "metric_set.mtopology (topspace S) \ = S" "\x y. \ x y < 1" proof - obtain \ where "complete_metric_set (topspace S) \" "metric_set.mtopology (topspace S) \ = S" by(rule cmetric) then have "\\. complete_metric_set (topspace S) \ \ metric_set.mtopology (topspace S) \ = S \ (\x y. \ x y < 1)" using metric_set.bounded_dist_dist(1) metric_set.bounded_dist_dist(2) metric_set.bounded_dist_generate_same_topology complete_metric_set.bounded_dist_complete complete_metric_set_def by(fastforce intro!: exI[where x="bounded_dist \"]) thus ?thesis using that by auto qed lemma metrizable: "metrizable S" using complete_metric_set_def complete_metrizable_axioms complete_metrizable_def metrizable_def by blast sublocale metrizable by(rule metrizable) lemma closedin_complete_metrizable: assumes "closedin S A" shows "complete_metrizable (subtopology S A)" by (metis assms closedin_def complete_metric_set.submetric_complete_iff complete_metric_set_def complete_metrizable_axioms complete_metrizable_def metric_set.submetric_subtopology topspace_subtopology_subset) lemma homeomorphic_complete_metrizable: assumes "S homeomorphic_space S'" shows "complete_metrizable S'" proof(rule cmetric) fix d assume h: "complete_metric_set (topspace S) d" "metric_set.mtopology (topspace S) d = S" then interpret m: complete_metric_set "topspace S" d by simp from assms obtain f g where fg: "homeomorphic_maps S S' f g" by(auto simp: homeomorphic_space_def) hence g: "g \ topspace S' \ topspace S" "inj_on g (topspace S')" "g ` (topspace S') = topspace S" by (auto simp: homeomorphic_eq_injective_perfect_map homeomorphic_maps_map perfect_map_def) have f: "f \ topspace S \ topspace S'" "inj_on f (topspace S)" "f ` (topspace S) = topspace S'" using fg by (auto simp: homeomorphic_eq_injective_perfect_map homeomorphic_maps_map perfect_map_def) interpret m': complete_metric_set "topspace S'" "m.ed g (topspace S')" by(auto intro!: m.embed_dist_complete[OF g(1,2)] simp: h(2) g(3)) show "complete_metrizable S'" unfolding complete_metrizable_def proof(safe intro!: exI[where x="m.ed g (topspace S')"]) have [simp]:"m'.ed f (topspace S) = d" by standard+ (insert f g fg m.dist_notin m.dist_notin',auto simp: m'.embed_dist_on_def m.embed_dist_on_def homeomorphic_maps_def) have [simp]:"((`) f ` {m.open_ball a \ |a \. a \ topspace S \ 0 < \}) = {m'.open_ball a \ |a \. a \ topspace S' \ 0 < \}" proof safe fix a and e :: real assume "a \ topspace S" "0 < e" then show "\b e'. f ` m.open_ball a e = m'.open_ball b e' \ b \ topspace S' \ 0 < e'" using f g fg by(auto simp: m.open_ball_def m'.open_ball_def m.embed_dist_on_def homeomorphic_maps_def intro!: exI[where x="f a"] exI[where x=e]) (metis (no_types, lifting) image_eqI mem_Collect_eq) next fix a and e :: real assume "a \ topspace S'" "0 < e" then show "m'.open_ball a e \ (`) f ` {m.open_ball a \ |a \. a \ topspace S \ 0 < \}" using m'.embed_dist_open_ball[OF f(1,2),simplified,of "g a" e] f g fg m'.open_ballD'(1) by(auto simp: m.embed_dist_on_def homeomorphic_maps_def image_def intro!: exI[where x="g a"] exI[where x=e] exI[where x="m.open_ball (g a) e"]) blast qed show "S' = m'.mtopology" using topology_generated_by_homeomorphic_spaces[OF homeomorphic_maps_imp_map[OF fg] h(2)[symmetric,simplified m.mtopology_def2]] by(simp add: m'.mtopology_def2) qed(rule m'.complete_metric_set_axioms) qed end lemma euclidean_complete_metrizable[simp]: "complete_metrizable (euclidean :: ('a ::complete_space) topology)" by (metis complete_metrizable.intro complete_space_complete_metric_set euclidean_mtopology topspace_euclidean) sublocale complete_metric_set \ complete_metrizable "mtopology" using complete_metric_set_axioms complete_metrizable_def mtopology_topspace by fastforce lemma complete_metrizable_prod: assumes "complete_metrizable X" "complete_metrizable Y" shows "complete_metrizable (prod_topology X Y)" proof obtain dx dy where "complete_metric_set (topspace X) dx" "metric_set.mtopology (topspace X) dx = X" "complete_metric_set (topspace Y) dy" "metric_set.mtopology (topspace Y) dy = Y" using complete_metrizable.cmetric[OF assms(2)] complete_metrizable.cmetric[OF assms(1)] by metis then show "\\. complete_metric_set (topspace (prod_topology X Y)) \ \ prod_topology X Y = metric_set.mtopology (topspace (prod_topology X Y)) \" using binary_distance_complete by(auto intro!: exI[where x="binary_distance (topspace X) dx (topspace Y) dy"] simp: binary_distance_mtopology complete_metric_set_def) qed lemma complete_metrizable_product: assumes "countable I" "\i. i \ I \ complete_metrizable (X i)" shows "complete_metrizable (product_topology X I)" proof - obtain d where hd:"\i. i \ I \ complete_metric_set (topspace (X i)) (d i)" "\i. i \ I \ X i = metric_set.mtopology (topspace (X i)) (d i)" using assms(2) by(auto simp: complete_metrizable_def) metis from product_complete_metricI'[of "1/2" _ _ d,OF _ _ assms(1) this(1)] interpret pd: product_complete_metric "1 / 2" I "to_nat_on I" "from_nat_into I" "\i. topspace (X i)" "\i x y. if i \ I then bounded_dist (d i) x y else 0" 1 by simp show ?thesis using hd(2) by(auto simp: complete_metrizable_def pd.product_dist_distance pd.product_dist_mtopology[symmetric] hd(1) complete_metric_set.axioms(1) metric_set.bounded_dist_generate_same_topology pd.complete_metric_set_axioms intro!: exI[where x=pd.product_dist] product_topology_cong) qed lemma(in complete_metrizable) g_delta_of_complete_metrizable: assumes "g_delta_of S B" shows "complete_metrizable (subtopology S B)" proof - obtain d where d:"complete_metric_set (topspace S) d" "metric_set.mtopology (topspace S) d = S" by(rule cmetric) interpret m: complete_metric_set "topspace S" d by fact obtain U :: "nat \ _" where U: "\n. openin S (U n)" "B = \ (range U)" using g_delta_ofD'[OF assms] by metis consider "topspace (subtopology S B) = {}" | "topspace (subtopology S B) = topspace S" | "topspace (subtopology S B) \ {}" "topspace (subtopology S B) \ topspace S" by (metis assms g_delta_of_subset order_le_less topspace_subtopology_subset) then show ?thesis proof cases case 1 with empty_metric_polish show ?thesis by(auto intro!: exI[where x="\x y. 0"] simp: complete_metrizable_def polish_metric_set_def separable_metric_set_def Int_absorb1 assms empty_metric_mtopology g_delta_of_subset subtopology_eq_discrete_topology_eq) next case 2 then have "B = topspace S" using g_delta_of_subset[OF assms] by auto thus ?thesis by(simp add: complete_metrizable_axioms) next case 3 then have h: "B \ {}" "\n. U n \ {}" by(auto simp: U(2)) define f where "f \ (\x. (x, (\i. 1 / m.dist_set (topspace S - (U i)) x)))" have f_inj:"inj f" by(auto simp: inj_def f_def) have f_inv: "\x. x \ f ` B \ f (fst x) = x" "\x. fst (f x) = x" by(auto simp: f_def) have "continuous_map (subtopology S B) (prod_topology S (powertop_real UNIV)) f" unfolding continuous_map_pairwise continuous_map_componentwise_UNIV proof safe have [simp]:"fst \ f = id" by(auto simp: f_def) show "continuous_map (subtopology S B) S (fst \ f)" by simp next fix k show "continuous_map (subtopology S B) euclideanreal (\x. (snd \ f) x k)" proof(cases "U k = topspace S") case True then show ?thesis by(simp add: f_def) next case False then have [simp]:"(\x. snd (f x) k) = (\x. 1 / m.dist_set (topspace S - (U k)) x)" by(simp add: f_def) have "continuous_map (subtopology S B) euclideanreal ..." proof(rule continuous_map_real_divide) show "continuous_map (subtopology S B) euclideanreal (m.dist_set (topspace S - U k))" using m.dist_set_continuous[simplified d(2),of "topspace S - U k"] by (simp add: continuous_map_from_subtopology) next fix x assume "x \ topspace (subtopology S B)" then have h':"x \ topspace S" "x \ B" by auto have 1: "closedin S (topspace S - U k)" "topspace S - U k \ {}" using U(1) d(2) m.mtopology_openin_iff2 False by auto with h'(2) m.dist_set_closed_ge0[simplified d(2),OF 1 h'(1)] show "m.dist_set (topspace S - U k) x \ 0" by(auto simp: U(2)) qed simp thus ?thesis by simp qed qed hence f_cont: "continuous_map (subtopology S B) (subtopology (prod_topology S (powertop_real UNIV)) (f ` B)) f" using g_delta_of_subset[OF assms] by(auto simp: continuous_map_in_subtopology) have f_invcont: "continuous_map (subtopology (prod_topology S (powertop_real UNIV)) (f ` B)) (subtopology S B) fst" by(auto intro!: continuous_map_into_subtopology simp: continuous_map_subtopology_fst f_def) have homeo: "subtopology (prod_topology S (powertop_real UNIV)) (f ` B) homeomorphic_space subtopology S B" using f_inv(2) by(auto simp: homeomorphic_space_def homeomorphic_maps_def f_cont f_invcont intro!: exI[where x=f] exI[where x=fst]) show ?thesis proof(safe intro!: complete_metrizable.homeomorphic_complete_metrizable[OF _ homeo] complete_metrizable.closedin_complete_metrizable[of _ "f ` B"] complete_metrizable_prod complete_metrizable_product complete_metrizable_axioms) interpret r: polish_metric_set UNIV "dist :: real \ _" by simp interpret pd: product_complete_metric "1/2" UNIV id id "\n. UNIV" "\n. bounded_dist (dist :: real \ _)" 1 by(auto intro!: product_complete_metric_natI' simp: r.complete_metric_set_axioms) interpret bpd: complete_metric_set "topspace S \ (\\<^sub>E x\(UNIV::nat set). (UNIV::real set))" "binary_distance (topspace S) d (\\<^sub>E x\(UNIV::nat set). (UNIV::real set)) pd.product_dist" using pd.complete_metric_set_axioms by(auto intro!: binary_distance_complete d(1)) have "closedin bpd.mtopology (f ` B)" proof - { fix a b and zn :: "nat \ _" assume h':"zn \ UNIV \ f ` B" "m.converge_to_inS (\n. fst (zn n)) a" "\i. r.converge_to_inS (\n. snd (zn n) i) (b i)" then obtain xn where xn: "\n. xn n \ B" "\n. zn n = f (xn n)" by (metis PiE UNIV_I f_inv(2) imageE) have h: "m.converge_to_inS xn a" "\i. r.converge_to_inS (\n. 1 / m.dist_set (topspace S - U i) (xn n)) (b i)" proof - { fix i have "(\n. snd (zn n) i) = (\n. 1 / m.dist_set (topspace S - U i) (xn n))" by standard (simp add: xn(2) f_def) } thus "m.converge_to_inS xn a" "\i. r.converge_to_inS (\n. 1 / m.dist_set (topspace S - U i) (xn n)) (b i)" using h' by(auto simp: xn(2) f_def) qed have conv1: "r.converge_to_inS (\n. m.dist_set (topspace S - U i) (xn n)) (m.dist_set (topspace S - U i) a)" for i using m.dist_set_continuous h(1) by(simp add: metric_set_continuous_map_eq'[OF m.metric_set_axioms r.metric_set_axioms,simplified euclidean_mtopology]) have dista_n0:"m.dist_set (topspace S - U i) a \ 0" if "U i \ topspace S" for i proof(rule LIMSEQ_inverse_not0[OF _ conv1[simplified converge_to_def_set[symmetric]] h(2)[simplified converge_to_def_set[symmetric]]]) fix n have "0 < m.dist_set (topspace S - U i) (xn n)" using xn(1) U(1)[of i] by(auto intro!: m.dist_set_closed_ge0 simp: U(2) d(2) in_mono openin_subset) (use openin_subset that in blast)+ thus "m.dist_set (topspace S - U i) (xn n) \ 0" by simp qed from tendsto_inverse_real[OF conv1[simplified converge_to_def_set[symmetric]] this] have conv1':"r.converge_to_inS (\n. 1 / m.dist_set (topspace S - U i) (xn n)) (1 / m.dist_set (topspace S - U i) a)" if "U i \ topspace S" for i by(simp add: that converge_to_def_set) have "a \ U n" for n proof(cases "U n = topspace S") case True then show ?thesis using h'(2) by(auto simp: m.converge_to_inS_def) next case False with m.dist_set_nzeroD(2)[OF dista_n0[OF this]] dista_n0 show ?thesis by fastforce qed hence "a \ B" by(auto simp: U(2)) moreover have "b n = 1 / m.dist_set (topspace S - (U n)) a" for n proof(cases "U n = topspace S") case True then show ?thesis using h(2)[of n,simplified converge_to_def_set[symmetric]] by (simp add: LIMSEQ_const_iff) next case False from conv1'[OF this] h(2)[of n] show ?thesis by(simp add: r.converge_to_inS_unique) qed ultimately have "(a, b) \ f ` B" by(auto simp: f_def image_def) } thus ?thesis unfolding bpd.mtopology_closedin_iff binary_distance_converge_to_inS_iff'[OF m.metric_set_axioms pd.metric_set_axioms] using pd.converge_to_iff[simplified r.bounded_dist_converge_to_inS_iff[symmetric]] g_delta_of_subset[OF assms] f_def by auto qed thus "closedin (prod_topology S (powertop_real UNIV)) (f ` B)" by(simp only: binary_distance_mtopology[OF m.metric_set_axioms pd.metric_set_axioms] pd.product_dist_mtopology[symmetric] r.bounded_dist_generate_same_topology[symmetric] euclidean_mtopology d(2)) qed simp_all qed qed corollary(in complete_metrizable) openin_complete_metrizable: assumes "openin S u" shows "complete_metrizable (subtopology S u)" using assms by(auto intro!: g_delta_of_complete_metrizable ) subsection \ Polish Spaces \ locale polish_topology = complete_metrizable + assumes S_separable:"separable S" begin lemma S_second_countable: "second_countable S" by(rule second_countable_if_separable[OF S_separable]) lemma closedin_polish: assumes "closedin S A" shows "polish_topology (subtopology S A)" by (simp add: S_second_countable assms closedin_complete_metrizable polish_topology_axioms_def polish_topology_def second_countable_subtopology separable_if_second_countable) lemma g_delta_of_polish: assumes "g_delta_of S A" shows "polish_topology (subtopology S A)" by(simp add: polish_topology_def g_delta_of_complete_metrizable[OF assms] polish_topology_axioms_def S_second_countable second_countable_subtopology separable_if_second_countable) corollary openin_polish: assumes "openin S A" shows "polish_topology (subtopology S A)" by (simp add: assms g_delta_of_polish) lemma homeomorphic_polish_topology: assumes "S homeomorphic_space S'" shows "polish_topology S'" by(simp add: polish_topology_def homeomorphic_complete_metrizable[OF assms] homeomorphic_separable[OF S_separable assms] polish_topology_axioms_def) end lemma polish_topology_def2: "polish_topology S \ (\\. polish_metric_set (topspace S) \ \ S = metric_set.mtopology (topspace S) \)" by (metis complete_metric_set.axioms(1) complete_metrizable_def metric_set.separable_iff_topological_separable polish_metric_set.axioms(1) polish_metric_set.axioms(2) polish_metric_set.intro polish_topology_axioms_def polish_topology_def) lemma(in polish_topology) polish_metric: obtains d where "polish_metric_set (topspace S) d" and "S = metric_set.mtopology (topspace S) d" using polish_topology_axioms by(auto simp: polish_topology_def2) lemma(in polish_topology) bounded_polish_metric: obtains d where "polish_metric_set (topspace S) d" and "S = metric_set.mtopology (topspace S) d" and "\x y. d x y < 1" proof - obtain d where d:"polish_metric_set (topspace S) d" "S = metric_set.mtopology (topspace S) d" by(rule polish_metric) interpret d: polish_metric_set "topspace S" d by fact have "\d'. polish_metric_set (topspace S) d' \ S = metric_set.mtopology (topspace S) d' \ (\x y. d' x y < 1)" using d by(auto intro!: exI[where x="bounded_dist d"] polish_metric_set.bounded_dist_polish simp:d.bounded_dist_generate_same_topology d.bounded_dist_dist) with that show ?thesis by auto qed sublocale polish_metric_set \ polish_topology mtopology using mtopology_topspace by(auto simp: polish_topology_def2 polish_metric_set_axioms intro!: exI[where x=dist]) lemma polish_topology_euclidean[simp]: "polish_topology (euclidean :: ('a :: polish_space) topology)" using polish_class_polish_set by(auto simp: polish_topology_def2 intro!: exI[where x=dist]) (use open_openin open_openin_set topology_eq in blast) lemma polish_topology_countable[simp]: "polish_topology (euclidean :: 'a :: {countable,discrete_topology} topology)" proof - interpret polish_metric_set "UNIV :: 'a set" "discrete_dist UNIV" by(simp add: discrete_dist_polish_iff) show ?thesis unfolding polish_topology_def2 by(auto intro!: exI[where x="discrete_dist UNIV"] simp: topology_eq polish_metric_set_axioms discrete_dist_topology[of "UNIV :: 'a set"] discrete_topology_class.open_discrete) qed lemma polish_topology_prod: assumes "polish_topology S" and "polish_topology S'" shows "polish_topology (prod_topology S S')" proof - obtain \ \' where hr: "polish_metric_set (topspace S) \" "S = metric_set.mtopology (topspace S) \" "polish_metric_set (topspace S') \'" "S' = metric_set.mtopology (topspace S') \'" using assms by(auto simp: polish_topology_def2) interpret m1:polish_metric_set "topspace S" \ by fact interpret m2:polish_metric_set "topspace S'" \' by fact interpret m: polish_metric_set "topspace S \ topspace S'" "binary_distance (topspace S) \ (topspace S') \'" by(auto intro!: binary_distance_polish simp: m1.polish_metric_set_axioms m2.polish_metric_set_axioms) show ?thesis unfolding polish_topology_def2 using binary_distance_mtopology[OF m1.metric_set_axioms m2.metric_set_axioms,simplified space_pair_measure[symmetric]] hr(2,4) by(auto intro!: exI[where x="binary_distance (topspace S) \ (topspace S') \'"] m.polish_metric_set_axioms) qed lemma polish_topology_product: assumes "countable I" and "\i. i \ I \ polish_topology (S i)" shows "polish_topology (product_topology S I)" proof - obtain \ where hr: "\i. i \ I \ polish_metric_set (topspace (S i)) (\ i)" "\i. i \ I \ S i = metric_set.mtopology (topspace (S i)) (\ i)" using assms(2) by(auto simp: polish_topology_def2) metis define \' where "\' \ (\i x y. if i \ I then bounded_dist (\ i) x y else 0)" interpret pd: product_polish_metric "1/2" I "to_nat_on I" "from_nat_into I" "\i. topspace (S i)" \' 1 using assms hr by(auto intro!: product_polish_metricI' simp: \'_def) have "product_topology S I = product_topology (\i. metric_set.mtopology (topspace (S i)) (\ i)) I" by(auto intro!: product_topology_cong hr(2)) also have "... = product_topology (\i. metric_set.mtopology (topspace (S i)) (\' i)) I" by(auto intro!: product_topology_cong simp: \'_def) (use hr(1) metric_set.bounded_dist_generate_same_topology polish_metric_set.axioms(2) separable_metric_set_def in blast) also have "... = pd.mtopology" by(rule pd.product_dist_mtopology) finally have "product_topology S I = pd.mtopology" . show ?thesis unfolding polish_topology_def2 by(auto intro!: exI[where x="pd.product_dist"] simp: pd.polish_metric_set_axioms) fact qed lemma polish_topology_closedin_polish: assumes "polish_topology S" and "closedin S U" shows "polish_topology (subtopology S U)" proof - obtain \ where *: "polish_metric_set (topspace S) \" "S = metric_set.mtopology (topspace S) \" using assms by(auto simp: polish_topology_def2) interpret m:polish_metric_set "topspace S" \ by fact interpret m':polish_metric_set U "submetric U \" using m.submetric_complete_iff[OF closedin_subset[OF assms(2)]] m.submetric_separable[OF closedin_subset[OF assms(2)]] assms(2) * by(simp add: polish_metric_set_def) have "subtopology S U = m'.mtopology" using m.submetric_subtopology[OF closedin_subset[OF assms(2)]] * by simp thus ?thesis using m'.mtopology_topspace by(auto simp: polish_topology_def2 m'.polish_metric_set_axioms intro!: exI[where x="submetric U \"]) qed subsection \ Compact Metrizable Spaces \ locale compact_metrizable = metrizable + assumes compact: "compact_space S" begin sublocale polish_topology proof - obtain d where "compact_metric_set (topspace S) d" "metric_set.mtopology (topspace S) d = S" using metric compact by(auto simp: compact_metric_set_def compact_metric_set_axioms.intro) then interpret m: polish_metric_set "topspace S" d by(simp add: compact_metric_set.polish) show "polish_topology S" using \m.mtopology = S\ m.polish_topology_axioms by simp qed lemma compact_metric: obtains d where "compact_metric_set (topspace S) d" "metric_set.mtopology (topspace S) d = S" by (metis metric compact compact_metric_set.intro compact_metric_set_axioms.intro) end subsection \Continuous Embddings\ abbreviation Hilbert_cube_as_topology :: "(nat \ real) topology" where "Hilbert_cube_as_topology \ (product_topology (\n. top_of_set {0..1}) UNIV)" lemma topspace_Hilbert_cube: "topspace Hilbert_cube_as_topology = (\\<^sub>E x\UNIV. {0..1})" by simp lemma Hilbert_cube_Polish_topology: "polish_topology Hilbert_cube_as_topology" by(auto intro!: polish_topology_closedin_polish polish_topology_product) abbreviation Cantor_space_as_topology :: "(nat \ real) topology" where "Cantor_space_as_topology \ (product_topology (\n. top_of_set {0,1}) UNIV)" lemma topspace_Cantor_space: "topspace Cantor_space_as_topology = (\\<^sub>E x\UNIV. {0,1})" by simp lemma Cantor_space_Polish_topology: "polish_topology Cantor_space_as_topology" by(auto intro!: polish_topology_closedin_polish polish_topology_product) text \ Proposition 2.2.3 in \cite{borelsets} \ lemma continuous_map_metrizable_extension: assumes "A \ topspace W" "metrizable W" "complete_metrizable Z" "continuous_map (subtopology W A) Z f" shows "\h gd. g_delta_of W gd \ (\a\A. f a = h a) \ A \ gd \ continuous_map (subtopology W gd) Z h" proof - obtain dz where hdz: "complete_metric_set (topspace Z) dz" "metric_set.mtopology (topspace Z) dz = Z" "\x y. dz x y < 1" using complete_metrizable.bounded_cmetric[OF assms(3)] by auto interpret dz: complete_metric_set "topspace Z" dz by fact obtain dw where hdw: "metric_set (topspace W) dw" "metric_set.mtopology (topspace W) dw = W" using metrizable.metric[OF assms(2)] by auto interpret dw: metric_set "topspace W" dw by fact interpret subd: metric_set A "submetric A dw" using assms by(auto intro!: dw.submetric_metric_set) have "subd.mtopology = subtopology W A" using assms(1) dw.submetric_subtopology hdw(2) by auto let ?oscf = "dz.osc_on A W f" define gd where "gd \ {x\W closure_of A. ?oscf x = 0}" have g_delta: "g_delta_of W gd" proof - have *:"{x\W closure_of A. ?oscf x < t} = \ {V \ (W closure_of A)| V. openin W V \ dz.diam (f ` (A \ V)) < t}" for t by(auto simp: dz.osc_on_less_iff) have 1:"gd = \ {{x\W closure_of A. ?oscf x < 1 / real n}|n. n \ {0<..}}" proof - have "x \ gd" if h:"\n. n \ {0<..} \ x \ {x\W closure_of A. ?oscf x < 1 / real n}" for x proof - have "?oscf x < \" if he:"\>0" for \ proof - obtain n where "1 / real (Suc n) < \" by (meson enn2real_le_iff enn2real_positive_iff ennreal_less_top ennreal_less_zero_iff he linorder_not_le nat_approx_posE order_le_less_trans) thus ?thesis using h[of "Suc n"] by auto qed hence "?oscf x = 0" using not_gr_zero by blast thus ?thesis using that by(auto simp: gd_def) qed thus ?thesis by (auto simp: gd_def) qed also have "... = \ {\ {V \ (W closure_of A)| V. openin W V \ dz.diam (f ` (A \ V)) < 1 / real n}|n. n \ {0<..}}" using * by auto also have "... = W closure_of A \ \ {\ {V. openin W V \ dz.diam (f ` (A \ V)) < 1 / real n}|n. n \ {0<..}}" by blast also have "g_delta_of W ..." proof - have "{\ {V. openin W V \ dz.diam (f ` (A \ V)) < ennreal (1 / real n)} | n. 0 < n} = (\n. \ {V. openin W V \ dz.diam (f ` (A \ V)) < ennreal (1 / real n)}) ` {0<..}" by auto also have "countable ..." by auto finally show ?thesis by(auto intro!: dw.g_delta_of_closed[simplified hdw(2),of "W closure_of A"] g_delta_of_inter[OF _ g_delta_ofI[of "{\ {V. openin W V \ dz.diam (f ` (A \ V)) < ennreal (1 / real n)} | n. n \ {0<..}}" _ "\ {\ {V. openin W V \ dz.diam (f ` (A \ V)) < 1 / real n}|n. 0 < n}"]] ) qed finally show ?thesis . qed have oscf0: "?oscf a = 0" if "a \ A" for a using assms that by(auto intro!: osc_on_inA_0[OF dw.metric_set_axioms dz.metric_set_axioms,simplified \dz.mtopology = Z\ \dw.mtopology = W\] simp: le_iff_inf) hence A_subst_of_gd: "A \ gd" using closure_of_subset[OF assms(1)] by(auto simp add: gd_def) define h where "h x \ let xn = (SOME an. an \ UNIV \ A \ dw.converge_to_inS an x) in dz.the_limit_of (\n. f (xn n))" for x have h_extends:"f a = h a" if "a \ A" for a proof - obtain an where han: "an \ UNIV \ A" "dw.converge_to_inS an a" using dw.closure_of_mtopology_an[of a A] A_subst_of_gd \a \ A\ gd_def hdw(2) by auto show ?thesis unfolding h_def Let_def proof(rule someI2[of _ an "\t. f a = dz.the_limit_of (\n. f (t n))"]) fix bn assume h:"bn \ UNIV \ A \ dw.converge_to_inS bn a" hence "subd.converge_to_inS bn a" using assms(1) dw.convergent_insubmetric that by fastforce hence "dz.converge_to_inS (\n. f (bn n)) (f a)" using metric_set_continuous_map_eq'[OF subd.metric_set_axioms dz.metric_set_axioms,of f,simplified \subd.mtopology = subtopology W A\ \dz.mtopology = Z\ assms(4)] by auto thus "f a = dz.the_limit_of (\n. f (bn n))" by(simp add: dz.the_limit_of_eq) qed(use han in auto) qed have "gd \ topspace W" by(simp add: gd_def in_closure_of) then interpret subd_on_gd: metric_set gd "submetric gd dw" by(auto intro!: dw.submetric_metric_set) have "subtopology W gd = subd_on_gd.mtopology" using \gd \ topspace W\ dw.submetric_subtopology hdw(2) by auto have Cauchyf:"dz.Cauchy_inS (\n. f (an n))" if "subd.Cauchy_inS an" "dw.converge_to_inS an a" "?oscf a = 0" for an a proof - have "{dz.diam (f ` (A \ U)) |U. a \ U \ openin W U} = (\U. dz.diam (f ` (A \ U))) ` {U. a \ U \ openin W U}" by auto hence "(\i\{U. a \ U \ openin W U}. dz.diam (f ` (A \ i))) = \" using that(3) by(auto simp: dz.osc_on_def bot_ennreal) from this[simplified INF_eq_bot_iff] have "\\. \ > 0 \ \u\{U. a \ U \ openin W U}. dz.diam (f ` (A \ u)) < \" by(simp add: bot_ennreal) hence he:"\\. \ > 0 \ \u\{U. a \ U \ openin W U}. dz.diam (f ` (A \ u)) < ennreal \" by auto show ?thesis unfolding dz.Cauchy_inS_def proof safe show "\x. f (an x) \ topspace Z" using assms(1,4) subd.Cauchy_inS_dest1[OF that(1)] by(auto simp: continuous_map_def) next fix \ assume "(0 :: real) < \" from he[OF this] obtain U where hu:"a \ U" "openin W U" "dz.diam (f ` (A \ U)) < ennreal \" by auto then obtain e where he:"e > 0" "a \ dw.open_ball a e" "dw.open_ball a e \ U" by (metis \dw.converge_to_inS an a\ dw.metric_set_axioms dw.mtopology_openin_iff dw.open_ball_ina hdw(2) metric_set.converge_to_inS_def2') then obtain N where "\n. n \ N \ an n \ dw.open_ball a e" using \dw.converge_to_inS an a\ dw.converge_to_inS_def2' by blast hence hn: "\n. n \ N \ an n \ A \ U" using he(3) that(1) by(auto simp: subd.Cauchy_inS_def) show "\N. \n\N. \m\N. dz (f (an n)) (f (an m)) < \" proof(safe intro!: exI[where x=N]) fix n m assume "N \ n" "N \ m" then have "an n \ A \ U" "an m \ A \ U" using hn by auto hence "f (an n) \ f ` (A \ U)" "f (an m) \ f ` (A \ U)" by auto then have "ennreal (dz (f (an n)) (f (an m))) \ dz.diam (f ` (A \ U))" using assms(4) subd.mtopology_topspace by(auto intro!: dz.diam_is_sup simp:\subd.mtopology = subtopology W A\ continuous_map_def) also have "... < ennreal \" by fact finally show "dz (f (an n)) (f (an m)) < \" using dz.dist_geq0 by (simp add: ennreal_less_iff) qed qed qed have "continuous_map (subtopology W gd) Z h" proof - have h_image:"h \ gd \ topspace Z" proof fix x assume "x \ gd" then obtain xn where hxn: "xn \ UNIV \ A" "dw.converge_to_inS xn x" using dw.closure_of_mtopology_an[of x A] by(auto simp: gd_def hdw(2)) show "h x \ topspace Z" unfolding h_def Let_def proof(rule someI2[of _ xn "\t. dz.the_limit_of (\n. f (t n)) \ topspace Z"]) fix an assume "an \ subd.sequence \ dw.converge_to_inS an x" then have h:"an \ subd.sequence" "dw.converge_to_inS an x" by auto then have "dz.Cauchy_inS (\n. f (an n))" using \x \ gd\ by(auto intro!: Cauchyf[OF dw.Cauchy_insub_Cauchy_inverse[OF assms(1) h(1) dw.Cauchy_if_convergent_inS] h(2)] simp: gd_def dw.convergent_inS_def) thus "dz.the_limit_of (\n. f (an n)) \ topspace Z" by(simp add: dz.convergence dz.the_limit_of_inS) qed(use hxn in auto) qed show ?thesis unfolding metric_set_continuous_map_eq[OF subd_on_gd.metric_set_axioms dz.metric_set_axioms,simplified \subtopology W gd = subd_on_gd.mtopology\[symmetric] \dz.mtopology = Z\] proof safe fix x and \ :: real assume "x \ gd" "0 < \" then have "?oscf x < \ / 3" by(auto simp: gd_def) then obtain u where hu: "openin W u" "x \ u" "dz.diam (f ` (A \ u)) < \ / 3" by(auto simp: dz.osc_on_def Inf_less_iff) hence "openin subd_on_gd.mtopology (u \ gd)" by(auto simp : \subtopology W gd = subd_on_gd.mtopology\[symmetric] openin_subtopology) then obtain \ where hd: "\ > 0" "subd_on_gd.open_ball x \ \ u \ gd" "x \ subd_on_gd.open_ball x \" by (metis Int_iff \x \ gd\ hu(2) subd_on_gd.mtopology_openin_iff subd_on_gd.open_ball_ina) show "\\>0. \y\gd. submetric gd dw x y < \ \ dz (h x) (h y) < \" proof(safe intro!: exI[where x=\] \\ > 0\) fix y assume h':"y \ gd" "submetric gd dw x y < \" then have "y \ subd_on_gd.open_ball x \" by(simp add: \x \ gd\ subd_on_gd.open_ball_def) then obtain \y where hdy: "\y > 0" "subd_on_gd.open_ball y \y \ subd_on_gd.open_ball x \" "y \ subd_on_gd.open_ball y \y" using h'(1) subd_on_gd.mtopology_open_ball_in' subd_on_gd.open_ball_ina by blast obtain xn' yn' where hxyn':"xn' \ UNIV \ A" "dw.converge_to_inS xn' x" "yn' \ UNIV \ A" "dw.converge_to_inS yn' y" using dw.closure_of_mtopology_an[of _ A] \y \ gd\ \x \ gd\ by(simp add: gd_def hdw(2)) metis show "dz (h x) (h y) < \" proof - { fix xn yn assume hxyn:"xn \ subd.sequence" "dw.converge_to_inS xn x" "yn \ subd.sequence" "dw.converge_to_inS yn y" then have Cauchyxyn: "dz.Cauchy_inS (\n. f (xn n))" "dz.Cauchy_inS (\n. f (yn n))" using Cauchyf[OF dw.Cauchy_insub_Cauchy_inverse[OF assms(1) hxyn(1) dw.Cauchy_if_convergent_inS] hxyn(2)] Cauchyf[OF dw.Cauchy_insub_Cauchy_inverse[OF assms(1) hxyn(3) dw.Cauchy_if_convergent_inS] hxyn(4)] \x \ gd\ \y \ gd\ by(auto simp: gd_def dw.convergent_inS_def) have convxyn:"subd_on_gd.converge_to_inS xn x" "subd_on_gd.converge_to_inS yn y" using hxyn \x \ gd\ \y \ gd\ \A \ gd\ by(auto intro!: dw.convergent_insubmetric \gd \ topspace W\) then obtain Nx Ny where hnxy: "\n. n \ Nx \ xn n \ subd_on_gd.open_ball x \" "\n. n \ Ny \ yn n \ subd_on_gd.open_ball y \y" using hd(1) hdy(1) subd_on_gd.converge_to_inS_def2' by blast have "0 < \ / 3" using \0 < \\ by simp obtain Nfx Nfy where hnfxy: "\n. n \ Nfx \ dz (f (xn n)) (dz.the_limit_of (\n. f (xn n))) < \ / 3" "\n. n \ Nfy \ dz (f (yn n)) (dz.the_limit_of (\n. f (yn n))) < \ / 3" using dz.the_limit_if_converge[OF dz.convergence[OF Cauchyxyn(1)]] dz.the_limit_if_converge[OF dz.convergence[OF Cauchyxyn(2)]] by(auto simp: dz.converge_to_inS_def2) (meson \0 < \ / 3\ less_divide_eq_numeral1(1)) define N where "N \ Max {Nx,Ny,Nfx,Nfy}" have N:"N \ Nx" "N \ Ny" "N \ Nfx" "N \ Nfy" by(simp_all add: N_def) have "dz (dz.the_limit_of (\n. f (xn n))) (dz.the_limit_of (\n. f (yn n))) < \" (is "?lhs < _") proof - have "?lhs \ dz (dz.the_limit_of (\n. f (xn n))) (f (xn N)) + dz (f (xn N)) (dz.the_limit_of (\n. f (yn n)))" using dz.dist_tr[OF dz.the_limit_of_inS[OF dz.convergence[OF Cauchyxyn(1)]] _ dz.the_limit_of_inS[OF dz.convergence[OF Cauchyxyn(2)]],of \f (xn N)\] dz.Cauchy_inS_dest1[OF Cauchyxyn(1)] by simp also have "... \ dz (dz.the_limit_of (\n. f (xn n))) (f (xn N)) + dz (f (xn N)) (f (yn N)) + dz (f (yn N)) (dz.the_limit_of (\n. f (yn n)))" using dz.dist_tr[OF _ _ dz.the_limit_of_inS[OF dz.convergence[OF Cauchyxyn(2)]],of "f (xn N)" "f (yn N)"] dz.Cauchy_inS_dest1[OF Cauchyxyn(1)] dz.Cauchy_inS_dest1[OF Cauchyxyn(2)] by simp also have "... < \ / 3 + dz (f (xn N)) (f (yn N)) + \ / 3" using hnfxy[of N] N by(simp add: dz.dist_sym[of "dz.the_limit_of (\n. f (xn n))"]) also have "... < \" proof - have "xn N \ A \ u" "yn N \ A \ u" using hdy(2) hd(2) hnxy[of N] N hxyn(1,3) by auto hence "ennreal (dz (f (xn N)) (f (yn N))) \ dz.diam (f ` (A \ u))" by(auto intro!: dz.diam_is_sup dz.Cauchy_inS_dest1[OF Cauchyxyn(1)] dz.Cauchy_inS_dest1[OF Cauchyxyn(2)]) also have "... < ennreal (\ / 3)" by fact finally have "dz (f (xn N)) (f (yn N)) < \ / 3" using dz.dist_geq0 ennreal_less_iff by blast thus ?thesis by simp qed finally show ?thesis . qed } note h = this show ?thesis apply(simp only: h_def[of x] Let_def) apply(rule someI2[of "\k. k \ subd.sequence \ dw.converge_to_inS k x" xn',OF conjI[OF hxyn'(1,2)]]) apply(simp only: h_def[of y] Let_def) apply(rule someI2[of "\k. k \ subd.sequence \ dw.converge_to_inS k y" yn',OF conjI[OF hxyn'(3,4)]]) using h by auto qed qed qed(use h_image in auto) qed with h_extends g_delta A_subst_of_gd show ?thesis by auto qed lemma Lavrentiev_theorem: assumes "complete_metrizable X" "complete_metrizable Y" "A \ topspace X" "B \ topspace Y" "homeomorphic_map (subtopology X A) (subtopology Y B) f" shows "\h gda gdb. g_delta_of X gda \ g_delta_of Y gdb \ A \ gda \ B \ gdb \ (\x\A. f x = h x) \ homeomorphic_map (subtopology X gda) (subtopology Y gdb) h" proof - interpret cmx: complete_metrizable X by fact interpret cmy: complete_metrizable Y by fact interpret mxy: metrizable "prod_topology X Y" by(auto intro!: metrizable_prod cmx.metrizable cmy.metrizable) obtain g where "homeomorphic_maps (subtopology X A) (subtopology Y B) f g" using assms(5) homeomorphic_map_maps by blast then have hfg: "continuous_map (subtopology X A) (subtopology Y B) f" "continuous_map (subtopology Y B) (subtopology X A) g" "\x. x \ A \ g (f x) = x" "\y. y \ B \ f (g y) = y" using assms(3,4) by(auto simp: homeomorphic_maps_def) obtain f' g' gda gdb where h: "g_delta_of X gda" "\a. a \ A \ f a = f' a" "A \ gda" "continuous_map (subtopology X gda) Y f'" "g_delta_of Y gdb" "\b. b \ B \ g b = g' b" "B \ gdb" "continuous_map (subtopology Y gdb) X g'" using continuous_map_metrizable_extension[OF assms(3) cmx.metrizable assms(2) continuous_map_into_fulltopology[OF hfg(1)]] continuous_map_metrizable_extension[OF assms(4) cmy.metrizable assms(1) continuous_map_into_fulltopology[OF hfg(2)]] by auto define H where "H \ SIGMA x:gda. {f' x}" have Heq:"H = {(x,y). x \ gda \ y \ topspace Y \ y = f' x}" using g_delta_of_subset[OF h(1)] h(4) by(auto simp: continuous_map_def H_def) define K where Keq:"K = {(x,y). x \ topspace X \ y \ gdb \ x = g' y}" define A' where "A' \ fst ` (H \ K)" define B' where "B' \ snd ` (H \ K)" - have A'eq: "A' = {x \ gda. (x, f' x) \ K}" - using h(4) by(auto simp: A'_def Keq Heq image_def continuous_map_def) (metis (mono_tags, lifting) IntI case_prod_conv fst_conv mem_Collect_eq) + have A'eq: "A' = {x \ gda. (x, f' x) \ K}" + using h(4) + by (auto simp: A'_def Keq Heq image_def continuous_map_def Pi_def) + (metis (mono_tags, lifting) IntI case_prod_conv fst_conv mem_Collect_eq) have B'eq: "B' = {y \ gdb. (g' y, y) \ H}" - using h(8) by(auto simp: B'_def Keq Heq image_def continuous_map_def) (metis (mono_tags, lifting) IntI case_prod_conv snd_conv mem_Collect_eq) + using h(8) + by (auto simp: B'_def Keq Heq image_def continuous_map_def Pi_def) + (metis (mono_tags, lifting) IntI case_prod_conv snd_conv mem_Collect_eq) have A'_gd: "g_delta_of X A'" proof - have K_gd:"g_delta_of (prod_topology X Y) K" proof - have "closedin (subtopology (prod_topology X Y) (topspace X \ gdb)) K" proof - have "K = ((\y. (g' y, y)) ` topspace (subtopology Y gdb))" using h(8) g_delta_of_subset[OF h(5)] by(auto simp add: Keq continuous_map_def) thus ?thesis using cmx.Hausdorff continuous_map_imp_closed_graph'[OF h(8)] by(auto simp: prod_topology_subtopology(2)) qed then obtain T where hT:"closedin (prod_topology X Y) T" "K = T \ (topspace X \ gdb)" using closedin_subtopology by metis thus ?thesis by(auto intro!: g_delta_of_inter g_delta_of_prod simp: h(5) mxy.g_delta_of_closedin) qed have "A' = ((\x. (x,f' x)) -` K \ topspace (subtopology X gda))" by(auto simp add: A'eq Keq) also have "g_delta_of X ..." by(rule g_delta_of_subtopology_inverse[OF g_delta_of_continuous_map[OF _ K_gd] h(1)]) (auto intro!: continuous_map_pairedI h(4)) finally show ?thesis . qed have A_subst_A': "A \ A'" proof fix a assume 0:"a \ A" then have "f' a = f a" "f' a \ B" using h(2)[OF 0,symmetric] hfg(1) assms(3) by(auto simp: continuous_map_def) thus "a \ A'" using h(6)[OF \f' a \ B\,symmetric] hfg(3)[OF 0] 0 assms(3) h(3) h(7) by(auto simp: A'eq Keq) qed have B'_gd: "g_delta_of Y B'" proof - have H_gd:"g_delta_of (prod_topology X Y) H" proof - have "closedin (subtopology (prod_topology X Y) (gda \ topspace Y)) H" proof - have "H = ((\y. (y, f' y)) ` topspace (subtopology X gda))" using h(4) g_delta_of_subset[OF h(1)] by(auto simp add: Heq continuous_map_def) thus ?thesis using cmy.Hausdorff continuous_map_imp_closed_graph[OF h(4)] by(auto simp: prod_topology_subtopology(1)) qed then obtain T where hT:"closedin (prod_topology X Y) T" "H = T \ (gda \ topspace Y)" using closedin_subtopology by metis thus ?thesis by(auto intro!: g_delta_of_inter g_delta_of_prod simp: h(1) mxy.g_delta_of_closedin) qed have "B' = ((\x. (g' x,x)) -` H \ topspace (subtopology Y gdb))" by(auto simp add: B'eq Heq) also have "g_delta_of Y ..." by(rule g_delta_of_subtopology_inverse[OF g_delta_of_continuous_map[OF _ H_gd] h(5)]) (auto intro!: continuous_map_pairedI h(8)) finally show ?thesis . qed have B_subst_B': "B \ B'" proof fix b assume 0:"b \ B" then have "g' b = g b" "g' b \ A" using h(6)[OF 0,symmetric] hfg(2) assms(4) by(auto simp: continuous_map_def) thus "b \ B'" using h(2)[OF \g' b \ A\,symmetric] hfg(4)[OF 0] 0 assms(4) h(3) h(7) by(auto simp: B'eq Heq) qed have "homeomorphic_map (subtopology X A') (subtopology Y B') f'" proof(rule homeomorphic_maps_imp_map[where g=g']) show "homeomorphic_maps (subtopology X A') (subtopology Y B') f' g'" unfolding homeomorphic_maps_def proof safe show "continuous_map (subtopology X A') (subtopology Y B') f'" using g_delta_of_subset[OF h(5)] by(auto intro!: continuous_map_into_subtopology continuous_map_from_subtopology_mono[OF h(4)] simp: A'eq B'eq Heq Keq) next show "continuous_map (subtopology Y B') (subtopology X A') g'" using g_delta_of_subset[OF h(1)] by(auto intro!: continuous_map_into_subtopology continuous_map_from_subtopology_mono[OF h(8)] simp: A'eq B'eq Heq Keq) qed(auto simp: A'eq B'eq Keq Heq) qed with A'_gd B'_gd A_subst_A' B_subst_B' h(2) show ?thesis by auto qed corollary(in complete_metrizable) complete_metrizable_subtopology_is_g_delta: assumes "A \ topspace S" "complete_metrizable (subtopology S A)" shows "g_delta_of S A" proof - obtain h gda gdb where h: "g_delta_of S gda" "g_delta_of (subtopology S A) gdb" "A \ gda" "A \ gdb" "\x\A. x = h x" "homeomorphic_map (subtopology (subtopology S A) gdb) (subtopology S gda) h" using Lavrentiev_theorem[OF assms(2) complete_metrizable_axioms _ assms(1),of A id] assms(1) by simp (metis subtopology_topspace topspace_subtopology_subset) have "gdb = A" using g_delta_of_subset[OF h(2)] h(4) assms(1) by auto hence "homeomorphic_map (subtopology S A) (subtopology S gda) h" using h(6) by (simp add: subtopology_subtopology) hence "homeomorphic_map (subtopology S A) (subtopology S gda) id" by(rule homeomorphic_map_eq) (use assms(1) h(5) in auto) hence "subtopology S A = subtopology S gda" by simp hence "A = gda" by (metis assms(1) g_delta_of_subset h(1) topspace_subtopology_subset) thus ?thesis by(simp add: h(1)) qed corollary(in complete_metrizable) subtopology_complete_metrizable_iff: assumes "A \ topspace S" shows "complete_metrizable (subtopology S A) \ g_delta_of S A" by(auto simp : g_delta_of_complete_metrizable complete_metrizable_subtopology_is_g_delta[OF assms]) corollary complete_metrizable_homeo_image_g_delta: assumes "complete_metrizable X" "complete_metrizable Y" "B \ topspace Y" "X homeomorphic_space subtopology Y B" shows "g_delta_of Y B" proof - obtain f where f:"homeomorphic_map X (subtopology Y B) f" using assms(4) homeomorphic_space by blast obtain h gda gdb where h: "g_delta_of X gda" "g_delta_of Y gdb" "topspace X \ gda" "B \ gdb" "\x\topspace X. f x = h x" "homeomorphic_map (subtopology X gda) (subtopology Y gdb) h" using Lavrentiev_theorem[OF assms(1,2) subset_refl assms(3),simplified,OF f] by metis hence [simp]: "gda = topspace X" using g_delta_of_subset by blast have "homeomorphic_map X (subtopology Y gdb) f" using h(5,6) by(auto intro!: homeomorphic_map_eq[where f=h]) hence "f ` topspace X = B" "f ` topspace X = gdb" using homeomorphic_imp_surjective_map[OF f] assms(3) g_delta_of_subset[OF h(2)] h(4) homeomorphic_imp_surjective_map[OF \homeomorphic_map X (subtopology Y gdb) f\] by auto with h(2) show ?thesis by auto qed lemma(in metrizable) embedding_into_Hilbert_cube: assumes "separable S" shows "\A \ topspace Hilbert_cube_as_topology. S homeomorphic_space (subtopology Hilbert_cube_as_topology A)" proof - consider "topspace S = {}" | "topspace S \ {}" by auto then show ?thesis proof cases case 1 then show ?thesis by(auto intro!: exI[where x="{}"] simp: homeomorphic_empty_space_eq) next case S_ne:2 then obtain U where U:"countable U" "dense_of S U" "U \ {}" using assms(1) by(auto simp: separable_def dense_of_nonempty) obtain xn where xn:"\n::nat. xn n \ U" "U = range xn" by (metis U(1) U(3) from_nat_into range_from_nat_into) then have xns:"xn n \ topspace S" for n using dense_of_subset[OF U(2)] by auto obtain d where d:"metric_set (topspace S) d" "metric_set.mtopology (topspace S) d = S" "\x y. d x y < 1" using bounded_metric by auto interpret ms: metric_set "topspace S" d by fact define f where "f \ (\x n. d x (xn n))" have f_inj:"inj_on f (topspace S)" proof fix x y assume xy:"x \ topspace S" "y \ topspace S" "f x = f y" then have "\n. d x (xn n) = d y (xn n)" by(auto simp: f_def dest: fun_cong) hence d2:"d x y \ 2 * d x (xn n)" for n using ms.dist_tr[OF xy(1) _ xy(2),of "xn n",simplified ms.dist_sym[of "xn n" y]] dense_of_subset[OF U(2)] xn(1)[of n] by auto have "d x y < \" if "\ > 0" for \ proof - have "0 < \ / 2" using that by simp then obtain n where "d x (xn n) < \ / 2" using ms.dense_set_def2[of U,simplified d(2)] U(2) xy(1) xn(2) by blast with d2[of n] show ?thesis by simp qed hence "d x y = 0" using ms.dist_geq0[of x y] by (metis dual_order.irrefl order_neq_le_trans) thus "x = y" using ms.dist_0[OF xy(1,2)] by simp qed have f_img: "f ` topspace S \ topspace Hilbert_cube_as_topology" using d(3) ms.dist_geq0 by(auto simp: topspace_Hilbert_cube f_def less_le_not_le) have f_cont: "continuous_map S Hilbert_cube_as_topology f" unfolding continuous_map_componentwise_UNIV f_def continuous_map_in_subtopology proof safe show "continuous_map S euclideanreal (\x. d x (xn k))" for k using ms.dist_set_continuous[of "{xn k}"] by(simp add: d(2)) next show "d x (xn k) \ {0..1}" for x k using d(3) ms.dist_geq0 by(auto simp: less_le_not_le) qed hence f_cont': "continuous_map S (subtopology Hilbert_cube_as_topology (f ` topspace S)) f" using continuous_map_into_subtopology by blast obtain g where g: "g ` (f ` topspace S) = topspace S" "\x. x \ topspace S \ g (f x) = x" "\x. x \ f ` topspace S \ f (g x) = x" by (meson f_inj f_the_inv_into_f the_inv_into_f_eq the_inv_into_onto) have g_cont: "continuous_map (subtopology Hilbert_cube_as_topology (f ` topspace S)) S g" proof - interpret m01: polish_metric_set "{0..1::real}" "submetric {0..1} dist" by (metis closed_atLeastAtMost closed_closedin euclidean_mtopology polish_class_polish_set polish_metric_set.submetric_polish subset_UNIV) have m01_eq: "m01.mtopology = top_of_set {0..1}" by(rule submetric_of_euclidean(2)[of "{0..1::real}"]) have "submetric {0..1::real} dist x y \ 1" "submetric {0..1::real} dist x y \ 0" for x y using dist_real_def by(auto simp: submetric_def) then interpret ppm: product_polish_metric "1/2" "UNIV :: nat set" id id "\_. {0..1}" "\_. submetric {0..1::real} dist" 1 by(auto intro!: product_polish_metric_natI m01.polish_metric_set_axioms) have Hilbert_cube_eq: "ppm.mtopology = Hilbert_cube_as_topology" by(simp add: ppm.product_dist_mtopology[symmetric] m01_eq) interpret f_S: metric_set "f ` topspace S" "submetric (f ` topspace S) ppm.product_dist" using f_img by(auto intro!: ppm.submetric_metric_set) have 1:"subtopology Hilbert_cube_as_topology (f ` topspace S) = f_S.mtopology" using ppm.submetric_subtopology[of "f ` topspace S"] f_img by(simp add: Hilbert_cube_eq) have "continuous_map f_S.mtopology ms.mtopology g" unfolding metric_set_continuous_map_eq'[OF f_S.metric_set_axioms ms.metric_set_axioms] proof safe show "x \ topspace S \ g (f x) \ topspace S" for x by(simp add: g(2)) next fix yn y assume h:"f_S.converge_to_inS yn y" have "ppm.converge_to_inS yn y" using ppm.converge_to_insub_converge_to_inS[OF _ h] f_img by auto hence m01_conv:"\n. m01.converge_to_inS (\i. yn i n) (y n)" using ppm.converge_to_iff[of yn y] by(auto simp: ppm.converge_to_inS_def) have "\n. \zn. yn n = f zn \ zn \ topspace S" using h by(auto simp: f_S.converge_to_inS_def) then obtain zn where zn:"\n. f (zn n) = yn n" "\n. zn n \ topspace S" by metis obtain z where z:"f z = y" "z \ topspace S" using h by(auto simp: f_S.converge_to_inS_def) show "ms.converge_to_inS (\n. g (yn n)) (g y)" unfolding ms.converge_to_inS_def2 proof safe show "g (yn n) \ topspace S" "g y \ topspace S" for n using g(2)[of z] g(2)[of "zn n"] zn[of n] z by simp_all next fix \ :: real assume he: "0 < \" then have "0 < \ / 3" by simp then obtain m where m:"d z (xn m) < \ / 3" using ms.dense_set_def2[of U,simplified d(2)] U(2) z(2) xn(2) by blast obtain N where "\n. n \ N \ \yn n m - y m \ < \ / 3" using m01_conv[of m,simplified m01.converge_to_inS_def2] \0 < \ / 3\ by(simp only: submetric_def dist_real_def) (metis (full_types, lifting) PiE UNIV_I) hence N:"\n. n \ N \ yn n m < \ / 3 + y m" by (metis abs_diff_less_iff add.commute) have "\N. \n\N. d (zn n) z < \" proof(safe intro!: exI[where x=N]) fix n assume "N \ n" have "d (zn n) z \ f (zn n) m + d z (xn m)" using ms.dist_tr[OF zn(2)[of n] xns[of m] z(2),simplified ms.dist_sym[of "xn m" z]] by(auto simp: f_def) also have "... < \ / 3 + y m + d z (xn m)" using N[OF \N\n\] zn(1)[of n] by simp also have "... = \ / 3 + d z (xn m) + d z (xn m)" by(simp add: z(1)[symmetric] f_def) also have "... < \" using m by auto finally show "d (zn n) z < \" . qed thus "\N. \n\N. d (g (yn n)) (g y) < \" using zn(1) z(1) g(2)[OF z(2)] g(2)[OF zn(2)] by auto qed qed thus ?thesis by(simp add: d(2) 1) qed show ?thesis using f_img g(2,3) f_cont' g_cont by(auto intro!: exI[where x="f ` topspace S"] homeomorphic_maps_imp_homeomorphic_space[where f=f and g=g] simp: homeomorphic_maps_def) qed qed corollary(in complete_metrizable) embedding_into_Hilbert_cube_g_delta_of: assumes "separable S" shows "\A. g_delta_of Hilbert_cube_as_topology A \ S homeomorphic_space (subtopology Hilbert_cube_as_topology A)" proof - obtain A where h:"A \ topspace Hilbert_cube_as_topology" "S homeomorphic_space subtopology Hilbert_cube_as_topology A" using embedding_into_Hilbert_cube[OF assms(1)] by blast with complete_metrizable_homeo_image_g_delta[OF complete_metrizable_axioms polish_topology.axioms(1)[OF Hilbert_cube_Polish_topology] h(1,2)] show ?thesis by(auto intro!: exI[where x=A]) qed corollary(in polish_topology) embedding_into_Hilbert_cube_g_delta_of: "\A. g_delta_of Hilbert_cube_as_topology A \ S homeomorphic_space (subtopology Hilbert_cube_as_topology A)" by(rule embedding_into_Hilbert_cube_g_delta_of[OF S_separable]) lemma(in polish_topology) uncountable_contains_Cantor_space': assumes "uncountable (topspace S)" shows "\A\ topspace S. Cantor_space_as_topology homeomorphic_space (subtopology S A)" proof - obtain U P where up: "countable U" "openin S U" "perfect_set S P""U \ P = topspace S" "U \ P = {}" "\a. a \ {} \ openin (subtopology S P) a \ uncountable a" using Cantor_Bendixon[OF S_second_countable] by auto have P: "closedin S P" "P \ topspace S" "uncountable P" using countable_Un_iff[of U P] up(1) assms up(4) by(simp_all add: perfect_setD[OF up(3)]) then interpret pp: polish_topology "subtopology S P" by(simp add: closedin_polish) have Ptop: "topspace (subtopology S P) = P" using P(2) by auto obtain U where U: "countable U" "dense_of (subtopology S P) U" using pp.S_separable separable_def by blast with uncountable_infinite[OF P(3)] pp.dense_of_infinite P(2) have "infinite U" by (metis topspace_subtopology_subset) obtain d where "complete_metric_set P d" and d:"metric_set.mtopology P d = subtopology S P" using pp.cmetric by(simp only: Ptop,auto) interpret md: complete_metric_set P d by fact define xn where "xn \ from_nat_into U" have xn: "bij_betw xn UNIV U" "\n m. n \ m \ xn n \ xn m" "\n. xn n \ U" "\n. xn n \ P" "md.dense_set (range xn)" using bij_betw_from_nat_into[OF U(1) \infinite U\] dense_of_subset[OF U(2)] d U(2) range_from_nat_into[OF infinite_imp_nonempty[OF \infinite U\] U(1)] by(auto simp add: xn_def U(1) \infinite U\ from_nat_into[OF infinite_imp_nonempty[OF \infinite U\]]) have [simp]:"topspace md.mtopology = P" using Ptop by(simp add: md.mtopology_topspace) have perfect:"perfect_space md.mtopology" using d perfect_set_subtopology up(3) by simp define jn where "jn \ (\n. LEAST i. i > n \ md.closed_ball (xn i) ((1/2)^i) \ md.open_ball (xn n) ((1/2)^n) - md.open_ball (xn n) ((1/2)^i))" define kn where "kn \ (\n. LEAST k. k > jn n \ md.closed_ball (xn k) ((1/2)^k) \ md.open_ball (xn n) ((1/2)^jn n))" have dxmxn: "\n n'. \m. m > n \ m > n' \ (1/2)^(m-1) < d (xn n) (xn m) \ d (xn n) (xn m) < (1/2)^(Suc n')" proof safe fix n n' have hinfin':"infinite (md.open_ball x e \ (range xn))" if "x \ P" "e > 0" for x e proof assume h_fin:"finite (md.open_ball x e \ range xn)" have h_nen:"md.open_ball x e \ range xn \ {}" using xn(5) that by(auto simp: md.dense_set_def) have infin: "infinite (md.open_ball x e)" using md.perfect_set_open_ball_infinite[OF perfect] that by simp then obtain y where y:"y \ md.open_ball x e" "y \ range xn" using h_fin by(metis inf.absorb_iff2 inf_commute subsetI) define e' where "e' = Min {d y xk |xk. xk \ md.open_ball x e \ range xn}" have fin: "finite {d y xk |xk. xk \ md.open_ball x e \ range xn}" using finite_imageI[OF h_fin,of "d y"] by (metis Setcompr_eq_image) have nen: "{d y xk |xk. xk \ md.open_ball x e \ range xn} \ {}" using h_nen by auto have "e' > 0" unfolding e'_def Min_gr_iff[OF fin nen] proof safe fix l assume "xn l \ md.open_ball x e" from y(2) md.dist_0[OF md.open_ballD'(1)[OF y(1)] md.open_ballD'(1)[OF this]] md.dist_geq0[of y "xn l"] show "0 < d y (xn l)" by auto qed obtain e'' where e'': "e'' > 0" "md.open_ball y e'' \ md.open_ball x e" "y \ md.open_ball y e''" by (meson md.mtopology_open_ball_in' md.open_ballD'(1) md.open_ball_ina y(1)) define \ where "\ \ min e' e''" have "\ > 0" using e''(1) \e' > 0\ by(simp add: \_def) then obtain m where m: "d y (xn m) < \" using md.dense_set_def2[of "range xn"] xn(5) md.open_ballD'(1)[OF y(1)] by blast consider "xn m \ md.open_ball x e" | "xn m \ P - md.open_ball x e" using xn(4) by auto then show False proof cases case 1 then have "e' \ d y (xn m)" using Min_le_iff[OF fin nen] by(auto simp: e'_def) thus ?thesis using m by(simp add: \_def) next case 2 then have "xn m \ md.open_ball y e''" using e''(2) by auto hence "e'' \ d y (xn m)" by(rule md.open_ball_nin_le[OF md.open_ballD'(1)[OF y(1)] e''(1) xn(4)[of m]]) thus ?thesis using m by(simp add: \_def) qed qed have hinfin:"infinite (md.open_ball x e \ (xn ` {l<..}))" if "x \ P" "e > 0" for x e l proof assume "finite (md.open_ball x e \ xn ` {l<..})" moreover have "finite (md.open_ball x e \ xn ` {..l})" by simp moreover have "(md.open_ball x e \ (range xn)) = (md.open_ball x e \ xn ` {l<..}) \ (md.open_ball x e \ xn ` {..l})" by fastforce ultimately have "finite (md.open_ball x e \ (range xn))" by auto with hinfin'[OF that] show False .. qed have "infinite (md.open_ball (xn n) ((1/2)^Suc n'))" using md.perfect_set_open_ball_infinite[OF perfect] xn(4)[of n] by simp then obtain x where x: "x \ md.open_ball (xn n) ((1/2)^Suc n')" "x \ xn n" by (metis finite_insert finite_subset infinite_imp_nonempty singletonI subsetI) then obtain e where e: "e > 0" "md.open_ball x e \ md.open_ball (xn n) ((1/2)^Suc n')" "x \ md.open_ball x e" by (meson md.mtopology_open_ball_in' md.open_ballD'(1) md.open_ball_ina) have "d (xn n) x > 0" using md.dist_geq0[of "xn n" x] md.dist_0[OF xn(4)[of n] md.open_ballD'(1)[OF x(1)]] x(2) by simp then obtain m' where m': "m' - 1 > 0" "(1/2)^(m' - 1) < d (xn n) x" by (metis One_nat_def diff_Suc_Suc diff_zero one_less_numeral_iff reals_power_lt_ex semiring_norm(76)) define m where "m \ max m' (max n' (Suc n))" then have "m \ m'" "m \ n'" "m \ Suc n" by simp_all hence m: "m - 1 > 0" "(1/2)^(m - 1) < d (xn n) x" "m > n" using m' less_trans[OF _ m'(2),of "(1 / 2) ^ (m - 1)"] by auto (metis diff_less_mono le_eq_less_or_eq) define \ where "\ \ min e (d (xn n) x - (1/2)^(m - 1))" have "\ > 0" using e m by(simp add: \_def) have ball_le:"md.open_ball x \ \ md.open_ball (xn n) ((1 / 2) ^ Suc n')" using md.open_ball_le[of \ e x] e(2) by(simp add: \_def) obtain k where k: "xn k \ md.open_ball x \" "k > m" using infinite_imp_nonempty[OF hinfin[OF md.open_ballD'(1)[OF x(1)] \\ > 0\,of m]] by auto show "\m>n. n' < m \ (1 / 2) ^ (m - 1) < d (xn n) (xn m) \ d (xn n) (xn m) < (1 / 2) ^ Suc n'" proof(intro exI[where x=k] conjI) have "(1 / 2) ^ (k - 1) < (1 / (2 :: real)) ^ (m - 1)" using k(2) m(3) by simp also have "... = d (xn n) x + ((1/2)^ (m - 1) - d (xn n) x)" by simp also have "... < d (xn n) x - d (xn k) x" using md.open_ballD[OF k(1)] by(simp add: \_def md.dist_sym[of x _]) also have "... \ d (xn n) (xn k)" using md.dist_tr[OF xn(4)[of n] xn(4)[of k] md.open_ballD'(1)[OF x(1)]] by simp finally show "(1 / 2) ^ (k - 1) < d (xn n) (xn k)" . qed(use \m \ n'\ k ball_le md.open_ballD[of "xn k" "xn n" "(1 / 2) ^ Suc n'"] m(3) in auto) qed have "jn n > n \ md.closed_ball (xn (jn n)) ((1/2)^(jn n)) \ md.open_ball (xn n) ((1/2)^n) - md.open_ball (xn n) ((1/2)^(jn n))" for n unfolding jn_def proof(rule LeastI_ex) obtain m where m:"m > n" "(1 / 2) ^ (m - 1) < d (xn n) (xn m)" "d (xn n) (xn m) < (1 / 2) ^ Suc n" using dxmxn by auto show "\x>n. md.closed_ball (xn x) ((1 / 2) ^ x) \ md.open_ball (xn n) ((1 / 2) ^ n) - md.open_ball (xn n) ((1 / 2) ^ x)" proof(safe intro!: exI[where x=m] m(1)) fix x assume h:"x \ md.closed_ball (xn m) ((1 / 2) ^ m)" have 1:"d (xn n) x < (1 / 2) ^ n" proof - have "d (xn n) x < (1 / 2) ^ Suc n + (1 / 2) ^ m" using m(3) md.dist_tr[OF xn(4)[of n] xn(4)[of m] md.closed_ballD'(1)[OF h]] md.closed_ballD[OF h] by simp also have "... \ (1 / 2) ^ Suc n + (1 / 2) ^ Suc n" by (metis Suc_lessI add_mono divide_less_eq_1_pos divide_pos_pos less_eq_real_def m(1) one_less_numeral_iff power_strict_decreasing_iff semiring_norm(76) zero_less_numeral zero_less_one) finally show ?thesis by simp qed have 2:"(1 / 2) ^ m \ d (xn n) x" proof - have "(1 / 2) ^ (m - 1) < d (xn n) x + (1 / 2) ^ m" using order.strict_trans2[OF m(2) md.dist_tr[OF xn(4)[of n] md.closed_ballD'(1)[OF h] xn(4)[of m]]] md.closed_ballD(1)[OF h] by(simp add: md.dist_sym) hence "(1 / 2) ^ (m - 1) - (1 / 2) ^ m \ d (xn n) x" by simp thus ?thesis using not0_implies_Suc[OF gr_implies_not0[OF m(1)]] by auto qed show "x \ md.open_ball (xn n) ((1 / 2) ^ n)" "x \ md.open_ball (xn n) ((1 / 2) ^ m) \ False" using xn(4)[of n] md.closed_ballD'(1)[OF h] 1 2 by(auto simp: md.open_ball_def) qed qed hence jn: "\n. jn n > n" "\n. md.closed_ball (xn (jn n)) ((1/2)^(jn n)) \ md.open_ball (xn n) ((1/2)^n) - md.open_ball (xn n) ((1/2)^(jn n))" by simp_all have "kn n > jn n \ md.closed_ball (xn (kn n)) ((1/2)^(kn n)) \ md.open_ball (xn n) ((1/2)^jn n)" for n unfolding kn_def proof(rule LeastI_ex) obtain m where m:"m > jn n" "d (xn n) (xn m) < (1 / 2) ^ Suc (jn n)" using dxmxn by blast show "\x>jn n. md.closed_ball (xn x) ((1 / 2) ^ x) \ md.open_ball (xn n) ((1 / 2) ^ jn n)" proof(intro exI[where x=m] conjI) show "md.closed_ball (xn m) ((1 / 2) ^ m) \ md.open_ball (xn n) ((1 / 2) ^ jn n)" proof fix x assume h:"x \ md.closed_ball (xn m) ((1 / 2) ^ m)" have "d (xn n) x < (1 / 2)^ Suc (jn n) + (1 / 2) ^ m" using md.dist_tr[OF xn(4)[of n] xn(4)[of m] md.closed_ballD'(1)[OF h]] m(2) md.closed_ballD[OF h] by simp also have "... \ (1 / 2)^ Suc (jn n) + (1 / 2)^ Suc (jn n)" by (metis Suc_le_eq add_mono dual_order.refl less_divide_eq_1_pos linorder_not_less m(1) not_numeral_less_one power_decreasing zero_le_divide_1_iff zero_le_numeral zero_less_numeral) finally show "x \ md.open_ball (xn n) ((1 / 2) ^ jn n)" by(simp add: xn(4)[of n] md.closed_ballD'(1)[OF h] md.open_ball_def) qed qed(use m(1) in auto) qed hence kn: "\n. kn n > jn n" "\n. md.closed_ball (xn (kn n)) ((1/2)^(kn n)) \ md.open_ball (xn n) ((1/2)^(jn n))" by simp_all have jnkn_pos: "jn n > 0" "kn n > 0" for n using not0_implies_Suc[OF gr_implies_not0[OF jn(1)[of n]]] kn(1)[of n] by auto define bn :: "real list \ nat" where "bn \ rec_list 1 (\a l t. if a = 0 then jn t else kn t)" have bn_simp: "bn [] = 1" "bn (a # l) = (if a = 0 then jn (bn l) else kn (bn l))" for a l by(simp_all add: bn_def) define to_listn :: "(nat \ real) \ nat \ real list" where "to_listn \ (\x . rec_nat [] (\n t. x n # t))" have to_listn_simp: "to_listn x 0 = []" "to_listn x (Suc n) = x n # to_listn x n" for x n by(simp_all add: to_listn_def) have to_listn_eq: "(\m. m < n \ x m = y m) \ to_listn x n = to_listn y n" for x y n by(induction n) (auto simp: to_listn_simp) have bn_gtn: "bn (to_listn x n) > n" for x n apply(induction n arbitrary: x) using jn(1) kn(1) by(auto simp: bn_simp to_listn_simp) (meson Suc_le_eq le_less less_trans_Suc)+ define rn where "rn \ (\n. Min (range (\x. (1 / 2 :: real) ^ bn (to_listn x n))))" have rn_fin: "finite (range (\x. (1 / 2 :: real) ^ bn (to_listn x n)))" for n proof - have "finite (range (\x. bn (to_listn x n)))" proof(induction n) case ih:(Suc n) have "(range (\x. bn (to_listn x (Suc n)))) \ (range (\x. jn (bn (to_listn x n)))) \ (range (\x. kn (bn (to_listn x n))))" by(auto simp: to_listn_simp bn_simp) moreover have "finite ..." using ih finite_range_imageI by auto ultimately show ?case by(rule finite_subset) qed(simp add: to_listn_simp) thus ?thesis using finite_range_imageI by blast qed have rn_nen: "(range (\x. (1 / 2 :: real) ^ bn (to_listn x n))) \ {}" for n by simp have rn_pos: "0 < rn n" for n by(simp add: Min_gr_iff[OF rn_fin rn_nen] rn_def) have rn_less: "rn n < (1/2)^n" for n using bn_gtn[of n] by(auto simp: rn_def Min_less_iff[OF rn_fin rn_nen]) have cball_le_ball:"md.closed_ball (xn (bn (a#l))) ((1/2)^(bn (a#l))) \ md.open_ball (xn (bn l)) ((1/2) ^ (bn l))" for a l using kn(2)[of "bn l"] md.open_ball_le[of "(1 / 2) ^ jn (bn l)" "(1 / 2) ^ bn l" "xn (bn l)"] less_imp_le [OF jn(1)] jn(2) by(simp add: bn_simp) blast hence cball_le:"md.closed_ball (xn (bn (a#l))) ((1/2)^(bn (a#l))) \ md.closed_ball (xn (bn l)) ((1/2) ^ (bn l))" for a l using md.open_ball_closed_ball by blast have cball_disj: "md.closed_ball (xn (bn (0#l))) ((1/2)^(bn (0#l))) \ md.closed_ball (xn (bn (1#l))) ((1/2)^(bn (1#l))) = {}" for l using jn(2) kn(2) by(auto simp: bn_simp) have "\x. \xa\P. (\n. md.closed_ball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))) = {xa}" proof fix x show "\xa\P. (\n. md.closed_ball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))) = {xa}" proof(rule md.closed_decseq_Inter) show "md.closed_ball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n)) \ {}" for n using md.closed_ball_ina[OF xn(4)[of "bn (to_listn x n)"],of "(1 / 2) ^ bn (to_listn x n)"] by auto next show "decseq (\n. md.closed_ball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n)))" by(intro decseq_SucI,simp add: to_listn_simp cball_le) next fix \ :: real assume "0 < \" then obtain N where N: "(1 / 2) ^ N < (1/2) * \" by (metis divide_pos_pos mult.commute mult.right_neutral one_less_numeral_iff reals_power_lt_ex semiring_norm(76) times_divide_eq_right zero_less_numeral) show "\N. \n\N. md.diam (md.closed_ball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))) < \" proof(safe intro!: exI[where x=N]) fix n assume "N \ n" have "md.diam (md.closed_ball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))) \ md.diam (md.closed_ball (xn (bn (to_listn x n))) ((1 / 2) ^ n))" using bn_gtn[of n x] by(auto intro!: md.diam_subset md.closed_ball_le) also have "... \ ennreal (2 * (1 / 2) ^ n)" by(simp add: md.diam_cball_leq) also have "... \ ennreal (2 * (1 / 2) ^ N)" using \N \ n\ by (simp add: numeral_mult_ennreal) also have "... < ennreal (2 *(1/2) * \)" using N by (simp add: \0 < \\ ennreal_lessI le_less numeral_mult_ennreal) also have "... = ennreal \" by (simp add: \0 < \\ le_less numeral_mult_ennreal) finally show "md.diam (md.closed_ball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))) < ennreal \" . qed qed(rule md.closedin_closed_ball) qed then obtain f where f:"\x. f x \ P" "\x. (\n. md.closed_ball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))) = {f x}" by metis hence f': "\n x. f x \ md.closed_ball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))" by blast have f'': "f x \ md.open_ball (xn (bn (to_listn x n))) ((1 / 2) ^ bn (to_listn x n))" for n x using f'[of x "Suc n"] cball_le_ball[of _ "to_listn x n"] by(auto simp: to_listn_simp) from f interpret bdmd: metric_set "f ` (\\<^sub>E i\UNIV. {0,1})" "submetric (f ` (\\<^sub>E i\UNIV. {0,1})) d" by(auto intro!: md.submetric_metric_set) have bdmd_top: "bdmd.mtopology = subtopology md.mtopology (f ` (\\<^sub>E i\UNIV. {0,1}))" by (simp add: f(1) image_subset_iff md.submetric_subtopology) have bdmd_sub: "bdmd.mtopology = subtopology S (f ` (\\<^sub>E i\UNIV. {0,1}))" using f(1) Int_absorb1[of "f ` (UNIV \\<^sub>E {0, 1})" P] by(fastforce simp: bdmd_top d subtopology_subtopology) interpret d01: polish_metric_set "{0,1::real}" "submetric {0,1::real} dist" by(auto intro!: polish_metric_set.submetric_polish[OF polish_class_polish_set] simp: euclidean_mtopology) interpret pd: product_polish_metric "1/2" UNIV id id "\_. {0,1::real}" "\_. submetric {0,1::real} dist" 1 by(auto intro!: product_polish_metric_natI simp: d01.polish_metric_set_axioms) (auto simp: submetric_def) have mpd_top: "pd.mtopology = Cantor_space_as_topology" by(auto simp: pd.product_dist_mtopology[symmetric] submetric_of_euclidean(2) intro!: product_topology_cong) define def_at where "def_at x y \ LEAST n. x n \ y n" for x y :: "nat \ real" have def_atxy: "\n. n < def_at x y \ x n = y n" "x (def_at x y) \ y (def_at x y)" if "x \ y" for x y proof - have "\n. x n \ y n" using that by auto from LeastI_ex[OF this] show "\n. n < def_at x y \ x n = y n" "x (def_at x y) \ y (def_at x y)" using not_less_Least by(auto simp: def_at_def) qed have def_at_le_if: "pd.product_dist x y \ (1/2)^n \ n \ def_at x y" if assm:"x \ y" "x \ (\\<^sub>E i\UNIV. {0,1})" "y \ (\\<^sub>E i\UNIV. {0,1})" for x y n proof - assume h:"pd.product_dist x y \ (1 / 2) ^ n" have "x m = y m" if m_less_n: "m < n" for m proof(rule ccontr) assume nen: "x m \ y m" then have "submetric {0, 1} dist (x m) (y m) = 1" using assm(2,3) by(auto simp: submetric_def) hence "1 \ 2 ^ m * pd.product_dist x y" using pd.product_dist_geq[of m m,simplified,OF assm(2,3)] by simp hence "(1/2)^m \ 2^m * (1/2)^m * pd.product_dist x y" by simp hence "(1/2)^m \ pd.product_dist x y" by (simp add: power_one_over) also have "... \ (1 / 2) ^ n" by(simp add: h) finally show False using that by auto qed thus "n \ def_at x y" by (meson def_atxy(2) linorder_not_le that(1)) qed have def_at_le_then: "pd.product_dist x y \ 2 * (1/2)^n" if assm:"x \ y" "x \ (\\<^sub>E i\UNIV. {0,1})" "y \ (\\<^sub>E i\UNIV. {0,1})" "n \ def_at x y" for x y n proof - have "\m. m < n \ x m = y m" by (metis def_atxy(1) order_less_le_trans that(4)) hence 1:"\m. m < n \ submetric {0, 1} dist (x m) (y m) = 0" by (simp add: submetric_def) have "pd.product_dist x y = (\i. (1/2)^(i + n) * (submetric {0, 1} dist (x (i + n)) (y (i + n)))) + (\ii. (1/2)^(i + n) * (submetric {0, 1} dist (x (i + n)) (y (i + n))))" by(simp add: 1) also have "... \ (\i. (1/2)^(i + n))" using pd.product_dist_summable'[simplified] pd.d_bound by(auto intro!: suminf_le summable_ignore_initial_segment) finally show ?thesis using pd.nsum_of_rK[of n] by simp qed have d_le_def: "d (f x) (f y) \ (1/2)^(def_at x y)" if assm:"x \ y" "x \ (\\<^sub>E i\UNIV. {0,1})" "y \ (\\<^sub>E i\UNIV. {0,1})" for x y proof - have 1:"to_listn x n = to_listn y n" if "n \ def_at x y" for n proof - have "\m. m < n \ x m = y m" by (metis def_atxy(1) order_less_le_trans that) then show ?thesis by(auto intro!: to_listn_eq) qed have "f x \ md.closed_ball (xn (bn (to_listn x (def_at x y)))) ((1 / 2) ^ bn (to_listn x (def_at x y)))" "f y \ md.closed_ball (xn (bn (to_listn x (def_at x y)))) ((1 / 2) ^ bn (to_listn x (def_at x y)))" using f'[of x "def_at x y"] f'[of y "def_at x y"] by(auto simp: 1[OF order_refl]) hence "d (f x) (f y) \ 2 * (1 / 2) ^ bn (to_listn x (def_at x y))" using f(1) by(auto intro!: md.diam_is_sup'[OF _ _ md.diam_cball_leq]) also have "... \ (1/2)^(def_at x y)" proof - have "Suc (def_at x y) \ bn (to_listn x (def_at x y))" using bn_gtn[of "def_at x y" x] by simp hence "(1 / 2) ^ bn (to_listn x (def_at x y)) \ (1 / 2 :: real) ^ Suc (def_at x y)" using power_decreasing_iff[OF pd.r] by blast thus ?thesis by simp qed finally show "d (f x) (f y) \ (1/2)^(def_at x y)" . qed have fy_in:"f y \ md.closed_ball (xn (bn (to_listn x m))) ((1/2)^bn (to_listn x m)) \ \l (\\<^sub>E i\UNIV. {0,1})" "y \ (\\<^sub>E i\UNIV. {0,1})" for x y m proof(induction m) case ih:(Suc m) have "f y \ md.closed_ball (xn (bn (to_listn x m))) ((1 / 2) ^ bn (to_listn x m))" using ih(2) cball_le by(auto simp: to_listn_simp) with ih(1) have k:"k < m \ x k = y k" for k by simp show ?case proof safe fix l assume "l < Suc m" then consider "l < m" | "l = m" using \l < Suc m\ by fastforce thus "x l = y l" proof cases case 2 have 3:"f y \ md.closed_ball (xn (bn (y l # to_listn y l))) ((1 / 2) ^ bn (y l # to_listn y l))" using f'[of y "Suc l"] by(simp add: to_listn_simp) have 4:"f y \ md.closed_ball (xn (bn (x l # to_listn y l))) ((1 / 2) ^ bn (x l # to_listn y l))" using ih(2) to_listn_eq[of m x y,OF k] by(simp add: to_listn_simp 2) show ?thesis proof(rule ccontr) assume "x l \ y l" then consider "x l = 0" "y l = 1" | "x l = 1" "y l = 0" using assm(1,2) by(auto simp: PiE_def Pi_def) metis thus False by cases (use cball_disj[of "to_listn y l"] 3 4 in auto) qed qed(simp add: k) qed qed simp have d_le_rn_then: "\e>0. \y \ (\\<^sub>E i\UNIV. {0,1}). x \ y \ d (f x) (f y) < e \ n \ def_at x y" if assm: "x \ (\\<^sub>E i\UNIV. {0,1})" for x n proof(safe intro!: exI[where x="(1/2)^bn (to_listn x n) - d (xn (bn (to_listn x n))) (f x)"]) show "0 < (1 / 2) ^ bn (to_listn x n) - d (xn (bn (to_listn x n))) (f x)" using md.open_ballD[OF f''] by auto next fix y assume h:"y \ (\\<^sub>E i\UNIV. {0,1})" "d (f x) (f y) < (1 / 2) ^ bn (to_listn x n) - d (xn (bn (to_listn x n))) (f x)" "x \ y" then have "f y \ md.closed_ball (xn (bn (to_listn x n))) ((1/2)^bn (to_listn x n))" using md.dist_tr[OF xn(4)[of "bn (to_listn x n)"] f(1)[of x] f(1)[of y]] by(simp add: xn(4)[of "bn (to_listn x n)"] f(1)[of y] md.closed_ball_def) with fy_in[OF assm h(1)] have "\m < n. x m = y m" by simp thus "n \ def_at x y" by (meson def_atxy(2) linorder_not_le h(3)) qed have 0: "f ` (\\<^sub>E i\UNIV. {0,1}) \ topspace S" using f(1) P(2) by auto have 1: "continuous_map pd.mtopology bdmd.mtopology f" unfolding metric_set_continuous_map_eq[OF pd.metric_set_axioms bdmd.metric_set_axioms] proof safe fix x :: "nat \ real" and \ :: real assume h:"x \ (\\<^sub>E i\UNIV. {0,1})" "0 < \" then obtain n where n:"(1/2)^n < \" using real_arch_pow_inv[OF _ pd.r(2)] by auto show "\\>0. \y\UNIV \\<^sub>E {0, 1}. pd.product_dist x y < \ \ submetric (f ` (UNIV \\<^sub>E {0, 1})) d (f x) (f y) < \" proof(safe intro!: exI[where x="(1/2)^n"]) fix y assume y:"y \ (\\<^sub>E i\UNIV. {0,1})" "pd.product_dist x y < (1 / 2) ^ n" consider "x = y" | "x \ y" by auto thus "submetric (f ` (UNIV \\<^sub>E {0, 1})) d (f x) (f y) < \" proof cases case 1 with y(1) h md.dist_0[OF f(1)[of y] f(1)[of y]] show ?thesis by(auto simp add: submetric_def) next case 2 then have "n \ def_at x y" using h(1) y by(auto intro!: def_at_le_if) have "submetric (f ` (UNIV \\<^sub>E {0, 1})) d (f x) (f y) \ (1/2)^(def_at x y)" using h(1) y(1) by(auto simp: d_le_def[OF 2 h(1) y(1)] submetric_def) also have "... \ (1/2)^n" using \n \ def_at x y\ by simp finally show ?thesis using n by simp qed qed simp qed simp have 2: "open_map pd.mtopology bdmd.mtopology f" proof(rule metric_set_opem_map_from_dist[OF pd.metric_set_axioms bdmd.metric_set_axioms,of f,simplified subtopology_topspace[of bdmd.mtopology,simplified bdmd.mtopology_topspace]]) fix x :: "nat \ real" and \ :: real assume h:"x \ (\\<^sub>E i\UNIV. {0,1})" "0 < \" then obtain n where n: "(1/2)^n < \" using real_arch_pow_inv[OF _ pd.r(2)] by auto obtain e where e: "e > 0" "\y. y \ (\\<^sub>E i\UNIV. {0,1}) \ x \ y \ d (f x) (f y) < e \ Suc n \ def_at x y" using d_le_rn_then[OF h(1),of "Suc n"] by auto show "\\>0. \y\UNIV \\<^sub>E {0, 1}. submetric (f ` (UNIV \\<^sub>E {0, 1})) d (f x) (f y) < \ \ pd.product_dist x y < \" proof(safe intro!: exI[where x=e]) fix y assume y:"y \ (\\<^sub>E i\UNIV. {0,1})" and "submetric (f ` (UNIV \\<^sub>E {0, 1})) d (f x) (f y) < e" then have d':"d (f x) (f y) < e" using h(1) by(simp add: submetric_def) consider "x = y" | "x \ y" by auto thus "pd.product_dist x y < \" by cases (use pd.dist_0[OF y y] h(2) def_at_le_then[OF _ h(1) y e(2)[OF y _ d']] n in auto) qed(use e(1) in auto) qed simp have 3: "f ` (topspace pd.mtopology) = topspace bdmd.mtopology" by(simp add: bdmd.mtopology_topspace pd.mtopology_topspace) have 4: "inj_on f (topspace pd.mtopology)" unfolding pd.mtopology_topspace proof fix x y assume h:"x \ (\\<^sub>E i\UNIV. {0,1})" "y \ (\\<^sub>E i\UNIV. {0,1})" "f x = f y" show "x = y" proof fix n have "f y \ md.closed_ball (xn (bn (to_listn x (Suc n)))) ((1/2)^bn (to_listn x (Suc n)))" using f'[of x "Suc n"] by(simp add: h) thus "x n = y n" using fy_in[OF h(1,2),of "Suc n"] by simp qed qed show ?thesis using homeomorphic_map_imp_homeomorphic_space[OF bijective_open_imp_homeomorphic_map[OF 1 2 3 4]] 0 by(auto simp: bdmd_sub mpd_top) qed lemma(in polish_topology) uncountable_contains_Cantor_space: assumes "uncountable (topspace S)" shows "\A. g_delta_of S A \ Cantor_space_as_topology homeomorphic_space (subtopology S A)" proof - obtain A where A:"A \ topspace S" "Cantor_space_as_topology homeomorphic_space (subtopology S A)" using uncountable_contains_Cantor_space'[OF assms] by auto then have "g_delta_of S A" using Cantor_space_Polish_topology by(auto intro!: complete_metrizable_homeo_image_g_delta simp: polish_topology_def complete_metrizable_axioms) thus ?thesis by(auto intro!: exI[where x=A] A(2)) qed subsection \Borel Spaces\ text \ Borel spaces generated from abstract topology \ definition borel_of :: "'a topology \ 'a measure" where "borel_of S \ sigma (topspace S) {U. openin S U}" lemma emeasure_borel_of: "emeasure (borel_of S) A = 0" by (simp add: borel_of_def emeasure_sigma) lemma borel_of_euclidean: "borel_of euclidean = borel" by(simp add: borel_of_def borel_def) lemma space_borel_of: "space (borel_of S) = topspace S" by(simp add: space_measure_of_conv borel_of_def) lemma sets_borel_of: "sets (borel_of S) = sigma_sets (topspace S) {U. openin S U}" by (simp add: subset_Pow_Union topspace_def borel_of_def) lemma sets_borel_of_closed: "sets (borel_of S) = sigma_sets (topspace S) {U. closedin S U}" unfolding sets_borel_of proof(safe intro!: sigma_sets_eqI) fix a assume a:"openin S a" have "topspace S - (topspace S - a) \ sigma_sets (topspace S) {U. closedin S U}" by(rule sigma_sets.Compl) (use a in auto) thus "a \ sigma_sets (topspace S) {U. closedin S U}" using openin_subset[OF a] by (simp add: Diff_Diff_Int inf.absorb_iff2) next fix b assume b:"closedin S b" have "topspace S - (topspace S - b) \ sigma_sets (topspace S) {U. openin S U}" by(rule sigma_sets.Compl) (use b in auto) thus "b \ sigma_sets (topspace S) {U. openin S U}" using closedin_subset[OF b] by (simp add: Diff_Diff_Int inf.absorb_iff2) qed lemma borel_of_open: assumes "openin S U" shows "U \ sets (borel_of S)" using assms by (simp add: subset_Pow_Union topspace_def borel_of_def) lemma borel_of_closed: assumes "closedin S U" shows "U \ sets (borel_of S)" using assms sigma_sets.Compl[of "topspace S - U" "topspace S"] by (simp add: closedin_def double_diff sets_borel_of) lemma(in metric_set) nbh_sets[measurable]: "(\a\A. open_ball a e) \ sets (borel_of mtopology)" by(auto intro!: borel_of_open openin_clauses(3) openin_open_ball) lemma borel_of_g_delta_of: assumes "g_delta_of S U" shows "U \ sets (borel_of S)" using g_delta_ofD[OF assms] borel_of_open by(auto intro!: sets.countable_INT'[of _ id,simplified]) lemma borel_of_subtopology: "borel_of (subtopology S U) = restrict_space (borel_of S) U" proof(rule measure_eqI) show "sets (borel_of (subtopology S U)) = sets (restrict_space (borel_of S) U)" unfolding restrict_space_eq_vimage_algebra' sets_vimage_algebra sets_borel_of topspace_subtopology space_borel_of Int_commute[of U] proof(rule sigma_sets_eqI) fix a assume "a \ Collect (openin (subtopology S U))" then obtain T where "openin S T" "a = T \ U" by(auto simp: openin_subtopology) show "a \ sigma_sets (topspace S \ U) {(\x. x) -` A \ (topspace S \ U) |A. A \ sigma_sets (topspace S) (Collect (openin S))}" using openin_subset[OF \openin S T\] \a = T \ U\ by(auto intro!: exI[where x=T] \openin S T\) next fix b assume "b \ {(\x. x) -` A \ (topspace S \ U) |A. A \ sigma_sets (topspace S) (Collect (openin S))}" then obtain T where ht:"b = T \ (topspace S \ U)" "T \ sigma_sets (topspace S) (Collect (openin S))" by auto hence "b = T \ U" proof - have "T \ topspace S" by(rule sigma_sets_into_sp[OF _ ht(2)]) (simp add: subset_Pow_Union topspace_def) thus ?thesis by(auto simp: ht(1)) qed with ht(2) show "b \ sigma_sets (topspace S \ U) (Collect (openin (subtopology S U)))" proof(induction arbitrary: b U) case (Basic a) then show ?case by(auto simp: openin_subtopology) next case Empty then show ?case by simp next case ih:(Compl a) then show ?case by (simp add: Diff_Int_distrib2 sigma_sets.Compl) next case (Union a) then show ?case by (metis UN_extend_simps(4) sigma_sets.Union) qed qed qed(simp add: emeasure_borel_of restrict_space_def emeasure_measure_of_conv) lemma(in metrizable) sigma_sets_eq_cinter_dunion: "sigma_sets (topspace S) {U. openin S U} = sigma_sets_cinter_dunion (topspace S) {U. openin S U}" proof safe fix a interpret sa: sigma_algebra "topspace S" "sigma_sets (topspace S) {U. openin S U}" by(auto intro!: sigma_algebra_sigma_sets openin_subset) assume "a \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}" then show "a \ sigma_sets (topspace S) {U. openin S U}" by induction auto next have c:"sigma_sets_cinter_dunion (topspace S) {U. openin S U} \ {U\sigma_sets_cinter_dunion (topspace S) {U. openin S U}. topspace S - U \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}}" proof fix a assume a: "a \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}" then show "a \ {U \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}. topspace S - U \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}}" proof induction case a:(Basic_cd a) then have "g_delta_of S (topspace S - a)" by(auto intro!: g_delta_of_closedin) from g_delta_ofD'[OF this] obtain U where U: "\n :: nat. openin S (U n)" "topspace S - a = \ (range U)" by auto show ?case using a U(1) by(auto simp: U(2) intro!: Inter_cd) next case Top_cd then show ?case by auto next case ca:(Inter_cd a) define b where "b \ (\n. (topspace S - a n) \ (\i. if i < n then a i else topspace S))" have bd:"disjoint_family b" using nat_neq_iff by(fastforce simp: disjoint_family_on_def b_def) have bin:"b i \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}" for i unfolding b_def apply(rule sigma_sets_cinter_dunion_int) using ca(2)[of i] apply auto[1] apply(rule Inter_cd) using ca by auto have bun:"topspace S - (\ (range a)) = (\i. b i)" (is "?lhs = ?rhs") proof - { fix x have "x \ ?lhs \ x \ topspace S \ x \ (\i. topspace S - a i)" by auto also have "... \ x \ topspace S \ (\n. x \ topspace S - a n)" by auto also have "... \ x \ topspace S \ (\n. x \ topspace S - a n \ (\i a i))" proof safe fix n assume 1:"x \ a n" "x \ topspace S" define N where "N \ Min {m. m \ n \ x \ a m}" have N:"x \ a N" "N \ n" using linorder_class.Min_in[of "{m. m \ n \ x \ a m}"] 1 by(auto simp: N_def) have N':"x \ a i" if "i < N" for i proof(rule ccontr) assume "x \ a i" then have "N \ i" using linorder_class.Min_le[of "{m. m \ n \ x \ a m}" i] that N(2) by(auto simp: N_def) with that show False by auto qed show "\n. x \ topspace S - a n \ (\i a i)" using N N' by(auto intro!: exI[where x=N] 1) qed auto also have "... \ x \ ?rhs" by(auto simp: b_def) finally have "x \ ?lhs \ x \ ?rhs" . } thus ?thesis by auto qed have "... \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}" by(rule Union_cd) (use bin bd in auto) thus ?case using Inter_cd[of a,OF ca(1)] by(auto simp: bun) next case ca:(Union_cd a) have "topspace S - (\ (range a)) = (\i. (topspace S - a i))" by simp have "... \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}" by(rule Inter_cd) (use ca in auto) then show ?case using Union_cd[of a,OF ca(1,2)] by auto qed qed fix a assume "a \ sigma_sets (topspace S) {U. openin S U}" then show "a \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}" proof induction case a:(Union a) define b where "b \ (\n. a n \ (\i. if i < n then topspace S - a i else topspace S))" have bd:"disjoint_family b" by(auto simp: disjoint_family_on_def b_def) (metis Diff_iff UnCI image_eqI linorder_neqE_nat mem_Collect_eq) have bin:"b i \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}" for i unfolding b_def apply(rule sigma_sets_cinter_dunion_int) using a(2)[of i] apply auto[1] apply(rule Inter_cd) using c a by auto have bun:"(\i. a i) = (\i. b i)" (is "?lhs = ?rhs") proof - { fix x have "x \ ?lhs \ x \ topspace S \ x \ ?lhs" using sigma_sets_cinter_dunion_into_sp[OF _ a(2)] by (metis UN_iff subsetD subset_Pow_Union topspace_def) also have "... \ x \ topspace S \ (\n. x \ a n)" by auto also have "... \ x \ topspace S \ (\n. x \ a n \ (\i topspace S - a i))" proof safe fix n assume 1:"x \ topspace S" "x \ a n" define N where "N \ Min {m. m \ n \ x \ a m}" have N:"x \ a N" "N \ n" using linorder_class.Min_in[of "{m. m \ n \ x \ a m}"] 1 by(auto simp: N_def) have N':"x \ a i" if "i < N" for i proof(rule ccontr) assume "\ x \ a i" then have "N \ i" using linorder_class.Min_le[of "{m. m \ n \ x \ a m}" i] that N(2) by(auto simp: N_def) with that show False by auto qed show "\n. x \ a n \ (\i topspace S - a i)" using N N' 1 by(auto intro!: exI[where x=N]) qed auto also have "... \ x \ ?rhs" proof safe fix m assume "x \ b m" then show "x \ topspace S" "\n. x \ a n \ (\i topspace S - a i)" by(auto intro!: exI[where x=m] simp: b_def) qed(auto simp: b_def) finally have "x \ ?lhs \ x \ ?rhs" . } thus ?thesis by auto qed have "... \ sigma_sets_cinter_dunion (topspace S) {U. openin S U}" by(rule Union_cd) (use bin bd in auto) thus ?case by(auto simp: bun) qed(use c in auto) qed lemma(in metrizable) sigma_sets_eq_cinter: "sigma_sets (topspace S) {U. openin S U} = sigma_sets_cinter (topspace S) {U. openin S U}" proof safe fix a interpret sa: sigma_algebra "topspace S" "sigma_sets (topspace S) {U. openin S U}" by(auto intro!: sigma_algebra_sigma_sets openin_subset) assume "a \ sigma_sets_cinter (topspace S) {U. openin S U}" then show "a \ sigma_sets (topspace S) {U. openin S U}" by induction auto qed (use sigma_sets_cinter_dunion_subset sigma_sets_eq_cinter_dunion in auto) lemma continuous_map_measurable: assumes "continuous_map X Y f" shows "f \ borel_of X \\<^sub>M borel_of Y" proof(rule measurable_sigma_sets[OF sets_borel_of[of Y]]) show "{U. openin Y U} \ Pow (topspace Y)" by (simp add: subset_Pow_Union topspace_def) next show "f \ space (borel_of X) \ topspace Y" using continuous_map_image_subset_topspace[OF assms] by(auto simp: space_borel_of) next fix U assume "U \ {U. openin Y U}" then have "openin X (f -` U \ topspace X)" using continuous_map[of X Y f] assms by auto thus "f -` U \ space (borel_of X) \ sets (borel_of X)" by(simp add: space_borel_of sets_borel_of) qed lemma open_map_preserves_sets: assumes "open_map S T f" "inj_on f (topspace S)" "A \ sets (borel_of S)" shows "f ` A \ sets (borel_of T)" using assms(3)[simplified sets_borel_of] proof(induction) case (Basic a) with assms(1) show ?case by(auto simp: sets_borel_of open_map_def) next case Empty show ?case by simp next case (Compl a) moreover have "f ` (topspace S - a) = f ` (topspace S) - f ` a" by (metis Diff_subset assms(2) calculation(1) inj_on_image_set_diff sigma_sets_into_sp subset_Pow_Union topspace_def) moreover have "f ` (topspace S) \ sets (borel_of T)" by (meson assms(1) borel_of_open open_map_def openin_topspace) ultimately show ?case by auto next case (Union a) then show ?case by (simp add: image_UN) qed lemma open_map_preserves_sets': assumes "open_map S (subtopology T (f ` (topspace S))) f" "inj_on f (topspace S)" "f ` (topspace S) \ sets (borel_of T)" "A \ sets (borel_of S)" shows "f ` A \ sets (borel_of T)" using assms(4)[simplified sets_borel_of] proof(induction) case (Basic a) then have "openin (subtopology T (f ` (topspace S))) (f ` a)" using assms(1) by(auto simp: open_map_def) hence "f ` a \ sets (borel_of (subtopology T (f ` (topspace S))))" by(simp add: sets_borel_of) hence "f ` a \ sets (restrict_space (borel_of T) (f ` (topspace S)))" by(simp add: borel_of_subtopology) thus ?case by (metis sets_restrict_space_iff assms(3) sets.Int_space_eq2) next case Empty show ?case by simp next case (Compl a) moreover have "f ` (topspace S - a) = f ` (topspace S) - f ` a" by (metis Diff_subset assms(2) calculation(1) inj_on_image_set_diff sigma_sets_into_sp subset_Pow_Union topspace_def) ultimately show ?case using assms(3) by auto next case (Union a) then show ?case by (simp add: image_UN) qed text \ Abstract topology version of @{thm second_countable_borel_measurable}. \ lemma borel_of_second_countable': assumes "second_countable S" and "subbase_of S \" shows "borel_of S = sigma (topspace S) \" unfolding borel_of_def proof(rule sigma_eqI) show "{U. openin S U} \ Pow (topspace S)" by (simp add: subset_Pow_Union topspace_def) next show "\ \ Pow (topspace S)" using subbase_of_subset[OF assms(2)] by auto next interpret s: sigma_algebra "topspace S" "sigma_sets (topspace S) \" using subbase_of_subset[OF assms(2)] by(auto intro!: sigma_algebra_sigma_sets) obtain \ where ho: "countable \" "base_of S \" using assms(1) by(auto simp: second_countable_def) show "sigma_sets (topspace S) {U. openin S U} = sigma_sets (topspace S) \" proof(rule sigma_sets_eqI) fix U assume "U \ {U. openin S U}" then have "generate_topology_on \ U" using assms(2) by(simp add: subbase_of_def openin_topology_generated_by_iff) thus "U \ sigma_sets (topspace S) \" proof induction case (UN K) with ho(2) obtain V where hv: "\k. k \ K \ V k \ \" "\k. k \ K \ \ (V k) = k" by(simp add: base_of_def openin_topology_generated_by_iff[symmetric] assms(2)[simplified subbase_of_def,symmetric]) metis define \k where "\k = (\k\K. V k)" have 0:"countable \k" using hv by(auto intro!: countable_subset[OF _ ho(1)] simp: \k_def) have "\ \k = (\A\\k. A)" by auto also have "... = \ K" unfolding \k_def UN_simps by(simp add: hv(2)) finally have 1:"\ \k = \ K" . have "\b\\k. \k\K. b \ k" using hv by (auto simp: \k_def) then obtain V' where hv': "\b. b \ \k \ V' b \ K" and "\b. b \ \k \ b \ V' b" by metis then have "(\b\\k. V' b) \ \K" "\\k \ (\b\\k. V' b)" by auto then have "\K = (\b\\k. V' b)" unfolding 1 by auto also have "\ \ sigma_sets (topspace S) \" using hv' UN by(auto intro!: s.countable_UN' simp: 0) finally show "\K \ sigma_sets (topspace S) \" . qed auto next fix U assume "U \ \" from assms(2)[simplified subbase_of_def] openin_topology_generated_by_iff generate_topology_on.Basis[OF this] show "U \ sigma_sets (topspace S) {U. openin S U}" by auto qed qed text \ Abstract topology version @{thm borel_prod}.\ lemma borel_of_prod: assumes "second_countable S" and "second_countable S'" shows "borel_of S \\<^sub>M borel_of S' = borel_of (prod_topology S S')" proof - have "borel_of S \\<^sub>M borel_of S' = sigma (topspace S \ topspace S') {a \ b |a b. a \ {a. openin S a} \ b \ {b. openin S' b}}" proof - obtain \ \' where ho: "countable \" "base_of S \" "countable \'" "base_of S' \'" using assms by(auto simp: second_countable_def) show ?thesis unfolding borel_of_def apply(rule sigma_prod) using topology_generated_by_topspace[of \,simplified base_is_subbase[OF ho(2),simplified subbase_of_def,symmetric]] topology_generated_by_topspace[of \',simplified base_is_subbase[OF ho(4),simplified subbase_of_def,symmetric]] base_of_openin[OF ho(2)] base_of_openin[OF ho(4)] by(auto intro!: exI[where x=\] exI[where x=\'] simp: ho subset_Pow_Union topspace_def) qed also have "... = borel_of (prod_topology S S')" using borel_of_second_countable'[OF prod_topology_second_countable[OF assms],simplified subbase_of_def,OF prod_topology_generated_by_open] by simp finally show ?thesis . qed lemma product_borel_of_measurable: assumes "i \ I" shows "(\x. x i) \ (borel_of (product_topology S I)) \\<^sub>M borel_of (S i)" by(auto intro!: continuous_map_measurable simp: assms) text \ Abstract topology version of @{thm sets_PiM_subset_borel} \ lemma sets_PiM_subset_borel_of: "sets (\\<^sub>M i\I. borel_of (S i)) \ sets (borel_of (product_topology S I))" proof - have *: "(\\<^sub>E i\I. X i) \ sets (borel_of (product_topology S I))" if [measurable]:"\i. X i \ sets (borel_of (S i))" "finite {i. X i \ topspace (S i)}" for X proof - note [measurable] = product_borel_of_measurable define I' where "I' = {i. X i \ topspace (S i)} \ I" have "finite I'" unfolding I'_def using that by simp have "(\\<^sub>E i\I. X i) = (\i\I'. (\x. x i)-`(X i) \ space (borel_of (product_topology S I))) \ space (borel_of (product_topology S I))" proof(standard;standard) fix x assume "x \ Pi\<^sub>E I X" then show "x \ (\i\I'. (\x. x i) -` X i \ space (borel_of (product_topology S I))) \ space (borel_of (product_topology S I))" using sets.sets_into_space[OF that(1)] by(auto simp: PiE_def I'_def Pi_def space_borel_of) next fix x assume 1:"x \ (\i\I'. (\x. x i) -` X i \ space (borel_of (product_topology S I))) \ space (borel_of (product_topology S I))" have "x i \ X i" if hi:"i \ I" for i proof - consider "i \ I' \ I' \ {}" | "i \ I' \ I' = {}" | "i \ I' \ I' \ {}" by auto then show ?thesis apply cases using sets.sets_into_space[OF \\i. X i \ sets (borel_of (S i))\] 1 that by(auto simp: space_borel_of I'_def) qed then show "x \ Pi\<^sub>E I X" using 1 by(auto simp: space_borel_of) qed also have "... \ sets (borel_of (product_topology S I))" using that \finite I'\ by(auto simp: I'_def) finally show ?thesis . qed then have "{Pi\<^sub>E I X |X. (\i. X i \ sets (borel_of (S i))) \ finite {i. X i \ space (borel_of (S i))}} \ sets (borel_of (product_topology S I))" by(auto simp: space_borel_of) show ?thesis unfolding sets_PiM_finite by(rule sets.sigma_sets_subset',fact) (simp add: borel_of_open[OF openin_topspace, of "product_topology S I",simplified] space_borel_of) qed text \ Abstract topology version of @{thm sets_PiM_equal_borel}.\ lemma sets_PiM_equal_borel_of: assumes "countable I" and "\i. i \ I \ second_countable (S i)" shows "sets (\\<^sub>M i\I. borel_of (S i)) = sets (borel_of (product_topology S I))" proof obtain K where hk: "countable K" "base_of (product_topology S I) K" "\k. k \ K \ \X. (k = (\\<^sub>E i\I. X i)) \ (\i. openin (S i) (X i)) \ finite {i. X i \ topspace (S i)} \ {i. X i \ topspace (S i)} \ I" using product_topology_countable_base_of[OF assms(1)] assms(2) by force have *:"k \ sets (\\<^sub>M i\I. borel_of (S i))" if "k \ K" for k proof - obtain X where H: "k = (\\<^sub>E i\I. X i)" "\i. openin (S i) (X i)" "finite {i. X i \ topspace (S i)}" "{i. X i \ topspace (S i)} \ I" using hk(3)[OF \k \ K\] by blast show ?thesis unfolding H(1) sets_PiM_finite using borel_of_open[OF H(2)] H(3) by(auto simp: space_borel_of) qed have **: "U \ sets (\\<^sub>M i\I. borel_of (S i))" if "openin (product_topology S I) U" for U proof - obtain B where "B \ K" "U = (\B)" using \openin (product_topology S I) U\ \base_of (product_topology S I) K\ by (metis base_of_def) have "countable B" using \B \ K\ \countable K\ countable_subset by blast moreover have "k \ sets (\\<^sub>M i\I. borel_of (S i))" if "k \ B" for k using \B \ K\ * that by auto ultimately show ?thesis unfolding \U = (\B)\ by auto qed have "sigma_sets (topspace (product_topology S I)) {U. openin (product_topology S I) U} \ sets (\\<^sub>M i\I. borel_of (S i))" apply (rule sets.sigma_sets_subset') using ** by(auto intro!: sets_PiM_I_countable[OF assms(1)] simp: borel_of_open[OF openin_topspace]) thus " sets (borel_of (product_topology S I)) \ sets (\\<^sub>M i\I. borel_of (S i))" by (simp add: subset_Pow_Union topspace_def borel_of_def) qed(rule sets_PiM_subset_borel_of) lemma homeomorphic_map_borel_isomorphic: assumes "homeomorphic_map X Y f" shows "measurable_isomorphic_map (borel_of X) (borel_of Y) f" proof - obtain g where "homeomorphic_maps X Y f g" using assms by(auto simp: homeomorphic_map_maps) hence "continuous_map X Y f" "continuous_map Y X g" "\x. x \ topspace X \ g (f x) = x" "\y. y \ topspace Y \ f (g y) = y" by(auto simp: homeomorphic_maps_def) thus ?thesis by(auto intro!: measurable_isomorphic_map_byWitness dest: continuous_map_measurable simp: space_borel_of) qed lemma homeomorphic_space_measurable_isomorphic: assumes "S homeomorphic_space T" shows "borel_of S measurable_isomorphic borel_of T" using homeomorphic_map_borel_isomorphic[of S T] assms by(auto simp: measurable_isomorphic_def homeomorphic_space) lemma measurable_isomorphic_borel_map: assumes "sets M = sets (borel_of S)" and f: "measurable_isomorphic_map M N f" shows "\S'. homeomorphic_map S S' f \ sets N = sets (borel_of S')" proof - obtain g where fg:"f \ M \\<^sub>M N" "g \ N \\<^sub>M M" "\x. x\space M \ g (f x) = x" "\y. y\space N \ f (g y) = y" "\A. A\sets M \ f ` A \ sets N" "\A. A\sets N \ g ` A \ sets M" "bij_betw g (space N) (space M)" using measurable_isomorphic_mapD'[OF f] by metis have g:"measurable_isomorphic_map N M g" by(auto intro!: measurable_isomorphic_map_byWitness fg) have g':"bij_betw g (space N) (topspace S)" using fg(7) sets_eq_imp_space_eq[OF assms(1)] by(auto simp: space_borel_of) show ?thesis proof(intro exI[where x="pullback_topology (space N) g S"] conjI) have [simp]: "{U. openin (pullback_topology (space N) g S) U} = (`) f ` {U. openin S U}" unfolding openin_pullback_topology'[OF g'] proof safe fix u assume u:"openin S u" then have 1:"u \ space M" by(simp add: sets_eq_imp_space_eq[OF assms(1)] space_borel_of openin_subset) with fg(3) have "g ` f ` u = u" by(fastforce simp: image_def) with u show "openin S (g ` f ` u)" by simp fix x assume "x \ u" with 1 fg(1) show "f x \ space N" by(auto simp: measurable_space) next fix u assume "openin S (g ` u)" "u \ space N" with fg(4) show "u \ (`) f ` {U. openin S U}" by(auto simp: image_def intro!: exI[where x="g ` u"]) (metis in_mono) qed have [simp]:"g -` topspace S \ space N = space N" using bij_betw_imp_surj_on g' by blast show "sets N = sets (borel_of (pullback_topology (space N) g S))" by(auto simp: sets_borel_of topspace_pullback_topology intro!: measurable_isomorphic_map_sigma_sets[OF assms(1)[simplified sets_borel_of space_borel_of[symmetric] sets_eq_imp_space_eq[OF assms(1),symmetric]] f]) next show "homeomorphic_map S (pullback_topology (space N) g S) f" proof(rule homeomorphic_maps_imp_map[where g=g]) obtain f' where f':"homeomorphic_maps (pullback_topology (space N) g S) S g f'" using topology_from_bij(1)[OF g'] homeomorphic_map_maps by blast have f'2:"f' y = f y" if y:"y \ topspace S" for y proof - have [simp]:"g -` topspace S \ space N = space N" using bij_betw_imp_surj_on g' by blast obtain x where "x \ space N" "y = g x" using g' y by(auto simp: bij_betw_def image_def) thus ?thesis using fg(4) f' by(auto simp: homeomorphic_maps_def topspace_pullback_topology) qed thus "homeomorphic_maps S (pullback_topology (space N) g S) f g" by(auto intro!: homeomorphic_maps_eq[OF f'] simp: homeomorphic_maps_sym[of S]) qed qed qed lemma measurable_isomorphic_borels: assumes "sets M = sets (borel_of S)" "M measurable_isomorphic N" shows "\S'. S homeomorphic_space S' \ sets N = sets (borel_of S')" using measurable_isomorphic_borel_map[OF assms(1)] assms(2) homeomorphic_map_maps by(fastforce simp: measurable_isomorphic_def homeomorphic_space_def ) lemma(in polish_topology) closedin_clopen_topology: assumes "closedin S a" shows "\S'. polish_topology S' \ (\u. openin S u \ openin S' u) \ topspace S = topspace S' \ sets (borel_of S) = sets (borel_of S') \ openin S' a \ closedin S' a" proof - have "polish_topology (subtopology S a)" by(rule closedin_polish[OF assms]) from polish_topology.bounded_polish_metric[OF this] obtain da where da: "polish_metric_set a da" "subtopology S a = metric_set.mtopology a da" "\x y. da x y < 1" by (metis topspace_subtopology_subset closedin_subset[OF assms]) interpret pa: polish_metric_set a da by fact have "polish_topology (subtopology S (topspace S - a))" using assms by(auto intro!: openin_polish) from polish_topology.bounded_polish_metric[OF this] obtain db where db: "polish_metric_set (topspace S - a) db" "subtopology S (topspace S - a) = metric_set.mtopology (topspace S - a) db" "\x y. db x y < 1" by (metis Diff_subset topspace_subtopology_subset) interpret pb: polish_metric_set "topspace S - a" db by fact interpret p: sum_polish_metric UNIV "\b. if b then a else topspace S - a" "\b. if b then da else db" using da db by(auto intro!: sum_polish_metricI simp: disjoint_family_on_def) have 0: "(\i. if i then a else topspace S - a) = topspace S" using closedin_subset assms by auto have 1: "sets (borel_of S) = sets (borel_of p.mtopology)" proof - have "sigma_sets (topspace S) (Collect (openin S)) = sigma_sets (topspace S) (Collect (openin p.mtopology))" proof(rule sigma_sets_eqI) fix a assume "a \ Collect (openin S)" then have "openin p.mtopology a" by(simp only: p.openin_sum_mtopology_iff) (auto simp: 0 da(2)[symmetric] db(2)[symmetric] openin_subtopology dest:openin_subset) thus "a \ sigma_sets (topspace S) (Collect (openin p.mtopology))" by auto next interpret s: sigma_algebra "topspace S" "sigma_sets (topspace S) (Collect (openin S))" by(auto intro!: sigma_algebra_sigma_sets openin_subset) fix b assume "b \ Collect (openin p.mtopology)" then have "openin p.mtopology b" by auto then have b:"b \ topspace S" "openin (subtopology S a) (b \ a)" "openin (subtopology S (topspace S - a)) (b \ (topspace S - a))" by(simp_all only: p.openin_sum_mtopology_iff,insert 0 da(2) db(2)) (auto simp: all_bool_eq) have [simp]: "(b \ a) \ (b \ (topspace S - a)) = b" using Diff_partition b(1) by blast have "(b \ a) \ (b \ (topspace S - a)) \ sigma_sets (topspace S) (Collect (openin S))" proof(rule sigma_sets_Un) have [simp]:"a \ sigma_sets (topspace S) (Collect (openin S))" proof - have "topspace S - (topspace S - a) \ sigma_sets (topspace S) (Collect (openin S))" by(rule sigma_sets.Compl) (use assms in auto) thus ?thesis using double_diff[OF closedin_subset[OF assms]] by simp qed from b(2,3) obtain T T' where T:"openin S T" "openin S T'" and [simp]:"b \ a = T \ a" "b \ (topspace S - a) = T' \ (topspace S - a)" by(auto simp: openin_subtopology) show "b \ a \ sigma_sets (topspace S) (Collect (openin S))" "b \ (topspace S - a) \ sigma_sets (topspace S) (Collect (openin S))" using T assms by auto qed thus "b \ sigma_sets (topspace S) (Collect (openin S))" by simp qed thus ?thesis by(simp only: sets_borel_of p.mtopology_topspace) (use 0 in auto) qed have 2:"\u. openin S u \ openin p.mtopology u" by(simp only: p.openin_sum_mtopology_iff) (auto simp: all_bool_eq da(2)[symmetric] db(2)[symmetric] openin_subtopology dest:openin_subset) have 3:"openin p.mtopology a" by(simp only: p.openin_sum_mtopology_iff) (auto simp: all_bool_eq) have 4:"closedin p.mtopology a" by (metis 0 2 assms closedin_def p.mtopology_topspace) have 5: "topspace S = topspace p.mtopology" by(simp only: p.mtopology_topspace) (simp only: 0) have 6: "polish_topology p.mtopology" using p.polish_topology_axioms by blast show ?thesis by(rule exI[where x=p.mtopology]) (insert 5 2 6, simp only: 1 3 4 ,auto) qed lemma polish_topology_union_polish: fixes X :: "nat \ 'a topology" assumes "\n. polish_topology (X n)" "\n. topspace (X n) = Xt" "\x y. x \ Xt \ y \ Xt \ x \ y \ \Ox Oy. (\n. openin (X n) Ox) \ (\n. openin (X n) Oy) \ x \ Ox \ y \ Oy \ disjnt Ox Oy" defines "Xun \ topology_generated_by (\n. {u. openin (X n) u})" shows "polish_topology Xun" proof - have topsXun:"topspace Xun = Xt" using assms(2) by(auto simp: Xun_def dest:openin_subset) define f :: "'a \ nat \ 'a" where "f \ (\x n. x)" have "continuous_map Xun (product_topology X UNIV) f" by(auto simp: assms(2) topsXun f_def continuous_map_componentwise, auto simp: Xun_def openin_topology_generated_by_iff continuous_map_def assms(2) dest:openin_subset[of "X _",simplified assms(2)] ) (insert openin_subopen, fastforce intro!: generate_topology_on.Basis) hence 1: "continuous_map Xun (subtopology (product_topology X UNIV) (f ` (topspace Xun))) f" by(auto simp: continuous_map_in_subtopology) have 2: "inj_on f (topspace Xun)" by(auto simp: inj_on_def f_def dest:fun_cong) have 3: "f ` (topspace Xun) = topspace (subtopology (product_topology X UNIV) (f ` (topspace Xun)))" by(auto simp: topsXun assms(2) f_def) have 4: "open_map Xun (subtopology (product_topology X UNIV) (f ` (topspace Xun))) f" proof(safe intro!: open_map_generated_topo[OF _ 2[simplified Xun_def],simplified Xun_def[symmetric]]) fix u n assume u:"openin (X n) u" show "openin (subtopology (product_topology X UNIV) (f ` topspace Xun)) (f ` u)" unfolding openin_subtopology proof(safe intro!: exI[where x="{ \i. if i = n then a else b i |a b. a \u \ b \ UNIV \ Xt}"]) show "openin (product_topology X UNIV) {\i. if i = n then a else b i |a b. a \u \ b \ UNIV \ Xt}" by(auto simp: openin_product_topology_alt u assms(2) openin_topspace[of "X _",simplified assms(2)] intro!: exI[where x="\i. if i = n then u else Xt"]) (auto simp: PiE_def Pi_def, metis openin_subset[OF u,simplified assms(2)] in_mono) next show "\y. y \ u \ \a b. f y = (\i. if i = n then a else b i) \ a \ u \ b \ UNIV \ Xt" using assms(2) f_def openin_subset u by fastforce next show "\y. y \ u \ f y \ f ` topspace Xun" using openin_subset[OF u] by(auto simp: assms(2) topsXun) next show "\x xa a b. xa \ topspace Xun \ f xa = (\i. if i = n then a else b i) \ a \ u \ b \ UNIV \ Xt \ f xa \ f ` u" using openin_subset[OF u] by(auto simp: topsXun assms(2)) (metis f_def imageI) qed qed have 5:"(subtopology (product_topology X UNIV) (f ` topspace Xun)) homeomorphic_space Xun" using homeomorphic_map_imp_homeomorphic_space[OF bijective_open_imp_homeomorphic_map[OF 1 4 3 2]] by(simp add: homeomorphic_space_sym[of Xun]) show ?thesis proof(safe intro!: polish_topology.homeomorphic_polish_topology[OF polish_topology.closedin_polish[OF polish_topology_product] 5] assms) show "closedin (product_topology X UNIV) (f ` topspace Xun)" proof - have 1: "openin (product_topology X UNIV) ((UNIV \\<^sub>E Xt) - f ` Xt)" proof(rule openin_subopen[THEN iffD2]) show "\x\(UNIV \\<^sub>E Xt) - f ` Xt. \T. openin (product_topology X UNIV) T \ x \ T \ T \ (UNIV \\<^sub>E Xt) - f ` Xt" proof safe fix x assume x:"x \ UNIV \\<^sub>E Xt" "x \ f ` Xt" have "\n. x n \ x 0" proof(rule ccontr) assume " \n. x n \ x 0" then have "\n. x n = x 0" by auto hence "x = (\_. x 0)" by auto thus False using x by(auto simp: f_def topsXun assms(2)) qed then obtain n where n: "n \ 0" "x n \ x 0" by metis from assms(3)[OF _ _ this(2)] x obtain On O0 where h:"\n. openin (X n) On" "\n. openin (X n) O0" "x n \ On" "x 0 \ O0" "disjnt On O0" by fastforce have "openin (product_topology X UNIV) ((\x. x 0) -` O0 \ topspace (product_topology X UNIV))" using continuous_map_product_coordinates[of 0 UNIV X] h(2)[of 0] by blast moreover have "openin (product_topology X UNIV) ((\x. x n) -` On \ topspace (product_topology X UNIV))" using continuous_map_product_coordinates[of n UNIV X] h(1)[of n] by blast ultimately have op: "openin (product_topology X UNIV) ((\T. T 0) -` O0 \ topspace (product_topology X UNIV) \ ((\T. T n) -` On \ topspace (product_topology X UNIV)))" by auto have xin:"x \ (\T. T 0) -` O0 \ topspace (product_topology X UNIV) \ ((\T. T n) -` On \ topspace (product_topology X UNIV))" using x h(3,4) by(auto simp: assms(2)) have subset:"(\T. T 0) -` O0 \ topspace (product_topology X UNIV) \ ((\T. T n) -` On \ topspace (product_topology X UNIV)) \ (UNIV \\<^sub>E Xt) - f ` Xt" using h(5) by(auto simp: assms(2) disjnt_def f_def) show "\T. openin (product_topology X UNIV) T \ x \ T \ T \ (UNIV \\<^sub>E Xt) - f ` Xt" by(rule exI[where x="((\x. x 0) -` O0 \ topspace (product_topology X UNIV)) \ ((\x. x n) -` On \ topspace (product_topology X UNIV))"]) (use op xin subset in auto) qed qed thus ?thesis by(auto simp: closedin_def assms(2) topsXun f_def) qed qed(simp add: f_def) qed lemma(in polish_topology) sets_clopen_topology: assumes "a \ sets (borel_of S)" shows "\S'. polish_topology S' \ (\u. openin S u \ openin S' u) \ topspace S = topspace S' \ sets (borel_of S) = sets (borel_of S') \ openin S' a \ closedin S' a" proof - have "a \ sigma_sets (topspace S) {U. closedin S U}" using assms by(simp add: sets_borel_of_closed) thus ?thesis proof induction case (Basic a) then show ?case by(simp add: closedin_clopen_topology) next case Empty with polish_topology_axioms show ?case by auto next case (Compl a) then obtain S' where S':"polish_topology S'" "(\u. openin S u \ openin S' u)" "topspace S = topspace S'" "sets (borel_of S) = sets (borel_of S')" "openin S' a" "closedin S' a" by auto from polish_topology.closedin_clopen_topology[OF S'(1) S'(6)] S' show ?case by auto next case ih:(Union a) then obtain Si where Si: "\i. polish_topology (Si i)" "\u i. openin S u \ openin (Si i) u" "\i::nat. topspace S = topspace (Si i)" "\i. sets (borel_of S) = sets (borel_of (Si i))" "\i. openin (Si i) (a i)" "\i. closedin (Si i) (a i)" by metis define Sun where "Sun \ topology_generated_by (\n. {u. openin (Si n) u})" have Sun1: "polish_topology Sun" unfolding Sun_def proof(safe intro!: polish_topology_union_polish[where Xt="topspace S"]) fix x y assume xy:"x \ topspace S" "y \ topspace S" "x \ y" then obtain Ox Oy where Oxy: "x \ Ox" "y \ Oy" "openin S Ox" "openin S Oy" "disjnt Ox Oy" using Hausdorff by(auto simp: Hausdorff_space_def) metis show "\Ox Oy. (\x. openin (Si x) Ox) \ (\x. openin (Si x) Oy) \ x \ Ox \ y \ Oy \ disjnt Ox Oy" by(rule exI[where x=Ox],insert Si(2) Oxy, auto intro!: exI[where x=Oy]) qed (use Si in auto) have Suntop:"topspace S = topspace Sun" using Si(3) by(auto simp: Sun_def dest: openin_subset) have Sunsets: "sets (borel_of S) = sets (borel_of Sun)" (is "?lhs = ?rhs") proof - have "?lhs = sigma_sets (topspace S) (\n. {u. openin (Si n) u})" proof show "sets (borel_of S) \ sigma_sets (topspace S) (\n. {u. openin (Si n) u})" using Si(2) by(auto simp: sets_borel_of intro!: sigma_sets_mono') next show "sigma_sets (topspace S) (\n. {u. openin (Si n) u}) \ sets (borel_of S)" by(simp add: sigma_sets_le_sets_iff[of "borel_of S" "\n. {u. openin (Si n) u}",simplified space_borel_of]) (use Si(4) sets_borel_of in fastforce) qed also have "... = ?rhs" using borel_of_second_countable'[OF polish_topology.S_second_countable[OF Sun1],of "\n. {u. openin (Si n) u}"] by (simp add: Sun_def Suntop subbase_of_def subset_Pow_Union) finally show ?thesis . qed have Sun_open: "\u i. openin (Si i) u \ openin Sun u" by(auto simp: Sun_def openin_topology_generated_by_iff intro!: generate_topology_on.Basis) have Sun_opena: "openin Sun (\i. a i)" using Sun_open[OF Si(5),simplified Sun_def] by(auto simp: Sun_def openin_topology_generated_by_iff intro!: generate_topology_on.UN) hence "closedin Sun (topspace Sun - (\i. a i))" by auto from polish_topology.closedin_clopen_topology[OF Sun1 this] show ?case using Suntop Sunsets Sun_open[OF Si(2)] Sun_opena by (metis closedin_def openin_closedin_eq) qed qed end \ No newline at end of file diff --git a/thys/Standard_Borel_Spaces/Lemmas_StandardBorel.thy b/thys/Standard_Borel_Spaces/Lemmas_StandardBorel.thy --- a/thys/Standard_Borel_Spaces/Lemmas_StandardBorel.thy +++ b/thys/Standard_Borel_Spaces/Lemmas_StandardBorel.thy @@ -1,2323 +1,2327 @@ (* Title: Lemmas_StandardBorel.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) text \ We refer to the HOL-Analysis library, the textbooks by Matsuzaka~\cite{topology} and Srivastava~\cite{borelsets}, and the lecture note by Biskup~\cite{standardborel}.\ section \Lemmas\ theory Lemmas_StandardBorel imports "HOL-Probability.Probability" begin subsection \Lemmas for Abstract Topology\ subsubsection \ Generated By \ lemma topology_generated_by_sub: assumes "\U. U \ \ \ (openin X U)" and "openin (topology_generated_by \) U" shows "openin X U" proof - have "generate_topology_on \ U" by (simp add: assms(2) openin_topology_generated_by) then show ?thesis by induction (use assms(1) in auto) qed lemma topology_generated_by_open: "S = topology_generated_by {U | U . openin S U}" unfolding topology_eq proof standard+ fix U assume "openin (topology_generated_by {U |U. openin S U}) U" note this[simplified openin_topology_generated_by_iff] then show "openin S U" by induction auto qed(simp add: openin_topology_generated_by_iff generate_topology_on.Basis) lemma topology_generated_by_eq: assumes "\U. U \ \ \ (openin (topology_generated_by \) U)" and "\U. U \ \ \ (openin (topology_generated_by \) U)" shows "topology_generated_by \ = topology_generated_by \" using topology_generated_by_sub[of \, OF assms(1)] topology_generated_by_sub[of \,OF assms(2)] by(auto simp: topology_eq) lemma topology_generated_by_homeomorphic_spaces: assumes "homeomorphic_map X Y f" "X = topology_generated_by \" shows "Y = topology_generated_by ((`) f ` \)" unfolding topology_eq proof have f:"open_map X Y f" "inj_on f (topspace X)" using assms(1) by (simp_all add: homeomorphic_imp_open_map perfect_injective_eq_homeomorphic_map[symmetric]) obtain g where g: "\x. x \ topspace X \ g (f x) = x" "\y. y \ topspace Y \ f (g y) = y" "open_map Y X g" "inj_on g (topspace Y)" using homeomorphic_map_maps[of X Y f,simplified assms(1)] homeomorphic_imp_open_map homeomorphic_maps_map[of X Y f] homeomorphic_imp_injective_map[of Y X] by blast show "\S. openin Y S = openin (topology_generated_by ((`) f ` \)) S" proof safe fix S assume "openin Y S" then have "openin X (g ` S)" using g(3) by (simp add: open_map_def) hence h:"generate_topology_on \ (g ` S)" by(simp add: assms(2) openin_topology_generated_by_iff) have "S = f ` (g ` S)" using openin_subset[OF \openin Y S\] g(2) by(fastforce simp: image_def) also have "openin (topology_generated_by ((`) f ` \)) ..." using h proof induction case Empty then show ?case by simp next case (Int a b) with inj_on_image_Int[OF f(2),of a b] show ?case by (metis assms(2) openin_Int openin_subset openin_topology_generated_by_iff) next case (UN K) then show ?case by(auto simp: image_Union) next case (Basis s) then show ?case by(auto intro!: generate_topology_on.Basis simp: openin_topology_generated_by_iff) qed finally show "openin (topology_generated_by ((`) f ` \)) S" . next fix S assume "openin (topology_generated_by ((`) f ` \)) S" then have "generate_topology_on ((`) f ` \) S" by(simp add: openin_topology_generated_by_iff) thus "openin Y S" proof induction case (Basis s) then obtain U where u:"U \ \" "s = f ` U" by auto then show ?case using assms(1) assms(2) homeomorphic_map_openness_eq topology_generated_by_Basis by blast qed auto qed qed lemma open_map_generated_topo: assumes "\u. u \ U \ openin S (f ` u)" "inj_on f (topspace (topology_generated_by U))" shows "open_map (topology_generated_by U) S f" unfolding open_map_def proof safe fix u assume "openin (topology_generated_by U) u" then have "generate_topology_on U u" by(simp add: openin_topology_generated_by_iff) thus "openin S (f ` u)" proof induction case (Int a b) then have [simp]:"f ` (a \ b) = f ` a \ f ` b" by (meson assms(2) inj_on_image_Int openin_subset openin_topology_generated_by_iff) from Int show ?case by auto qed (simp_all add: image_Union openin_clauses(3) assms) qed lemma subtopology_generated_by: "subtopology (topology_generated_by \) T = topology_generated_by {T \ U | U. U \ \}" unfolding topology_eq openin_subtopology openin_topology_generated_by_iff proof safe fix A assume "generate_topology_on \ A" then show "generate_topology_on {T \ U |U. U \ \} (A \ T)" proof induction case Empty then show ?case by (simp add: generate_topology_on.Empty) next case (Int a b) moreover have "a \ b \ T = (a \ T) \ (b \ T)" by auto ultimately show ?case by(auto intro!: generate_topology_on.Int) next case (UN K) moreover have "(\ K \ T) = (\ { k \ T | k. k \ K})" by auto ultimately show ?case by(auto intro!: generate_topology_on.UN) next case (Basis s) then show ?case by(auto intro!: generate_topology_on.Basis) qed next fix A assume "generate_topology_on {T \ U |U. U \ \} A" then show "\L. generate_topology_on \ L \ A = L \ T" proof induction case Empty show ?case by(auto intro!: exI[where x="{}"] generate_topology_on.Empty) next case ih:(Int a b) then obtain La Lb where "generate_topology_on \ La" "a = La \ T" "generate_topology_on \ Lb" "b = Lb \ T" by auto thus ?case using ih by(auto intro!: exI[where x="La \ Lb"] generate_topology_on.Int) next case ih:(UN K) then obtain L where "\k. k \ K \ generate_topology_on \ (L k) " "\k. k \ K \ k = (L k) \ T" by metis thus ?case using ih by(auto intro!: exI[where x="\k\K. L k"] generate_topology_on.UN) next case (Basis s) then show ?case using generate_topology_on.Basis by fastforce qed qed lemma prod_topology_generated_by: "topology_generated_by { U \ V | U V. U \ \ \ V \ \} = prod_topology (topology_generated_by \) (topology_generated_by \)" unfolding topology_eq proof safe fix U assume h:"openin (topology_generated_by {U \ V |U V. U \ \ \ V \ \}) U" show "openin (prod_topology (topology_generated_by \) (topology_generated_by \)) U" by(auto simp: openin_prod_Times_iff[of "topology_generated_by \" "topology_generated_by \"] intro!: topology_generated_by_Basis topology_generated_by_sub[OF _ h]) next fix U assume "openin (prod_topology (topology_generated_by \) (topology_generated_by \)) U" then have "\z\U. \V1 V2. openin (topology_generated_by \) V1 \ openin (topology_generated_by \) V2 \ fst z \ V1 \ snd z \ V2 \ V1 \ V2 \ U" by(auto simp: openin_prod_topology_alt) hence "\V1. \z\U. \V2. openin (topology_generated_by \) (V1 z) \ openin (topology_generated_by \) V2 \ fst z \ (V1 z) \ snd z \ V2 \ (V1 z) \ V2 \ U" by(rule bchoice) then obtain V1 where "\z\U. \V2. openin (topology_generated_by \) (V1 z) \ openin (topology_generated_by \) V2 \ fst z \ (V1 z) \ snd z \ V2 \ (V1 z) \ V2 \ U" by auto hence "\V2. \z\U. openin (topology_generated_by \) (V1 z) \ openin (topology_generated_by \) (V2 z) \ fst z \ (V1 z) \ snd z \ (V2 z) \ (V1 z) \ (V2 z) \ U" by(rule bchoice) then obtain V2 where hv12:"\z. z\U \ openin (topology_generated_by \) (V1 z) \ openin (topology_generated_by \) (V2 z) \ fst z \ (V1 z) \ snd z \ (V2 z) \ (V1 z) \ (V2 z) \ U" by auto hence 1:"U = (\z\U. (V1 z) \ (V2 z))" by auto have "openin (topology_generated_by {U \ V |U V. U \ \ \ V \ \}) (\z\U. (V1 z) \ (V2 z))" proof(rule openin_Union) show "\S. S \ (\z. V1 z \ V2 z) ` U \ openin (topology_generated_by {U \ V |U V. U \ \ \ V \ \}) S" proof safe fix x y assume h:"(x,y) \ U" then have "generate_topology_on \ (V1 (x,y))" using hv12 by(auto simp: openin_topology_generated_by_iff) thus "openin (topology_generated_by {U \ V |U V. U \ \ \ V \ \}) (V1 (x, y) \ V2 (x, y))" proof induction case Empty then show ?case by auto next case (Int a b) thus ?case by (auto simp: Sigma_Int_distrib1) next case (UN K) then have "openin (topology_generated_by {U \ V |U V. U \ \ \ V \ \}) (\{ k \ V2 (x, y) | k. k \ K})" by auto moreover have "(\ {k \ V2 (x, y) |k. k \ K}) = (\ K \ V2 (x, y))" by blast ultimately show ?case by simp next case ho:(Basis s) have "generate_topology_on \ (V2 (x,y))" using h hv12 by(auto simp: openin_topology_generated_by_iff) thus ?case proof induction case Empty then show ?case by auto next case (Int a b) then show ?case by (auto simp: Sigma_Int_distrib2) next case (UN K) then have "openin (topology_generated_by {U \ V |U V. U \ \ \ V \ \}) (\ { s \ k | k. k \K})" by auto moreover have "(\ { s \ k | k. k \K}) = s \ \K" by blast ultimately show ?case by simp next case (Basis s') then show ?case using ho by(auto intro!: topology_generated_by_Basis) qed qed qed qed thus "openin (topology_generated_by {U \ V |U V. U \ \ \ V \ \}) U" using 1 by auto qed lemma prod_topology_generated_by_open: "prod_topology S S' = topology_generated_by {U \ V | U V. openin S U \ openin S' V}" using prod_topology_generated_by[of " {U |U. openin S U}" "{U |U. openin S' U}"] topology_generated_by_open[of S,symmetric] topology_generated_by_open[of S'] by auto lemma product_topology_cong: assumes "\i. i \ I \ S i = K i" shows "product_topology S I = product_topology K I" proof - have 1:"{\\<^sub>E i\I. X i |X. (\i. openin (S i) (X i)) \ finite {i. X i \ topspace (S i)}} \ {\\<^sub>E i\I. X i |X. (\i. openin (K i) (X i)) \ finite {i. X i \ topspace (K i)}}" if "\i. i \ I \ S i = K i" for S K :: "_ \ 'b topology" proof fix x assume hx:"x \ {\\<^sub>E i\I. X i |X. (\i. openin (S i) (X i)) \ finite {i. X i \ topspace (S i)}}" then obtain X where hX: "x = (\\<^sub>E i\I. X i)" "\i. openin (S i) (X i)" "finite {i. X i \ topspace (S i)}" by auto define X' where "X' \ (\i. if i \ I then X i else topspace (K i))" have "x = (\\<^sub>E i\I. X' i)" by(auto simp: hX(1) X'_def PiE_def Pi_def) moreover have "finite {i. X' i \ topspace (K i)}" using that by(auto intro!: finite_subset[OF _ hX(3)] simp: X'_def) moreover have "openin (K i) (X' i)" for i using hX(2)[of i] that[of i] by(auto simp: X'_def) ultimately show "x \ {\\<^sub>E i\I. X i |X. (\i. openin (K i) (X i)) \ finite {i. X i \ topspace (K i)}}" by(auto intro!: exI[where x="X'"]) qed have "{\\<^sub>E i\I. X i |X. (\i. openin (S i) (X i)) \ finite {i. X i \ topspace (S i)}} = {\\<^sub>E i\I. X i |X. (\i. openin (K i) (X i)) \ finite {i. X i \ topspace (K i)}}" using 1[of S K] 1[of K S] assms by auto thus ?thesis by(simp add: product_topology_def) qed lemma topology_generated_by_without_empty: "topology_generated_by \ = topology_generated_by { U \ \. U \ {}}" proof(rule topology_generated_by_eq) fix U show "U \ \ \ openin (topology_generated_by { U \ \. U \ {}}) U" by(cases "U = {}") (simp_all add: topology_generated_by_Basis) qed (simp add: topology_generated_by_Basis) lemma topology_from_bij: assumes "bij_betw f A (topspace S)" shows "homeomorphic_map (pullback_topology A f S) S f" "topspace (pullback_topology A f S) = A" proof - note h = bij_betw_imp_surj_on[OF assms] bij_betw_inv_into_left[OF assms] bij_betw_inv_into_right[OF assms] then show [simp]:"topspace (pullback_topology A f S) = A" by(auto simp: topspace_pullback_topology) show "homeomorphic_map (pullback_topology A f S) S f" by(auto simp: homeomorphic_map_maps homeomorphic_maps_def h continuous_map_pullback[OF continuous_map_id,simplified] inv_into_into intro!: exI[where x="inv_into A f"] continuous_map_pullback'[where f=f]) (metis (mono_tags, opaque_lifting) comp_apply continuous_map_eq continuous_map_id h(3) id_apply) qed lemma openin_pullback_topology': assumes "bij_betw f A (topspace S)" shows "openin (pullback_topology A f S) u \ (openin S (f ` u)) \ u \ A" unfolding openin_pullback_topology proof safe fix U assume h:"openin S U" "u = f -` U \ A" from openin_subset[OF this(1)] assms have [simp]:"f ` (f -` U \ A) = U" by(auto simp: image_def vimage_def bij_betw_def) show "openin S (f ` (f -` U \ A))" by(simp add: h) next assume "openin S (f ` u)" "u \ A" with assms show "\U. openin S U \ u = f -` U \ A" by(auto intro!: exI[where x="f ` u"] simp: bij_betw_def inj_on_def) qed subsubsection \ Isolated Point \ definition isolated_points_of :: "'a topology \ 'a set \ 'a set" (infixr "isolated'_points'_of" 80) where "X isolated_points_of A \ {x\topspace X \ A. x \ X derived_set_of A}" lemma isolated_points_of_eq: "X isolated_points_of A = {x\topspace X \ A. \U. x \ U \ openin X U \ U \ (A - {x}) = {}}" unfolding isolated_points_of_def by(auto simp: in_derived_set_of) lemma in_isolated_points_of: "x \ X isolated_points_of A \ x \ topspace X \ x \ A \ (\U. x \ U \ openin X U \ U \ (A - {x}) = {})" by(simp add: isolated_points_of_eq) lemma derived_set_of_eq: "x \ X derived_set_of A \ x \ X closure_of (A - {x})" by(auto simp: in_derived_set_of in_closure_of) subsubsection \ Perfect Set \ definition perfect_set :: "'a topology \ 'a set \ bool" where "perfect_set X A \ closedin X A \ X isolated_points_of A = {}" abbreviation "perfect_space X \ perfect_set X (topspace X)" lemma perfect_setI: assumes "closedin X A" and "\x T. \x \ A; x \ T; openin X T\ \ \y\x. y \ T \ y \ A" shows "perfect_set X A" using assms by(simp add: perfect_set_def isolated_points_of_def in_derived_set_of) blast lemma perfect_spaceI: assumes "\x T. \x \ T; openin X T\ \ \y\x. y \ T" shows "perfect_space X" using assms by(auto intro!: perfect_setI) (meson in_mono openin_subset) lemma perfect_setD: assumes "perfect_set X A" shows "closedin X A" "A \ topspace X" "\x T. \x \ A; x \ T; openin X T\ \ \y\x. y \ T \ y \ A" using assms closedin_subset[of X A] by(simp_all add: perfect_set_def isolated_points_of_def in_derived_set_of) blast lemma perfect_space_perfect: "perfect_set euclidean (UNIV :: 'a :: perfect_space set)" by(auto simp: perfect_set_def in_isolated_points_of) (metis Int_Diff inf_top.right_neutral insert_Diff not_open_singleton) lemma perfect_set_subtopology: assumes "perfect_set X A" shows "perfect_space (subtopology X A)" using perfect_setD[OF assms] by(auto intro!: perfect_setI simp: inf.absorb_iff2 openin_subtopology) subsubsection \ Bases and Sub-Bases in Abstract Topology\ definition subbase_of :: "['a topology, 'a set set] \ bool" where "subbase_of S \ \ S = topology_generated_by \" definition base_of :: "['a topology, 'a set set] \ bool" where "base_of S \ \ (\U. openin S U \ (\\. U = \\ \ \ \ \))" definition second_countable :: "'a topology \ bool" where "second_countable S \ (\\. countable \ \ base_of S \)" definition zero_dimensional :: "'a topology \ bool" where "zero_dimensional S \ (\\. base_of S \ \ (\u\\. openin S u \ closedin S u))" lemma openin_base: assumes "base_of S \ " "U = \\" and "\ \ \" shows "openin S U" using assms by(auto simp: base_of_def) lemma base_is_subbase: assumes "base_of S \" shows "subbase_of S \" unfolding subbase_of_def topology_eq openin_topology_generated_by_iff proof safe fix U assume "openin S U" then obtain \ where hu:"U = \\" "\ \ \" using assms by(auto simp: base_of_def) thus "generate_topology_on \ U" by(auto intro!: generate_topology_on.UN) (auto intro!: generate_topology_on.Basis) next fix U assume "generate_topology_on \ U" then show "openin S U" proof induction case (Basis s) then show ?case using openin_base[OF assms,of s "{s}"] by auto qed auto qed lemma subbase_of_subset: assumes "subbase_of S \" and "U \ \" shows "U \ topspace S" using assms(1)[simplified subbase_of_def] topology_generated_by_topspace assms by auto lemma subbase_of_openin: assumes "subbase_of S \" and "U \ \" shows "openin S U" using assms by(simp add: subbase_of_def openin_topology_generated_by_iff generate_topology_on.Basis) lemma base_of_subset: assumes "base_of S \" and "U \ \" shows "U \ topspace S" using subbase_of_subset[OF base_is_subbase[OF assms(1)] assms(2)] . lemma base_of_openin: assumes "base_of S \" and "U \ \" shows "openin S U" using subbase_of_openin[OF base_is_subbase[OF assms(1)] assms(2)] . lemma base_of_def2: assumes "\U. U \ \ \ openin S U" shows "base_of S \ \ (\U. openin S U \ (\x\U. \W\\. x \ W \ W \ U))" proof assume h:"base_of S \" show "\U. openin S U \ (\x\U. \W\\. x \ W \ W \ U)" proof safe fix U x assume h':"openin S U" "x \ U" then obtain \ where hu: "U = \\" "\ \ \" using h by(auto simp: base_of_def) then obtain W where "x \ W" "W \ \" using h'(2) by blast thus "\W\\. x \ W \ W \ U" using hu by(auto intro!: bexI[where x=W]) qed next assume h:"\U. openin S U \ (\x\U. \W\\. x \ W \ W \ U)" show "base_of S \" unfolding base_of_def proof safe fix U assume "openin S U" then have "\x\U. \W. W\\ \ x \ W \ W \ U" using h by blast hence "\W. \x\U. W x \ \ \ x \ W x \ W x \ U" by(rule bchoice) then obtain W where hw: "\x\U. W x \ \ \ x \ W x \ W x \ U" by auto thus "\\. U = \ \ \ \ \ \" by(auto intro!: exI[where x="W ` U"]) next fix U \ show "\ \ \ \ openin S (\ \)" using assms by auto qed qed lemma base_of_def2': "base_of S \ \ (\b\\. openin S b) \ (\x. openin S x \ (\B'\\. \ B' = x))" proof assume h:"base_of S \" show "(\b\\. openin S b) \ (\x. openin S x \ (\B'\\. \ B' = x))" proof(rule conjI) show "\b\\. openin S b" using openin_base[OF h,of _ "{_}"] by auto next show "\x. openin S x \ (\B'\\. \ B' = x)" using h by(auto simp: base_of_def) qed next assume h:"(\b\\. openin S b) \ (\x. openin S x \ (\B'\\. \ B' = x))" show "base_of S \" unfolding base_of_def proof safe fix U assume "openin S U" then obtain B' where "B'\\" "\ B' = U" using h by blast thus "\\. U = \ \ \ \ \ \" by(auto intro!: exI[where x=B']) next fix U \ show "\ \ \ \ openin S (\ \)" using h by auto qed qed corollary base_of_in_subset: assumes "base_of S \" "openin S u" "x \ u" shows "\v\\. x \ v \ v \ u" using assms base_of_def2 base_of_def2' by fastforce lemma base_of_without_empty: assumes "base_of S \" shows "base_of S {U \ \. U \ {}}" unfolding base_of_def2' proof safe fix x assume "x \ \" " \ openin S x" thus "\y. y \ {}" using base_of_openin[OF assms \x \ \\] by simp next fix x assume "openin S x" then obtain B' where "B' \\" "\ B' = x" using assms by(simp add: base_of_def2') metis thus "\B'\{U \ \. U \ {}}. \ B' = x" by(auto intro!: exI[where x="{y \ B'. y \ {}}"]) qed lemma second_countable_ex_without_empty: assumes "second_countable S" shows "\\. countable \ \ base_of S \ \ (\U\\. U \ {})" proof - obtain \ where "countable \" "base_of S \" using assms second_countable_def by blast thus ?thesis by(auto intro!: exI[where x="{U \ \. U \ {}}"] base_of_without_empty) qed lemma subtopology_subbase_of: assumes "subbase_of S \" shows "subbase_of (subtopology S T) {T \ U | U. U \ \}" using assms subtopology_generated_by by(auto simp: subbase_of_def) lemma subtopology_base_of: assumes "base_of S \" shows "base_of (subtopology S T) {T \ U | U. U \ \}" unfolding base_of_def proof fix L show "openin (subtopology S T) L = (\\. L = \ \ \ \ \ {T \ U |U. U \ \})" proof assume "openin (subtopology S T) L " then obtain T' where ht: "openin S T'" "L = T' \ T" by(auto simp: openin_subtopology) then obtain \ where hu: "T' = (\ \)" "\ \ \" using assms by(auto simp: base_of_def) show "\\. L = \ \ \ \ \ {T \ U |U. U \ \}" using hu ht by(auto intro!: exI[where x="{T \ U | U. U \ \}"]) next assume "\\. L = \ \ \ \ \ {T \ U |U. U \ \}" then obtain \ where hu: "L = \ \" "\ \ {T \ U |U. U \ \}" by auto hence "\U\\. \U'\\. U = T \ U'" by blast then obtain k where hk:"\U. U \ \ \ k U \ \" "\U. U \ \ \ U = T \ k U" by metis hence "L = \ {T \ k U |U. U \ \}" using hu by auto also have "... = \ {k U |U. U \ \} \ T" by auto finally have 1:"L = \ {k U |U. U \ \} \ T" . moreover have "openin S (\ {k U |U. U \ \})" using hu hk assms by(auto simp: base_of_def) ultimately show "openin (subtopology S T) L" by(auto intro!: exI[where x="\ {k U |U. U \ \}"] simp: openin_subtopology) qed qed lemma second_countable_subtopology: assumes "second_countable S" shows "second_countable (subtopology S T)" proof - obtain \ where "countable \" "base_of S \" using assms second_countable_def by blast thus ?thesis by(auto intro!: exI[where x="{T \ U | U. U \ \}"] simp: second_countable_def Setcompr_eq_image dest: subtopology_base_of) qed lemma Lindelof_of: assumes "second_countable S" "\u. u \ U \ openin S u" "\ U = topspace S" shows "\U'. countable U' \ U' \ U \ \ U' = topspace S" proof - from assms(1) obtain \ where h: "countable \" "base_of S \" by(auto simp: second_countable_def) define B' where "B' \ {v\\. \u\U. v \ u}" have B': "countable B'" using h(1) by(auto simp: B'_def) have "\v. v \ B' \ (\u\U. v \ u)" by(auto simp: B'_def) then obtain U' where U':"\v. v \ B' \ U' v \ U" "\v. v \ B' \ v \ U' v" by metis show ?thesis proof(rule exI[where x="U' ` B'"]) show "countable (U' ` B') \ U' ` B' \ U \ \ (U' ` B') = topspace S" proof safe fix x assume "x \ topspace S" then obtain u where u:"x \ u" "u \ U" using assms(3) by auto obtain v where v:"x \ v" "v \ \" "v \ u" using base_of_in_subset[OF h(2) assms(2)[OF u(2)] u(1)] by auto show "x \ \ (U' ` B')" using u v U' by(auto intro!: bexI[where x=v]) (auto simp: B'_def intro!: exI[where x=u]) qed(use B' U' assms(2) openin_subset in blast)+ qed qed lemma open_map_with_base: assumes "base_of S \" "\A. A \ \ \ openin S' (f ` A)" shows "open_map S S' f" unfolding open_map_def proof safe fix U assume "openin S U" then obtain \ where "U = \\" "\ \ \" using assms(1) by(auto simp: base_of_def) hence "f ` U = \{ f ` A | A. A \ \}" by blast also have "openin S' ..." using assms(2) \\ \ \\ by auto finally show "openin S' (f ` U)" . qed text \ Construct a base from a subbase.\ definition finite_intersections :: "'a set set \ 'a set set" where "finite_intersections \ \ { \\' | \'. \' \ {} \ finite \' \ \' \ \}" lemma finite_intersections_inI: assumes "U = \\'" "\' \ {}" " finite \'" and "\' \ \" shows "U \ finite_intersections \" using assms by(auto simp: finite_intersections_def) lemma finite_intersections_Uin: assumes "U \ \" shows "U \ finite_intersections \" using assms by(auto intro!: finite_intersections_inI[of U "{U}"]) lemma finite_intersections_int: assumes "U \ finite_intersections \" and "V \ finite_intersections \" shows "U \ V \ finite_intersections \" proof - obtain \U \V where "U = \\U" "\U \ {}" "finite \U" "\U \ \" "V = \\V" "finite \V" "\V \ \" using assms by(auto simp: finite_intersections_def) thus ?thesis by(auto intro!: finite_intersections_inI[of _ "\U \ \V"]) qed lemma finite_intersections_countable: assumes "countable \" shows "countable (finite_intersections \)" proof - have "finite_intersections \ = (\i\{\'. \' \ {} \ finite \' \ \' \ \}. {\ i})" by(auto simp: finite_intersections_def) also have "countable ..." using countable_Collect_finite_subset[OF assms] by(auto intro!: countable_UN[of "{ \'. \' \ {} \ finite \' \ \' \ \}" "\\'. {\\'}"]) (auto intro!: countable_subset[of "{\'. \' \ {} \ finite \' \ \' \ \}" "{A. finite A \ A \ \}"]) finally show ?thesis . qed lemma finite_intersections_openin: assumes "U \ finite_intersections \" shows "openin (topology_generated_by \) U" proof - obtain \U where hu: "U = \\U" "\U \ {}" "finite \U" "\U \ \" using assms by(auto simp: finite_intersections_def) show ?thesis using hu by(auto intro: topology_generated_by_Basis) qed lemma topology_generated_by_finite_intersections: "topology_generated_by \ = topology_generated_by (finite_intersections \)" proof(rule topology_generated_by_eq) fix U assume "U \ \" then show "openin (topology_generated_by (finite_intersections \)) U" by(auto intro!: topology_generated_by_Basis simp: finite_intersections_Uin) qed (rule finite_intersections_openin) lemma topology_generated_by_is_union_of_finite_intersections: "openin (topology_generated_by \) U \ (\\. U = \\ \ \ \ finite_intersections \)" proof assume "openin (topology_generated_by \) U" then have "generate_topology_on \ U" by (simp add: openin_topology_generated_by_iff) thus "\\. U = \ \ \ \ \ finite_intersections \" proof induction case Empty then show ?case by auto next case (Int a b) then obtain \a \b where hab: "a = \ \a" "\a \ finite_intersections \" "b = \ \b" "\b \ finite_intersections \" by auto then have "a \ b = \{ Ua \ Ub | Ua Ub. Ua \ \a \ Ub \ \b}" by blast moreover have "{ Ua \ Ub | Ua Ub. Ua \ \a \ Ub \ \b} \ finite_intersections \" using hab(2,4) finite_intersections_int by blast ultimately show ?case by auto next case (UN K) then have "\\. \k\K. k = \ (\ k) \ \ k \ finite_intersections \" by(auto intro!: bchoice) then obtain \ where "\k\K. k = \ (\ k) \ \ k \ finite_intersections \" by auto thus ?case by(auto intro!: exI[where x="\k\K. (\ k)"]) (metis UnionE) next case (Basis s) then show ?case by(auto intro!: exI[where x="{s}"] finite_intersections_Uin) qed next assume "\\. U = \ \ \ \ \ finite_intersections \" then obtain \ where "U = \ \" "\ \ finite_intersections \" by auto thus "openin (topology_generated_by \) U" using finite_intersections_openin by(auto simp: openin_topology_generated_by_iff intro!: generate_topology_on.UN) qed lemma base_from_subbase: assumes "subbase_of S \" shows "base_of S (finite_intersections \)" using topology_generated_by_is_union_of_finite_intersections[of \,simplified assms[simplified subbase_of_def,symmetric]] by(simp add: base_of_def) lemma countable_base_from_countable_subbase: assumes "countable \" and "subbase_of S \" shows "second_countable S" using finite_intersections_countable[OF assms(1)] base_from_subbase[OF assms(2)] by(auto simp: second_countable_def) lemma prod_topology_second_countable: assumes "second_countable S" and "second_countable S'" shows "second_countable (prod_topology S S')" proof - obtain \ \' where ho: "countable \" "base_of S \" "countable \'" "base_of S' \'" using assms by(auto simp: second_countable_def) show ?thesis proof(rule countable_base_from_countable_subbase[where \="{ U \ V | U V. U \ \ \ V \ \'}"]) have "{U \ V |U V. U \ \ \ V \ \'} = (\(U,V). U \ V) ` (\ \ \')" by auto also have "countable ..." using ho(1,3) by auto finally show "countable {U \ V |U V. U \ \ \ V \ \'}" . next show "subbase_of (prod_topology S S') {U \ V |U V. U \ \ \ V \ \'}" using base_is_subbase[OF ho(2)] base_is_subbase[OF ho(4)] by(simp add: subbase_of_def prod_topology_generated_by) qed qed text \ Abstract version of the theorem @{thm product_topology_countable_basis}.\ lemma product_topology_countable_base_of: assumes "countable I" and "\i. i \ I \ second_countable (S i)" shows "\\'. countable \' \ base_of (product_topology S I) \' \ (\k \ \'. \X. k = (\\<^sub>E i\I. X i) \ (\i. openin (S i) (X i)) \ finite {i. X i \ topspace (S i)} \ {i. X i \ topspace (S i)} \ I)" proof - obtain \ where ho: "\i. i \ I \ countable (\ i)" "\i. i \ I \ base_of (S i) (\ i)" using assms(2)[simplified second_countable_def] by metis show ?thesis unfolding second_countable_def proof(intro exI[where x="{\\<^sub>E i\I. U i | U. finite {i\I. U i \ topspace (S i)} \ (\i\{i\I. U i \ topspace (S i)}. U i \ \ i)}"] conjI) show "countable {\\<^sub>E i\I. U i | U. finite {i\I. U i \ topspace (S i)} \ (\i\{i\I. U i \ topspace (S i)}. U i \ \ i)}" (is "countable ?X") proof - have "?X = {\\<^sub>E i\I. U i | U. finite {i\I. U i \ topspace (S i)} \ (\i\{i\I. U i \ topspace (S i)}. U i \ \ i) \ (\i \(UNIV- I). U i = {undefined})}" (is "_ = ?Y") proof (rule set_eqI) show "\x. x \ ?X \ x \ ?Y" proof fix x assume "x \ ?X" then obtain U where hu: "x = (\\<^sub>E i\I. U i)" "finite {i\I. U i \ topspace (S i)}" "(\i\{i\I. U i \ topspace (S i)}. U i \ \ i)" by auto define U' where "U' i \ (if i \ I then U i else {undefined})" for i have "x = (\\<^sub>E i\I. U' i)" using hu(1) by(auto simp: U'_def PiE_def extensional_def Pi_def) moreover have "finite {i\I. U' i \ topspace (S i)}" "(\i\{i\I. U' i \ topspace (S i)}. U' i \ \ i)" "\i \(UNIV- I). U' i = {undefined}" using hu(2,3) by(auto simp: U'_def) (metis (mono_tags, lifting) Collect_cong) ultimately show "x \ ?Y" by auto qed auto qed also have "... = (\U. \\<^sub>E i\I. U i) ` {U. finite {i\I. U i \ topspace (S i)} \ (\i\{i\I. U i \ topspace (S i)}. U i \ \ i) \ (\i \(UNIV- I). U i = {undefined})}" by auto also have "countable ..." proof(rule countable_image) have "{U. finite {i \ I. U i \ topspace (S i)} \ (\i\{i \ I. U i \ topspace (S i)}. U i \ \ i) \ (\i\UNIV - I. U i = {undefined})} = {U. \I'. finite I' \ I' \ I \ (\i\I'. U i \ \ i) \ (\i\(I - I'). U i = topspace (S i)) \ (\i\UNIV - I. U i = {undefined})}" (is "?A = ?B") proof (rule set_eqI) show "\x. x \ ?A \ x \ ?B" proof fix U assume "U \ {U. finite {i \ I. U i \ topspace (S i)} \ (\i\{i \ I. U i \ topspace (S i)}. U i \ \ i) \ (\i\UNIV - I. U i = {undefined})}" then show "U \ {U. \I'. finite I' \ I' \ I \ (\i\I'. U i \ \ i) \ (\i\I - I'. U i = topspace (S i)) \ (\i\UNIV - I. U i = {undefined})}" by auto next fix U assume assm:"U \ {U. \I'. finite I' \ I' \ I \ (\i\I'. U i \ \ i) \ (\i\I - I'. U i = topspace (S i)) \ (\i\UNIV - I. U i = {undefined})}" then obtain I' where hi': "finite I'" "I' \ I" "\i\I'. U i \ \ i" "\i\I - I'. U i = topspace (S i)" "\i\UNIV - I. U i = {undefined}" by auto then have "\i. i \ I \ U i \ topspace (S i) \ i \ I'" by auto hence "{i \ I. U i \ topspace (S i)} \ I'" by auto hence "finite {i \ I. U i \ topspace (S i)}" using hi'(1) by (simp add: rev_finite_subset) thus "U \ {U. finite {i \ I. U i \ topspace (S i)} \ (\i\{i \ I. U i \ topspace (S i)}. U i \ \ i) \ (\i\UNIV - I. U i = {undefined})}" using hi' by auto qed qed also have "... = (\I'\{I'. finite I' \ I' \ I}. {U. (\i\I'. U i \ \ i) \ (\i\I - I'. U i = topspace (S i)) \ (\i\UNIV - I. U i = {undefined})})" by auto also have "countable ..." proof(rule countable_UN[OF countable_Collect_finite_subset[OF assms(1)]]) fix I' assume "I' \ {I'. finite I' \ I' \ I}" hence hi':"finite I'" "I' \ I" by auto have "(\U i. if i \ I' then U i else undefined) ` {U. (\i\I'. U i \ \ i) \ (\i\I - I'. U i = topspace (S i)) \ (\i\UNIV - I. U i = {undefined})} \ (\\<^sub>E i\I'. \ i)" by auto moreover have "countable ..." using hi' by(auto intro!: countable_PiE ho) ultimately have "countable ((\U i. if i \ I' then U i else undefined) ` {U. (\i\I'. U i \ \ i) \ (\i\I - I'. U i = topspace (S i)) \ (\i\UNIV - I. U i = {undefined})})" by(simp add: countable_subset) moreover have "inj_on (\U i. if i \ I' then U i else undefined) {U. (\i\I'. U i \ \ i) \ (\i\I - I'. U i = topspace (S i)) \ (\i\UNIV - I. U i = {undefined})}" (is "inj_on ?f ?X") proof fix x y assume hxy: "x \ ?X" "y \ ?X" "?f x = ?f y" show "x = y" proof fix i consider "i \ I'" | "i \ I - I'" | "i \ UNIV - I" using hi'(2) by blast then show "x i = y i" proof cases case i:1 then show ?thesis using fun_cong[OF hxy(3),of i] by auto next case i:2 then show ?thesis using hxy(1,2) by auto next case i:3 then show ?thesis using hxy(1,2) by auto qed qed qed ultimately show "countable {U. (\i\I'. U i \ \ i) \ (\i\I - I'. U i = topspace (S i)) \ (\i\UNIV - I. U i = {undefined})}" using countable_image_inj_on by auto qed finally show "countable {U. finite {i \ I. U i \ topspace (S i)} \ (\i\{i \ I. U i \ topspace (S i)}. U i \ \ i) \ (\i\UNIV - I. U i = {undefined})}" . qed finally show ?thesis . qed next show "base_of (product_topology S I) {\\<^sub>E i\I. U i |U. finite {i \ I. U i \ topspace (S i)} \ (\i\{i \ I. U i \ topspace (S i)}. U i \ \ i)}" (is "base_of (product_topology S I) ?X") unfolding base_of_def proof safe fix U assume "openin (product_topology S I) U" then have "\x\U. \Ux. finite {i \ I. Ux i \ topspace (S i)} \ (\i\I. openin (S i) (Ux i)) \ x \ Pi\<^sub>E I Ux \ Pi\<^sub>E I Ux \ U" by(simp add: openin_product_topology_alt) hence "\Ux. \x\U. finite {i \ I. Ux x i \ topspace (S i)} \ (\i\I. openin (S i) (Ux x i)) \ x \ Pi\<^sub>E I (Ux x) \ Pi\<^sub>E I (Ux x) \ U" by(rule bchoice) then obtain Ux where hui: "\x. x \ U \ finite {i \ I. Ux x i \ topspace (S i)}" "\x i. x \ U \ i \ I \ openin (S i) (Ux x i)" "\x. x \ U \ x \ Pi\<^sub>E I (Ux x)" "\x. x \ U \ Pi\<^sub>E I (Ux x) \ U" by fastforce then have 1:"\x\U. \i\{i \ I. Ux x i \ topspace (S i)}. \\xj. \xj \ \ i \ Ux x i = \ \xj" using ho[simplified base_of_def] by (metis (no_types, lifting) mem_Collect_eq) have "\x\U. \\xj. \i\{i \ I. Ux x i \ topspace (S i)}. \xj i \ \ i \ Ux x i = \ (\xj i)" by(standard, rule bchoice) (use 1 in simp) hence "\\xj. \x\U. \i\{i \ I. Ux x i \ topspace (S i)}. \xj x i \ \ i \ Ux x i = \ (\xj x i)" by(rule bchoice) then obtain \xj where "\x\U. \i\{i \ I. Ux x i \ topspace (S i)}. \xj x i \ \ i \ Ux x i = \ (\xj x i)" by auto hence huxj: "\x i. x \ U \ i \ {i \ I. Ux x i \ topspace (S i)} \ \xj x i \ \ i" "\x i. x \ U \ i \ {i \ I. Ux x i \ topspace (S i)} \ Ux x i = \ (\xj x i)" by blast+ show "\\. U = \ \ \ \ \ ?X" proof(intro exI[where x="{\\<^sub>E i\I. K i | K. \x\U. finite {i \ I. Ux x i \ topspace (S i)} \ (\i\{i \ I. Ux x i \ topspace (S i)}. K i \ \xj x i) \ (\i\UNIV -{i \ I. Ux x i \ topspace (S i)}. K i = topspace (S i))}"] conjI) show "U = \ {\\<^sub>E i\I. K i | K. \x\U. finite {i \ I. Ux x i \ topspace (S i)} \ (\i\{i \ I. Ux x i \ topspace (S i)}. K i \ \xj x i) \ (\i\UNIV -{i \ I. Ux x i \ topspace (S i)}. K i = topspace (S i))}" proof safe fix x assume hxu:"x \ U" have "\i\{i \ I. Ux x i \ topspace (S i)}. Ux x i = \ (\xj x i)" using huxj[OF hxu] by blast hence "\i\{i \ I. Ux x i \ topspace (S i)}. \Uxj. Uxj \ \xj x i \ x i \ Uxj" using hui(3)[OF hxu] by auto hence "\Uxj. \i\{i \ I. Ux x i \ topspace (S i)}. Uxj i \ \xj x i \ x i \ Uxj i" by(rule bchoice) then obtain Uxj where huxj': "\i. i \ {i \ I. Ux x i \ topspace (S i)} \ Uxj i \ \xj x i" "\i. i \ {i \ I. Ux x i \ topspace (S i)} \ x i \ Uxj i" by auto define K where "K \ (\i. if i \ {i \ I. Ux x i \ topspace (S i)} then Uxj i else topspace (S i))" have "x \ (\\<^sub>E i\I. K i)" using huxj'(2) hui(3,4)[OF hxu] openin_subset[OF hui(2)[OF hxu]] by(auto simp: K_def PiE_def Pi_def) moreover have "\x\U. finite {i \ I. Ux x i \ topspace (S i)} \ (\i\{i \ I. Ux x i \ topspace (S i)}. K i \ \xj x i) \ (\i\UNIV -{i \ I. Ux x i \ topspace (S i)}. K i = topspace (S i))" by(rule bexI[OF _ hxu], rule conjI,simp add: hui(1)[OF hxu]) (use hui(2) hxu openin_subset huxj'(1) K_def in auto) ultimately show "x \ \ {\\<^sub>E i\I. K i | K. \x\U. finite {i \ I. Ux x i \ topspace (S i)} \ (\i\{i \ I. Ux x i \ topspace (S i)}. K i \ \xj x i) \ (\i\UNIV -{i \ I. Ux x i \ topspace (S i)}. K i = topspace (S i))}" by auto next fix x X K u assume hu: "x \ (\\<^sub>E i\I. K i)" "u \ U" "finite {i \ I. Ux u i \ topspace (S i)}" "\i\{i \ I. Ux u i \ topspace (S i)}. K i \ \xj u i" "\i\UNIV -{i \ I. Ux u i \ topspace (S i)}. K i = topspace (S i)" have "\i. i \ {i \ I. Ux u i \ topspace (S i)} \ K i \ Ux u i" using huxj[OF hu(2)] hu(4) by blast moreover have "\i. i \ I - {i \ I. Ux u i \ topspace (S i)} \ K i = Ux u i" using hu(5) by auto ultimately have "\i. i \ I \ K i \ Ux u i" by blast thus "x \ U" using hui(4)[OF hu(2)] hu(1) by blast qed next show "{\\<^sub>E i\I. K i | K. \x\U. finite {i \ I. Ux x i \ topspace (S i)} \ (\i\{i \ I. Ux x i \ topspace (S i)}. K i \ \xj x i) \ (\i\UNIV -{i \ I. Ux x i \ topspace (S i)}. K i = topspace (S i))} \ ?X" proof fix x assume "x \ {\\<^sub>E i\I. K i | K. \x\U. finite {i \ I. Ux x i \ topspace (S i)} \ (\i\{i \ I. Ux x i \ topspace (S i)}. K i \ \xj x i) \ (\i\UNIV -{i \ I. Ux x i \ topspace (S i)}. K i = topspace (S i))}" then obtain u K where hu: "x = (\\<^sub>E i\I. K i)" "u \ U" "finite {i \ I. Ux u i \ topspace (S i)}" "\i\{i \ I. Ux u i \ topspace (S i)}. K i \ \xj u i" "\i\UNIV -{i \ I. Ux u i \ topspace (S i)}. K i = topspace (S i)" by auto have hksubst:"{i \ I. K i \ topspace (S i)} \ {i \ I. Ux u i \ topspace (S i)}" using hu(5) by fastforce hence "finite {i \ I. K i \ topspace (S i)}" using hu(3) by (simp add: finite_subset) moreover have "\i\{i \ I. K i \ topspace (S i)}. K i \ \ i" using huxj(1)[OF hu(2)] hu(4) hksubst by (meson subsetD) ultimately show "x \ ?X" using hu(1) by auto qed qed next fix \ assume "\ \ ?X" have "openin (product_topology S I) u" if hu:"u \ \" for u proof - have hu': "u \ ?X" using \\ \ ?X\ hu by auto then obtain U where hU: "u = (\\<^sub>E i\I. U i)" "finite {i \ I. U i \ topspace (S i)}" "\i\{i \ I. U i \ topspace (S i)}. U i \ \ i" by auto define U' where "U' \ (\i. if i \ {i \ I. U i \ topspace (S i)} then U i else topspace (S i))" have hU': "u = (\\<^sub>E i\I. U' i)" by(auto simp: hU(1) U'_def PiE_def Pi_def) have hUfinite : "finite {i. U' i \ topspace (S i)}" using hU(2) by(auto simp: U'_def) have hUoi: "\i\{i. U' i \ topspace (S i)}. U' i \ \ i" using hU(3) by(auto simp: U'_def) have hUi: "\i\{i. U' i \ topspace (S i)}. i \ I" using hU(2) by(auto simp: U'_def) have hallopen:"openin (S i) (U' i)" for i proof - consider "i \ {i. U' i \ topspace (S i)}" | "i \ {i. U' i \ topspace (S i)}" by auto then show ?thesis proof cases case 1 then show ?thesis using hUoi ho(2)[of i] base_of_openin[of "S i" "\ i" "U' i"] hUi by auto next case 2 then have "U' i = topspace (S i)" by auto thus ?thesis by auto qed qed show "openin (product_topology S I) u" using hallopen hUfinite by(auto intro!: product_topology_basis simp: hU') qed thus "openin (product_topology S I) (\ \)" by auto qed next show "\k\{Pi\<^sub>E I U |U. finite {i \ I. U i \ topspace (S i)} \ (\i\{i \ I. U i \ topspace (S i)}. U i \ \ i)}. \X. k = Pi\<^sub>E I X \ (\i. openin (S i) (X i)) \ finite {i. X i \ topspace (S i)} \ {i. X i \ topspace (S i)} \ I" proof fix k assume "k \ {Pi\<^sub>E I U |U. finite {i \ I. U i \ topspace (S i)} \ (\i\{i \ I. U i \ topspace (S i)}. U i \ \ i)}" then obtain U where hu: "k = (\\<^sub>E i\I. U i)" "finite {i \ I. U i \ topspace (S i)}" "\i\{i \ I. U i \ topspace (S i)}. U i \ \ i" by auto define X where "X \ (\i. if i \ {i \ I. U i \ topspace (S i)} then U i else topspace (S i))" have hX1: "k = (\\<^sub>E i\I. X i)" using hu(1) by(auto simp: X_def PiE_def Pi_def) have hX2: "openin (S i) (X i)" for i using hu(3) base_of_openin[of "S i" _ "U i",OF ho(2)] by(auto simp: X_def) have hX3: "finite {i. X i \ topspace (S i)}" using hu(2) by(auto simp: X_def) have hX4: "{i. X i \ topspace (S i)} \ I" by(auto simp: X_def) show "\X. k = (\\<^sub>E i\I. X i) \ (\i. openin (S i) (X i)) \ finite {i. X i \ topspace (S i)} \ {i. X i \ topspace (S i)} \ I" using hX1 hX2 hX3 hX4 by(auto intro!: exI[where x=X]) qed qed qed lemma product_topology_second_countable: assumes "countable I" and "\i. i \ I \ second_countable (S i)" shows "second_countable (product_topology S I)" using product_topology_countable_base_of[OF assms(1)] assms(2) by(fastforce simp: second_countable_def) lemma Cantor_Bendixon: assumes "second_countable X" shows "\U P. countable U \ openin X U \ perfect_set X P \ U \ P = topspace X \ U \ P = {} \ (\a\{}. openin (subtopology X P) a \ uncountable a)" proof - obtain \ where o: "countable \" "base_of X \" using assms by(auto simp: second_countable_def) define U where "U \ \ {u\\. countable u}" define P where "P \ topspace X - U" have 1: "countable U" using o(1) by(auto simp: U_def intro!: countable_UN[of _ id,simplified]) have 2: "openin X U" using base_of_openin[OF o(2)] by(auto simp: U_def) have openin_c:"countable v \ v \ U" if "openin X v" for v proof assume "countable v" obtain \ where "v = \\" "\ \ \" using \openin X v\ o(2) by(auto simp: base_of_def) with \countable v\ have "\u. u \ \ \ countable u" by (meson Sup_upper countable_subset) thus "v \ U" using \\ \ \\ by(auto simp: \v = \\\ U_def) qed(rule countable_subset[OF _ 1]) have 3: "perfect_set X P" proof(rule perfect_setI) fix x T assume h:"x \ P" "x \ T" "openin X T" have T_unc:"uncountable T" using openin_c[OF h(3)] h(1,2) by(auto simp: P_def) obtain \ where U:"T = \\" "\ \ \" using h(3) o(2) by(auto simp: base_of_def) then obtain u where u:"u \ \" "uncountable u" using T_unc U_def h(3) openin_c by auto hence "uncountable (u - {x})" by simp hence "\ (u - {x} \ U)" using 1 by (metis countable_subset) then obtain y where "y \ u - {x}" "y \ U" by blast thus "\y. y \ x \ y \ T \ y \ P" using U u base_of_subset[OF o(2),of u] by(auto intro!: exI[where x=y] simp:P_def) qed(use 2 P_def in auto) have 4 : "uncountable a" if "openin (subtopology X P) a" "a \ {}" for a proof assume contable:"countable a" obtain b where b: "openin X b" "a = P \ b" using \openin (subtopology X P) a\ by(auto simp: openin_subtopology) hence "uncountable b" using P_def openin_c that(2) by auto thus False by (metis 1 Diff_Int_distrib2 Int_absorb1 P_def b(1) b(2) contable countable_Int1 openin_subset uncountable_minus_countable) qed show ?thesis using 1 2 3 4 by(auto simp: P_def) qed subsubsection \ Dense and Separable in Abstract Topology\ definition dense_of :: "['a topology, 'a set] \ bool" where "dense_of S U \ (U \ topspace S \ (\V. openin S V \ V \ {} \ U \ V \ {}))" lemma dense_of_def2: "dense_of S U \ (U \ topspace S \ (S closure_of U) = topspace S)" using dense_intersects_open by(auto simp: dense_of_def closure_of_subset_topspace in_closure_of) auto lemma dense_of_subset: assumes "dense_of S U" shows "U \ topspace S" using assms by(simp add: dense_of_def) lemma dense_of_nonempty: assumes "topspace S \ {}" "dense_of S U" shows "U \ {}" using assms by(auto simp: dense_of_def) definition separable :: "'a topology \ bool" where "separable S \ (\U. countable U \ dense_of S U)" lemma dense_ofI: assumes "U \ topspace S" and "\V. openin S V \ V \ {} \ U \ V \ {}" shows "dense_of S U" using assms by(auto simp: dense_of_def) lemma separable_if_second_countable: assumes "second_countable S" shows "separable S" proof - obtain \ where ho: "countable \" "base_of S \" "\u. u \ \ \ u \ {}" using second_countable_ex_without_empty[OF assms] by auto then obtain x where hx: "\u. u \ \ \ x u \ u" by (metis all_not_in_conv) show ?thesis unfolding separable_def proof(intro exI[where x="{x u|u. u \ \}"] conjI) show "countable {x u |u. u \ \}" using ho(1) by (simp add: Setcompr_eq_image) next show "dense_of S {x u |u. u \ \}" proof(rule dense_ofI) show "{x u |u. u \ \} \ topspace S" using hx base_of_subset[OF ho(2)] by auto next fix V assume "openin S V" "V \ {}" then obtain B where hb:"B \ \" "V = \ B" using base_of_def2' ho(2) by metis with \V \ {}\ obtain b where "b \ B" by auto hence "{x u |u. u \ \} \ b \ {x u |u. u \ \} \ V" using hb(2) by auto moreover have "x b \ {x u |u. u \ \} \ b" using hb(1) \b \ B\ hx[of b] by auto ultimately show "{x u |u. u \ \} \ V \ {}" by auto qed qed qed lemma dense_of_prod: assumes "dense_of S U" and "dense_of S' U'" shows "dense_of (prod_topology S S') (U \ U')" proof(rule dense_ofI) fix V assume h:"openin (prod_topology S S') V" "V \ {}" then obtain x y where hxy:"(x,y) \ V" by auto then obtain V1 V2 where hv12: "openin S V1" "openin S' V2" "x \ V1" "y \ V2" "V1 \ V2 \ V" using h(1) openin_prod_topology_alt[of S S' V] by blast hence "V1 \ {}" "V2 \ {}" by auto hence "U \ V1 \ {}" "U' \ V2 \ {}" using assms hv12 by(auto simp: dense_of_def) thus "U \ U' \ V \ {}" using hv12 by auto next show "U \ U' \ topspace (prod_topology S S')" using assms by(auto simp add: dense_of_def) qed lemma separable_prod: assumes "separable S" and "separable S'" shows "separable (prod_topology S S')" proof - obtain U U' where "countable U" "dense_of S U" "countable U'" "dense_of S' U'" using assms by(auto simp: separable_def) thus ?thesis by(auto intro!: exI[where x="U\U'"] dense_of_prod simp: separable_def) qed lemma dense_of_product: assumes "\i. i \ I \ dense_of (T i) (U i)" shows "dense_of (product_topology T I) (\\<^sub>E i\I. U i)" proof(rule dense_ofI) fix V assume h:"openin (product_topology T I) V" "V \ {}" then obtain x where hx:"x \ V" by auto then obtain K where hk: "finite {i \ I. K i \ topspace (T i)}" "\i\I. openin (T i) (K i)" "x \ (\\<^sub>E i\I. K i)" "(\\<^sub>E i\I. K i) \ V" using h(1) openin_product_topology_alt[of T I V] by auto hence "\i. i \ I \ K i \ {}" by auto hence "\i. i \ I \ U i \ K i \ {}" using assms hk by(auto simp: dense_of_def) hence "(\\<^sub>E i\I. U i) \ (\\<^sub>E i\I. K i) \ {}" by (simp add: PiE_Int PiE_eq_empty_iff) thus "(\\<^sub>E i\I. U i) \ V \ {}" using hk by auto next show "(\\<^sub>E i\I. U i) \ topspace (product_topology T I)" using assms by(auto simp: dense_of_def) qed lemma separable_countable_product: assumes "countable I" and "\i. i \ I \ separable (T i)" shows "separable (product_topology T I)" proof - consider "\i\I. topspace (T i) = {}" | "\i. i \ I \ topspace (T i) \ {}" by auto thus ?thesis proof cases case 1 then obtain i where i:"i \ I" "topspace (T i) = {}" by auto show ?thesis unfolding separable_def dense_of_def proof(intro exI[where x="{}"] conjI) show " \V. openin (product_topology T I) V \ V \ {} \ {} \ V \ {}" proof safe fix V x assume h: "openin (product_topology T I) V" "x \ V" from i have "topspace (product_topology T I) = {}" by auto with h(1) have "V = {}" - by(simp add: open_in_topspace_empty) + using openin_subset by blast thus "x \ {}" using h(2) by auto qed qed auto next case 2 - then have "\x. \i\I. x i \ topspace (T i)" "\U. \i\I. countable (U i) \ dense_of (T i) (U i)" + then have "\x. \i\I. x i \ topspace (T i)" + by (meson all_not_in_conv) + moreover from "2" + have "\U. \i\I. countable (U i) \ dense_of (T i) (U i)" using assms(2) by(auto intro!: bchoice simp: separable_def) - then obtain x U where hxu: + ultimately + obtain x U where hxu: "\i. i \ I \ x i \ topspace (T i)" "\i. i \ I \ countable (U i)" "\i. i \ I \ dense_of (T i) (U i)" by auto define U' where "U' \ (\J i. if i \ J then U i else {x i})" show ?thesis unfolding separable_def proof(intro exI[where x="\{ \\<^sub>E i\I. U' J i | J. finite J \ J \ I}"] conjI) have "(\{ \\<^sub>E i\I. U' J i | J. finite J \ J \ I}) = (\ ((\J. \\<^sub>E i\I. U' J i) ` {J. finite J \ J \ I}))" by auto also have "countable ..." proof(rule countable_UN) fix J assume hj:"J \ {J. finite J \ J \ I}" have "inj_on (\f. (\i\J. f i, \i\(I-J). f i)) (\\<^sub>E i\I. U' J i)" proof(rule inj_onI) fix f g assume h:"f \ Pi\<^sub>E I (U' J)" "g \ Pi\<^sub>E I (U' J)" "(restrict f J, restrict f (I - J)) = (restrict g J, restrict g (I - J))" then have "\i. i \ J \ f i = g i" "\i. i \(I-J) \ f i = g i" by(auto simp: restrict_def) meson+ thus "f = g" using h(1,2) by(auto simp: U'_def) (meson PiE_ext) qed moreover have "countable ((\f. (\i\J. f i, \i\(I-J). f i)) ` (\\<^sub>E i\I. U' J i))" (is "countable ?K") proof - have 1:"?K \ (\\<^sub>E i\J. U i) \ (\\<^sub>E i\(I-J). {x i})" using hj by(auto simp: U'_def PiE_def Pi_def) have 2:"countable ..." proof(rule countable_SIGMA) show "countable (Pi\<^sub>E J U)" using hj hxu(2) by(auto intro!: countable_PiE) next have "(\\<^sub>E i\I - J. {x i}) = { \i\I-J. x i }" by(auto simp: PiE_def extensional_def restrict_def Pi_def) thus "countable (\\<^sub>E i\I - J. {x i})" by simp qed show ?thesis by(rule countable_subset[OF 1 2]) qed ultimately show "countable (\\<^sub>E i\I. U' J i)" by(simp add: countable_image_inj_eq) qed(rule countable_Collect_finite_subset[OF assms(1)]) finally show "countable (\{ \\<^sub>E i\I. U' J i | J. finite J \ J \ I})" . next show "dense_of (product_topology T I) (\ {\\<^sub>E i\I. U' J i |J. finite J \ J \ I})" proof(rule dense_ofI) fix V assume h:"openin (product_topology T I) V" "V \ {}" then obtain y where hx:"y \ V" by auto then obtain K where hk: "finite {i \ I. K i \ topspace (T i)}" "\i. i\I \ openin (T i) (K i)" "y \ (\\<^sub>E i\I. K i)" "(\\<^sub>E i\I. K i) \ V" using h(1) openin_product_topology_alt[of T I V] by auto hence 3:"\i. i \ I \ K i \ {}" by auto hence 4:"i \ {i \ I. K i \ topspace (T i)} \ K i \ U' {i \ I. K i \ topspace (T i)} i \ {}" for i using hxu(3)[of i] hk(2)[of i] by(auto simp: U'_def dense_of_def) have "\z. \i\{i \ I. K i \ topspace (T i)}. z i \ K i \ U' {i \ I. K i \ topspace (T i)} i" by(rule bchoice) (use 4 in auto) then obtain z where hz: "\i\{i \ I. K i \ topspace (T i)}. z i \ K i \ U' {i \ I. K i \ topspace (T i)} i" by auto have 5: "i \ {i \ I. K i \ topspace (T i)} \ i \ I \ x i \ K i" for i using hxu(1)[of i] by auto have "(\i. if i \ {i \ I. K i \ topspace (T i)} then z i else if i \ I then x i else undefined) \ (\\<^sub>E i\I. U' {i \ I. K i \ topspace (T i)} i) \ (\\<^sub>E i\I. K i)" using 4 5 hz by(auto simp: U'_def) thus "\ {Pi\<^sub>E I (U' J) |J. finite J \ J \ I} \ V \ {}" using hk(1,4) by blast next have "\J. J \ I \ (\\<^sub>E i\I. U' J i) \ topspace (product_topology T I)" using hxu by(auto simp: dense_of_def U'_def PiE_def Pi_def) (metis subsetD) thus "(\ {\\<^sub>E i\I. U' J i |J. finite J \ J \ I}) \ topspace (product_topology T I)" by auto qed qed qed qed lemma separable_finite_product: assumes "finite I" and "\i. i \ I \ separable (T i)" shows "separable (product_topology T I)" using separable_countable_product[OF countable_finite[OF assms(1)]] assms by auto lemma homeomorphic_separable: assumes "separable X" "X homeomorphic_space Y" shows "separable Y" proof - obtain f g where "homeomorphic_maps X Y f g" using assms(2) by(auto simp: homeomorphic_space_def) hence fg:"continuous_map X Y f" "continuous_map Y X g" "\x. x \ topspace X \ g(f x) = x" "\y. y \ topspace Y \ f(g y) = y" by(auto simp: homeomorphic_maps_def) obtain U where U: "countable U" "dense_of X U" using assms(1) by(auto simp: separable_def) show ?thesis unfolding separable_def dense_of_def countable_image[OF U(1)] proof(intro exI[where x="f ` U"] conjI) show "f ` U \ topspace Y" using U(2) fg(1) by(auto simp: dense_of_def continuous_map_def) next show "\V. openin Y V \ V \ {} \ f ` U \ V \ {}" proof safe fix V x assume h:"openin Y V" "f ` U \ V = {}" "x \ V" then have "U \ (f -` V \ topspace X) = {}" by blast moreover have "f -` V \ topspace X \ {}" - using h(3) openin_subset[OF h(1)] by (metis (no_types, lifting) continuous_map_def disjoint_iff fg(2) fg(4) subsetD vimageI) + using continuous_map_preimage_topspace fg(2) fg(4) h(1) h(3) openin_subset by fastforce moreover have "openin X (f -` V \ topspace X)" using h(1) fg(1) by auto ultimately show "x \ {}" using U(2) by(auto simp: dense_of_def) qed qed(rule countable_image[OF U(1)]) qed subsubsection \ $G_{\delta}$ Set in Abstract Topology\ definition g_delta_of :: "['a topology, 'a set] \ bool" where "g_delta_of S A \ (\\. \ \ {} \ countable \ \ (\b\\. openin S b) \ A = \ \)" lemma g_delta_ofI: assumes "U \ {}" "countable U" "\b. b \ U \ openin S b" "A = \ U" shows "g_delta_of S A" using assms by(auto simp: g_delta_of_def) lemma g_delta_ofD: assumes "g_delta_of S A" shows "\\. \ \ {} \ countable \ \ (\b\\. openin S b) \ A = \ \" using assms by(simp add: g_delta_of_def) lemma g_delta_ofD': assumes "g_delta_of S A" shows "\U. (\n::nat. openin S (U n)) \ A = \ (range U)" proof- obtain \ where h:"\ \ {}" "countable \" "\b. b\\ \ openin S b" "A = \ \" using g_delta_ofD[OF assms] by metis show ?thesis using range_from_nat_into[OF h(1,2)] h(3,4) by(auto intro!: exI[where x="from_nat_into \"]) qed lemma g_delta_of_subset: assumes "g_delta_of S A" shows "A \ topspace S" using assms openin_subset by(auto simp: g_delta_of_def) lemma g_delta_of_open_set[simp]: assumes "openin S A" shows "g_delta_of S A" using assms by(auto simp: g_delta_of_def intro!: exI[where x="{A}"]) lemma g_delta_of_empty[simp]: "g_delta_of S {}" by simp lemma g_delta_of_topspace[simp]: "g_delta_of S (topspace S)" by simp lemma g_delta_of_inter: assumes "g_delta_of S A" and "g_delta_of S B" shows "g_delta_of S (A \ B)" proof - obtain Ua Ub where hu: "Ua \ {}" "countable Ua" "\b. b \ Ua \ openin S b" "A = \ Ua" "countable Ub" "\b. b \ Ub \ openin S b" "B = \ Ub" using assms by(auto simp: g_delta_of_def) thus ?thesis by(auto intro!: g_delta_ofI[where U="Ua \ Ub"]) qed lemma g_delta_of_Int: assumes "\a. a \ \ \ g_delta_of X a" "countable \" "\ \ {}" shows "g_delta_of X (\ \)" proof - obtain Ua where u: "\a. a \ \ \ Ua a \ {}" "\a. a \ \ \ countable (Ua a)" "\a b. a \ \ \ b \ Ua a \ openin X b" "\a. a \ \ \ a = \ (Ua a)" using g_delta_ofD[OF assms(1)] by metis have 1: "\ {Ua a |a. a \ \} \ {}" using assms(3) u(1) by auto have 2: "countable (\ {Ua a |a. a \ \})" by (simp add: Setcompr_eq_image assms(2) u(2)) have 3: "\b. b \ \ {Ua a |a. a \ \} \ openin X b" using u(3) by auto show ?thesis using u(4) by(fastforce intro!: g_delta_ofI[OF 1 2 3]) qed lemma g_delta_of_continuous_map: assumes "continuous_map X Y f" "g_delta_of Y a" shows "g_delta_of X (f -` a \ topspace X)" proof - obtain Ua where u: "Ua \ {}" "countable Ua" "\b. b \ Ua \ openin Y b" "a = \ Ua" using g_delta_ofD[OF assms(2)] by metis then have 0:"f -` a \ topspace X = \ {f -` b \ topspace X|b. b \ Ua}" by auto have 1: "{f -` b \ topspace X |b. b \ Ua} \ {}" using u(1) by simp have 2:"countable {f -` b \ topspace X|b. b \ Ua}" using u by (simp add: Setcompr_eq_image) have 3:"\c. c \ {f -` b \ topspace X|b. b \ Ua} \ openin X c" using assms u(3) by blast show ?thesis using g_delta_ofI[OF 1 2 3] by(simp add: 0) qed lemma g_delta_of_inj_open_map: assumes "open_map X Y f" "inj_on f (topspace X)" "g_delta_of X a" shows "g_delta_of Y (f ` a)" proof - obtain Ua where u: "Ua \ {}" "countable Ua" "\b. b \ Ua \ openin X b" "a = \ Ua" using g_delta_ofD[OF assms(3)] by metis then obtain j where "j \ Ua" by auto have "f ` a = f ` \ Ua" by(simp add: u(4)) also have "... = \ ((`) f ` Ua)" using u openin_subset by(auto intro!: image_INT[OF assms(2) _ \j \ Ua\,of id,simplified]) also have "... = \ {f ` u|u. u \ Ua}" by auto finally have 0: "f ` a = \ {f ` u |u. u \ Ua}" . have 1:"{f ` u |u. u \ Ua} \ {}" using u(1) by auto have 2:"countable {f ` u |u. u \ Ua}" using u(2) by (simp add: Setcompr_eq_image) have 3: "\c. c \ {f ` u |u. u \ Ua} \ openin Y c" using assms(1) u(3) by(auto simp: open_map_def) show ?thesis using g_delta_ofI[OF 1 2 3] by(simp add: 0) qed lemma g_delta_of_homeo_morphic: assumes "g_delta_of X a" "homeomorphic_map X Y f" shows "g_delta_of Y (f ` a)" by(auto intro!: g_delta_of_inj_open_map[of X Y f] simp: assms(1) homeomorphic_imp_injective_map[OF assms(2)] homeomorphic_imp_open_map[OF assms(2)]) lemma g_delta_of_prod: assumes "g_delta_of X A" "g_delta_of Y B" shows "g_delta_of (prod_topology X Y) (A \ B)" proof - obtain Ua Ub where hu: "Ua \ {}" "countable Ua" "\b. b \ Ua \ openin X b" "A = \ Ua" "Ub \ {}" "countable Ub" "\b. b \ Ub \ openin Y b" "B = \ Ub" using assms by(auto simp: g_delta_of_def) then have 0:"A \ B = \ {a \ b | a b. a \ Ua \ b \ Ub}" by blast have 1: "{a \ b | a b. a \ Ua \ b \ Ub} \ {}" using hu(1,5) by auto have 2: "countable {a \ b | a b. a \ Ua \ b \ Ub}" proof - have "countable ((\(x, y). x \ y) ` (Ua \ Ub))" using hu(2,6) by(auto intro!: countable_image[of "Ua \ Ub" "\(x,y). x \ y"]) moreover have "... = {a \ b | a b. a \ Ua \ b \ Ub}" by auto ultimately show ?thesis by simp qed have 3: "\c. c \ {a \ b | a b. a \ Ua \ b \ Ub} \ openin (prod_topology X Y) c" using hu(3,7) by(auto simp: openin_prod_Times_iff) show ?thesis using g_delta_ofI[OF 1 2 3] by(simp add: 0) qed lemma g_delta_of_prod1: assumes "g_delta_of X A" shows "g_delta_of (prod_topology X Y) (A \ topspace Y)" by(auto intro!: g_delta_of_prod assms) lemma g_delta_of_prod2: assumes "g_delta_of Y B" shows "g_delta_of (prod_topology X Y) (topspace X \ B)" by(auto intro!: g_delta_of_prod assms) lemma g_delta_of_subtopology: assumes "g_delta_of X A" "A \ S" shows "g_delta_of (subtopology X S) A" proof - obtain Ua where u: "Ua \ {}" "countable Ua" "\b. b \ Ua \ openin X b" "A = \ Ua" using g_delta_ofD[OF assms(1)] by metis have 0: "\ Ua = \ {ua \ S | ua. ua \ Ua } " using assms(2) u(4) by auto have 1: "{ua \ S | ua. ua \ Ua } \ {}" using u(1) by auto have 2: "countable {ua \ S | ua. ua \ Ua }" using u(2) by (simp add: Setcompr_eq_image) have 3: "\b. b \ {ua \ S | ua. ua \ Ua } \ openin (subtopology X S) b" using u(3) by(auto simp: openin_subtopology) show ?thesis using g_delta_ofI[OF 1 2 3 0] by(simp add: u(4)) qed lemma g_delta_of_subtopology_inverse: assumes "g_delta_of (subtopology X S) A" "g_delta_of X S" shows "g_delta_of X A" proof - obtain Ua where ua: "Ua \ {}" "countable Ua" "\b. b \ Ua \ openin (subtopology X S) b" "A = \ Ua" using g_delta_ofD[OF assms(1)] by metis then obtain T where t: "\b. b \ Ua \ openin X (T b)" "\b. b \ Ua \ b = T b \ S" by(auto simp: openin_subtopology) metis have 0: "A = \ {T b|b. b \ Ua} \ S" using ua(1,4) t(2) by blast have "{T b |b. b \ Ua} \ {}" "countable {T b |b. b \ Ua}" using ua(1,2) by(simp_all add: Setcompr_eq_image) from g_delta_ofI[OF this] t(1) show ?thesis by(auto intro!: g_delta_of_inter[OF _ assms(2)] simp: 0) qed lemma continuous_map_imp_closed_graph': assumes "continuous_map X Y f" "Hausdorff_space Y" shows "closedin (prod_topology Y X) ((\x. (f x,x)) ` topspace X)" using assms closed_map_def closed_map_paired_continuous_map_left by blast subsubsection \ Upper-Semicontinuous \ definition upper_semicontinuous_map :: "['a topology, 'a \ 'b :: linorder_topology] \ bool" where "upper_semicontinuous_map X f \ (\a. openin X {x\topspace X. f x < a})" lemma continuous_upper_semicontinuous: assumes "continuous_map X (euclidean :: ('b :: linorder_topology) topology) f" shows "upper_semicontinuous_map X f" unfolding upper_semicontinuous_map_def proof safe fix a :: 'b have *:"openin euclidean U \ openin X {x \ topspace X. f x \ U}" for U using assms by(simp add: continuous_map) have "openin euclidean {.. topspace X. f x < a}" by auto qed lemma upper_semicontinuous_map_iff_closed: "upper_semicontinuous_map X f \ (\a. closedin X {x\topspace X. f x \ a})" proof - have "{x \ topspace X. f x < a} = topspace X - {x \ topspace X. f x \ a}" for a by auto thus ?thesis by (simp add: closedin_def upper_semicontinuous_map_def) qed lemma upper_semicontinuous_map_real_iff: fixes f :: "'a \ real" shows "upper_semicontinuous_map X f \ upper_semicontinuous_map X (\x. ereal (f x))" unfolding upper_semicontinuous_map_def proof safe fix a :: ereal assume h:"\a::real. openin X {x \ topspace X. f x < a}" consider "a = - \" | "a = \" | "a \ - \ \ a \ \" by auto then show "openin X {x \ topspace X. ereal (f x) < a}" proof cases case 3 then have "ereal (f x) < a \ f x < real_of_ereal a" for x by (metis ereal_less_eq(3) linorder_not_less real_of_ereal.elims) thus ?thesis using h by simp qed simp_all next fix a :: real assume h:"\a::ereal. openin X {x \ topspace X. ereal (f x) < a}" then have "openin X {x \ topspace X. ereal (f x) < ereal a}" by blast moreover have"ereal (f x) < real_of_ereal a \ f x < a" for x by auto ultimately show "openin X {x \ topspace X. f x < a}" by auto qed subsection \ Lemmas for Limits\ lemma qlim_eq_lim_mono_at_bot: fixes g :: "rat \ 'a :: linorder_topology" assumes "mono f" "(g \ a) at_bot" "\r::rat. f (real_of_rat r) = g r" shows "(f \ a) at_bot" proof - have "mono g" by(metis assms(1,3) mono_def of_rat_less_eq) have ga:"\r. g r \ a" proof(rule ccontr) fix r assume "\ a \ g r" then have "g r < a" by simp from order_topology_class.order_tendstoD(1)[OF assms(2) this] obtain Q :: rat where q: "\q. q \ Q \ g r < g q" by(auto simp: eventually_at_bot_linorder) define q where "q \ min r Q" show False using q[of q] \mono g\ by(auto simp: q_def mono_def) (meson linorder_not_less min.cobounded1) qed show ?thesis proof(rule decreasing_tendsto) show "\\<^sub>F n in at_bot. a \ f n" unfolding eventually_at_bot_linorder by(rule exI[where x=undefined],auto) (metis Ratreal_def assms(1,3) dual_order.trans ga less_eq_real_def lt_ex monoD of_rat_dense) (*metis assms(1) assms(3) ga less_eq_real_def lfp.leq_trans lt_ex monoD of_rat_dense*) next fix x assume "a < x" with topological_space_class.topological_tendstoD[OF assms(2),of "{..q. q \ Q \ g q < x" by(auto simp: eventually_at_bot_linorder) show "\\<^sub>F n in at_bot. f n < x" using q assms(1,3) by(auto intro!: exI[where x="real_of_rat Q"] simp: eventually_at_bot_linorder) (metis dual_order.refl monoD order_le_less_trans) qed qed lemma qlim_eq_lim_mono_at_top: fixes g :: "rat \ 'a :: linorder_topology" assumes "mono f" "(g \ a) at_top" "\r::rat. f (real_of_rat r) = g r" shows "(f \ a) at_top" proof - have "mono g" by(metis assms(1,3) mono_def of_rat_less_eq) have ga:"\r. g r \ a" proof(rule ccontr) fix r assume "\ g r \ a" then have "a < g r" by simp from order_topology_class.order_tendstoD(2)[OF assms(2) this] obtain Q :: rat where q: "\q. Q \ q \ g q < g r" by(auto simp: eventually_at_top_linorder) define q where "q \ max r Q" show False using q[of q] \mono g\ by(auto simp: q_def mono_def leD) qed show ?thesis proof(rule increasing_tendsto) show "\\<^sub>F n in at_top. f n \ a" unfolding eventually_at_top_linorder by(rule exI[where x=undefined],auto) (metis (no_types, opaque_lifting) assms(1) assms(3) dual_order.trans ga gt_ex monoD of_rat_dense order_le_less) next fix x assume "x < a" with topological_space_class.topological_tendstoD[OF assms(2),of "{x<..}"] obtain Q :: rat where q: "\q. Q \ q \ x < g q" by(auto simp: eventually_at_top_linorder) show "\\<^sub>F n in at_top. x < f n" using q assms(1,3) by(auto simp: eventually_at_top_linorder intro!: exI[where x="real_of_rat Q"]) (metis dual_order.refl monoD order_less_le_trans) qed qed lemma tendsto_enn2real: assumes "k < top" and "(f \ k) F" shows "((\n. enn2real (f n)) \ enn2real k) F" proof - have 1:"ennreal (enn2real k) = k" "enn2real k \ 0" using assms(1) by auto show ?thesis using assms tendsto_enn2real[OF _ 1(2),of f] by(simp add: 1(1)) qed lemma LIMSEQ_inverse_not0: fixes xn :: "nat \ real" assumes "\n. xn n \ 0" "xn \ x" "(\n. 1 / (xn n)) \ b" shows "x \ 0" proof assume x:"x = 0" then have xn:"\e. e > 0 \ \N. \n\N. \xn n\ < e" using LIMSEQ_D[OF assms(2)] by simp have "\N. \n\N. \1 / (xn n) - b\ \ r" if r:"r > 0" for r proof - have "0 < 1 / (r + \b\)" using that by auto with xn[OF this] obtain N where N':"\n. n \ N \ \xn n\ < 1 / (r + \b\)" by auto show ?thesis proof(rule exI[where x=N]) show "\n\N. r \ \1 / xn n - b\" proof safe fix n assume "n \ N" note N'[OF this] hence "(r + \b\) * \xn n\ < 1" by (metis \0 < 1 / (r + \b\)\ mult.commute pos_less_divide_eq zero_less_divide_1_iff) hence "1 / \xn n\ > r + \b\" using assms(1)[of n] by (simp add: less_divide_eq) hence "r + \b\ - \b\ < 1 / \xn n\ - \b\" by simp also have "... = \1 / xn n\ - \b\" by simp also have "... \ \1 / xn n - b\" by simp finally show "r \ \1 / xn n - b\" by simp qed qed qed with LIMSEQ_D[OF assms(3)] show False by (metis less_le_not_le linorder_le_cases real_norm_def zero_less_one) qed lemma obtain_subsequence: fixes xn :: "nat \ _" assumes "infinite {n. P n (xn n)}" obtains a :: "nat \ nat" where "strict_mono a" "\n. P (a n) (xn (a n))" proof - have inf: "infinite {n. n > m \ P n (xn n)}" for m proof assume "finite {n. n > m \ P n (xn n)}" then have "finite ({..m} \ {n. n > m \ P n (xn n)})" by auto hence "finite {n. P n (xn n)}" by(auto intro!: finite_subset[where B="{..m} \ {n. n > m \ P n (xn n)}"]) with assms show False by simp qed define an where "an \ rec_nat (SOME n. P n (xn n)) (\n an. SOME m. m > an \ P m (xn m))" have anSome: "an (Suc n) = (SOME m. m > an n \ P m (xn m))" for n by(auto simp: an_def) have an1: "P (an n) (xn (an n))" for n proof(cases n) case 0 obtain m where m:"P m (xn m)" using assms not_finite_existsD by blast show ?thesis by(simp add: an_def 0,rule someI,rule m) next case (Suc n') obtain m where m:"m > an n'" "P m (xn m)" using inf not_finite_existsD by blast show ?thesis by(simp add: Suc anSome, rule someI2[where a=m],auto simp: m) qed have an2: "strict_mono an" unfolding strict_mono_Suc_iff anSome proof safe fix n obtain m where m:"m > an n" "P m (xn m)" using inf not_finite_existsD by blast show "an n < (SOME m. an n < m \ P m (xn m))" by (rule someI2[where a=m],auto simp: m) qed show ?thesis using an1 that[OF an2] by auto qed subsection \Lemmas for Measure Theory\ lemma measurable_preserve_sigma_sets: assumes "sets M = sigma_sets \ S" "S \ Pow \" "\a. a \ S \ f ` a \ sets N" "inj_on f (space M)" "f ` space M \ sets N" and "b \ sets M" shows "f ` b \ sets N" proof - have "b \ sigma_sets \ S" using assms(1,6) by simp thus ?thesis proof induction case (Basic a) then show ?case by(rule assms(3)) next case Empty then show ?case by simp next case (Compl a) moreover have " \ = space M" by (metis assms(1) assms(2) sets.sets_into_space sets.top sigma_sets_into_sp sigma_sets_top subset_antisym) ultimately show ?case by (metis Diff_subset assms(2) assms(4) assms(5) inj_on_image_set_diff sets.Diff sigma_sets_into_sp) next case (Union a) then show ?case by (simp add: image_UN) qed qed lemma integral_measurable_subprob_algebra2: fixes f :: "_ \ _ \ _::{banach,second_countable_topology}" assumes [measurable]: "(\(x, y). f x y) \ borel_measurable (M \\<^sub>M N)" "L \ measurable M (subprob_algebra N)" shows "(\x. integral\<^sup>L (L x) (f x)) \ borel_measurable M" proof - note integral_measurable_subprob_algebra[measurable] note measurable_distr2[measurable] have "(\x. integral\<^sup>L (distr (L x) (M \\<^sub>M N) (\y. (x, y))) (\(x, y). f x y)) \ borel_measurable M" by measurable then show "(\x. integral\<^sup>L (L x) (f x)) \ borel_measurable M" by (rule measurable_cong[THEN iffD1, rotated]) (simp add: integral_distr) qed inductive_set sigma_sets_cinter :: "'a set \ 'a set set \ 'a set set" for sp :: "'a set" and A :: "'a set set" where Basic_c[intro, simp]: "a \ A \ a \ sigma_sets_cinter sp A" | Top_c[simp]: "sp \ sigma_sets_cinter sp A" | Inter_c: "(\i::nat. a i \ sigma_sets_cinter sp A) \ (\i. a i) \ sigma_sets_cinter sp A" | Union_c: "(\i::nat. a i \ sigma_sets_cinter sp A) \ (\i. a i) \ sigma_sets_cinter sp A" inductive_set sigma_sets_cinter_dunion :: "'a set \ 'a set set \ 'a set set" for sp :: "'a set" and A :: "'a set set" where Basic_cd[intro, simp]: "a \ A \ a \ sigma_sets_cinter_dunion sp A" | Top_cd[simp]: "sp \ sigma_sets_cinter_dunion sp A" | Inter_cd: "(\i::nat. a i \ sigma_sets_cinter_dunion sp A) \ (\i. a i) \ sigma_sets_cinter_dunion sp A" | Union_cd: "(\i::nat. a i \ sigma_sets_cinter_dunion sp A) \ disjoint_family a \ (\i. a i) \ sigma_sets_cinter_dunion sp A" lemma sigma_sets_cinter_dunion_subset: "sigma_sets_cinter_dunion sp A \ sigma_sets_cinter sp A" proof safe fix x assume "x \ sigma_sets_cinter_dunion sp A" then show "x \ sigma_sets_cinter sp A" by induction (auto intro!: Union_c Inter_c) qed lemma sigma_sets_cinter_into_sp: assumes "A \ Pow sp" "x \ sigma_sets_cinter sp A" shows "x \ sp" using assms(2) by induction (use assms(1) subsetD in blast)+ lemma sigma_sets_cinter_dunion_into_sp: assumes "A \ Pow sp" "x \ sigma_sets_cinter_dunion sp A" shows "x \ sp" using assms(2) by induction (use assms(1) subsetD in blast)+ lemma sigma_sets_cinter_int: assumes "a \ sigma_sets_cinter sp A" "b \ sigma_sets_cinter sp A" shows "a \ b \ sigma_sets_cinter sp A" proof - have 1:"a \ b = (\i::nat. if i = 0 then a else b)" by auto show ?thesis unfolding 1 by(rule Inter_c,use assms in auto) qed lemma sigma_sets_cinter_dunion_int: assumes "a \ sigma_sets_cinter_dunion sp A" "b \ sigma_sets_cinter_dunion sp A" shows "a \ b \ sigma_sets_cinter_dunion sp A" proof - have 1:"a \ b = (\i::nat. if i = 0 then a else b)" by auto show ?thesis unfolding 1 by(rule Inter_cd,use assms in auto) qed lemma sigma_sets_cinter_un: assumes "a \ sigma_sets_cinter sp A" "b \ sigma_sets_cinter sp A" shows "a \ b \ sigma_sets_cinter sp A" proof - have 1:"a \ b = (\i::nat. if i = 0 then a else b)" by auto show ?thesis unfolding 1 by(rule Union_c,use assms in auto) qed text \ Measurable isomorphisms.\ definition measurable_isomorphic_map::"['a measure, 'b measure, 'a \ 'b] \ bool" where "measurable_isomorphic_map M N f \ bij_betw f (space M) (space N) \ f \ M \\<^sub>M N \ the_inv_into (space M) f \ N \\<^sub>M M" lemma measurable_isomorphic_map_sets_cong: assumes "sets M = sets M'" "sets N = sets N'" shows "measurable_isomorphic_map M N f \ measurable_isomorphic_map M' N' f" by(simp add: measurable_isomorphic_map_def sets_eq_imp_space_eq[OF assms(1)] sets_eq_imp_space_eq[OF assms(2)] measurable_cong_sets[OF assms] measurable_cong_sets[OF assms(2,1)]) lemma measurable_isomorphic_map_surj: assumes "measurable_isomorphic_map M N f" shows "f ` space M = space N" using assms by(auto simp: measurable_isomorphic_map_def bij_betw_def) lemma measurable_isomorphic_mapI: assumes "bij_betw f (space M) (space N)" "f \ M \\<^sub>M N" "the_inv_into (space M) f \ N \\<^sub>M M" shows "measurable_isomorphic_map M N f" using assms by(simp add: measurable_isomorphic_map_def) lemma measurable_isomorphic_map_byWitness: assumes "f \ M \\<^sub>M N" "g \ N \\<^sub>M M" "\x. x \ space M \ g (f x) = x" "\x. x \ space N \ f (g x) = x" shows "measurable_isomorphic_map M N f" proof - have *:"bij_betw f (space M) (space N)" using assms by(auto intro!: bij_betw_byWitness[where f'=g] dest:measurable_space) show ?thesis proof(rule measurable_isomorphic_mapI) have "the_inv_into (space M) f x = g x" if "x \ space N" for x by (metis * assms(2) assms(4) bij_betw_imp_inj_on measurable_space that the_inv_into_f_f) thus "the_inv_into (space M) f \ N \\<^sub>M M" using measurable_cong assms(2) by blast qed (simp_all add: * assms(1)) qed lemma measurable_isomorphic_map_restrict_space: assumes "f \ M \\<^sub>M N" "\A. A \ sets M \ f ` A \ sets N" "inj_on f (space M)" shows "measurable_isomorphic_map M (restrict_space N (f ` space M)) f" proof(rule measurable_isomorphic_mapI) show "bij_betw f (space M) (space (restrict_space N (f ` space M)))" by (simp add: assms(2,3) inj_on_imp_bij_betw) next show "f \ M \\<^sub>M restrict_space N (f ` space M)" by (simp add: assms(1) measurable_restrict_space2) next show "the_inv_into (space M) f \ restrict_space N (f ` space M) \\<^sub>M M" proof(rule measurableI) show "x \ space (restrict_space N (f ` space M)) \ the_inv_into (space M) f x \ space M" for x by (simp add: assms(2,3) the_inv_into_into) next fix A assume "A \ sets M" have "the_inv_into (space M) f -` A \ space (restrict_space N (f ` space M)) = f ` A" by (simp add: \A \ sets M\ assms(2,3) sets.sets_into_space the_inv_into_vimage) also note assms(2)[OF \A \ sets M\] finally show "the_inv_into (space M) f -` A \ space (restrict_space N (f ` space M)) \ sets (restrict_space N (f ` space M))" by (simp add: assms(2) sets_restrict_space_iff) qed qed lemma measurable_isomorphic_mapD': assumes "measurable_isomorphic_map M N f" shows "\A. A \ sets M \ f ` A \ sets N" "f \ M \\<^sub>M N" "\g. bij_betw g (space N) (space M) \ g \ N \\<^sub>M M \ (\x \ space M. g (f x) = x) \ (\x\ space N. f (g x) = x) \ (\A\sets N. g ` A \ sets M)" proof - have h:"bij_betw f (space M) (space N)" "f \ M \\<^sub>M N" "the_inv_into (space M) f \ N \\<^sub>M M" using assms by(simp_all add: measurable_isomorphic_map_def) show "f ` A \ sets N" if "A \ sets M" for A proof - have "f ` A = the_inv_into (space M) f -` A \ space N" using the_inv_into_vimage[OF bij_betw_imp_inj_on[OF h(1)] sets.sets_into_space[OF that]] by(simp add: bij_betw_imp_surj_on[OF h(1)]) also have "... \ sets N" using that h(3) by auto finally show ?thesis . qed show "f \ M \\<^sub>M N" using assms by(simp add: measurable_isomorphic_map_def) show "\g. bij_betw g (space N) (space M) \ g \ N \\<^sub>M M \ (\x \ space M. g (f x) = x) \ (\x\ space N. f (g x) = x) \ (\A\sets N. g ` A \ sets M)" proof(rule exI[where x="the_inv_into (space M) f"]) have *:"the_inv_into (space M) f ` A \ sets M" if "A \ sets N" for A proof - have "\x. x \ space M \ the_inv_into (space N) (the_inv_into (space M) f) x = f x" by (metis bij_betw_imp_inj_on bij_betw_the_inv_into h(1) h(2) measurable_space the_inv_into_f_f) from vimage_inter_cong[of "space M" _ f A,OF this] the_inv_into_vimage[OF bij_betw_imp_inj_on[OF bij_betw_the_inv_into[OF h(1)]] sets.sets_into_space[OF that]] bij_betw_imp_surj_on[OF bij_betw_the_inv_into[OF h(1)]] measurable_sets[OF h(2) that] show ?thesis by fastforce qed show "bij_betw (the_inv_into (space M) f) (space N) (space M) \ the_inv_into (space M) f \ N \\<^sub>M M \ (\x\space M. the_inv_into (space M) f (f x) = x) \ (\x\space N. f (the_inv_into (space M) f x) = x) \ (\A\sets N. the_inv_into (space M) f ` A \ sets M)" using bij_betw_the_inv_into[OF h(1)] by (meson * bij_betw_imp_inj_on f_the_inv_into_f_bij_betw h(1) h(3) the_inv_into_f_f) qed qed lemma measurable_isomorphic_map_inv: assumes "measurable_isomorphic_map M N f" shows "measurable_isomorphic_map N M (the_inv_into (space M) f)" using assms[simplified measurable_isomorphic_map_def] by(auto intro!: measurable_isomorphic_map_byWitness[where g=f] bij_betw_the_inv_into f_the_inv_into_f_bij_betw[of f] bij_betw_imp_inj_on the_inv_into_f_f) lemma measurable_isomorphic_map_comp: assumes "measurable_isomorphic_map M N f" and "measurable_isomorphic_map N L g" shows "measurable_isomorphic_map M L (g \ f)" proof - obtain f' g' where [measurable]: "f' \ N \\<^sub>M M" and hf:"\x. x\space M \ f' (f x) = x" "\x. x\space N \ f (f' x) = x" and [measurable]: "g' \ L \\<^sub>M N" and hg:"\x. x\space N \ g' (g x) = x" "\x. x\space L \ g (g' x) = x" using measurable_isomorphic_mapD'[OF assms(1)] measurable_isomorphic_mapD'[OF assms(2)] by metis have [measurable]: "f \ M \\<^sub>M N" "g \ N \\<^sub>M L" using assms by(auto simp: measurable_isomorphic_map_def) from hf hg measurable_space[OF \f \ M \\<^sub>M N\] measurable_space[OF \g' \ L \\<^sub>M N\] show ?thesis by(auto intro!: measurable_isomorphic_map_byWitness[where g="f'\g'"]) qed definition measurable_isomorphic::"['a measure, 'b measure] \ bool" (infixr "measurable'_isomorphic" 50) where "M measurable_isomorphic N \ (\f. measurable_isomorphic_map M N f)" lemma measurable_isomorphic_sets_cong: assumes "sets M = sets M'" "sets N = sets N'" shows "M measurable_isomorphic N \ M' measurable_isomorphic N'" using measurable_isomorphic_map_sets_cong[OF assms] by(auto simp: measurable_isomorphic_def) lemma measurable_isomorphicD: assumes "M measurable_isomorphic N" shows "\f g. f \ M \\<^sub>M N \ g \ N \\<^sub>M M \ (\x\space M. g (f x) = x) \ (\y\space N. f (g y) = y) \ (\A\sets M. f ` A \ sets N) \ (\A\sets N. g ` A \ sets M)" using assms measurable_isomorphic_mapD'[of M N] by (metis (mono_tags, lifting) measurable_isomorphic_def) lemma measurable_isomorphic_byWitness: assumes "f \ M \\<^sub>M N" "\x. x\space M \ g (f x) = x" and "g \ N \\<^sub>M M" "\y. y\space N \ f (g y) = y" shows "M measurable_isomorphic N" by(auto simp: measurable_isomorphic_def assms intro!: exI[where x = f] measurable_isomorphic_map_byWitness[where g=g]) lemma measurable_isomorphic_refl: "M measurable_isomorphic M" by(auto intro!: measurable_isomorphic_byWitness[where f=id and g=id]) lemma measurable_isomorphic_sym: assumes "M measurable_isomorphic N" shows "N measurable_isomorphic M" using assms measurable_isomorphic_map_inv[of M N] by(auto simp: measurable_isomorphic_def) lemma measurable_isomorphic_trans: assumes "M measurable_isomorphic N" and "N measurable_isomorphic L" shows "M measurable_isomorphic L" using assms measurable_isomorphic_map_comp[of M N _ L] by(auto simp: measurable_isomorphic_def) lemma measurable_isomorphic_empty: assumes "space M = {}" "space N = {}" shows "M measurable_isomorphic N" using assms by(auto intro!: measurable_isomorphic_byWitness[where f=undefined and g=undefined] simp: measurable_empty_iff) lemma measurable_isomorphic_empty1: assumes "space M = {}" "M measurable_isomorphic N" shows "space N = {}" using measurable_isomorphicD[OF assms(2)] by(auto simp: measurable_empty_iff[OF assms(1)]) lemma measurable_ismorphic_empty2: assumes "space N = {}" "M measurable_isomorphic N" shows "space M = {}" using measurable_isomorphic_sym[OF assms(2)] assms(1) by(simp add: measurable_isomorphic_empty1) lemma measurable_lift_product: assumes "\i. i \ I \ f i \ (M i) \\<^sub>M (N i)" shows "(\x i. if i \ I then f i (x i) else undefined) \ (\\<^sub>M i\I. M i) \\<^sub>M (\\<^sub>M i\I. N i)" using measurable_space[OF assms] by(auto intro!: measurable_PiM_single' simp: assms measurable_PiM_component_rev space_PiM PiE_iff) lemma measurable_isomorphic_map_lift_product: assumes "\i. i \ I \ measurable_isomorphic_map (M i) (N i) (h i)" shows "measurable_isomorphic_map (\\<^sub>M i\I. M i) (\\<^sub>M i\I. N i) (\x i. if i \ I then h i (x i) else undefined)" proof - obtain h' where "\i. i \ I \ h' i \ (N i) \\<^sub>M (M i)" "\i x. i \ I \ x\space (M i) \ h' i (h i x) = x" "\i x. i \ I \ x\space (N i) \ h i (h' i x) = x" using measurable_isomorphic_mapD'(3)[OF assms] by metis thus ?thesis by(auto intro!: measurable_isomorphic_map_byWitness[OF measurable_lift_product[of I h M N,OF measurable_isomorphic_mapD'(2)[OF assms]] measurable_lift_product[of I h' N M,OF \\i. i \ I \ h' i \ (N i) \\<^sub>M (M i)\]] simp: space_PiM PiE_iff extensional_def) qed lemma measurable_isomorphic_lift_product: assumes "\i. i \ I \ (M i) measurable_isomorphic (N i)" shows "(\\<^sub>M i\I. M i) measurable_isomorphic (\\<^sub>M i\I. N i)" proof - obtain h where "\i. i \ I \ measurable_isomorphic_map (M i) (N i) (h i)" using assms by(auto simp: measurable_isomorphic_def) metis thus ?thesis by(auto intro!: measurable_isomorphic_map_lift_product exI[where x="\x i. if i \ I then h i (x i) else undefined"] simp: measurable_isomorphic_def) qed text \\<^url>\https://math24.net/cantor-schroder-bernstein-theorem.html\\ lemma Schroeder_Bernstein_measurable': assumes "f ` (space M) \ sets N" "g ` (space N) \ sets M" and "measurable_isomorphic_map M (restrict_space N (f ` (space M))) f" and "measurable_isomorphic_map N (restrict_space M (g ` (space N))) g" shows "\h. measurable_isomorphic_map M N h" proof - have hset:"\A. A \ sets M \ f ` A \ sets (restrict_space N (f ` space M))" "\A. A \ sets N \ g ` A \ sets (restrict_space M (g ` space N))" and hfg[measurable]:"f \ M \\<^sub>M restrict_space N (f ` space M)" "g \ N \\<^sub>M restrict_space M (g ` space N)" using measurable_isomorphic_mapD'(1,2)[OF assms(3)] measurable_isomorphic_mapD'(1,2)[OF assms(4)] assms(1,2) by auto have hset2:"\A. A \ sets M \ f ` A \ sets N" "\A. A \ sets N \ g ` A \ sets M" and hfg2[measurable]: "f \ M \\<^sub>M N" "g \ N \\<^sub>M M" using sets.Int_space_eq2[OF assms(1)] sets.Int_space_eq2[OF assms(2)] sets_restrict_space_iff[of "f ` space M" N] sets_restrict_space_iff[of "g ` space N" M] hset measurable_restrict_space2_iff[of f M N] measurable_restrict_space2_iff[of g N M] hfg assms(1,2) by auto have bij1:"bij_betw f (space M) (f ` (space M))" "bij_betw g (space N) (g ` (space N))" using assms(3,4) by(auto simp: measurable_isomorphic_map_def space_restrict_space sets.Int_space_eq2[OF assms(1)] sets.Int_space_eq2[OF assms(2)]) obtain f' g' where hfg1'[measurable]: "f' \ restrict_space N (f ` (space M)) \\<^sub>M M" "g' \ restrict_space M (g ` (space N)) \\<^sub>M N" and hfg':"\x. x\space M \ f' (f x) = x" "\x. x\f ` space M \ f (f' x) = x" "\x. x\space N \ g' (g x) = x" "\x. x\g ` space N \ g (g' x) = x" "bij_betw f' (f ` space M) (space M)" "bij_betw g' (g ` space N) (space N)" using measurable_isomorphic_mapD'(3)[OF assms(3)] measurable_isomorphic_mapD'(3)[OF assms(4)] sets.Int_space_eq2[OF assms(1)] sets.Int_space_eq2[OF assms(2)] by (metis space_restrict_space) have hgfA:"(g \ f) ` A \ sets M" if "A \ sets M" for A using hset2(2)[OF hset2(1)[OF that]] by(simp add: image_comp) define An where "An \ (\n. ((g \ f)^^n) ` (space M - g ` (space N)))" define A where "A \ (\n\UNIV. An n)" have "An n \ sets M" for n proof(induction n) case 0 thus ?case using hset2[OF sets.top] by(simp add: An_def) next case ih:(Suc n) have "An (Suc n) = (g \ f) ` (An n)" by(auto simp add: An_def) thus ?case using hgfA[OF ih] by simp qed hence Asets:"A \ sets M" by(simp add: A_def) have Acompl:"space M - A \ g ` space N" proof - have "space M - A \ space M - An 0" by(auto simp: A_def) also have "... \ g ` space N" by(auto simp: An_def) finally show ?thesis . qed define h where "h \ (\x. if x \ A \ (- space M) then f x else g' x)" define h' where "h' \ (\x. if x \ f ` A then f' x else g x)" have xinA_iff:"x \ A \ h x \ f ` A" if "x \ space M" for x proof assume "h x \ f ` A" show "x \ A" proof(rule ccontr) assume "x \ A" then have "\n. x \ An n" by(auto simp: A_def) from this[of 0] have "x \ g ` (space N)" using that by(auto simp: An_def) have "g' x \ f ` A " using \h x \ f ` A\ \x \ A\ by (simp add: h_def that) hence "g (g' x) \ (g \ f) ` A" by auto hence "x \ (g \ f) ` A" using \x \ g ` (space N)\ by (simp add: hfg'(4)) then obtain n where "x \ (g \ f) ` (An n)" by(auto simp: A_def) hence "x \ An (Suc n)" by(auto simp: An_def) thus False using \\n. x \ An n\ by simp qed qed(simp add: h_def) show ?thesis proof(intro exI[where x=h] measurable_isomorphic_map_byWitness[where g=h']) have "{x \ space M. x \ A \ (- space M)} \ sets M" using sets.Int_space_eq2[OF Asets] Asets by simp moreover have "f \ restrict_space M {x. x \ A \ - space M} \\<^sub>M N" by (simp add: measurable_restrict_space1) moreover have "g' \ restrict_space M {x. x \ A \ (- space M)} \\<^sub>M N" proof - have "sets (restrict_space (restrict_space M (g ` space N)) {x. x \ A \ - space M}) = sets (restrict_space M (g ` space N \ {x. x \ A \ - space M}))" by(simp add: sets_restrict_restrict_space) also have "... = sets (restrict_space M (g ` space N \ {x. x \ space M - A}))" by (metis Compl_iff DiffE DiffI Un_iff) also have "... = sets (restrict_space M {x. x \ space M - A})" by (metis Acompl le_inf_iff mem_Collect_eq subsetI subset_antisym) also have "... = sets (restrict_space M {x. x \ A \ (- space M)})" by (metis Compl_iff DiffE DiffI Un_iff) finally have "sets (restrict_space (restrict_space M (g ` space N)) {x. x \ A \ - space M}) = sets (restrict_space M {x. x \ A \ - space M})" . from measurable_cong_sets[OF this refl] measurable_restrict_space1[OF hfg1'(2),of " {x. x \ A \ - space M}"] show ?thesis by auto qed ultimately show "h \ M \\<^sub>M N" by(simp add: h_def measurable_If_restrict_space_iff) next have "{x \ space N. x \ f ` A} \ sets N" using sets.Int_space_eq2[OF hset2(1)[OF Asets]] hset2(1)[OF Asets] by simp moreover have "f' \ restrict_space N {x. x \ f ` A} \\<^sub>M M" proof - have "sets (restrict_space (restrict_space N (f ` space M)) {x. x \ f ` A}) = sets (restrict_space N (f ` space M \ {x. x \ f ` A}))" by(simp add: sets_restrict_restrict_space) also have "... = sets (restrict_space N {x. x \ f ` A})" proof - have "f ` space M \ {x. x \ f ` A} = {x. x \ f ` A}" using sets.sets_into_space[OF Asets] by auto thus ?thesis by simp qed finally have "sets (restrict_space (restrict_space N (f ` space M)) {x. x \ f ` A}) = sets (restrict_space N {x. x \ f ` A})" . from measurable_cong_sets[OF this refl] measurable_restrict_space1[OF hfg1'(1),of "{x. x \ f ` A}"] show ?thesis by auto qed moreover have "g \ restrict_space N {x. x \ f ` A} \\<^sub>M M" by (simp add: measurable_restrict_space1) ultimately show "h' \ N \\<^sub>M M" by(simp add: h'_def measurable_If_restrict_space_iff) next fix x assume "x \ space M" then consider "x \ A" | "x \ space M - A" by auto thus "h' (h x) = x" proof cases case xa:2 hence "h x \ f ` A" using \x \ space M\ xinA_iff by blast thus ?thesis using Acompl hfg'(4) xa by(auto simp add: h_def h'_def) qed(simp add: h_def h'_def \x \ space M\ hfg'(1)) next fix x assume "x \ space N" then consider "x \ f ` A" | "x \ space N - f ` A" by auto thus "h (h' x) = x" proof cases case hx:1 hence "x \ f ` (space M)" using image_mono[OF sets.sets_into_space[OF Asets],of f] by auto have "h' x = f' x" using hx by(simp add: h'_def) also have "... \ A" using hx sets.sets_into_space[OF Asets] hfg'(1) by auto finally show ?thesis using hfg'(2)[OF \x \ f ` (space M)\] hx by(auto simp: h_def h'_def) next case hx:2 then have "h' x = g x" by(simp add: h'_def) also have "... \ A" proof(rule ccontr) assume "\ g x \ A" then have "g x \ A" by simp then obtain n where hg:"g x \ An n" by(auto simp: A_def) hence "0 < n" using hx by(auto simp: An_def) then obtain n' where [simp]:"n = Suc n'" using not0_implies_Suc by blast then have "g x \ g ` f ` An n'" using hg by(auto simp: An_def) hence "x \ f ` An n'" using inj_on_image_mem_iff[OF bij_betw_imp_inj_on[OF bij1(2)] \x \ space N\,of "f ` An n'"] sets.sets_into_space[OF \An n' \ sets M\] measurable_space[OF hfg2(1)] by auto also have "... \ f ` A" by(auto simp: A_def) finally show False using hx by simp qed finally show ?thesis using hx hfg'(3)[OF \x \ space N\] measurable_space[OF hfg2(2) \x \ space N\] by(auto simp: h_def h'_def) qed qed qed lemma Schroeder_Bernstein_measurable: assumes "f \ M \\<^sub>M N" "\A. A \ sets M \ f ` A \ sets N" "inj_on f (space M)" and "g \ N \\<^sub>M M" "\A. A \ sets N \ g ` A \ sets M" "inj_on g (space N)" shows "\h. measurable_isomorphic_map M N h" using Schroeder_Bernstein_measurable'[OF assms(2)[OF sets.top] assms(5)[OF sets.top] measurable_isomorphic_map_restrict_space[OF assms(1-3)] measurable_isomorphic_map_restrict_space[OF assms(4-6)]] by simp lemma measurable_isomorphic_from_embeddings: assumes "M measurable_isomorphic (restrict_space N B)" "N measurable_isomorphic (restrict_space M A)" and "A \ sets M" "B \ sets N" shows "M measurable_isomorphic N" proof - obtain f g where fg:"measurable_isomorphic_map M (restrict_space N B) f" "measurable_isomorphic_map N (restrict_space M A) g" using assms(1,2) by(auto simp: measurable_isomorphic_def) have [simp]:"f ` space M = B" "g ` space N = A" using measurable_isomorphic_map_surj[OF fg(1)] measurable_isomorphic_map_surj[OF fg(2)] sets.sets_into_space[OF assms(3)] sets.sets_into_space[OF assms(4)] by(auto simp: space_restrict_space) obtain h where "measurable_isomorphic_map M N h" using Schroeder_Bernstein_measurable'[of f M N g] assms(3,4) fg by auto thus ?thesis by(auto simp: measurable_isomorphic_def) qed lemma measurable_isomorphic_antisym: assumes "B measurable_isomorphic (restrict_space C c)" "A measurable_isomorphic (restrict_space B b)" and "c \ sets C" "b \ sets B" "C measurable_isomorphic A" shows "C measurable_isomorphic B" by(rule measurable_isomorphic_from_embeddings[OF measurable_isomorphic_trans[OF assms(5,2)] assms(1) assms(3,4)]) lemma countable_infinite_isomorphisc_to_nat_index: assumes "countable I" and "infinite I" shows "(\\<^sub>M x\I. M) measurable_isomorphic (\\<^sub>M (x::nat)\UNIV. M)" proof(rule measurable_isomorphic_byWitness[where f="\x n. x (from_nat_into I n)" and g="\x. \i\I. x (to_nat_on I i)"]) show "(\x n. x (from_nat_into I n)) \ (\\<^sub>M x\I. M) \\<^sub>M (\\<^sub>M (x::nat)\UNIV. M)" by(auto intro!: measurable_PiM_single' measurable_component_singleton[OF from_nat_into[OF infinite_imp_nonempty[OF assms(2)]]]) (simp add: PiE_iff infinite_imp_nonempty space_PiM from_nat_into[OF infinite_imp_nonempty[OF assms(2)]]) next show "(\x. \i\I. x (to_nat_on I i)) \ (\\<^sub>M (x::nat)\UNIV. M) \\<^sub>M (\\<^sub>M x\I. M)" by(auto intro!: measurable_PiM_single') next show "x \ space (\\<^sub>M x\I. M) \ (\i\I. x (from_nat_into I (to_nat_on I i))) = x" for x by (simp add: assms(1) restrict_ext space_PiM) next show "y \ space (Pi\<^sub>M UNIV (\x. M)) \ (\n. (\i\I. y (to_nat_on I i)) (from_nat_into I n)) = y" for y by (simp add: assms(1) assms(2) from_nat_into infinite_imp_nonempty) qed lemma PiM_PiM_isomorphic_to_PiM: "(\\<^sub>M i\I. \\<^sub>M j\J. M i j) measurable_isomorphic (\\<^sub>M (i,j)\I\J. M i j)" proof(rule measurable_isomorphic_byWitness[where f="\x (i,j). if (i,j) \ I \ J then x i j else undefined" and g="\x i j. if i \ I then undefined j else if j \ J then undefined else x (i,j)"]) have [simp]: "(\\. \ a b) \ (\\<^sub>M i\I. \\<^sub>M j\J. M i j) \\<^sub>M M a b" if "a \ I" "b \ J" for a b using measurable_component_singleton[OF that(1),of "\i. \\<^sub>M j\J. M i j"] measurable_component_singleton[OF that(2),of "M a"] by auto show "(\x (i, j). if (i, j) \ I \ J then x i j else undefined) \ (\\<^sub>M i\I. \\<^sub>M j\J. M i j) \\<^sub>M (\\<^sub>M (i,j)\I\J. M i j)" apply(rule measurable_PiM_single') apply auto[1] apply(auto simp: PiE_def Pi_def space_PiM extensional_def;meson) done next have [simp]: "(\\. \ (i, j)) \ Pi\<^sub>M (I \ J) (\(i, j). M i j) \\<^sub>M M i j" if "i \ I" "j \ J" for i j using measurable_component_singleton[of "(i,j)" "I \ J" "\(i, j). M i j"] that by auto show "(\x i j. if i \ I then undefined j else if j \ J then undefined else x (i, j)) \ (\\<^sub>M (i,j)\I\J. M i j) \\<^sub>M (\\<^sub>M i\I. \\<^sub>M j\J. M i j)" by(auto intro!: measurable_PiM_single') (simp_all add: PiE_iff space_PiM extensional_def) next show "x \ space (\\<^sub>M i\I. \\<^sub>M j\J. M i j) \ (\i j. if i \ I then undefined j else if j \ J then undefined else case (i, j) of (i, j) \ if (i, j) \ I \ J then x i j else undefined) = x" for x by standard+ (auto simp: space_PiM PiE_def Pi_def extensional_def) next show "y \ space (\\<^sub>M (i,j)\I\J. M i j) \ (\(i, j). if (i, j) \ I \ J then if i \ I then undefined j else if j \ J then undefined else y (i, j) else undefined) = y" for y by standard+ (auto simp: space_PiM PiE_def Pi_def extensional_def) qed lemma measurable_isomorphic_map_sigma_sets: assumes "sets M = sigma_sets (space M) U" "measurable_isomorphic_map M N f" shows "sets N = sigma_sets (space N) ((`) f ` U)" proof - from measurable_isomorphic_mapD'[OF assms(2)] obtain g where h: "\A. A \ sets M \ f ` A \ sets N" "f \ M \\<^sub>M N" "bij_betw g (space N) (space M)" "g \ N \\<^sub>M M" "\x. x\space M \ g (f x) = x" "\x. x\space N \ f (g x) = x" "\A. A\sets N \ g ` A \ sets M" by metis interpret s: sigma_algebra "space N" "sigma_sets (space N) ((`) f ` U)" by(auto intro!: sigma_algebra_sigma_sets) (metis assms(1) h(2) measurable_space sets.sets_into_space sigma_sets_superset_generator subsetD) show ?thesis proof safe fix x assume "x \ sets N" from h(7)[OF this] assms(1) have "g ` x \ sigma_sets (space M) U" by simp hence "f ` (g ` x) \ sigma_sets (space N) ((`) f ` U)" proof induction case h:(Compl a) have "f ` (space M - a) = f ` (space M) - f ` a" by(rule inj_on_image_set_diff[where C="space M"], insert assms h) (auto simp: measurable_isomorphic_map_def bij_betw_def sets.sets_into_space) with h show ?case by (metis assms(2) measurable_isomorphic_map_surj s.Diff s.top) qed (auto simp: image_UN) moreover have "f ` (g ` x) = x" using sets.sets_into_space[OF \x \ sets N\] h(6) by(fastforce simp: image_def) ultimately show "x \ sigma_sets (space N) ((`) f ` U)" by simp next interpret s': sigma_algebra "space M" "sigma_sets (space M) U" by(simp add: assms(1)[symmetric] sets.sigma_algebra_axioms) have 1:"\x. x \ U \ x \ space M" by (simp add: s'.sets_into_space) fix x assume assm:"x \ sigma_sets (space N) ((`) f ` U)" then show "x \ sets N" by induction (auto simp: assms(1) h(1)) qed qed end \ No newline at end of file diff --git a/thys/Standard_Borel_Spaces/ROOT b/thys/Standard_Borel_Spaces/ROOT --- a/thys/Standard_Borel_Spaces/ROOT +++ b/thys/Standard_Borel_Spaces/ROOT @@ -1,13 +1,14 @@ chapter AFP session "Standard_Borel_Spaces" = "HOL-Probability" + options [timeout = 600] theories "Lemmas_StandardBorel" - "Set_Based_Metric_Space" "Set_Based_Metric_Product" + "Set_Based_Metric_Space" + "Set_Based_Metric_Product" "Abstract_Metrizable_Topology" "StandardBorel" "Space_of_Continuous_Maps" document_files "root.tex" "root.bib" diff --git a/thys/Standard_Borel_Spaces/Space_of_Continuous_Maps.thy b/thys/Standard_Borel_Spaces/Space_of_Continuous_Maps.thy --- a/thys/Standard_Borel_Spaces/Space_of_Continuous_Maps.thy +++ b/thys/Standard_Borel_Spaces/Space_of_Continuous_Maps.thy @@ -1,444 +1,446 @@ (* Title: Space_of_Continuous_Maps.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) subsection \Example: The Metric Space of Continuous Functions\ theory Space_of_Continuous_Maps imports "StandardBorel" begin definition cmaps :: "['a topology, 'b topology] \ ('a \ 'b) set" where "cmaps X Y \ {f. f \ extensional (topspace X) \ continuous_map X Y f}" definition cmaps_dist :: "['a topology, 'b topology, 'b \ 'b \ real, 'a \ 'b, 'a \ 'b] \ real" where "cmaps_dist X Y d f g \ if f \ cmaps X Y \ g \ cmaps X Y \ topspace X \ {} then (\ {d (f x) (g x) |x. x \ topspace X}) else 0" lemma cmaps_X_empty: assumes "topspace X = {}" shows "cmaps X Y = {\x. undefined}" - by(auto simp: cmaps_def assms) + by(auto simp: cmaps_def assms simp flip: null_topspace_iff_trivial) lemma cmaps_Y_empty: assumes "topspace X \ {}" "topspace Y = {}" shows "cmaps X Y = {}" - by(auto simp: cmaps_def assms continuous_map_def) + by(auto simp: cmaps_def assms continuous_map_def Pi_def simp flip: null_topspace_iff_trivial) lemma cmaps_dist_X_empty: assumes "topspace X = {}" shows "cmaps_dist X = (\Y d f g. 0)" by standard+ (auto simp: cmaps_dist_def assms) lemma cmaps_dist_Y_empty: assumes "topspace X \ {}" "topspace Y = {}" shows "cmaps_dist X Y = (\d f g. 0)" by standard+ (auto simp: cmaps_dist_def assms cmaps_Y_empty) subsubsection \Definition\ context metric_set begin context fixes K and X :: "'b topology" assumes m_bounded :"\x y. dist x y \ K" begin lemma cm_dest: shows "\f x. f \ (cmaps X mtopology) \ x \ topspace X \ f x \ S" and "\f x. f \ (cmaps X mtopology) \ x \ topspace X \ f x = undefined" and "\f. f \ (cmaps X mtopology) \ continuous_map X mtopology f" using continuous_map_image_subset_topspace[of X mtopology,simplified mtopology_topspace] by(auto simp: cmaps_def extensional_def) lemma cmaps_dist_bdd_above[simp]: "bdd_above {dist (f x) (g x) |x. x \ A}" using m_bounded by(auto intro!: bdd_aboveI[where M=K]) lemma cmaps_metric_set: "metric_set (cmaps X mtopology) (cmaps_dist X mtopology dist)" proof(cases "topspace X = {}") case True then show ?thesis by(simp add: singleton_metric cmaps_X_empty cmaps_dist_X_empty) next case h:False then have nen[simp]:"{dist (f x) (g x)|x. x \ topspace X} \ {}" for f g by auto show ?thesis proof show "(cmaps_dist X mtopology dist) f g \ 0" for f g - by(auto simp: cmaps_dist_def dist_geq0 intro!: cSup_upper2[where x="dist _ _"]) + by(auto simp: cmaps_dist_def dist_geq0 intro!: cSup_upper2[where x="dist _ _"] + simp flip: null_topspace_iff_trivial) next fix f g assume "f \ (cmaps X mtopology)" then show "(cmaps_dist X mtopology dist) f g = 0" by(simp add: cmaps_dist_def) next show "(cmaps_dist X mtopology dist) f g = (cmaps_dist X mtopology dist) g f" for f g by(simp add: cmaps_dist_def dist_sym) next fix f g assume fg:"f \ (cmaps X mtopology)" "g \ (cmaps X mtopology)" show "f = g \ (cmaps_dist X mtopology dist) f g = 0" proof safe have "{dist (g x) (g x) |x. x \ topspace X} = {0}" using h by fastforce thus "(cmaps_dist X mtopology dist) g g = 0" by(simp add: cmaps_dist_def) next assume "(cmaps_dist X mtopology dist) f g = 0" with fg h have "\ {dist (f x) (g x)|x. x \ topspace X} \ 0" by(auto simp: cmaps_dist_def) hence "\x. x \ topspace X \ dist (f x) (g x) \ 0" by(auto simp: cSup_le_iff[OF nen]) from antisym[OF this dist_geq0] have fgeq:"\x. x \ topspace X \ f x = g x" using dist_0[OF cm_dest(1)[OF fg(1)] cm_dest(1)[OF fg(2)]] by auto show "f = g" proof fix x show "f x = g x" by(cases "x \ topspace X",insert fg) (auto simp: cm_dest fgeq) qed qed next fix f g h assume fgh: "f \ (cmaps X mtopology)" "g \ (cmaps X mtopology)" "h \ (cmaps X mtopology)" show "(cmaps_dist X mtopology dist) f h \ (cmaps_dist X mtopology dist) f g + (cmaps_dist X mtopology dist) g h" (is "?lhs \ ?rhs") proof - have bdd1:"bdd_above {dist (f x) (g x) + dist (g x) (h x) | x. x \ topspace X}" using add_mono[OF m_bounded m_bounded] by(auto simp: bdd_above_def intro!: exI[where x="K + K"]) have nen1:"{dist (f x) (g x) + dist (g x) (h x) |x. x \ topspace X} \ {}" using h by auto have "?lhs \ (\ {dist (f x) (g x) + dist (g x) (h x)|x. x \ topspace X})" proof - { fix x assume "x \ topspace X" hence "\z. (\x. z = dist (f x) (g x) + dist (g x) (h x) \ x \ topspace X) \ dist (f x) (h x) \ z" by(auto intro!: exI[where x="dist (f x) (g x) + dist (g x) (h x)"] exI[where x=x] dist_tr cm_dest fgh) } thus ?thesis - by(auto simp: cmaps_dist_def fgh h intro!: cSup_mono bdd1) + by(auto simp: cmaps_dist_def fgh h intro!: cSup_mono bdd1 simp flip: null_topspace_iff_trivial) qed also have "... \ ?rhs" by(auto simp: cSup_le_iff[OF nen1 bdd1] cmaps_dist_def fgh h intro!: add_mono cSup_upper) finally show ?thesis . qed qed qed end end subsubsection \Topology of Uniform Convergence\ locale topology_of_uniform_convergence_c = complete_metric_set + compact_metrizable X for X + fixes K assumes d_bounded: "\x y. dist x y \ K" begin lemmas cm_dist_bdd_above[simp] = cmaps_dist_bdd_above[OF d_bounded] abbreviation "cm \ cmaps X mtopology" abbreviation "cm_dist \ cmaps_dist X mtopology dist" lemma cm_complete_metric_set: "complete_metric_set cm cm_dist" proof - interpret m: metric_set cm cm_dist by(auto intro!: cmaps_metric_set d_bounded) show ?thesis proof obtain dx where dx: "compact_metric_set (topspace X) dx" "metric_set.mtopology (topspace X) dx = X" by(rule compact_metric) interpret dx: compact_metric_set "topspace X" dx by fact fix fn assume h:"m.Cauchy_inS fn" note fn_cm = m.Cauchy_inS_dest1[OF this] have c:"\N. \n\N. \m\N. \x\topspace X. dist (fn n x) (fn m x) < e" if e:"e > 0" for e proof - obtain N where N:"\n m. n \ N \ m \ N \ cm_dist (fn n) (fn m) < e" by(metis e h m.Cauchy_inS_def) show ?thesis proof(safe intro!: exI[where x=N]) fix n m x assume nmx: "n \ N" "m \ N" "x \ topspace X" then have "dist (fn n x) (fn m x) \ cm_dist (fn n) (fn m)" using fn_cm by(auto simp: cmaps_dist_def intro!: cSup_upper) also have "... < e" by(auto intro!: N nmx) finally show "dist (fn n x) (fn m x) < e" . qed qed have "convergent_inS (\n. fn n x)" if x:"x \ topspace X" for x - by(rule convergence,auto simp: Cauchy_inS_def,insert c x fn_cm) (auto simp: cmaps_def continuous_map_def mtopology_topspace, meson) + by (rule convergence,auto simp: Cauchy_inS_def,insert c x fn_cm) + (auto simp: cmaps_def continuous_map_def mtopology_topspace, blast, meson) then obtain f where f:"\x. x \ topspace X \ converge_to_inS (\n. fn n x) (f x)" by(auto simp: convergent_inS_def) metis define f' where "f' \ (\x\topspace X. f x)" have f':"\x. x \ topspace X \ converge_to_inS (\n. fn n x) (f' x)" using f by(auto simp: f'_def) have cu:"converges_uniformly (topspace X) S dist fn f'" unfolding converges_uniformly_def[OF dx.metric_set_axioms metric_set_axioms] proof safe fix e :: real assume e:"0 < e" obtain N where N: "\n m x. n\N \ m\N \ x\topspace X \ dist (fn n x) (fn m x) < e / 2" by(metis c[OF half_gt_zero[OF e]]) show "\N. \n\N. \x\topspace X. dist (fn n x) (f' x) < e" proof(rule ccontr) assume "\N. \n\N. \x\topspace X. dist (fn n x) (f' x) < e" with N obtain n x where nx: "n \ N" "x \ topspace X" "e \ dist (fn n x) (f' x)" by (meson linorder_le_less_linear) from f'[OF this(2)] half_gt_zero[OF e] obtain N' where N':"\n. n \ N' \ dist (fn n x) (f' x) < e / 2" by(metis converge_to_inS_def2) define N0 where "N0 \ max N N'" have N0 : "N0 \ N" "N0 \ N'" by(auto simp: N0_def) have "e \ dist (fn n x) (f' x)" by fact also have "... \ dist (fn n x) (fn N0 x) + dist (fn N0 x) (f' x)" using f'[OF nx(2)] by(auto intro!: dist_tr simp: converge_to_inS_def) also have "... < e" using N[OF nx(1) N0(1) nx(2)] N'[OF N0(2)] by auto finally show False .. qed qed(use f' converge_to_inS_def in auto) show "m.convergent_inS fn" unfolding m.convergent_inS_def m.converge_to_inS_def2 proof(safe intro!: exI[where x=f']) have "continuous_map dx.mtopology mtopology f'" using fn_cm by(auto intro!: converges_uniformly_continuous[OF dx.metric_set_axioms metric_set_axioms _ cu] simp: cmaps_def,auto simp: dx) thus f'_cm:"f' \ cm" by(auto simp: cmaps_def dx f'_def) fix e :: real assume e:"0 < e" obtain N where N:"\n x. n \ N \ x \ topspace X \ dist (fn n x) (f' x) < e / 2" by(metis half_gt_zero[OF e] cu[simplified converges_uniformly_def[OF dx.metric_set_axioms metric_set_axioms]]) show "\N. \n\N. cm_dist (fn n) f' < e" proof(safe intro!: exI[where x=N]) fix n assume n:"N \ n" have "cm_dist (fn n) f' \ e / 2" proof(cases "topspace X = {}") case True then show ?thesis by(auto simp: order.strict_implies_order[OF e] cmaps_X_empty cmaps_dist_X_empty) next case False then have 1:"{dist (fn n x) (f' x) |x. x \ topspace X} \ {}" by auto hence "cm_dist (fn n) f' = (\ {dist (fn n x) (f' x) |x. x \ topspace X})" by(auto simp: f'_cm fn_cm cmaps_dist_def) also have "... \ e / 2" by(simp only: cSup_le_iff[OF 1,simplified]) (insert N[OF n], auto intro!: order.strict_implies_order) finally show ?thesis . qed also have "... < e" using e by simp finally show "cm_dist (fn n) f' < e" . qed qed(use fn_cm in auto) qed qed end locale topology_of_uniform_convergence = polish_metric_set + compact_metrizable X for X + fixes K assumes d_bounded: "\x y. dist x y \ K" begin sublocale topology_of_uniform_convergence_c by (simp add: compact_metrizable_axioms complete_metric_set_axioms d_bounded topology_of_uniform_convergence_c_axioms_def topology_of_uniform_convergence_c_def) lemma cm_polish_metric_set: "polish_metric_set cm cm_dist" proof - consider "topspace X = {}" | "topspace X \ {}" "S = {}" | "topspace X \ {}" "S \ {}" by auto thus ?thesis proof cases case 1 then show ?thesis by(simp add: singleton_metric_polish cmaps_X_empty cmaps_dist_X_empty) next case 2 then show ?thesis by(simp add: empty_metric_polish cmaps_Y_empty[of _ mtopology,simplified mtopology_topspace] cmaps_dist_Y_empty[of _ mtopology,simplified mtopology_topspace]) next case XS_nem:3 interpret m: complete_metric_set cm cm_dist by(rule cm_complete_metric_set) show ?thesis proof obtain dx where dx: "compact_metric_set (topspace X) dx" "metric_set.mtopology (topspace X) dx = X" by(rule compact_metric) interpret dx: compact_metric_set "topspace X" dx by fact have "\B. finite B \ B \ topspace X \ topspace X = (\a\B. dx.open_ball a (1 / Suc m))" for m using dx.totally_boundedSD[OF dx.totally_bounded,of "1 / Suc m"] by fastforce then obtain Xm where Xm: "\m. finite (Xm m)" "\m. (Xm m) \ topspace X" "\m. topspace X = (\a\Xm m. dx.open_ball a (1 / Suc m))" by metis have Xm_nem:"\m. (Xm m) \ {}" - using XS_nem Xm(3) by auto + using XS_nem Xm(3) by fastforce define xmk where "xmk \ (\m. from_nat_into (Xm m))" define km where "km \ (\m. card (Xm m))" have km_pos:"km m > 0" for m by(simp add: km_def card_gt_0_iff Xm Xm_nem) have xmk_bij: "bij_betw (xmk m) {.. Xm m" for m i by (simp add: Xm_nem from_nat_into xmk_def) have "\U. countable U \ \ U = S \ (\u\U. diam u < 1 / (Suc l))" for l by(rule Lindelof_diam) auto then obtain U where U: "\l. countable (U l)" "\l. (\ (U l)) = S" "\l u. u \ U l \ diam u < 1 / Suc l" by metis have Ul_nem: "U l \ {}" for l using XS_nem U(2) by auto define uli where "uli \ (\l. from_nat_into (U l))" have uli_into:"uli l i \ U l" for l i by (simp add: Ul_nem from_nat_into uli_def) hence uli_diam: "diam (uli l i) < 1 / Suc l" for l i using U(3) by auto have uli_un:"S = (\i. uli l i)" for l by(auto simp: range_from_nat_into[OF Ul_nem[of l] U(1)] uli_def U) define Cmn where "Cmn \ (\m n. {f \ cm. \x\topspace X. \y\topspace X. dx x y < 1 / (Suc m) \ dist (f x) (f y) < 1 / Suc n})" define fmnls where "fmnls \ (\m n l s. SOME f. f \ Cmn m n \ (\j uli l (s j)))" define Dmnl where "Dmnl \ (\m n l. {fmnls m n l s |s. s \ {..\<^sub>E UNIV \ (\f \ Cmn m n. (\j uli l (s j))) })" have in_Dmnl: "fmnls m n l s \ Dmnl m n l" if "s\{..\<^sub>E UNIV" "f\ Cmn m n" "\j uli l (s j)"for m n l s f using Dmnl_def that by blast define Dmn where "Dmn \ (\m n. \l. Dmnl m n l)" have Dmn_subset: "Dmn m n \ Cmn m n" for m n proof - have "Dmnl m n l \ Cmn m n" for l by(auto simp: Dmnl_def fmnls_def someI[of "\f. f \ Cmn m n \ (\j uli l (_ j))"]) thus ?thesis by(auto simp: Dmn_def) qed have c_Dmn: "countable (Dmn m n)" for m n proof - have "countable (Dmnl m n l)" for l proof - have 1:"Dmnl m n l \ (\s. fmnls m n l s) ` ({..\<^sub>E UNIV)" by(auto simp: Dmnl_def) have "countable ..." by(auto intro!: countable_PiE) with 1 show ?thesis using countable_subset by blast qed thus ?thesis by(auto simp: Dmn_def) qed have claim: "\g\Dmn m n. \y\Xm m. dist (f y) (g y) < e" if f:"f \ Cmn m n" and e:"e > 0" for f m n e proof - obtain l where l:"1 / Suc l < e" using e nat_approx_posE by blast define s where "s \ (\i\{.. uli l j)" have s1:"s\{..\<^sub>E UNIV" by(simp add: s_def) have s2:"\i uli l (s i)" proof - fix i have "f (xmk m i) \ uli l (SOME j. f (xmk m i) \ uli l j)" for i proof(rule someI_ex) have "xmk m i \ topspace X" using Xm(2) xmk_into by auto hence "f (xmk m i) \ S" using f by(auto simp: Cmn_def cmaps_def continuous_map_def mtopology_topspace) thus "\x. f (xmk m i) \ uli l x" using uli_un by auto qed thus ?thesis by (auto simp: s_def) qed have fmnls:"fmnls m n l s \ Cmn m n \ (\j uli l (s j))" by(simp add: fmnls_def,rule someI[where x=f],auto simp: s2 f) show "\g\Dmn m n. \y\Xm m. dist (f y) (g y) < e" proof(safe intro!: bexI[where x="fmnls m n l s"]) fix y assume y:"y \ Xm m" then obtain i where i:"i < km m" "xmk m i = y" by (meson xmk_bij[of m] bij_betw_iff_bijections lessThan_iff) have "f y \ uli l (s i)" "fmnls m n l s y \ uli l (s i)" using i(1) s2 fmnls by(auto simp: i(2)[symmetric]) moreover have "f y \ S" "fmnls m n l s y \ S" using f fmnls y Xm(2)[of m] by(auto simp: Cmn_def cmaps_def continuous_map_def mtopology_topspace) ultimately have "ennreal (dist (f y) (fmnls m n l s y)) \ diam (uli l (s i))" by(auto intro!: diam_is_sup) also have "... < ennreal (1 / Suc l)" by(rule uli_diam) also have "... < ennreal e" using l e by(auto intro!: ennreal_lessI) finally show "dist (f y) (fmnls m n l s y) < e" by(simp add: ennreal_less_iff[OF dist_geq0]) qed(use in_Dmnl[OF s1 f s2] Dmn_def in auto) qed show "\U. countable U \ m.dense_set U" unfolding m.dense_set_def2 proof(safe intro!: exI[where x="\n. (\m. Dmn m n)"]) fix f and e :: real assume h:"f \ cm" "0 < e" then obtain n where n:"1 / Suc n < e / 4" by (metis zero_less_divide_iff zero_less_numeral nat_approx_posE) have "\m. \l\ m. f \ Cmn l n" proof - have "uniform_continuous_map (topspace X) dx S dist f" using h by(auto intro!: dx.continuous_map_is_uniform[OF metric_set_axioms] simp: cmaps_def dx) then obtain d where d:"d > 0" "\x y. x\topspace X \ y\topspace X \ dx x y < d \ dist (f x) (f y) < 1 / (Suc n)" by(auto simp: uniform_continuous_map_def[OF dx.metric_set_axioms metric_set_axioms]) (metis less_add_same_cancel2 linorder_neqE_linordered_idom of_nat_Suc of_nat_less_0_iff zero_less_divide_1_iff zero_less_one) then obtain m where m:"1 / Suc m < d" using nat_approx_posE by blast have l: "l \ m \ 1 / Suc l \ 1 / Suc m" for l by (simp add: frac_le) show ?thesis using d(2)[OF _ _ order.strict_trans[OF _ order.strict_trans1[OF l m]]] by(auto simp: Cmn_def h) qed then obtain m where m:"f \ Cmn m n" by auto obtain g where g:"g\Dmn m n" "\y. y\Xm m \ dist (f y) (g y) < e / 4" by (metis claim[OF m] h(2) zero_less_divide_iff zero_less_numeral) have "\n m. \g\Dmn m n. cm_dist f g < e" proof(rule exI[where x=n]) show "\m. \g\Dmn m n. cm_dist f g < e" proof(intro exI[where x=m] bexI[OF _ g(1)]) have g_cm:"g \ cm" using g(1) Dmn_subset[of m n] by(auto simp: Cmn_def) hence "cm_dist f g = (\ {dist (f x) (g x) |x. x \ topspace X})" - by(auto simp: cmaps_dist_def h XS_nem) + by(auto simp: cmaps_dist_def h XS_nem simp flip: null_topspace_iff_trivial) also have "... \ 3 * e / 4" proof - have 1:"{dist (f x) (g x) |x. x \ topspace X} \ {}" using XS_nem by auto have 2:"dist (f x) (g x) \ 3 * e / 4" if x:"x \ topspace X" for x proof - obtain y where y:"y \ Xm m" "x \ dx.open_ball y (1 / real (Suc m))" using Xm(3) x by auto hence ytop:"y \ topspace X" using Xm(2) by auto have "dist (f x) (g x) \ dist (f x) (f y) + dist (f y) (g x)" using x g_cm h(1) ytop by(auto intro!: dist_tr simp: cmaps_def continuous_map_def mtopology_topspace) also have "... \ dist (f x) (f y) + dist (f y) (g y) + dist (g y) (g x)" using x g_cm h(1) ytop by(auto intro!: dist_tr simp: cmaps_def continuous_map_def mtopology_topspace) also have "... \ e / 4 + e / 4 + e / 4" proof - have dxy: "dx x y < 1 / Suc m" "dx y x < 1 / Suc m" using dx.open_ballD[OF y(2)] by(auto simp: dx.dist_sym) hence "dist (f x) (f y) < 1 / (Suc n)" "dist (g y) (g x) < 1 / (Suc n)" using m x ytop g Dmn_subset[of m n] by(auto simp: Cmn_def) hence "dist (f x) (f y) < e / 4" "dist (g y) (g x) < e / 4" using n by auto thus ?thesis using g(2)[OF y(1)] by auto qed finally show "dist (f x) (g x) \ 3 * e / 4" by simp qed show ?thesis using 2 by(auto simp only: cSup_le_iff[OF 1,simplified]) qed also have "... < e" using h by auto finally show "cm_dist f g < e" . qed qed thus "\y\\n m. Dmn m n. cm_dist f y < e" by auto qed(use Dmn_subset c_Dmn Cmn_def in auto) qed qed qed end end \ No newline at end of file