new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
authorpaulson <lp15@cam.ac.uk>
Mon Mar 18 15:35:34 2019 +0000 (2 months ago)
changeset 69918eddcc7c726f3
parent 69917 66c4567664b5
child 69921 5f67c5e457e3
child 69922 4a9167f377b0
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Analysis/Cartesian_Space.thy
src/HOL/Analysis/Continuous_Extension.thy
src/HOL/Analysis/Elementary_Metric_Spaces.thy
src/HOL/Analysis/Elementary_Normed_Spaces.thy
src/HOL/Analysis/Finite_Product_Measure.thy
src/HOL/Analysis/Function_Topology.thy
src/HOL/Analysis/Homotopy.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Winding_Numbers.thy
src/HOL/Library/Set_Idioms.thy
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Sun Mar 17 21:26:42 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Mon Mar 18 15:35:34 2019 +0000
     1.3 @@ -403,8 +403,12 @@
     1.4       \<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
     1.5  by (simp add: closedin_subtopology) blast
     1.6  
     1.7 -
     1.8 -subsection \<open>The standard Euclidean topology\<close>
     1.9 +lemma openin_trans_full:
    1.10 +   "\<lbrakk>openin (subtopology X U) S; openin X U\<rbrakk> \<Longrightarrow> openin X S"
    1.11 +  by (simp add: openin_open_subtopology)
    1.12 +
    1.13 +
    1.14 +subsection \<open>The canonical topology from the underlying type class\<close>
    1.15  
    1.16  abbreviation%important euclidean :: "'a::topological_space topology"
    1.17    where "euclidean \<equiv> topology open"
    1.18 @@ -1269,6 +1273,144 @@
    1.19    by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures)
    1.20  
    1.21  
    1.22 +subsection\<open>Locally finite collections\<close>
    1.23 +
    1.24 +definition locally_finite_in
    1.25 +  where
    1.26 + "locally_finite_in X \<A> \<longleftrightarrow>
    1.27 +        (\<Union>\<A> \<subseteq> topspace X) \<and>
    1.28 +        (\<forall>x \<in> topspace X. \<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}})"
    1.29 +
    1.30 +lemma finite_imp_locally_finite_in:
    1.31 +   "\<lbrakk>finite \<A>; \<Union>\<A> \<subseteq> topspace X\<rbrakk> \<Longrightarrow> locally_finite_in X \<A>"
    1.32 +  by (auto simp: locally_finite_in_def)
    1.33 +
    1.34 +lemma locally_finite_in_subset:
    1.35 +  assumes "locally_finite_in X \<A>" "\<B> \<subseteq> \<A>"
    1.36 +  shows "locally_finite_in X \<B>"
    1.37 +proof -
    1.38 +  have "finite {U \<in> \<A>. U \<inter> V \<noteq> {}} \<Longrightarrow> finite {U \<in> \<B>. U \<inter> V \<noteq> {}}" for V
    1.39 +    apply (erule rev_finite_subset) using \<open>\<B> \<subseteq> \<A>\<close> by blast
    1.40 +  then show ?thesis
    1.41 +  using assms unfolding locally_finite_in_def by (fastforce simp add:)
    1.42 +qed
    1.43 +
    1.44 +lemma locally_finite_in_refinement:
    1.45 +  assumes \<A>: "locally_finite_in X \<A>" and f: "\<And>S. S \<in> \<A> \<Longrightarrow> f S \<subseteq> S"
    1.46 +  shows "locally_finite_in X (f ` \<A>)"
    1.47 +proof -
    1.48 +  show ?thesis
    1.49 +    unfolding locally_finite_in_def
    1.50 +  proof safe
    1.51 +    fix x
    1.52 +    assume "x \<in> topspace X"
    1.53 +    then obtain V where "openin X V" "x \<in> V" "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
    1.54 +      using \<A> unfolding locally_finite_in_def by blast
    1.55 +    moreover have "{U \<in> \<A>. f U \<inter> V \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}" for V
    1.56 +      using f by blast
    1.57 +    ultimately have "finite {U \<in> \<A>. f U \<inter> V \<noteq> {}}"
    1.58 +      using finite_subset by blast
    1.59 +    moreover have "f ` {U \<in> \<A>. f U \<inter> V \<noteq> {}} = {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
    1.60 +      by blast
    1.61 +    ultimately have "finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
    1.62 +      by (metis (no_types, lifting) finite_imageI)
    1.63 +    then show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
    1.64 +      using \<open>openin X V\<close> \<open>x \<in> V\<close> by blast
    1.65 +  next
    1.66 +    show "\<And>x xa. \<lbrakk>xa \<in> \<A>; x \<in> f xa\<rbrakk> \<Longrightarrow> x \<in> topspace X"
    1.67 +      by (meson Sup_upper \<A> f locally_finite_in_def subset_iff)
    1.68 +  qed
    1.69 +qed
    1.70 +
    1.71 +lemma locally_finite_in_subtopology:
    1.72 +  assumes \<A>: "locally_finite_in X \<A>" "\<Union>\<A> \<subseteq> S"
    1.73 +  shows "locally_finite_in (subtopology X S) \<A>"
    1.74 +  unfolding locally_finite_in_def
    1.75 +proof safe
    1.76 +  fix x
    1.77 +  assume x: "x \<in> topspace (subtopology X S)"
    1.78 +  then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
    1.79 +    using \<A> unfolding locally_finite_in_def topspace_subtopology by blast
    1.80 +  show "\<exists>V. openin (subtopology X S) V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
    1.81 +  proof (intro exI conjI)
    1.82 +    show "openin (subtopology X S) (S \<inter> V)"
    1.83 +      by (simp add: \<open>openin X V\<close> openin_subtopology_Int2)
    1.84 +    have "{U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}"
    1.85 +      by auto
    1.86 +    with fin show "finite {U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}}"
    1.87 +      using finite_subset by auto
    1.88 +    show "x \<in> S \<inter> V"
    1.89 +      using x \<open>x \<in> V\<close> by (simp add: topspace_subtopology)
    1.90 +  qed
    1.91 +next
    1.92 +  show "\<And>x A. \<lbrakk>x \<in> A; A \<in> \<A>\<rbrakk> \<Longrightarrow> x \<in> topspace (subtopology X S)"
    1.93 +    using assms unfolding locally_finite_in_def topspace_subtopology by blast
    1.94 +qed
    1.95 +
    1.96 +
    1.97 +lemma closedin_locally_finite_Union:
    1.98 +  assumes clo: "\<And>S. S \<in> \<A> \<Longrightarrow> closedin X S" and \<A>: "locally_finite_in X \<A>"
    1.99 +  shows "closedin X (\<Union>\<A>)"
   1.100 +  using \<A> unfolding locally_finite_in_def closedin_def
   1.101 +proof clarify
   1.102 +  show "openin X (topspace X - \<Union>\<A>)"
   1.103 +  proof (subst openin_subopen, clarify)
   1.104 +    fix x
   1.105 +    assume "x \<in> topspace X" and "x \<notin> \<Union>\<A>"
   1.106 +    then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
   1.107 +      using \<A> unfolding locally_finite_in_def by blast
   1.108 +    let ?T = "V - \<Union>{S \<in> \<A>. S \<inter> V \<noteq> {}}"
   1.109 +    show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> topspace X - \<Union>\<A>"
   1.110 +    proof (intro exI conjI)
   1.111 +      show "openin X ?T"
   1.112 +        by (metis (no_types, lifting) fin \<open>openin X V\<close> clo closedin_Union mem_Collect_eq openin_diff)
   1.113 +      show "x \<in> ?T"
   1.114 +        using \<open>x \<notin> \<Union>\<A>\<close> \<open>x \<in> V\<close> by auto
   1.115 +      show "?T \<subseteq> topspace X - \<Union>\<A>"
   1.116 +        using \<open>openin X V\<close> openin_subset by auto
   1.117 +    qed
   1.118 +  qed
   1.119 +qed
   1.120 +
   1.121 +lemma locally_finite_in_closure:
   1.122 +  assumes \<A>: "locally_finite_in X \<A>"
   1.123 +  shows "locally_finite_in X ((\<lambda>S. X closure_of S) ` \<A>)"
   1.124 +  using \<A> unfolding locally_finite_in_def
   1.125 +proof (intro conjI; clarsimp)
   1.126 +  fix x A
   1.127 +  assume "x \<in> X closure_of A"
   1.128 +  then show "x \<in> topspace X"
   1.129 +    by (meson in_closure_of)
   1.130 +next
   1.131 +  fix x
   1.132 +  assume "x \<in> topspace X" and "\<Union>\<A> \<subseteq> topspace X"
   1.133 +  then obtain V where V: "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
   1.134 +    using \<A> unfolding locally_finite_in_def by blast
   1.135 +  have eq: "{y \<in> f ` \<A>. Q y} = f ` {x. x \<in> \<A> \<and> Q(f x)}" for f Q
   1.136 +    by blast
   1.137 +  have eq2: "{A \<in> \<A>. X closure_of A \<inter> V \<noteq> {}} = {A \<in> \<A>. A \<inter> V \<noteq> {}}"
   1.138 +    using openin_Int_closure_of_eq_empty V  by blast
   1.139 +  have "finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
   1.140 +    by (simp add: eq eq2 fin)
   1.141 +  with V show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
   1.142 +    by blast
   1.143 +qed
   1.144 +
   1.145 +lemma closedin_Union_locally_finite_closure:
   1.146 +   "locally_finite_in X \<A> \<Longrightarrow> closedin X (\<Union>((\<lambda>S. X closure_of S) ` \<A>))"
   1.147 +  by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure)
   1.148 +
   1.149 +lemma closure_of_Union_subset: "\<Union>((\<lambda>S. X closure_of S) ` \<A>) \<subseteq> X closure_of (\<Union>\<A>)"
   1.150 +  by clarify (meson Union_upper closure_of_mono subsetD)
   1.151 +
   1.152 +lemma closure_of_locally_finite_Union:
   1.153 +   "locally_finite_in X \<A> \<Longrightarrow> X closure_of (\<Union>\<A>) = \<Union>((\<lambda>S. X closure_of S) ` \<A>)"
   1.154 +  apply (rule closure_of_unique)
   1.155 +  apply (simp add: SUP_upper2 Sup_le_iff closure_of_subset locally_finite_in_def)
   1.156 +  apply (simp add: closedin_Union_locally_finite_closure)
   1.157 +  by (simp add: Sup_le_iff closure_of_minimal)
   1.158 +
   1.159 +
   1.160  subsection\<open>Continuous maps\<close>
   1.161  
   1.162  definition continuous_map where
     2.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Sun Mar 17 21:26:42 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Mon Mar 18 15:35:34 2019 +0000
     2.3 @@ -9,6 +9,8 @@
     2.4    Topology_Euclidean_Space
     2.5    Operator_Norm
     2.6    Uniform_Limit
     2.7 +  Function_Topology
     2.8 +
     2.9  begin
    2.10  
    2.11  lemma onorm_componentwise:
    2.12 @@ -733,4 +735,86 @@
    2.13    bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
    2.14    bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]
    2.15  
    2.16 +
    2.17 +subsection \<open>The strong operator topology on continuous linear operators\<close>
    2.18 +
    2.19 +text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
    2.20 +operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
    2.21 +(the type classes instantiation are given in \<^file>\<open>Bounded_Linear_Function.thy\<close>).
    2.22 +
    2.23 +However, there is another topology on this space, the strong operator topology, where \<open>T\<^sub>n\<close> tends to
    2.24 +\<open>T\<close> iff, for all \<open>x\<close> in \<open>'a\<close>, then \<open>T\<^sub>n x\<close> tends to \<open>T x\<close>. This is precisely the product topology
    2.25 +where the target space is endowed with the norm topology. It is especially useful when \<open>'b\<close> is the set
    2.26 +of real numbers, since then this topology is compact.
    2.27 +
    2.28 +We can not implement it using type classes as there is already a topology, but at least we
    2.29 +can define it as a topology.
    2.30 +
    2.31 +Note that there is yet another (common and useful) topology on operator spaces, the weak operator
    2.32 +topology, defined analogously using the product topology, but where the target space is given the
    2.33 +weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
    2.34 +canonical embedding of a space into its bidual. We do not define it there, although it could also be
    2.35 +defined analogously.
    2.36 +\<close>
    2.37 +
    2.38 +definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
    2.39 +where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
    2.40 +
    2.41 +lemma strong_operator_topology_topspace:
    2.42 +  "topspace strong_operator_topology = UNIV"
    2.43 +unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
    2.44 +
    2.45 +lemma strong_operator_topology_basis:
    2.46 +  fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
    2.47 +  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
    2.48 +  shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
    2.49 +proof -
    2.50 +  have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
    2.51 +    by (rule product_topology_basis'[OF assms])
    2.52 +  moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
    2.53 +                = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
    2.54 +    by auto
    2.55 +  ultimately show ?thesis
    2.56 +    unfolding strong_operator_topology_def by (subst openin_pullback_topology) auto
    2.57 +qed
    2.58 +
    2.59 +lemma strong_operator_topology_continuous_evaluation:
    2.60 +  "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
    2.61 +proof -
    2.62 +  have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
    2.63 +    unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
    2.64 +    using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
    2.65 +  then show ?thesis unfolding comp_def by simp
    2.66 +qed
    2.67 +
    2.68 +lemma continuous_on_strong_operator_topo_iff_coordinatewise:
    2.69 +  "continuous_on_topo T strong_operator_topology f
    2.70 +    \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
    2.71 +proof (auto)
    2.72 +  fix x::"'b"
    2.73 +  assume "continuous_on_topo T strong_operator_topology f"
    2.74 +  with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
    2.75 +  have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
    2.76 +    by simp
    2.77 +  then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
    2.78 +    unfolding comp_def by auto
    2.79 +next
    2.80 +  assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
    2.81 +  have "continuous_on_topo T euclidean (blinfun_apply o f)"
    2.82 +    unfolding euclidean_product_topology
    2.83 +    apply (rule continuous_on_topo_coordinatewise_then_product, auto)
    2.84 +    using * unfolding comp_def by auto
    2.85 +  show "continuous_on_topo T strong_operator_topology f"
    2.86 +    unfolding strong_operator_topology_def
    2.87 +    apply (rule continuous_on_topo_pullback')
    2.88 +    by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
    2.89 +qed
    2.90 +
    2.91 +lemma strong_operator_topology_weaker_than_euclidean:
    2.92 +  "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
    2.93 +  by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
    2.94 +    auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
    2.95 +
    2.96 +
    2.97 +
    2.98  end
     3.1 --- a/src/HOL/Analysis/Cartesian_Space.thy	Sun Mar 17 21:26:42 2019 +0100
     3.2 +++ b/src/HOL/Analysis/Cartesian_Space.thy	Mon Mar 18 15:35:34 2019 +0000
     3.3 @@ -671,7 +671,7 @@
     3.4    by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
     3.5  
     3.6  
     3.7 -subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3\<close>\<close>
     3.8 +subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3/4\<close>\<close>
     3.9  
    3.10  lemma exhaust_2:
    3.11    fixes x :: 2
    3.12 @@ -699,6 +699,19 @@
    3.13  lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
    3.14    by (metis exhaust_3)
    3.15  
    3.16 +lemma exhaust_4:
    3.17 +  fixes x :: 4
    3.18 +  shows "x = 1 \<or> x = 2 \<or> x = 3 \<or> x = 4"
    3.19 +proof (induct x)
    3.20 +  case (of_int z)
    3.21 +  then have "0 \<le> z" and "z < 4" by simp_all
    3.22 +  then have "z = 0 \<or> z = 1 \<or> z = 2 \<or> z = 3" by arith
    3.23 +  then show ?case by auto
    3.24 +qed
    3.25 +
    3.26 +lemma forall_4: "(\<forall>i::4. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3 \<and> P 4"
    3.27 +  by (metis exhaust_4)
    3.28 +
    3.29  lemma UNIV_1 [simp]: "UNIV = {1::1}"
    3.30    by (auto simp add: num1_eq_iff)
    3.31  
    3.32 @@ -708,6 +721,9 @@
    3.33  lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
    3.34    using exhaust_3 by auto
    3.35  
    3.36 +lemma UNIV_4: "UNIV = {1::4, 2::4, 3::4, 4::4}"
    3.37 +  using exhaust_4 by auto
    3.38 +
    3.39  lemma sum_1: "sum f (UNIV::1 set) = f 1"
    3.40    unfolding UNIV_1 by simp
    3.41  
    3.42 @@ -717,6 +733,9 @@
    3.43  lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
    3.44    unfolding UNIV_3 by (simp add: ac_simps)
    3.45  
    3.46 +lemma sum_4: "sum f (UNIV::4 set) = f 1 + f 2 + f 3 + f 4"
    3.47 +  unfolding UNIV_4 by (simp add: ac_simps)
    3.48 +
    3.49  subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close>
    3.50  
    3.51  lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
     4.1 --- a/src/HOL/Analysis/Continuous_Extension.thy	Sun Mar 17 21:26:42 2019 +0100
     4.2 +++ b/src/HOL/Analysis/Continuous_Extension.thy	Mon Mar 18 15:35:34 2019 +0000
     4.3 @@ -14,7 +14,7 @@
     4.4     so the "support" must be made explicit in the summation below!\<close>
     4.5  
     4.6  proposition subordinate_partition_of_unity:
     4.7 -  fixes S :: "'a :: euclidean_space set"
     4.8 +  fixes S :: "'a::metric_space set"
     4.9    assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
    4.10        and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
    4.11    obtains F :: "['a set, 'a] \<Rightarrow> real"
    4.12 @@ -26,9 +26,7 @@
    4.13    case True
    4.14      then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
    4.15      then show ?thesis
    4.16 -      apply (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that)
    4.17 -      apply (auto simp: continuous_on_const supp_sum_def support_on_def)
    4.18 -      done
    4.19 +      by (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that) (auto simp: supp_sum_def support_on_def)
    4.20  next
    4.21    case False
    4.22      have nonneg: "0 \<le> supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" for x
    4.23 @@ -37,9 +35,9 @@
    4.24      proof -
    4.25        have "closedin (subtopology euclidean S) (S - V)"
    4.26          by (simp add: Diff_Diff_Int closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
    4.27 -      with that False setdist_eq_0_closedin [of S "S-V" x] setdist_pos_le [of "{x}" "S - V"]
    4.28 -        show ?thesis
    4.29 -          by (simp add: order_class.order.order_iff_strict)
    4.30 +      with that False  setdist_pos_le [of "{x}" "S - V"]
    4.31 +      show ?thesis
    4.32 +        using setdist_gt_0_closedin by fastforce
    4.33      qed
    4.34      have ss_pos: "0 < supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" if "x \<in> S" for x
    4.35      proof -
    4.36 @@ -50,17 +48,16 @@
    4.37        then have *: "finite {A \<in> \<C>. \<not> S \<subseteq> A \<and> x \<notin> closure (S - A)}"
    4.38          using closure_def that by (blast intro: rev_finite_subset)
    4.39        have "x \<notin> closure (S - U)"
    4.40 -        by (metis \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> less_irrefl sd_pos setdist_eq_0_sing_1 that)
    4.41 +        using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> opC open_Int_closure_eq_empty by fastforce
    4.42        then show ?thesis
    4.43          apply (simp add: setdist_eq_0_sing_1 supp_sum_def support_on_def)
    4.44          apply (rule ordered_comm_monoid_add_class.sum_pos2 [OF *, of U])
    4.45          using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> False
    4.46 -        apply (auto simp: setdist_pos_le sd_pos that)
    4.47 +        apply (auto simp: sd_pos that)
    4.48          done
    4.49      qed
    4.50      define F where
    4.51 -      "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>
    4.52 -                 else 0"
    4.53 +      "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_sum (\<lambda>V. setdist {x} (S - V)) \<C> else 0"
    4.54      show ?thesis
    4.55      proof (rule_tac F = F in that)
    4.56        have "continuous_on S (F U)" if "U \<in> \<C>" for U
    4.57 @@ -302,7 +299,7 @@
    4.58  text \<open>See \cite{dugundji}.\<close>
    4.59  
    4.60  theorem Dugundji:
    4.61 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
    4.62 +  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
    4.63    assumes "convex C" "C \<noteq> {}"
    4.64        and cloin: "closedin (subtopology euclidean U) S"
    4.65        and contf: "continuous_on S f" and "f ` S \<subseteq> C"
    4.66 @@ -325,9 +322,8 @@
    4.67      by (auto simp: sd_pos \<B>_def)
    4.68    obtain \<C> where USsub: "U - S \<subseteq> \<Union>\<C>"
    4.69         and nbrhd: "\<And>U. U \<in> \<C> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<B> \<and> U \<subseteq> T)"
    4.70 -       and fin: "\<And>x. x \<in> U - S
    4.71 -                     \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}"
    4.72 -    using paracompact [OF USS] by auto
    4.73 +       and fin: "\<And>x. x \<in> U - S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}"
    4.74 +    by (rule paracompact [OF USS]) auto
    4.75    have "\<exists>v a. v \<in> U \<and> v \<notin> S \<and> a \<in> S \<and>
    4.76                T \<subseteq> ball v (setdist {v} S / 2) \<and>
    4.77                dist v a \<le> 2 * setdist {v} S" if "T \<in> \<C>" for T
    4.78 @@ -353,7 +349,7 @@
    4.79    proof -
    4.80      have "dist (\<V> T) v < setdist {\<V> T} S / 2"
    4.81        using that VA mem_ball by blast
    4.82 -    also have "... \<le> setdist {v} S"
    4.83 +    also have "\<dots> \<le> setdist {v} S"
    4.84        using sdle [OF \<open>T \<in> \<C>\<close> \<open>v \<in> T\<close>] by simp
    4.85      also have vS: "setdist {v} S \<le> dist a v"
    4.86        by (simp add: setdist_le_dist setdist_sym \<open>a \<in> S\<close>)
    4.87 @@ -362,9 +358,9 @@
    4.88        using sdle that vS by force
    4.89      have "dist a (\<A> T) \<le> dist a v + dist v (\<V> T) + dist (\<V> T) (\<A> T)"
    4.90        by (metis add.commute add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
    4.91 -    also have "... \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)"
    4.92 +    also have "\<dots> \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)"
    4.93        using VTV by (simp add: dist_commute)
    4.94 -    also have "... \<le> 2 * dist a v + 2 * setdist {\<V> T} S"
    4.95 +    also have "\<dots> \<le> 2 * dist a v + 2 * setdist {\<V> T} S"
    4.96        using VA [OF \<open>T \<in> \<C>\<close>] by auto
    4.97      finally show ?thesis
    4.98        using VTS by linarith
    4.99 @@ -477,66 +473,65 @@
   4.100  
   4.101  
   4.102  corollary Tietze:
   4.103 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
   4.104 +  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   4.105    assumes "continuous_on S f"
   4.106 -      and "closedin (subtopology euclidean U) S"
   4.107 -      and "0 \<le> B"
   4.108 -      and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
   4.109 +    and "closedin (subtopology euclidean U) S"
   4.110 +    and "0 \<le> B"
   4.111 +    and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
   4.112    obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   4.113 -                  "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
   4.114 -  using assms
   4.115 -by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
   4.116 +    "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
   4.117 +  using assms by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
   4.118  
   4.119  corollary%unimportant Tietze_closed_interval:
   4.120 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.121 +  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
   4.122    assumes "continuous_on S f"
   4.123 -      and "closedin (subtopology euclidean U) S"
   4.124 -      and "cbox a b \<noteq> {}"
   4.125 -      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   4.126 +    and "closedin (subtopology euclidean U) S"
   4.127 +    and "cbox a b \<noteq> {}"
   4.128 +    and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   4.129    obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   4.130 -                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
   4.131 -apply (rule Dugundji [of "cbox a b" U S f])
   4.132 -using assms by auto
   4.133 +    "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
   4.134 +  apply (rule Dugundji [of "cbox a b" U S f])
   4.135 +  using assms by auto
   4.136  
   4.137  corollary%unimportant Tietze_closed_interval_1:
   4.138 -  fixes f :: "'a::euclidean_space \<Rightarrow> real"
   4.139 +  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
   4.140    assumes "continuous_on S f"
   4.141 -      and "closedin (subtopology euclidean U) S"
   4.142 -      and "a \<le> b"
   4.143 -      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   4.144 +    and "closedin (subtopology euclidean U) S"
   4.145 +    and "a \<le> b"
   4.146 +    and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   4.147    obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   4.148 -                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
   4.149 -apply (rule Dugundji [of "cbox a b" U S f])
   4.150 -using assms by (auto simp: image_subset_iff)
   4.151 +    "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
   4.152 +  apply (rule Dugundji [of "cbox a b" U S f])
   4.153 +  using assms by (auto simp: image_subset_iff)
   4.154  
   4.155  corollary%unimportant Tietze_open_interval:
   4.156 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.157 +  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
   4.158    assumes "continuous_on S f"
   4.159 -      and "closedin (subtopology euclidean U) S"
   4.160 -      and "box a b \<noteq> {}"
   4.161 -      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   4.162 +    and "closedin (subtopology euclidean U) S"
   4.163 +    and "box a b \<noteq> {}"
   4.164 +    and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   4.165    obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   4.166 -                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
   4.167 -apply (rule Dugundji [of "box a b" U S f])
   4.168 -using assms by auto
   4.169 +    "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
   4.170 +  apply (rule Dugundji [of "box a b" U S f])
   4.171 +  using assms by auto
   4.172  
   4.173  corollary%unimportant Tietze_open_interval_1:
   4.174 -  fixes f :: "'a::euclidean_space \<Rightarrow> real"
   4.175 +  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
   4.176    assumes "continuous_on S f"
   4.177 -      and "closedin (subtopology euclidean U) S"
   4.178 -      and "a < b"
   4.179 -      and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   4.180 +    and "closedin (subtopology euclidean U) S"
   4.181 +    and "a < b"
   4.182 +    and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   4.183    obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   4.184 -                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
   4.185 -apply (rule Dugundji [of "box a b" U S f])
   4.186 -using assms by (auto simp: image_subset_iff)
   4.187 +    "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
   4.188 +  apply (rule Dugundji [of "box a b" U S f])
   4.189 +  using assms by (auto simp: image_subset_iff)
   4.190  
   4.191  corollary%unimportant Tietze_unbounded:
   4.192 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
   4.193 +  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   4.194    assumes "continuous_on S f"
   4.195 -      and "closedin (subtopology euclidean U) S"
   4.196 +    and "closedin (subtopology euclidean U) S"
   4.197    obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   4.198 -apply (rule Dugundji [of UNIV U S f])
   4.199 -using assms by auto
   4.200 +  apply (rule Dugundji [of UNIV U S f])
   4.201 +  using assms by auto
   4.202  
   4.203  end
     5.1 --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Sun Mar 17 21:26:42 2019 +0100
     5.2 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Mar 18 15:35:34 2019 +0000
     5.3 @@ -3170,4 +3170,71 @@
     5.4  lemma setdist_le_sing: "x \<in> S ==> setdist S T \<le> setdist {x} T"
     5.5    using setdist_subset_left by auto
     5.6  
     5.7 +lemma infdist_eq_setdist: "infdist x A = setdist {x} A"
     5.8 +  by (simp add: infdist_def setdist_def Setcompr_eq_image)
     5.9 +
    5.10 +lemma setdist_eq_infdist: "setdist A B = (if A = {} then 0 else INF a\<in>A. infdist a B)"
    5.11 +proof -
    5.12 +  have "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} = (INF x\<in>A. Inf (dist x ` B))"
    5.13 +    if "b \<in> B" "a \<in> A" for a b
    5.14 +  proof (rule order_antisym)
    5.15 +    have "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> Inf (dist x ` B)"
    5.16 +      if  "b \<in> B" "a \<in> A" "x \<in> A" for x 
    5.17 +    proof -
    5.18 +      have *: "\<And>b'. b' \<in> B \<Longrightarrow> Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> dist x b'"
    5.19 +        by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist that(3))
    5.20 +      show ?thesis
    5.21 +        using that by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: *)+
    5.22 +    qed
    5.23 +    then show "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> (INF x\<in>A. Inf (dist x ` B))"
    5.24 +      using that
    5.25 +      by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: bdd_below_def)
    5.26 +  next
    5.27 +    have *: "\<And>x y. \<lbrakk>b \<in> B; a \<in> A; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> \<exists>a\<in>A. Inf (dist a ` B) \<le> dist x y"
    5.28 +      by (meson bdd_below_image_dist cINF_lower)
    5.29 +    show "(INF x\<in>A. Inf (dist x ` B)) \<le> Inf {dist x y |x y. x \<in> A \<and> y \<in> B}"
    5.30 +    proof (rule conditionally_complete_lattice_class.cInf_mono)
    5.31 +      show "bdd_below ((\<lambda>x. Inf (dist x ` B)) ` A)"
    5.32 +        by (metis (no_types, lifting) bdd_belowI2 ex_in_conv infdist_def infdist_nonneg that(1))
    5.33 +    qed (use that in \<open>auto simp: *\<close>)
    5.34 +  qed
    5.35 +  then show ?thesis
    5.36 +    by (auto simp: setdist_def infdist_def)
    5.37 +qed
    5.38 +
    5.39 +lemma continuous_on_infdist [continuous_intros]: "continuous_on B (\<lambda>y. infdist y A)"
    5.40 +  by (simp add: continuous_on_setdist infdist_eq_setdist)
    5.41 +
    5.42 +proposition setdist_attains_inf:
    5.43 +  assumes "compact B" "B \<noteq> {}"
    5.44 +  obtains y where "y \<in> B" "setdist A B = infdist y A"
    5.45 +proof (cases "A = {}")
    5.46 +  case True
    5.47 +  then show thesis
    5.48 +    by (metis assms diameter_compact_attained infdist_def setdist_def that)
    5.49 +next
    5.50 +  case False
    5.51 +  obtain y where "y \<in> B" and min: "\<And>y'. y' \<in> B \<Longrightarrow> infdist y A \<le> infdist y' A"
    5.52 +    using continuous_attains_inf [OF assms continuous_on_infdist] by blast
    5.53 +  show thesis
    5.54 +  proof
    5.55 +    have "setdist A B = (INF y\<in>B. infdist y A)"
    5.56 +      by (metis \<open>B \<noteq> {}\<close> setdist_eq_infdist setdist_sym)
    5.57 +    also have "\<dots> = infdist y A"
    5.58 +    proof (rule order_antisym)
    5.59 +      show "(INF y\<in>B. infdist y A) \<le> infdist y A"
    5.60 +      proof (rule cInf_lower)
    5.61 +        show "infdist y A \<in> (\<lambda>y. infdist y A) ` B"
    5.62 +          using \<open>y \<in> B\<close> by blast
    5.63 +        show "bdd_below ((\<lambda>y. infdist y A) ` B)"
    5.64 +          by (meson bdd_belowI2 infdist_nonneg)
    5.65 +      qed
    5.66 +    next
    5.67 +      show "infdist y A \<le> (INF y\<in>B. infdist y A)"
    5.68 +        by (simp add: \<open>B \<noteq> {}\<close> cINF_greatest min)
    5.69 +    qed
    5.70 +    finally show "setdist A B = infdist y A" .
    5.71 +  qed (fact \<open>y \<in> B\<close>)
    5.72 +qed
    5.73 +
    5.74  end
    5.75 \ No newline at end of file
     6.1 --- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Sun Mar 17 21:26:42 2019 +0100
     6.2 +++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon Mar 18 15:35:34 2019 +0000
     6.3 @@ -810,6 +810,9 @@
     6.4    shows "\<not> compact (UNIV::'a set)"
     6.5      by (simp add: compact_eq_bounded_closed)
     6.6  
     6.7 +lemma not_compact_space_euclideanreal [simp]: "\<not> compact_space euclideanreal"
     6.8 +  by (simp add: compact_space_def)
     6.9 +
    6.10  text\<open>Representing sets as the union of a chain of compact sets.\<close>
    6.11  lemma closed_Union_compact_subsets:
    6.12    fixes S :: "'a::{heine_borel,real_normed_vector} set"
     7.1 --- a/src/HOL/Analysis/Finite_Product_Measure.thy	Sun Mar 17 21:26:42 2019 +0100
     7.2 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Mar 18 15:35:34 2019 +0000
     7.3 @@ -5,7 +5,7 @@
     7.4  section \<open>Finite Product Measure\<close>
     7.5  
     7.6  theory Finite_Product_Measure
     7.7 -imports Binary_Product_Measure
     7.8 +imports Binary_Product_Measure Function_Topology
     7.9  begin
    7.10  
    7.11  lemma PiE_choice: "(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
    7.12 @@ -1202,4 +1202,142 @@
    7.13    with E show ?thesis by auto
    7.14  qed
    7.15  
    7.16 +
    7.17 +
    7.18 +subsection \<open>Measurability\<close>
    7.19 +
    7.20 +text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
    7.21 +generated by open sets in the product, and the product sigma algebra, countably generated by
    7.22 +products of measurable sets along finitely many coordinates. The second one is defined and studied
    7.23 +in \<^file>\<open>Finite_Product_Measure.thy\<close>.
    7.24 +
    7.25 +These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
    7.26 +but there is a fundamental difference: open sets are generated by arbitrary unions, not only
    7.27 +countable ones, so typically many open sets will not be measurable with respect to the product sigma
    7.28 +algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
    7.29 +only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
    7.30 +the factor is countably generated).
    7.31 +
    7.32 +In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
    7.33 +compare it with the product sigma algebra as explained above.
    7.34 +\<close>
    7.35 +
    7.36 +lemma measurable_product_coordinates [measurable (raw)]:
    7.37 +  "(\<lambda>x. x i) \<in> measurable borel borel"
    7.38 +by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
    7.39 +
    7.40 +lemma measurable_product_then_coordinatewise:
    7.41 +  fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
    7.42 +  assumes [measurable]: "f \<in> borel_measurable M"
    7.43 +  shows "(\<lambda>x. f x i) \<in> borel_measurable M"
    7.44 +proof -
    7.45 +  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
    7.46 +    unfolding comp_def by auto
    7.47 +  then show ?thesis by simp
    7.48 +qed
    7.49 +
    7.50 +text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
    7.51 +of the product sigma algebra that is more similar to the one we used above for the product
    7.52 +topology.\<close>
    7.53 +
    7.54 +lemma sets_PiM_finite:
    7.55 +  "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
    7.56 +        {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
    7.57 +proof
    7.58 +  have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
    7.59 +  proof (auto)
    7.60 +    fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
    7.61 +    then have *: "X i \<in> sets (M i)" for i by simp
    7.62 +    define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
    7.63 +    have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
    7.64 +    define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
    7.65 +    have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
    7.66 +      unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
    7.67 +    moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
    7.68 +      unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
    7.69 +      by (auto simp add: PiE_iff, blast)
    7.70 +    ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
    7.71 +  qed
    7.72 +  then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}
    7.73 +              \<subseteq> sets (Pi\<^sub>M I M)"
    7.74 +    by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
    7.75 +
    7.76 +  have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>
    7.77 +                (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
    7.78 +    if "i \<in> I" "A \<in> sets (M i)" for i A
    7.79 +  proof -
    7.80 +    define X where "X = (\<lambda>j. if j = i then A else space (M j))"
    7.81 +    have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
    7.82 +      unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
    7.83 +      by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
    7.84 +    moreover have "X j \<in> sets (M j)" for j
    7.85 +      unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
    7.86 +    moreover have "finite {j. X j \<noteq> space (M j)}"
    7.87 +      unfolding X_def by simp
    7.88 +    ultimately show ?thesis by auto
    7.89 +  qed
    7.90 +  show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
    7.91 +    unfolding sets_PiM_single
    7.92 +    apply (rule sigma_sets_mono')
    7.93 +    apply (auto simp add: PiE_iff *)
    7.94 +    done
    7.95 +qed
    7.96 +
    7.97 +lemma sets_PiM_subset_borel:
    7.98 +  "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
    7.99 +proof -
   7.100 +  have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
   7.101 +  proof -
   7.102 +    define I where "I = {i. X i \<noteq> UNIV}"
   7.103 +    have "finite I" unfolding I_def using that by simp
   7.104 +    have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
   7.105 +      unfolding I_def by auto
   7.106 +    also have "... \<in> sets borel"
   7.107 +      using that \<open>finite I\<close> by measurable
   7.108 +    finally show ?thesis by simp
   7.109 +  qed
   7.110 +  then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
   7.111 +    by auto
   7.112 +  then show ?thesis unfolding sets_PiM_finite space_borel
   7.113 +    by (simp add: * sets.sigma_sets_subset')
   7.114 +qed
   7.115 +
   7.116 +proposition sets_PiM_equal_borel:
   7.117 +  "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
   7.118 +proof
   7.119 +  obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
   7.120 +            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
   7.121 +    using product_topology_countable_basis by fast
   7.122 +  have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
   7.123 +  proof -
   7.124 +    obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
   7.125 +      using K(3)[OF \<open>k \<in> K\<close>] by blast
   7.126 +    show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
   7.127 +  qed
   7.128 +  have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
   7.129 +  proof -
   7.130 +    obtain B where "B \<subseteq> K" "U = (\<Union>B)"
   7.131 +      using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
   7.132 +    have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
   7.133 +    moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
   7.134 +      using \<open>B \<subseteq> K\<close> * that by auto
   7.135 +    ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
   7.136 +  qed
   7.137 +  have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
   7.138 +    apply (rule sets.sigma_sets_subset') using ** by auto
   7.139 +  then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
   7.140 +    unfolding borel_def by auto
   7.141 +qed (simp add: sets_PiM_subset_borel)
   7.142 +
   7.143 +lemma measurable_coordinatewise_then_product:
   7.144 +  fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
   7.145 +  assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
   7.146 +  shows "f \<in> borel_measurable M"
   7.147 +proof -
   7.148 +  have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
   7.149 +    by (rule measurable_PiM_single', auto simp add: assms)
   7.150 +  then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
   7.151 +qed
   7.152 +
   7.153 +
   7.154  end
     8.1 --- a/src/HOL/Analysis/Function_Topology.thy	Sun Mar 17 21:26:42 2019 +0100
     8.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Mon Mar 18 15:35:34 2019 +0000
     8.3 @@ -3,7 +3,7 @@
     8.4  *)
     8.5  
     8.6  theory Function_Topology
     8.7 -imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure 
     8.8 +imports Topology_Euclidean_Space   
     8.9  begin
    8.10  
    8.11  
    8.12 @@ -945,24 +945,37 @@
    8.13  
    8.14  lemma continuous_on_product_coordinates [simp]:
    8.15    "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
    8.16 -unfolding continuous_on_topo_UNIV euclidean_product_topology
    8.17 -by (rule continuous_on_topo_product_coordinates, simp)
    8.18 +  unfolding continuous_on_topo_UNIV euclidean_product_topology
    8.19 +  by (rule continuous_on_topo_product_coordinates, simp)
    8.20  
    8.21  lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
    8.22 -  assumes "\<And>i. continuous_on UNIV (\<lambda>x. f x i)"
    8.23 -  shows "continuous_on UNIV f"
    8.24 -using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
    8.25 -by (rule continuous_on_topo_coordinatewise_then_product, simp)
    8.26 +  fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
    8.27 +  assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
    8.28 +  shows "continuous_on S f"
    8.29 +  using continuous_on_topo_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclideanreal"]
    8.30 +  by (metis UNIV_I assms continuous_on_continuous_on_topo euclidean_product_topology)
    8.31  
    8.32 -lemma continuous_on_product_then_coordinatewise:
    8.33 +lemma continuous_on_product_then_coordinatewise_UNIV:
    8.34    assumes "continuous_on UNIV f"
    8.35    shows "continuous_on UNIV (\<lambda>x. f x i)"
    8.36  using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
    8.37  by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
    8.38  
    8.39 -lemma continuous_on_product_coordinatewise_iff:
    8.40 -  "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
    8.41 -by (auto intro: continuous_on_product_then_coordinatewise)
    8.42 +lemma continuous_on_product_then_coordinatewise:
    8.43 +  assumes "continuous_on S f"
    8.44 +  shows "continuous_on S (\<lambda>x. f x i)"
    8.45 +proof -
    8.46 +  have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
    8.47 +    by (metis assms continuous_on_compose continuous_on_id 
    8.48 +        continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
    8.49 +  then show ?thesis
    8.50 +    by auto
    8.51 +qed
    8.52 +
    8.53 +lemma continuous_on_coordinatewise_iff:
    8.54 +  fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
    8.55 +  shows "continuous_on (A \<inter> S) f \<longleftrightarrow> (\<forall>i. continuous_on (A \<inter> S) (\<lambda>x. f x i))"
    8.56 +  by (auto simp: continuous_on_product_then_coordinatewise)
    8.57  
    8.58  subsubsection%important \<open>Topological countability for product spaces\<close>
    8.59  
    8.60 @@ -1194,86 +1207,6 @@
    8.61    using product_topology_countable_basis topological_basis_imp_subbasis by auto
    8.62  
    8.63  
    8.64 -subsection \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
    8.65 -
    8.66 -text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
    8.67 -operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
    8.68 -(the type classes instantiation are given in \<^file>\<open>Bounded_Linear_Function.thy\<close>).
    8.69 -
    8.70 -However, there is another topology on this space, the strong operator topology, where \<open>T\<^sub>n\<close> tends to
    8.71 -\<open>T\<close> iff, for all \<open>x\<close> in \<open>'a\<close>, then \<open>T\<^sub>n x\<close> tends to \<open>T x\<close>. This is precisely the product topology
    8.72 -where the target space is endowed with the norm topology. It is especially useful when \<open>'b\<close> is the set
    8.73 -of real numbers, since then this topology is compact.
    8.74 -
    8.75 -We can not implement it using type classes as there is already a topology, but at least we
    8.76 -can define it as a topology.
    8.77 -
    8.78 -Note that there is yet another (common and useful) topology on operator spaces, the weak operator
    8.79 -topology, defined analogously using the product topology, but where the target space is given the
    8.80 -weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
    8.81 -canonical embedding of a space into its bidual. We do not define it there, although it could also be
    8.82 -defined analogously.
    8.83 -\<close>
    8.84 -
    8.85 -definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
    8.86 -where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
    8.87 -
    8.88 -lemma strong_operator_topology_topspace:
    8.89 -  "topspace strong_operator_topology = UNIV"
    8.90 -unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
    8.91 -
    8.92 -lemma strong_operator_topology_basis:
    8.93 -  fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
    8.94 -  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
    8.95 -  shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
    8.96 -proof -
    8.97 -  have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
    8.98 -    by (rule product_topology_basis'[OF assms])
    8.99 -  moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
   8.100 -                = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
   8.101 -    by auto
   8.102 -  ultimately show ?thesis
   8.103 -    unfolding strong_operator_topology_def by (subst openin_pullback_topology) auto
   8.104 -qed
   8.105 -
   8.106 -lemma strong_operator_topology_continuous_evaluation:
   8.107 -  "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
   8.108 -proof -
   8.109 -  have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
   8.110 -    unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
   8.111 -    using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
   8.112 -  then show ?thesis unfolding comp_def by simp
   8.113 -qed
   8.114 -
   8.115 -lemma continuous_on_strong_operator_topo_iff_coordinatewise:
   8.116 -  "continuous_on_topo T strong_operator_topology f
   8.117 -    \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
   8.118 -proof (auto)
   8.119 -  fix x::"'b"
   8.120 -  assume "continuous_on_topo T strong_operator_topology f"
   8.121 -  with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
   8.122 -  have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
   8.123 -    by simp
   8.124 -  then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
   8.125 -    unfolding comp_def by auto
   8.126 -next
   8.127 -  assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
   8.128 -  have "continuous_on_topo T euclidean (blinfun_apply o f)"
   8.129 -    unfolding euclidean_product_topology
   8.130 -    apply (rule continuous_on_topo_coordinatewise_then_product, auto)
   8.131 -    using * unfolding comp_def by auto
   8.132 -  show "continuous_on_topo T strong_operator_topology f"
   8.133 -    unfolding strong_operator_topology_def
   8.134 -    apply (rule continuous_on_topo_pullback')
   8.135 -    by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
   8.136 -qed
   8.137 -
   8.138 -lemma strong_operator_topology_weaker_than_euclidean:
   8.139 -  "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
   8.140 -  by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
   8.141 -    auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
   8.142 -
   8.143 -
   8.144  subsection \<open>Metrics on product spaces\<close>
   8.145  
   8.146  
   8.147 @@ -1650,142 +1583,4 @@
   8.148  instance "fun" :: (countable, polish_space) polish_space
   8.149  by standard
   8.150  
   8.151 -
   8.152 -
   8.153 -
   8.154 -subsection \<open>Measurability\<close> (*FIX ME move? *)
   8.155 -
   8.156 -text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
   8.157 -generated by open sets in the product, and the product sigma algebra, countably generated by
   8.158 -products of measurable sets along finitely many coordinates. The second one is defined and studied
   8.159 -in \<^file>\<open>Finite_Product_Measure.thy\<close>.
   8.160 -
   8.161 -These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
   8.162 -but there is a fundamental difference: open sets are generated by arbitrary unions, not only
   8.163 -countable ones, so typically many open sets will not be measurable with respect to the product sigma
   8.164 -algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
   8.165 -only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
   8.166 -the factor is countably generated).
   8.167 -
   8.168 -In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
   8.169 -compare it with the product sigma algebra as explained above.
   8.170 -\<close>
   8.171 -
   8.172 -lemma measurable_product_coordinates [measurable (raw)]:
   8.173 -  "(\<lambda>x. x i) \<in> measurable borel borel"
   8.174 -by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
   8.175 -
   8.176 -lemma measurable_product_then_coordinatewise:
   8.177 -  fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
   8.178 -  assumes [measurable]: "f \<in> borel_measurable M"
   8.179 -  shows "(\<lambda>x. f x i) \<in> borel_measurable M"
   8.180 -proof -
   8.181 -  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
   8.182 -    unfolding comp_def by auto
   8.183 -  then show ?thesis by simp
   8.184 -qed
   8.185 -
   8.186 -text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
   8.187 -of the product sigma algebra that is more similar to the one we used above for the product
   8.188 -topology.\<close>
   8.189 -
   8.190 -lemma sets_PiM_finite:
   8.191 -  "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
   8.192 -        {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
   8.193 -proof
   8.194 -  have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
   8.195 -  proof (auto)
   8.196 -    fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
   8.197 -    then have *: "X i \<in> sets (M i)" for i by simp
   8.198 -    define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
   8.199 -    have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
   8.200 -    define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
   8.201 -    have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
   8.202 -      unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
   8.203 -    moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
   8.204 -      unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
   8.205 -      by (auto simp add: PiE_iff, blast)
   8.206 -    ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
   8.207 -  qed
   8.208 -  then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}
   8.209 -              \<subseteq> sets (Pi\<^sub>M I M)"
   8.210 -    by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
   8.211 -
   8.212 -  have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>
   8.213 -                (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
   8.214 -    if "i \<in> I" "A \<in> sets (M i)" for i A
   8.215 -  proof -
   8.216 -    define X where "X = (\<lambda>j. if j = i then A else space (M j))"
   8.217 -    have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
   8.218 -      unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
   8.219 -      by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
   8.220 -    moreover have "X j \<in> sets (M j)" for j
   8.221 -      unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
   8.222 -    moreover have "finite {j. X j \<noteq> space (M j)}"
   8.223 -      unfolding X_def by simp
   8.224 -    ultimately show ?thesis by auto
   8.225 -  qed
   8.226 -  show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
   8.227 -    unfolding sets_PiM_single
   8.228 -    apply (rule sigma_sets_mono')
   8.229 -    apply (auto simp add: PiE_iff *)
   8.230 -    done
   8.231 -qed
   8.232 -
   8.233 -lemma sets_PiM_subset_borel:
   8.234 -  "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
   8.235 -proof -
   8.236 -  have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
   8.237 -  proof -
   8.238 -    define I where "I = {i. X i \<noteq> UNIV}"
   8.239 -    have "finite I" unfolding I_def using that by simp
   8.240 -    have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
   8.241 -      unfolding I_def by auto
   8.242 -    also have "... \<in> sets borel"
   8.243 -      using that \<open>finite I\<close> by measurable
   8.244 -    finally show ?thesis by simp
   8.245 -  qed
   8.246 -  then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
   8.247 -    by auto
   8.248 -  then show ?thesis unfolding sets_PiM_finite space_borel
   8.249 -    by (simp add: * sets.sigma_sets_subset')
   8.250 -qed
   8.251 -
   8.252 -proposition sets_PiM_equal_borel:
   8.253 -  "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
   8.254 -proof
   8.255 -  obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
   8.256 -            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
   8.257 -    using product_topology_countable_basis by fast
   8.258 -  have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
   8.259 -  proof -
   8.260 -    obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
   8.261 -      using K(3)[OF \<open>k \<in> K\<close>] by blast
   8.262 -    show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
   8.263 -  qed
   8.264 -  have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
   8.265 -  proof -
   8.266 -    obtain B where "B \<subseteq> K" "U = (\<Union>B)"
   8.267 -      using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
   8.268 -    have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
   8.269 -    moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
   8.270 -      using \<open>B \<subseteq> K\<close> * that by auto
   8.271 -    ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
   8.272 -  qed
   8.273 -  have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
   8.274 -    apply (rule sets.sigma_sets_subset') using ** by auto
   8.275 -  then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
   8.276 -    unfolding borel_def by auto
   8.277 -qed (simp add: sets_PiM_subset_borel)
   8.278 -
   8.279 -lemma measurable_coordinatewise_then_product:
   8.280 -  fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
   8.281 -  assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
   8.282 -  shows "f \<in> borel_measurable M"
   8.283 -proof -
   8.284 -  have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
   8.285 -    by (rule measurable_PiM_single', auto simp add: assms)
   8.286 -  then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
   8.287 -qed
   8.288 -
   8.289  end
     9.1 --- a/src/HOL/Analysis/Homotopy.thy	Sun Mar 17 21:26:42 2019 +0100
     9.2 +++ b/src/HOL/Analysis/Homotopy.thy	Mon Mar 18 15:35:34 2019 +0000
     9.3 @@ -3652,6 +3652,11 @@
     9.4      using \<open>S \<subseteq> box a b\<close> by auto
     9.5  qed
     9.6  
     9.7 +corollary bounded_path_connected_Compl_real:
     9.8 +  fixes S :: "real set"
     9.9 +  assumes "bounded S" "path_connected(- S)" shows "S = {}"
    9.10 +  by (simp add: assms bounded_connected_Compl_real path_connected_imp_connected)
    9.11 +
    9.12  lemma bounded_connected_Compl_1:
    9.13    fixes S :: "'a::{euclidean_space} set"
    9.14    assumes "bounded S" and conn: "connected(- S)" and 1: "DIM('a) = 1"
    10.1 --- a/src/HOL/Analysis/Starlike.thy	Sun Mar 17 21:26:42 2019 +0100
    10.2 +++ b/src/HOL/Analysis/Starlike.thy	Mon Mar 18 15:35:34 2019 +0000
    10.3 @@ -6715,13 +6715,12 @@
    10.4  subsection\<open>Paracompactness\<close>
    10.5  
    10.6  proposition paracompact:
    10.7 -  fixes S :: "'a :: euclidean_space set"
    10.8 +  fixes S :: "'a :: {metric_space,second_countable_topology} set"
    10.9    assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
   10.10    obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
   10.11                 and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
   10.12                 and "\<And>x. x \<in> S
   10.13 -                       \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
   10.14 -                               finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
   10.15 +                       \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
   10.16  proof (cases "S = {}")
   10.17    case True with that show ?thesis by blast
   10.18  next
   10.19 @@ -6737,7 +6736,7 @@
   10.20        apply (rule_tac x = "ball x e" in exI)
   10.21        using  \<open>T \<in> \<C>\<close>
   10.22        apply (simp add: closure_minimal)
   10.23 -      done
   10.24 +      using closed_cball closure_minimal by blast
   10.25    qed
   10.26    then obtain F G where Gin: "x \<in> G x" and oG: "open (G x)"
   10.27                      and clos: "closure (G x) \<subseteq> F x" and Fin: "F x \<in> \<C>"
   10.28 @@ -6802,7 +6801,7 @@
   10.29  qed
   10.30  
   10.31  corollary paracompact_closedin:
   10.32 -  fixes S :: "'a :: euclidean_space set"
   10.33 +  fixes S :: "'a :: {metric_space,second_countable_topology} set"
   10.34    assumes cin: "closedin (subtopology euclidean U) S"
   10.35        and oin: "\<And>T. T \<in> \<C> \<Longrightarrow> openin (subtopology euclidean U) T"
   10.36        and "S \<subseteq> \<Union>\<C>"
   10.37 @@ -6825,7 +6824,7 @@
   10.38    obtain \<D> where "U \<subseteq> \<Union>\<D>"
   10.39               and D1: "\<And>U. U \<in> \<D> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> insert (- K) (F ` \<C>) \<and> U \<subseteq> T)"
   10.40               and D2: "\<And>x. x \<in> U \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<D>. U \<inter> V \<noteq> {}}"
   10.41 -    using paracompact [OF 1 2] by auto
   10.42 +    by (blast intro: paracompact [OF 1 2])
   10.43    let ?C = "{U \<inter> V |V. V \<in> \<D> \<and> (V \<inter> K \<noteq> {})}"
   10.44    show ?thesis
   10.45    proof (rule_tac \<C>' = "{U \<inter> V |V. V \<in> \<D> \<and> (V \<inter> K \<noteq> {})}" in that)
   10.46 @@ -6847,7 +6846,7 @@
   10.47  qed
   10.48  
   10.49  corollary%unimportant paracompact_closed:
   10.50 -  fixes S :: "'a :: euclidean_space set"
   10.51 +  fixes S :: "'a :: {metric_space,second_countable_topology} set"
   10.52    assumes "closed S"
   10.53        and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
   10.54        and "S \<subseteq> \<Union>\<C>"
   10.55 @@ -6855,7 +6854,7 @@
   10.56                 and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
   10.57                 and "\<And>x. \<exists>V. open V \<and> x \<in> V \<and>
   10.58                                 finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
   10.59 -using paracompact_closedin [of UNIV S \<C>] assms by auto
   10.60 +  by (rule paracompact_closedin [of UNIV S \<C>]) (auto simp: assms)
   10.61  
   10.62    
   10.63  subsection%unimportant\<open>Closed-graph characterization of continuity\<close>
    11.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Mar 17 21:26:42 2019 +0100
    11.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Mar 18 15:35:34 2019 +0000
    11.3 @@ -2241,24 +2241,22 @@
    11.4  subsection \<open>Set Distance\<close>
    11.5  
    11.6  lemma setdist_compact_closed:
    11.7 -  fixes S :: "'a::{heine_borel,real_normed_vector} set"
    11.8 -  assumes S: "compact S" and T: "closed T"
    11.9 -      and "S \<noteq> {}" "T \<noteq> {}"
   11.10 -    shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
   11.11 +  fixes A :: "'a::heine_borel set"
   11.12 +  assumes A: "compact A" and B: "closed B"
   11.13 +    and "A \<noteq> {}" "B \<noteq> {}"
   11.14 +  shows "\<exists>x \<in> A. \<exists>y \<in> B. dist x y = setdist A B"
   11.15  proof -
   11.16 -  have "(\<Union>x\<in> S. \<Union>y \<in> T. {x - y}) \<noteq> {}"
   11.17 -    using assms by blast
   11.18 -  then have "\<exists>x \<in> S. \<exists>y \<in> T. dist x y \<le> setdist S T"
   11.19 -    apply (rule distance_attains_inf [where a=0, OF compact_closed_differences [OF S T]])
   11.20 -    apply (simp add: dist_norm le_setdist_iff)
   11.21 -    apply blast
   11.22 -    done
   11.23 -  then show ?thesis
   11.24 -    by (blast intro!: antisym [OF _ setdist_le_dist] )
   11.25 +  obtain x where "x \<in> A" "setdist A B = infdist x B"
   11.26 +    by (metis A assms(3) setdist_attains_inf setdist_sym)
   11.27 +  moreover
   11.28 +  obtain y where"y \<in> B" "infdist x B = dist x y"
   11.29 +    using B \<open>B \<noteq> {}\<close> infdist_attains_inf by blast
   11.30 +  ultimately show ?thesis
   11.31 +    using \<open>x \<in> A\<close> \<open>y \<in> B\<close> by auto
   11.32  qed
   11.33  
   11.34  lemma setdist_closed_compact:
   11.35 -  fixes S :: "'a::{heine_borel,real_normed_vector} set"
   11.36 +  fixes S :: "'a::heine_borel set"
   11.37    assumes S: "closed S" and T: "compact T"
   11.38        and "S \<noteq> {}" "T \<noteq> {}"
   11.39      shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
   11.40 @@ -2266,76 +2264,71 @@
   11.41    by (metis dist_commute setdist_sym)
   11.42  
   11.43  lemma setdist_eq_0_compact_closed:
   11.44 -  fixes S :: "'a::{heine_borel,real_normed_vector} set"
   11.45    assumes S: "compact S" and T: "closed T"
   11.46      shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
   11.47 -  apply (cases "S = {} \<or> T = {}", force)
   11.48 -  using setdist_compact_closed [OF S T]
   11.49 -  apply (force intro: setdist_eq_0I )
   11.50 -  done
   11.51 +proof (cases "S = {} \<or> T = {}")
   11.52 +  case True
   11.53 +  then show ?thesis
   11.54 +    by force
   11.55 +next
   11.56 +  case False
   11.57 +  then show ?thesis
   11.58 +    by (metis S T disjoint_iff_not_equal in_closed_iff_infdist_zero setdist_attains_inf setdist_eq_0I setdist_sym)
   11.59 +qed
   11.60  
   11.61  corollary setdist_gt_0_compact_closed:
   11.62 -  fixes S :: "'a::{heine_borel,real_normed_vector} set"
   11.63    assumes S: "compact S" and T: "closed T"
   11.64      shows "setdist S T > 0 \<longleftrightarrow> (S \<noteq> {} \<and> T \<noteq> {} \<and> S \<inter> T = {})"
   11.65 -  using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms]
   11.66 -  by linarith
   11.67 +  using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms] by linarith
   11.68  
   11.69  lemma setdist_eq_0_closed_compact:
   11.70 -  fixes S :: "'a::{heine_borel,real_normed_vector} set"
   11.71    assumes S: "closed S" and T: "compact T"
   11.72      shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
   11.73    using setdist_eq_0_compact_closed [OF T S]
   11.74    by (metis Int_commute setdist_sym)
   11.75  
   11.76  lemma setdist_eq_0_bounded:
   11.77 -  fixes S :: "'a::{heine_borel,real_normed_vector} set"
   11.78 +  fixes S :: "'a::heine_borel set"
   11.79    assumes "bounded S \<or> bounded T"
   11.80 -    shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> closure S \<inter> closure T \<noteq> {}"
   11.81 -  apply (cases "S = {} \<or> T = {}", force)
   11.82 -  using setdist_eq_0_compact_closed [of "closure S" "closure T"]
   11.83 -        setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
   11.84 -  apply (force simp add:  bounded_closure compact_eq_bounded_closed)
   11.85 -  done
   11.86 +  shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> closure S \<inter> closure T \<noteq> {}"
   11.87 +proof (cases "S = {} \<or> T = {}")
   11.88 +  case False
   11.89 +  then show ?thesis
   11.90 +    using setdist_eq_0_compact_closed [of "closure S" "closure T"]
   11.91 +          setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
   11.92 +    by (force simp:  bounded_closure compact_eq_bounded_closed)
   11.93 +qed force
   11.94  
   11.95  lemma setdist_eq_0_sing_1:
   11.96 -    fixes S :: "'a::{heine_borel,real_normed_vector} set"
   11.97 -    shows "setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
   11.98 -  by (auto simp: setdist_eq_0_bounded)
   11.99 +  "setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
  11.100 +  by (metis in_closure_iff_infdist_zero infdist_def infdist_eq_setdist)
  11.101  
  11.102  lemma setdist_eq_0_sing_2:
  11.103 -    fixes S :: "'a::{heine_borel,real_normed_vector} set"
  11.104 -    shows "setdist S {x} = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
  11.105 -  by (auto simp: setdist_eq_0_bounded)
  11.106 +  "setdist S {x} = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
  11.107 +  by (metis setdist_eq_0_sing_1 setdist_sym)
  11.108  
  11.109  lemma setdist_neq_0_sing_1:
  11.110 -    fixes S :: "'a::{heine_borel,real_normed_vector} set"
  11.111 -    shows "\<lbrakk>setdist {x} S = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
  11.112 -  by (auto simp: setdist_eq_0_sing_1)
  11.113 +  "\<lbrakk>setdist {x} S = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
  11.114 +  by (metis setdist_closure_2 setdist_empty2 setdist_eq_0I singletonI)
  11.115  
  11.116  lemma setdist_neq_0_sing_2:
  11.117 -    fixes S :: "'a::{heine_borel,real_normed_vector} set"
  11.118 -    shows "\<lbrakk>setdist S {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
  11.119 -  by (auto simp: setdist_eq_0_sing_2)
  11.120 +  "\<lbrakk>setdist S {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
  11.121 +  by (simp add: setdist_neq_0_sing_1 setdist_sym)
  11.122  
  11.123  lemma setdist_sing_in_set:
  11.124 -    fixes S :: "'a::{heine_borel,real_normed_vector} set"
  11.125 -    shows "x \<in> S \<Longrightarrow> setdist {x} S = 0"
  11.126 -  using closure_subset by (auto simp: setdist_eq_0_sing_1)
  11.127 +   "x \<in> S \<Longrightarrow> setdist {x} S = 0"
  11.128 +  by (simp add: setdist_eq_0I)
  11.129  
  11.130  lemma setdist_eq_0_closed:
  11.131 -  fixes S :: "'a::{heine_borel,real_normed_vector} set"
  11.132 -  shows  "closed S \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
  11.133 +   "closed S \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
  11.134  by (simp add: setdist_eq_0_sing_1)
  11.135  
  11.136  lemma setdist_eq_0_closedin:
  11.137 -  fixes S :: "'a::{heine_borel,real_normed_vector} set"
  11.138    shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U\<rbrakk>
  11.139           \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
  11.140    by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
  11.141  
  11.142  lemma setdist_gt_0_closedin:
  11.143 -  fixes S :: "'a::{heine_borel,real_normed_vector} set"
  11.144    shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U; S \<noteq> {}; x \<notin> S\<rbrakk>
  11.145           \<Longrightarrow> setdist {x} S > 0"
  11.146    using less_eq_real_def setdist_eq_0_closedin by fastforce
    12.1 --- a/src/HOL/Analysis/Winding_Numbers.thy	Sun Mar 17 21:26:42 2019 +0100
    12.2 +++ b/src/HOL/Analysis/Winding_Numbers.thy	Mon Mar 18 15:35:34 2019 +0000
    12.3 @@ -935,11 +935,10 @@
    12.4  proof -
    12.5    obtain e where "0 < e" and e: "\<And>t. t \<in> {0..1} \<Longrightarrow> e \<le> norm(exp(p t))"
    12.6    proof
    12.7 -     have "closed (path_image (exp \<circ> p))"
    12.8 -       by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
    12.9 +    have "closed (path_image (exp \<circ> p))"
   12.10 +      by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
   12.11      then show "0 < setdist {0} (path_image (exp \<circ> p))"
   12.12 -      by (metis (mono_tags, lifting) compact_sing exp_not_eq_zero imageE path_image_compose
   12.13 -               path_image_nonempty setdist_eq_0_compact_closed setdist_gt_0_compact_closed setdist_eq_0_closed)
   12.14 +      by (metis exp_not_eq_zero imageE image_comp infdist_eq_setdist infdist_pos_not_in_closed path_defs(4) path_image_nonempty)
   12.15    next
   12.16      fix t::real
   12.17      assume "t \<in> {0..1}"
    13.1 --- a/src/HOL/Library/Set_Idioms.thy	Sun Mar 17 21:26:42 2019 +0100
    13.2 +++ b/src/HOL/Library/Set_Idioms.thy	Mon Mar 18 15:35:34 2019 +0000
    13.3 @@ -44,6 +44,10 @@
    13.4  lemma all_intersection_of:
    13.5       "(\<forall>S. (P intersection_of Q) S \<longrightarrow> R S) \<longleftrightarrow> (\<forall>T. P T \<and> T \<subseteq> Collect Q \<longrightarrow> R(\<Inter>T))"
    13.6    by (auto simp: intersection_of_def)
    13.7 +             
    13.8 +lemma intersection_ofE:
    13.9 +     "\<lbrakk>(P intersection_of Q) S; \<And>T. \<lbrakk>P T; T \<subseteq> Collect Q\<rbrakk> \<Longrightarrow> R(\<Inter>T)\<rbrakk> \<Longrightarrow> R S"
   13.10 +  by (auto simp: intersection_of_def)
   13.11  
   13.12  lemma union_of_empty:
   13.13       "P {} \<Longrightarrow> (P union_of Q) {}"
   13.14 @@ -319,6 +323,9 @@
   13.15  lemma all_relative_to: "(\<forall>S. (P relative_to U) S \<longrightarrow> Q S) \<longleftrightarrow> (\<forall>S. P S \<longrightarrow> Q(U \<inter> S))"
   13.16    by (auto simp: relative_to_def)
   13.17  
   13.18 +lemma relative_toE: "\<lbrakk>(P relative_to U) S; \<And>S. P S \<Longrightarrow> Q(U \<inter> S)\<rbrakk> \<Longrightarrow> Q S"
   13.19 +  by (auto simp: relative_to_def)
   13.20 +
   13.21  lemma relative_to_inc:
   13.22     "P S \<Longrightarrow> (P relative_to U) (U \<inter> S)"
   13.23    by (auto simp: relative_to_def)
    14.1 --- a/src/HOL/Limits.thy	Sun Mar 17 21:26:42 2019 +0100
    14.2 +++ b/src/HOL/Limits.thy	Mon Mar 18 15:35:34 2019 +0000
    14.3 @@ -532,6 +532,9 @@
    14.4    shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))"
    14.5    unfolding continuous_on_def by (auto intro: tendsto_dist)
    14.6  
    14.7 +lemma continuous_at_dist: "isCont (dist a) b"
    14.8 +  using continuous_on_dist [OF continuous_on_const continuous_on_id] continuous_on_eq_continuous_within by blast
    14.9 +
   14.10  lemma tendsto_norm [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> norm a) F"
   14.11    unfolding norm_conv_dist by (intro tendsto_intros)
   14.12