some new material, also recasting some theorems using “obtains”
authorpaulson <lp15@cam.ac.uk>
Tue Feb 21 17:12:10 2017 +0000 (2017-02-21)
changeset 650372cf841ff23be
parent 65036 ab7e11730ad8
child 65038 9391ea7daa17
some new material, also recasting some theorems using “obtains”
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Uniform_Limit.thy
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Feb 21 15:04:01 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Feb 21 17:12:10 2017 +0000
     1.3 @@ -38,6 +38,53 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma path_connected_arc_complement:
     1.8 +  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
     1.9 +  assumes "arc \<gamma>" "2 \<le> DIM('a)"
    1.10 +  shows "path_connected(- path_image \<gamma>)"
    1.11 +proof -
    1.12 +  have "path_image \<gamma> homeomorphic {0..1::real}"
    1.13 +    by (simp add: assms homeomorphic_arc_image_interval)
    1.14 +  then
    1.15 +  show ?thesis
    1.16 +    apply (rule path_connected_complement_homeomorphic_convex_compact)
    1.17 +      apply (auto simp: assms)
    1.18 +    done
    1.19 +qed
    1.20 +
    1.21 +lemma connected_arc_complement:
    1.22 +  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
    1.23 +  assumes "arc \<gamma>" "2 \<le> DIM('a)"
    1.24 +  shows "connected(- path_image \<gamma>)"
    1.25 +  by (simp add: assms path_connected_arc_complement path_connected_imp_connected)
    1.26 +
    1.27 +lemma inside_arc_empty:
    1.28 +  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
    1.29 +  assumes "arc \<gamma>"
    1.30 +    shows "inside(path_image \<gamma>) = {}"
    1.31 +proof (cases "DIM('a) = 1")
    1.32 +  case True
    1.33 +  then show ?thesis
    1.34 +    using assms connected_arc_image connected_convex_1_gen inside_convex by blast
    1.35 +next
    1.36 +  case False
    1.37 +  show ?thesis
    1.38 +  proof (rule inside_bounded_complement_connected_empty)
    1.39 +    show "connected (- path_image \<gamma>)"
    1.40 +      apply (rule connected_arc_complement [OF assms])
    1.41 +      using False
    1.42 +      by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq order_class.order.antisym)
    1.43 +    show "bounded (path_image \<gamma>)"
    1.44 +      by (simp add: assms bounded_arc_image)
    1.45 +  qed
    1.46 +qed
    1.47 +
    1.48 +lemma inside_simple_curve_imp_closed:
    1.49 +  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
    1.50 +    shows "\<lbrakk>simple_path \<gamma>; x \<in> inside(path_image \<gamma>)\<rbrakk> \<Longrightarrow> pathfinish \<gamma> = pathstart \<gamma>"
    1.51 +  using arc_simple_path  inside_arc_empty by blast
    1.52 +
    1.53 +    
    1.54  subsection \<open>Piecewise differentiable functions\<close>
    1.55  
    1.56  definition piecewise_differentiable_on
    1.57 @@ -3998,29 +4045,29 @@
    1.58  
    1.59  lemma winding_number_constant:
    1.60    assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and cs: "connected s" and sg: "s \<inter> path_image \<gamma> = {}"
    1.61 -    shows "\<exists>k. \<forall>z \<in> s. winding_number \<gamma> z = k"
    1.62 +  obtains k where "\<And>z. z \<in> s \<Longrightarrow> winding_number \<gamma> z = k"
    1.63  proof -
    1.64 -  { fix y z
    1.65 -    assume ne: "winding_number \<gamma> y \<noteq> winding_number \<gamma> z"
    1.66 -    assume "y \<in> s" "z \<in> s"
    1.67 -    then have "winding_number \<gamma> y \<in> \<int>"  "winding_number \<gamma> z \<in>  \<int>"
    1.68 -      using integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> s\<close> by auto
    1.69 -    with ne have "1 \<le> cmod (winding_number \<gamma> y - winding_number \<gamma> z)"
    1.70 +  have *: "1 \<le> cmod (winding_number \<gamma> y - winding_number \<gamma> z)"
    1.71 +      if ne: "winding_number \<gamma> y \<noteq> winding_number \<gamma> z" and "y \<in> s" "z \<in> s" for y z
    1.72 +  proof -
    1.73 +    have "winding_number \<gamma> y \<in> \<int>"  "winding_number \<gamma> z \<in>  \<int>"
    1.74 +      using that integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> s\<close> by auto
    1.75 +    with ne show ?thesis
    1.76        by (auto simp: Ints_def of_int_diff [symmetric] simp del: of_int_diff)
    1.77 -  } note * = this
    1.78 -  show ?thesis
    1.79 -    apply (rule continuous_discrete_range_constant [OF cs])
    1.80 +  qed
    1.81 +  have cont: "continuous_on s (\<lambda>w. winding_number \<gamma> w)"
    1.82      using continuous_on_winding_number [OF \<gamma>] sg
    1.83 -    apply (metis Diff_Compl Diff_eq_empty_iff continuous_on_subset)
    1.84 -    apply (rule_tac x=1 in exI)
    1.85 -    apply (auto simp: *)
    1.86 -    done
    1.87 +    by (meson continuous_on_subset disjoint_eq_subset_Compl)
    1.88 +  show ?thesis
    1.89 +    apply (rule continuous_discrete_range_constant [OF cs cont])
    1.90 +    using "*" zero_less_one apply blast
    1.91 +    by (simp add: that)
    1.92  qed
    1.93  
    1.94  lemma winding_number_eq:
    1.95       "\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; w \<in> s; z \<in> s; connected s; s \<inter> path_image \<gamma> = {}\<rbrakk>
    1.96        \<Longrightarrow> winding_number \<gamma> w = winding_number \<gamma> z"
    1.97 -using winding_number_constant by fastforce
    1.98 +  using winding_number_constant by blast
    1.99  
   1.100  lemma open_winding_number_levelsets:
   1.101    assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
     2.1 --- a/src/HOL/Analysis/Further_Topology.thy	Tue Feb 21 15:04:01 2017 +0000
     2.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Tue Feb 21 17:12:10 2017 +0000
     2.3 @@ -4314,7 +4314,7 @@
     2.4      qed
     2.5    next
     2.6      case False
     2.7 -    have "\<exists>a. \<forall>x\<in>S \<inter> T. g x - h x = a"
     2.8 +    obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
     2.9      proof (rule continuous_discrete_range_constant [OF ST])
    2.10        show "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
    2.11          apply (intro continuous_intros)
    2.12 @@ -4338,15 +4338,14 @@
    2.13          then show ?thesis
    2.14            by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
    2.15        qed
    2.16 -    qed
    2.17 -    then obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a" by blast
    2.18 +    qed blast
    2.19      with False have "exp a = 1"
    2.20        by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
    2.21      with a show ?thesis
    2.22        apply (rule_tac x="\<lambda>x. if x \<in> S then g x else a + h x" in exI)
    2.23        apply (intro continuous_on_cases_local_open opeS opeT contg conth continuous_intros conjI)
    2.24         apply (auto simp: algebra_simps fg fh exp_add)
    2.25 -        done
    2.26 +      done
    2.27    qed
    2.28  qed
    2.29  
    2.30 @@ -4383,7 +4382,7 @@
    2.31      qed
    2.32    next
    2.33      case False
    2.34 -    have "\<exists>a. \<forall>x\<in>S \<inter> T. g x - h x = a"
    2.35 +    obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
    2.36      proof (rule continuous_discrete_range_constant [OF ST])
    2.37        show "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
    2.38          apply (intro continuous_intros)
    2.39 @@ -4407,15 +4406,14 @@
    2.40          then show ?thesis
    2.41            by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
    2.42        qed
    2.43 -    qed
    2.44 -    then obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a" by blast
    2.45 +    qed blast
    2.46      with False have "exp a = 1"
    2.47        by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
    2.48      with a show ?thesis
    2.49        apply (rule_tac x="\<lambda>x. if x \<in> S then g x else a + h x" in exI)
    2.50        apply (intro continuous_on_cases_local cloS cloT contg conth continuous_intros conjI)
    2.51         apply (auto simp: algebra_simps fg fh exp_add)
    2.52 -        done
    2.53 +      done
    2.54    qed
    2.55  qed
    2.56  
    2.57 @@ -4444,7 +4442,9 @@
    2.58    then obtain f' where f': "\<And>y. y \<in> T \<longrightarrow> f' y \<in> S \<and> f (f' y) = y"
    2.59      by metis
    2.60    have *: "\<exists>a. \<forall>x \<in> {x. x \<in> S \<and> f x = y}. h x - h(f' y) = a" if "y \<in> T" for y
    2.61 -  proof (rule continuous_discrete_range_constant, simp_all add: algebra_simps)
    2.62 +  proof (rule continuous_discrete_range_constant [OF conn [OF that], of "\<lambda>x. h x - h (f' y)"], simp_all add: algebra_simps)
    2.63 +    show "continuous_on {x \<in> S. f x = y} (\<lambda>x. h x - h (f' y))"
    2.64 +      by (intro continuous_intros continuous_on_subset [OF conth]) auto
    2.65      show "\<exists>e>0. \<forall>u. u \<in> S \<and> f u = y \<and> h u \<noteq> h x \<longrightarrow> e \<le> cmod (h u - h x)"
    2.66        if x: "x \<in> S \<and> f x = y" for x
    2.67      proof -
    2.68 @@ -4460,9 +4460,7 @@
    2.69        then show ?thesis
    2.70          by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
    2.71      qed
    2.72 -    show "continuous_on {x \<in> S. f x = y} (\<lambda>x. h x - h (f' y))"
    2.73 -      by (intro continuous_intros continuous_on_subset [OF conth]) auto
    2.74 -  qed (simp add: conn that)
    2.75 +  qed 
    2.76    have "h x = h (f' (f x))" if "x \<in> S" for x
    2.77      using * [of "f x"] fim that apply clarsimp
    2.78      by (metis f' imageI right_minus_eq)
     3.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Feb 21 15:04:01 2017 +0000
     3.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Feb 21 17:12:10 2017 +0000
     3.3 @@ -7527,47 +7527,97 @@
     3.4  
     3.5  text \<open>Continuity implies uniform continuity on a compact domain.\<close>
     3.6  
     3.7 -lemma compact_uniformly_continuous:
     3.8 +subsection \<open>Continuity implies uniform continuity on a compact domain.\<close>
     3.9 +
    3.10 +text\<open>From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of
    3.11 +J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)\<close>
    3.12 +
    3.13 +lemma Heine_Borel_lemma:
    3.14 +  assumes "compact S" and Ssub: "S \<subseteq> \<Union>\<G>" and op: "\<And>G. G \<in> \<G> \<Longrightarrow> open G"
    3.15 +  obtains e where "0 < e" "\<And>x. x \<in> S \<Longrightarrow> \<exists>G \<in> \<G>. ball x e \<subseteq> G"
    3.16 +proof -
    3.17 +  have False if neg: "\<And>e. 0 < e \<Longrightarrow> \<exists>x \<in> S. \<forall>G \<in> \<G>. \<not> ball x e \<subseteq> G"
    3.18 +  proof -
    3.19 +    have "\<exists>x \<in> S. \<forall>G \<in> \<G>. \<not> ball x (1 / Suc n) \<subseteq> G" for n
    3.20 +      using neg by simp
    3.21 +    then obtain f where "\<And>n. f n \<in> S" and fG: "\<And>G n. G \<in> \<G> \<Longrightarrow> \<not> ball (f n) (1 / Suc n) \<subseteq> G"
    3.22 +      by metis
    3.23 +    then obtain l r where "l \<in> S" "subseq r" and to_l: "(f \<circ> r) \<longlonglongrightarrow> l"
    3.24 +      using \<open>compact S\<close> compact_def that by metis
    3.25 +    then obtain G where "l \<in> G" "G \<in> \<G>"
    3.26 +      using Ssub by auto
    3.27 +    then obtain e where "0 < e" and e: "\<And>z. dist z l < e \<Longrightarrow> z \<in> G"
    3.28 +      using op open_dist by blast
    3.29 +    obtain N1 where N1: "\<And>n. n \<ge> N1 \<Longrightarrow> dist (f (r n)) l < e/2"
    3.30 +      using to_l apply (simp add: lim_sequentially)
    3.31 +      using \<open>0 < e\<close> half_gt_zero that by blast
    3.32 +    obtain N2 where N2: "of_nat N2 > 2/e"
    3.33 +      using reals_Archimedean2 by blast
    3.34 +    obtain x where "x \<in> ball (f (r (max N1 N2))) (1 / real (Suc (r (max N1 N2))))" and "x \<notin> G"
    3.35 +      using fG [OF \<open>G \<in> \<G>\<close>, of "r (max N1 N2)"] by blast
    3.36 +    then have "dist (f (r (max N1 N2))) x < 1 / real (Suc (r (max N1 N2)))"
    3.37 +      by simp
    3.38 +    also have "... \<le> 1 / real (Suc (max N1 N2))"
    3.39 +      apply (simp add: divide_simps del: max.bounded_iff)
    3.40 +      using \<open>subseq r\<close> seq_suble by blast
    3.41 +    also have "... \<le> 1 / real (Suc N2)"
    3.42 +      by (simp add: field_simps)
    3.43 +    also have "... < e/2"
    3.44 +      using N2 \<open>0 < e\<close> by (simp add: field_simps)
    3.45 +    finally have "dist (f (r (max N1 N2))) x < e / 2" .
    3.46 +    moreover have "dist (f (r (max N1 N2))) l < e/2"
    3.47 +      using N1 max.cobounded1 by blast
    3.48 +    ultimately have "dist x l < e"
    3.49 +      using dist_triangle_half_r by blast
    3.50 +    then show ?thesis
    3.51 +      using e \<open>x \<notin> G\<close> by blast
    3.52 +  qed
    3.53 +  then show ?thesis
    3.54 +    by (meson that)
    3.55 +qed
    3.56 +
    3.57 +lemma compact_uniformly_equicontinuous:
    3.58 +  assumes "compact S"
    3.59 +      and cont: "\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk>
    3.60 +                        \<Longrightarrow> \<exists>d. 0 < d \<and>
    3.61 +                                (\<forall>f \<in> \<F>. \<forall>x' \<in> S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
    3.62 +      and "0 < e"
    3.63 +  obtains d where "0 < d"
    3.64 +                  "\<And>f x x'. \<lbrakk>f \<in> \<F>; x \<in> S; x' \<in> S; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
    3.65 +proof -
    3.66 +  obtain d where d_pos: "\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk> \<Longrightarrow> 0 < d x e"
    3.67 +     and d_dist : "\<And>x x' e f. \<lbrakk>dist x' x < d x e; x \<in> S; x' \<in> S; 0 < e; f \<in> \<F>\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
    3.68 +    using cont by metis
    3.69 +  let ?\<G> = "((\<lambda>x. ball x (d x (e / 2))) ` S)"
    3.70 +  have Ssub: "S \<subseteq> \<Union> ?\<G>"
    3.71 +    by clarsimp (metis d_pos \<open>0 < e\<close> dist_self half_gt_zero_iff)
    3.72 +  then obtain k where "0 < k" and k: "\<And>x. x \<in> S \<Longrightarrow> \<exists>G \<in> ?\<G>. ball x k \<subseteq> G"
    3.73 +    by (rule Heine_Borel_lemma [OF \<open>compact S\<close>]) auto
    3.74 +  moreover have "dist (f v) (f u) < e" if "f \<in> \<F>" "u \<in> S" "v \<in> S" "dist v u < k" for f u v
    3.75 +  proof -
    3.76 +    obtain G where "G \<in> ?\<G>" "u \<in> G" "v \<in> G"
    3.77 +      using k that
    3.78 +      by (metis \<open>dist v u < k\<close> \<open>u \<in> S\<close> \<open>0 < k\<close> centre_in_ball subsetD dist_commute mem_ball)
    3.79 +    then obtain w where w: "dist w u < d w (e / 2)" "dist w v < d w (e / 2)" "w \<in> S"
    3.80 +      by auto
    3.81 +    with that d_dist have "dist (f w) (f v) < e/2"
    3.82 +      by (metis \<open>0 < e\<close> dist_commute half_gt_zero)
    3.83 +    moreover
    3.84 +    have "dist (f w) (f u) < e/2"
    3.85 +      using that d_dist w by (metis \<open>0 < e\<close> dist_commute divide_pos_pos zero_less_numeral)
    3.86 +    ultimately show ?thesis
    3.87 +      using dist_triangle_half_r by blast
    3.88 +  qed
    3.89 +  ultimately show ?thesis using that by blast
    3.90 +qed
    3.91 +
    3.92 +corollary compact_uniformly_continuous:
    3.93    fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
    3.94 -  assumes f: "continuous_on s f"
    3.95 -    and s: "compact s"
    3.96 -  shows "uniformly_continuous_on s f"
    3.97 -  unfolding uniformly_continuous_on_def
    3.98 -proof (cases, safe)
    3.99 -  fix e :: real
   3.100 -  assume "0 < e" "s \<noteq> {}"
   3.101 -  define R where [simp]:
   3.102 -    "R = {(y, d). y \<in> s \<and> 0 < d \<and> ball y d \<inter> s \<subseteq> {x \<in> s. f x \<in> ball (f y) (e/2)}}"
   3.103 -  let ?b = "(\<lambda>(y, d). ball y (d/2))"
   3.104 -  have "(\<forall>r\<in>R. open (?b r))" "s \<subseteq> (\<Union>r\<in>R. ?b r)"
   3.105 -  proof safe
   3.106 -    fix y
   3.107 -    assume "y \<in> s"
   3.108 -    from continuous_openin_preimage_gen[OF f open_ball]
   3.109 -    obtain T where "open T" and T: "{x \<in> s. f x \<in> ball (f y) (e/2)} = T \<inter> s"
   3.110 -      unfolding openin_subtopology open_openin by metis
   3.111 -    then obtain d where "ball y d \<subseteq> T" "0 < d"
   3.112 -      using \<open>0 < e\<close> \<open>y \<in> s\<close> by (auto elim!: openE)
   3.113 -    with T \<open>y \<in> s\<close> show "y \<in> (\<Union>r\<in>R. ?b r)"
   3.114 -      by (intro UN_I[of "(y, d)"]) auto
   3.115 -  qed auto
   3.116 -  with s obtain D where D: "finite D" "D \<subseteq> R" "s \<subseteq> (\<Union>(y, d)\<in>D. ball y (d/2))"
   3.117 -    by (rule compactE_image)
   3.118 -  with \<open>s \<noteq> {}\<close> have [simp]: "\<And>x. x < Min (snd ` D) \<longleftrightarrow> (\<forall>(y, d)\<in>D. x < d)"
   3.119 -    by (subst Min_gr_iff) auto
   3.120 -  show "\<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
   3.121 -  proof (rule, safe)
   3.122 -    fix x x'
   3.123 -    assume in_s: "x' \<in> s" "x \<in> s"
   3.124 -    with D obtain y d where x: "x \<in> ball y (d/2)" "(y, d) \<in> D"
   3.125 -      by blast
   3.126 -    moreover assume "dist x x' < Min (snd`D) / 2"
   3.127 -    ultimately have "dist y x' < d"
   3.128 -      by (intro dist_triangle_half_r[of x _ d]) (auto simp: dist_commute)
   3.129 -    with D x in_s show  "dist (f x) (f x') < e"
   3.130 -      by (intro dist_triangle_half_r[of "f y" _ e]) (auto simp: dist_commute subset_eq)
   3.131 -  qed (insert D, auto)
   3.132 -qed auto
   3.133 +  assumes f: "continuous_on S f" and S: "compact S"
   3.134 +  shows "uniformly_continuous_on S f"
   3.135 +  using f
   3.136 +    unfolding continuous_on_iff uniformly_continuous_on_def
   3.137 +    by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])
   3.138  
   3.139  subsection \<open>Topological stuff about the set of Reals\<close>
   3.140  
   3.141 @@ -10207,6 +10257,46 @@
   3.142         "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
   3.143  by (metis ex_countable_basis topological_basis_def)
   3.144  
   3.145 +lemma subset_second_countable:
   3.146 +  obtains \<B> :: "'a:: euclidean_space set set"
   3.147 +    where "countable \<B>"
   3.148 +          "{} \<notin> \<B>"
   3.149 +          "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
   3.150 +          "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
   3.151 +proof -
   3.152 +  obtain \<B> :: "'a set set"
   3.153 +    where "countable \<B>"
   3.154 +      and opeB: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
   3.155 +      and \<B>:    "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
   3.156 +  proof -
   3.157 +    obtain \<C> :: "'a set set"
   3.158 +      where "countable \<C>" and ope: "\<And>C. C \<in> \<C> \<Longrightarrow> open C"
   3.159 +        and \<C>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<C> \<and> S = \<Union>U"
   3.160 +      by (metis univ_second_countable that)
   3.161 +    show ?thesis
   3.162 +    proof
   3.163 +      show "countable ((\<lambda>C. S \<inter> C) ` \<C>)"
   3.164 +        by (simp add: \<open>countable \<C>\<close>)
   3.165 +      show "\<And>C. C \<in> op \<inter> S ` \<C> \<Longrightarrow> openin (subtopology euclidean S) C"
   3.166 +        using ope by auto
   3.167 +      show "\<And>T. openin (subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>\<subseteq>op \<inter> S ` \<C>. T = \<Union>\<U>"
   3.168 +        by (metis \<C> image_mono inf_Sup openin_open)
   3.169 +    qed
   3.170 +  qed
   3.171 +  show ?thesis
   3.172 +  proof
   3.173 +    show "countable (\<B> - {{}})"
   3.174 +      using \<open>countable \<B>\<close> by blast
   3.175 +    show "\<And>C. \<lbrakk>C \<in> \<B> - {{}}\<rbrakk> \<Longrightarrow> openin (subtopology euclidean S) C"
   3.176 +      by (simp add: \<open>\<And>C. C \<in> \<B> \<Longrightarrow> openin (subtopology euclidean S) C\<close>)
   3.177 +    show "\<exists>\<U>\<subseteq>\<B> - {{}}. T = \<Union>\<U>" if "openin (subtopology euclidean S) T" for T
   3.178 +      using \<B> [OF that]
   3.179 +      apply clarify
   3.180 +      apply (rule_tac x="\<U> - {{}}" in exI, auto)
   3.181 +        done
   3.182 +  qed auto
   3.183 +qed
   3.184 +
   3.185  lemma univ_second_countable_sequence:
   3.186    obtains B :: "nat \<Rightarrow> 'a::euclidean_space set"
   3.187      where "inj B" "\<And>n. open(B n)" "\<And>S. open S \<Longrightarrow> \<exists>k. S = \<Union>{B n |n. n \<in> k}"
   3.188 @@ -10244,6 +10334,52 @@
   3.189      done
   3.190  qed
   3.191  
   3.192 +proposition separable:
   3.193 +  fixes S :: "'a:: euclidean_space set"
   3.194 +  obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
   3.195 +proof -
   3.196 +  obtain \<B> :: "'a:: euclidean_space set set"
   3.197 +    where "countable \<B>"
   3.198 +      and "{} \<notin> \<B>"
   3.199 +      and ope: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
   3.200 +      and if_ope: "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
   3.201 +    by (meson subset_second_countable)
   3.202 +  then obtain f where f: "\<And>C. C \<in> \<B> \<Longrightarrow> f C \<in> C"
   3.203 +    by (metis equals0I)
   3.204 +  show ?thesis
   3.205 +  proof
   3.206 +    show "countable (f ` \<B>)"
   3.207 +      by (simp add: \<open>countable \<B>\<close>)
   3.208 +    show "f ` \<B> \<subseteq> S"
   3.209 +      using ope f openin_imp_subset by blast
   3.210 +    show "S \<subseteq> closure (f ` \<B>)"
   3.211 +    proof (clarsimp simp: closure_approachable)
   3.212 +      fix x and e::real
   3.213 +      assume "x \<in> S" "0 < e"
   3.214 +      have "openin (subtopology euclidean S) (S \<inter> ball x e)"
   3.215 +        by (simp add: openin_Int_open)
   3.216 +      with if_ope obtain \<U> where  \<U>: "\<U> \<subseteq> \<B>" "S \<inter> ball x e = \<Union>\<U>"
   3.217 +        by meson
   3.218 +      show "\<exists>C \<in> \<B>. dist (f C) x < e"
   3.219 +      proof (cases "\<U> = {}")
   3.220 +        case True
   3.221 +        then show ?thesis
   3.222 +          using \<open>0 < e\<close>  \<U> \<open>x \<in> S\<close> by auto
   3.223 +      next
   3.224 +        case False
   3.225 +        then obtain C where "C \<in> \<U>" by blast
   3.226 +        show ?thesis
   3.227 +        proof
   3.228 +          show "dist (f C) x < e"
   3.229 +            by (metis Int_iff Union_iff \<U> \<open>C \<in> \<U>\<close> dist_commute f mem_ball subsetCE)
   3.230 +          show "C \<in> \<B>"
   3.231 +            using \<open>\<U> \<subseteq> \<B>\<close> \<open>C \<in> \<U>\<close> by blast
   3.232 +        qed
   3.233 +      qed
   3.234 +    qed
   3.235 +  qed
   3.236 +qed
   3.237 +
   3.238  proposition Lindelof:
   3.239    fixes \<F> :: "'a::euclidean_space set set"
   3.240    assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
   3.241 @@ -10789,21 +10925,21 @@
   3.242  qed
   3.243  
   3.244  lemma continuous_disconnected_range_constant_eq:
   3.245 -      "(connected s \<longleftrightarrow>
   3.246 +      "(connected S \<longleftrightarrow>
   3.247             (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   3.248 -            \<forall>t. continuous_on s f \<and> f ` s \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
   3.249 -            \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis1)
   3.250 +            \<forall>t. continuous_on S f \<and> f ` S \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
   3.251 +            \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis1)
   3.252    and continuous_discrete_range_constant_eq:
   3.253 -      "(connected s \<longleftrightarrow>
   3.254 +      "(connected S \<longleftrightarrow>
   3.255           (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   3.256 -          continuous_on s f \<and>
   3.257 -          (\<forall>x \<in> s. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> s \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
   3.258 -          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis2)
   3.259 +          continuous_on S f \<and>
   3.260 +          (\<forall>x \<in> S. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> S \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
   3.261 +          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis2)
   3.262    and continuous_finite_range_constant_eq:
   3.263 -      "(connected s \<longleftrightarrow>
   3.264 +      "(connected S \<longleftrightarrow>
   3.265           (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   3.266 -          continuous_on s f \<and> finite (f ` s)
   3.267 -          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis3)
   3.268 +          continuous_on S f \<and> finite (f ` S)
   3.269 +          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis3)
   3.270  proof -
   3.271    have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
   3.272      \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
   3.273 @@ -10822,19 +10958,19 @@
   3.274  
   3.275  lemma continuous_discrete_range_constant:
   3.276    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
   3.277 -  assumes s: "connected s"
   3.278 -      and "continuous_on s f"
   3.279 -      and "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
   3.280 -    shows "\<exists>a. \<forall>x \<in> s. f x = a"
   3.281 -  using continuous_discrete_range_constant_eq [THEN iffD1, OF s] assms
   3.282 +  assumes S: "connected S"
   3.283 +      and "continuous_on S f"
   3.284 +      and "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
   3.285 +    obtains a where "\<And>x. x \<in> S \<Longrightarrow> f x = a"
   3.286 +  using continuous_discrete_range_constant_eq [THEN iffD1, OF S] assms
   3.287    by blast
   3.288  
   3.289  lemma continuous_finite_range_constant:
   3.290    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
   3.291 -  assumes "connected s"
   3.292 -      and "continuous_on s f"
   3.293 -      and "finite (f ` s)"
   3.294 -    shows "\<exists>a. \<forall>x \<in> s. f x = a"
   3.295 +  assumes "connected S"
   3.296 +      and "continuous_on S f"
   3.297 +      and "finite (f ` S)"
   3.298 +    obtains a where "\<And>x. x \<in> S \<Longrightarrow> f x = a"
   3.299    using assms continuous_finite_range_constant_eq
   3.300    by blast
   3.301  
     4.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Tue Feb 21 15:04:01 2017 +0000
     4.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Tue Feb 21 17:12:10 2017 +0000
     4.3 @@ -519,7 +519,7 @@
     4.4      using lte by (force intro: eventually_mono)
     4.5  qed
     4.6  
     4.7 -lemma uniform_lim_div:
     4.8 +lemma uniform_lim_divide:
     4.9    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_field"
    4.10    assumes f: "uniform_limit S f l F"
    4.11        and g: "uniform_limit S g m F"