# HG changeset patch
# User paulson
# Date 1556301644 -3600
# Node ID ebd40fa4da8aa5726644902e002c0e7b617c4aa3
# Parent  b7ef9090feed2f85c5c0f287e2692c9f25d3a1ec# Parent  e383580ffc3539f99dfb97812386f15ee4bbc8f8
merged

diff -r e383580ffc35 -r ebd40fa4da8a src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Apr 26 19:00:44 2019 +0100
@@ -3,9 +3,40 @@
 text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>
 
 theory Cauchy_Integral_Theorem
-imports Complex_Transcendental Weierstrass_Theorems Ordered_Euclidean_Space
+imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Ordered_Euclidean_Space
 begin
 
+lemma leibniz_rule_holomorphic:
+  fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex"
+  assumes "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>x. f x t) has_field_derivative fx x t) (at x within U)"
+  assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
+  assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
+  assumes "convex U"
+  shows "(\<lambda>x. integral (cbox a b) (f x)) holomorphic_on U"
+  using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)]
+  by (auto simp: holomorphic_on_def)
+
+lemma Ln_measurable [measurable]: "Ln \<in> measurable borel borel"
+proof -
+  have *: "Ln (-of_real x) = of_real (ln x) + \<i> * pi" if "x > 0" for x
+    using that by (subst Ln_minus) (auto simp: Ln_of_real)
+  have **: "Ln (of_real x) = of_real (ln (-x)) + \<i> * pi" if "x < 0" for x
+    using *[of "-x"] that by simp
+  have cont: "(\<lambda>x. indicat_real (- \<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel_measurable borel"
+    by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
+  have "(\<lambda>x. if x \<in> \<real>\<^sub>\<le>\<^sub>0 then ln (-Re x) + \<i> * pi else indicator (-\<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel \<rightarrow>\<^sub>M borel"
+    (is "?f \<in> _") by (rule measurable_If_set[OF _ cont]) auto
+  hence "(\<lambda>x. if x = 0 then Ln 0 else ?f x) \<in> borel \<rightarrow>\<^sub>M borel" by measurable
+  also have "(\<lambda>x. if x = 0 then Ln 0 else ?f x) = Ln"
+    by (auto simp: fun_eq_iff ** nonpos_Reals_def)
+  finally show ?thesis .
+qed
+
+lemma powr_complex_measurable [measurable]:
+  assumes [measurable]: "f \<in> measurable M borel" "g \<in> measurable M borel"
+  shows   "(\<lambda>x. f x powr g x :: complex) \<in> measurable M borel"
+  using assms by (simp add: powr_def)
+
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Homeomorphisms of arc images\<close>
 
 lemma homeomorphism_arc:
diff -r e383580ffc35 -r ebd40fa4da8a src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Apr 26 19:00:44 2019 +0100
@@ -5,7 +5,7 @@
 section \<open>Complex Analysis Basics\<close>
 
 theory Complex_Analysis_Basics
-imports Equivalence_Lebesgue_Henstock_Integration "HOL-Library.Nonpos_Ints"
+  imports Derivative "HOL-Library.Nonpos_Ints"
 begin
 
 (* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *)
@@ -83,31 +83,6 @@
 lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
   by (intro continuous_on_id continuous_on_norm)
 
-(*MOVE? But not to Finite_Cartesian_Product*)
-lemma sums_vec_nth :
-  assumes "f sums a"
-  shows "(\<lambda>x. f x $ i) sums a $ i"
-using assms unfolding sums_def
-by (auto dest: tendsto_vec_nth [where i=i])
-
-lemma summable_vec_nth :
-  assumes "summable f"
-  shows "summable (\<lambda>x. f x $ i)"
-using assms unfolding summable_def
-by (blast intro: sums_vec_nth)
-
-(* TODO: Move? *)
-lemma DERIV_zero_connected_constant:
-  fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
-  assumes "connected S"
-      and "open S"
-      and "finite K"
-      and "continuous_on S f"
-      and "\<forall>x\<in>(S - K). DERIV f x :> 0"
-    obtains c where "\<And>x. x \<in> S \<Longrightarrow> f(x) = c"
-using has_derivative_zero_connected_constant [OF assms(1-4)] assms
-by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def)
-
 lemmas DERIV_zero_constant = has_field_derivative_zero_constant
 
 lemma DERIV_zero_unique:
@@ -394,16 +369,6 @@
   finally show \<dots> .
 qed (insert assms, auto)
 
-lemma leibniz_rule_holomorphic:
-  fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex"
-  assumes "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>x. f x t) has_field_derivative fx x t) (at x within U)"
-  assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
-  assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
-  assumes "convex U"
-  shows "(\<lambda>x. integral (cbox a b) (f x)) holomorphic_on U"
-  using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)]
-  by (auto simp: holomorphic_on_def)
-
 lemma DERIV_deriv_iff_field_differentiable:
   "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
   unfolding field_differentiable_def by (metis DERIV_imp_deriv)
diff -r e383580ffc35 -r ebd40fa4da8a src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Fri Apr 26 19:00:44 2019 +0100
@@ -4,9 +4,7 @@
 
 theory Complex_Transcendental
 imports
-  Complex_Analysis_Basics
-  Summation_Tests
-   "HOL-Library.Periodic_Fun"
+  Complex_Analysis_Basics Summation_Tests "HOL-Library.Periodic_Fun"
 begin
 
 subsection\<open>Möbius transformations\<close>
@@ -875,7 +873,7 @@
   have zr: "z = (cmod z) * exp (\<i> * r)" and zs: "z = (cmod z) * exp (\<i> * s)"
     using r s by (auto simp: is_Arg_def)
   with \<open>z \<noteq> 0\<close> have eq: "exp (\<i> * r) = exp (\<i> * s)"
-    by (metis mult_eq_0_iff vector_space_over_itself.scale_left_imp_eq)
+    by (metis mult_eq_0_iff mult_left_cancel)
   have  "\<i> * r = \<i> * s"
     by (rule exp_complex_eqI) (use rs in \<open>auto simp: eq exp_complex_eqI\<close>)
   then show ?thesis
@@ -1728,27 +1726,6 @@
   finally show ?thesis .
 qed
 
-lemma Ln_measurable [measurable]: "Ln \<in> measurable borel borel"
-proof -
-  have *: "Ln (-of_real x) = of_real (ln x) + \<i> * pi" if "x > 0" for x
-    using that by (subst Ln_minus) (auto simp: Ln_of_real)
-  have **: "Ln (of_real x) = of_real (ln (-x)) + \<i> * pi" if "x < 0" for x
-    using *[of "-x"] that by simp
-  have cont: "(\<lambda>x. indicat_real (- \<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel_measurable borel"
-    by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
-  have "(\<lambda>x. if x \<in> \<real>\<^sub>\<le>\<^sub>0 then ln (-Re x) + \<i> * pi else indicator (-\<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel \<rightarrow>\<^sub>M borel"
-    (is "?f \<in> _") by (rule measurable_If_set[OF _ cont]) auto
-  hence "(\<lambda>x. if x = 0 then Ln 0 else ?f x) \<in> borel \<rightarrow>\<^sub>M borel" by measurable
-  also have "(\<lambda>x. if x = 0 then Ln 0 else ?f x) = Ln"
-    by (auto simp: fun_eq_iff ** nonpos_Reals_def)
-  finally show ?thesis .
-qed
-
-lemma powr_complex_measurable [measurable]:
-  assumes [measurable]: "f \<in> measurable M borel" "g \<in> measurable M borel"
-  shows   "(\<lambda>x. f x powr g x :: complex) \<in> measurable M borel"
-  using assms by (simp add: powr_def)
-
 subsection\<open>The Argument of a Complex Number\<close>
 
 text\<open>Finally: it's is defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>
diff -r e383580ffc35 -r ebd40fa4da8a src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Fri Apr 26 19:00:44 2019 +0100
@@ -3,7 +3,7 @@
 text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
 
 theory Further_Topology
-  imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental
+  imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration
 begin
 
 subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
@@ -4644,8 +4644,8 @@
     proof (rule upper_lower_hemicontinuous_explicit [of T "\<lambda>y. {z \<in> S. f z = y}" S])
       show "\<And>U. openin (top_of_set S) U
                  \<Longrightarrow> openin (top_of_set T) {x \<in> T. {z \<in> S. f z = x} \<subseteq> U}"
-        using continuous_imp_closed_map closed_map_iff_upper_hemicontinuous_preimage [OF fim [THEN equalityD1]]
-        by (simp add: continuous_imp_closed_map \<open>compact S\<close> contf fim)
+        using closed_map_iff_upper_hemicontinuous_preimage [OF fim [THEN equalityD1]]
+        by (simp add: Abstract_Topology_2.continuous_imp_closed_map \<open>compact S\<close> contf fim)
       show "\<And>U. closedin (top_of_set S) U \<Longrightarrow>
                  closedin (top_of_set T) {x \<in> T. {z \<in> S. f z = x} \<subseteq> U}"
         using  ope open_map_iff_lower_hemicontinuous_preimage [OF fim [THEN equalityD1]]
diff -r e383580ffc35 -r ebd40fa4da8a src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Fri Apr 26 19:00:44 2019 +0100
@@ -5,8 +5,9 @@
 section \<open>The Gamma Function\<close>
 
 theory Gamma_Function
-imports
+  imports
   Conformal_Mappings
+  Equivalence_Lebesgue_Henstock_Integration
   Summation_Tests
   Harmonic_Numbers
   "HOL-Library.Nonpos_Ints"
diff -r e383580ffc35 -r ebd40fa4da8a src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Apr 26 19:00:44 2019 +0100
@@ -7,8 +7,7 @@
 
 theory Henstock_Kurzweil_Integration
 imports
-  Lebesgue_Measure
-  Tagged_Division
+  Lebesgue_Measure Tagged_Division
 begin
 
 lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
@@ -4436,7 +4435,7 @@
 proof (cases "S = {}")
   case True
   then show ?thesis
-by (metis empty_iff that)
+    by (metis empty_iff that)
 next
   case False
   then obtain c where "c \<in> S"
@@ -4445,6 +4444,17 @@
     by (metis has_derivative_zero_unique_strong_connected assms that)
 qed
 
+lemma DERIV_zero_connected_constant:
+  fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
+  assumes "connected S"
+      and "open S"
+      and "finite K"
+      and "continuous_on S f"
+      and "\<forall>x\<in>(S - K). DERIV f x :> 0"
+    obtains c where "\<And>x. x \<in> S \<Longrightarrow> f(x) = c"
+  using has_derivative_zero_connected_constant [OF assms(1-4)] assms
+  by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def)
+
 
 subsection \<open>Integrating characteristic function of an interval\<close>
 
diff -r e383580ffc35 -r ebd40fa4da8a src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Fri Apr 26 19:00:44 2019 +0100
@@ -5655,22 +5655,20 @@
       by auto
     let ?h = "\<lambda>y. g (a + (fst y) *\<^sub>R (snd y - a))"
     have "continuous_on ({0..1} \<times> sphere a r) ?h"
-      apply (rule continuous_on_compose2 [OF contg])
-       apply (intro continuous_intros)
-      apply (auto simp: dist_norm norm_minus_commute mult_left_le_one_le)
-      done
+    proof (rule continuous_on_compose2 [OF contg])
+      show "continuous_on ({0..1} \<times> sphere a r) (\<lambda>x. a + fst x *\<^sub>R (snd x - a))"
+        by (intro continuous_intros)
+      qed (auto simp: dist_norm norm_minus_commute mult_left_le_one_le)
     moreover
     have "?h ` ({0..1} \<times> sphere a r) \<subseteq> S"
       by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gim [THEN subsetD])
     moreover
     have "\<forall>x\<in>sphere a r. ?h (0, x) = g a" "\<forall>x\<in>sphere a r. ?h (1, x) = f x"
       by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gf)
-    ultimately
-    show ?lhs
-      apply (subst homotopic_with_sym)
-      apply (rule_tac x="g a" in exI)
-      apply (auto simp: homotopic_with)
-      done
+    ultimately have "homotopic_with_canon (\<lambda>x. True) (sphere a r) S (\<lambda>x. g a) f"
+      by (auto simp: homotopic_with)
+    then show ?lhs
+      using homotopic_with_symD by blast
   qed
   ultimately
   show ?thesis by meson
diff -r e383580ffc35 -r ebd40fa4da8a src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Apr 26 19:00:44 2019 +0100
@@ -188,6 +188,18 @@
   shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
   by (metis interval_cbox vec_nth_1_iff_cbox)
 
+lemma sums_vec_nth :
+  assumes "f sums a"
+  shows "(\<lambda>x. f x $ i) sums a $ i"
+  using assms unfolding sums_def
+  by (auto dest: tendsto_vec_nth [where i=i])
+
+lemma summable_vec_nth :
+  assumes "summable f"
+  shows "summable (\<lambda>x. f x $ i)"
+  using assms unfolding summable_def
+  by (blast intro: sums_vec_nth)
+
 lemma closed_eucl_atLeastAtMost[simp, intro]:
   fixes a :: "'a::ordered_euclidean_space"
   shows "closed {a..b}"
diff -r e383580ffc35 -r ebd40fa4da8a src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Fri Apr 26 19:00:44 2019 +0100
@@ -5,7 +5,7 @@
 section \<open>Path-Connectedness\<close>
 
 theory Path_Connected
-  imports Starlike
+  imports Starlike T1_Spaces
 begin
 
 subsection \<open>Paths and Arcs\<close>
@@ -3786,8 +3786,192 @@
       apply (rule **)   (*such a horrible mess*)
       apply (rule connected_Int_frontier [where t = "f`S", OF connected_ball])
       using \<open>a \<in> S\<close> \<open>0 < r\<close>
-      apply (auto simp: disjoint_iff_not_equal  dist_norm)
+      apply (auto simp: disjoint_iff_not_equal dist_norm)
       by (metis dw_le norm_minus_commute not_less order_trans rle wy)
 qed
 
+
+subsubsection\<open>Special characterizations of classes of functions into and out of R.\<close>
+
+proposition embedding_map_into_euclideanreal:
+  assumes "path_connected_space X"
+  shows "embedding_map X euclideanreal f \<longleftrightarrow>
+         continuous_map X euclideanreal f \<and> inj_on f (topspace X)"
+  proof safe
+  show "continuous_map X euclideanreal f"
+    if "embedding_map X euclideanreal f"
+    using continuous_map_in_subtopology homeomorphic_imp_continuous_map that
+    unfolding embedding_map_def by blast
+  show "inj_on f (topspace X)"
+    if "embedding_map X euclideanreal f"
+    using that homeomorphic_imp_injective_map
+    unfolding embedding_map_def by blast
+  show "embedding_map X euclideanreal f"
+    if cont: "continuous_map X euclideanreal f" and inj: "inj_on f (topspace X)"
+  proof -
+    obtain g where gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g (f x) = x"
+      using inv_into_f_f [OF inj] by auto
+    show ?thesis
+      unfolding embedding_map_def homeomorphic_map_maps homeomorphic_maps_def
+    proof (intro exI conjI)
+      show "continuous_map X (top_of_set (f ` topspace X)) f"
+        by (simp add: cont continuous_map_in_subtopology)
+      let ?S = "f ` topspace X"
+      have eq: "{x \<in> ?S. g x \<in> U} = f ` U" if "openin X U" for U
+        using openin_subset [OF that] by (auto simp: gf)
+      have 1: "g ` ?S \<subseteq> topspace X"
+        using eq by blast
+      have "openin (top_of_set ?S) {x \<in> ?S. g x \<in> T}"
+        if "openin X T" for T
+      proof -
+        have "T \<subseteq> topspace X"
+          by (simp add: openin_subset that)
+        have RR: "\<forall>x \<in> ?S \<inter> g -` T. \<exists>d>0. \<forall>x' \<in> ?S \<inter> ball x d. g x' \<in> T"
+        proof (clarsimp simp add: gf)
+          have pcS: "path_connectedin euclidean ?S"
+            using assms cont path_connectedin_continuous_map_image path_connectedin_topspace by blast
+          show "\<exists>d>0. \<forall>x'\<in>f ` topspace X \<inter> ball (f x) d. g x' \<in> T"
+            if "x \<in> T" for x
+          proof -
+            have x: "x \<in> topspace X"
+              using \<open>T \<subseteq> topspace X\<close> \<open>x \<in> T\<close> by blast
+            obtain u v d where "0 < d" "u \<in> topspace X" "v \<in> topspace X"
+                         and sub_fuv: "?S \<inter> {f x - d .. f x + d} \<subseteq> {f u..f v}"
+            proof (cases "\<exists>u \<in> topspace X. f u < f x")
+              case True
+              then obtain u where u: "u \<in> topspace X" "f u < f x" ..
+              show ?thesis
+              proof (cases "\<exists>v \<in> topspace X. f x < f v")
+                case True
+                then obtain v where v: "v \<in> topspace X" "f x < f v" ..
+                show ?thesis
+                proof
+                  let ?d = "min (f x - f u) (f v - f x)"
+                  show "0 < ?d"
+                    by (simp add: \<open>f u < f x\<close> \<open>f x < f v\<close>)
+                  show "f ` topspace X \<inter> {f x - ?d..f x + ?d} \<subseteq> {f u..f v}"
+                    by fastforce
+                qed (auto simp: u v)
+              next
+                case False
+                show ?thesis
+                proof
+                  let ?d = "f x - f u"
+                  show "0 < ?d"
+                    by (simp add: u)
+                  show "f ` topspace X \<inter> {f x - ?d..f x + ?d} \<subseteq> {f u..f x}"
+                    using x u False by auto
+                qed (auto simp: x u)
+              qed
+            next
+              case False
+              note no_u = False
+              show ?thesis
+              proof (cases "\<exists>v \<in> topspace X. f x < f v")
+                case True
+                then obtain v where v: "v \<in> topspace X" "f x < f v" ..
+                show ?thesis
+                proof
+                  let ?d = "f v - f x"
+                  show "0 < ?d"
+                    by (simp add: v)
+                  show "f ` topspace X \<inter> {f x - ?d..f x + ?d} \<subseteq> {f x..f v}"
+                    using False by auto
+                qed (auto simp: x v)
+              next
+                case False
+                show ?thesis
+                proof
+                  show "f ` topspace X \<inter> {f x - 1..f x + 1} \<subseteq> {f x..f x}"
+                    using False no_u by fastforce
+                qed (auto simp: x)
+              qed
+            qed
+            then obtain h where "pathin X h" "h 0 = u" "h 1 = v"
+              using assms unfolding path_connected_space_def by blast
+            obtain C where "compactin X C" "connectedin X C" "u \<in> C" "v \<in> C"
+            proof
+              show "compactin X (h ` {0..1})"
+                using that by (simp add: \<open>pathin X h\<close> compactin_path_image)
+              show "connectedin X (h ` {0..1})"
+                using \<open>pathin X h\<close> connectedin_path_image by blast
+            qed (use \<open>h 0 = u\<close> \<open>h 1 = v\<close> in auto)
+            have "continuous_map (subtopology euclideanreal (?S \<inter> {f x - d .. f x + d})) (subtopology X C) g"
+            proof (rule continuous_inverse_map)
+              show "compact_space (subtopology X C)"
+                using \<open>compactin X C\<close> compactin_subspace by blast
+              show "continuous_map (subtopology X C) euclideanreal f"
+                by (simp add: cont continuous_map_from_subtopology)
+              have "{f u .. f v} \<subseteq> f ` topspace (subtopology X C)"
+              proof (rule connected_contains_Icc)
+                show "connected (f ` topspace (subtopology X C))"
+                  using connectedin_continuous_map_image [OF cont]
+                  by (simp add: \<open>compactin X C\<close> \<open>connectedin X C\<close> compactin_subset_topspace inf_absorb2)
+                show "f u \<in> f ` topspace (subtopology X C)"
+                  by (simp add: \<open>u \<in> C\<close> \<open>u \<in> topspace X\<close>)
+                show "f v \<in> f ` topspace (subtopology X C)"
+                  by (simp add: \<open>v \<in> C\<close> \<open>v \<in> topspace X\<close>)
+              qed
+              then show "f ` topspace X \<inter> {f x - d..f x + d} \<subseteq> f ` topspace (subtopology X C)"
+                using sub_fuv by blast
+            qed (auto simp: gf)
+            then have contg: "continuous_map (subtopology euclideanreal (?S \<inter> {f x - d .. f x + d})) X g"
+              using continuous_map_in_subtopology by blast
+            have "\<exists>e>0. \<forall>x \<in> ?S \<inter> {f x - d .. f x + d} \<inter> ball (f x) e. g x \<in> T"
+              using openin_continuous_map_preimage [OF contg \<open>openin X T\<close>] x \<open>x \<in> T\<close> \<open>0 < d\<close>
+              unfolding openin_euclidean_subtopology_iff
+              by (force simp: gf dist_commute)
+            then obtain e where "e > 0 \<and> (\<forall>x\<in>f ` topspace X \<inter> {f x - d..f x + d} \<inter> ball (f x) e. g x \<in> T)"
+              by metis
+            with \<open>0 < d\<close> have "min d e > 0" "\<forall>u. u \<in> topspace X \<longrightarrow> \<bar>f x - f u\<bar> < min d e \<longrightarrow> u \<in> T"
+              using dist_real_def gf by force+
+            then show ?thesis
+              by (metis (full_types) Int_iff dist_real_def image_iff mem_ball gf)
+          qed
+        qed
+        then obtain d where d: "\<And>r. r \<in> ?S \<inter> g -` T \<Longrightarrow>
+                d r > 0 \<and> (\<forall>x \<in> ?S \<inter> ball r (d r). g x \<in> T)"
+          by metis
+        show ?thesis
+          unfolding openin_subtopology
+        proof (intro exI conjI)
+          show "{x \<in> ?S. g x \<in> T} = (\<Union>r \<in> ?S \<inter> g -` T. ball r (d r)) \<inter> f ` topspace X"
+            using d by (auto simp: gf)
+        qed auto
+      qed
+      then show "continuous_map (top_of_set ?S) X g"
+        by (simp add: continuous_map_def gf)
+    qed (auto simp: gf)
+  qed
+qed
+
+subsubsection \<open>An injective function into R is a homeomorphism and so an open map.\<close>
+
+lemma injective_into_1d_eq_homeomorphism:
+  fixes f :: "'a::topological_space \<Rightarrow> real"
+  assumes f: "continuous_on S f" and S: "path_connected S"
+  shows "inj_on f S \<longleftrightarrow> (\<exists>g. homeomorphism S (f ` S) f g)"
+proof
+  show "\<exists>g. homeomorphism S (f ` S) f g"
+    if "inj_on f S"
+  proof -
+    have "embedding_map (top_of_set S) euclideanreal f"
+      using that embedding_map_into_euclideanreal [of "top_of_set S" f] assms by auto
+    then show ?thesis
+      by (simp add: embedding_map_def) (metis all_closedin_homeomorphic_image f homeomorphism_injective_closed_map that)
+  qed
+qed (metis homeomorphism_def inj_onI)
+
+lemma injective_into_1d_imp_open_map:
+  fixes f :: "'a::topological_space \<Rightarrow> real"
+  assumes "continuous_on S f" "path_connected S" "inj_on f S" "openin (subtopology euclidean S) T"
+  shows "openin (subtopology euclidean (f ` S)) (f ` T)"
+  using assms homeomorphism_imp_open_map injective_into_1d_eq_homeomorphism by blast
+
+lemma homeomorphism_into_1d:
+  fixes f :: "'a::topological_space \<Rightarrow> real"
+  assumes "path_connected S" "continuous_on S f" "f ` S = T" "inj_on f S"
+  shows "\<exists>g. homeomorphism S T f g"
+  using assms injective_into_1d_eq_homeomorphism by blast
+
 end
diff -r e383580ffc35 -r ebd40fa4da8a src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy	Fri Apr 26 19:00:44 2019 +0100
@@ -507,22 +507,22 @@
 qed
 
 lemma continuous_imp_closed_map:
-   "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f\<rbrakk> \<Longrightarrow> closed_map X Y f"
+   "\<lbrakk>continuous_map X Y f; compact_space X; Hausdorff_space Y\<rbrakk> \<Longrightarrow> closed_map X Y f"
   by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin)
 
 lemma continuous_imp_quotient_map:
-   "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f; f ` (topspace X) = topspace Y\<rbrakk>
+   "\<lbrakk>continuous_map X Y f; compact_space X; Hausdorff_space Y; f ` (topspace X) = topspace Y\<rbrakk>
         \<Longrightarrow> quotient_map X Y f"
   by (simp add: continuous_imp_closed_map continuous_closed_imp_quotient_map)
 
 lemma continuous_imp_homeomorphic_map:
-   "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f;
+   "\<lbrakk>continuous_map X Y f; compact_space X; Hausdorff_space Y; 
      f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
         \<Longrightarrow> homeomorphic_map X Y f"
   by (simp add: continuous_imp_closed_map bijective_closed_imp_homeomorphic_map)
 
 lemma continuous_imp_embedding_map:
-   "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f; inj_on f (topspace X)\<rbrakk>
+   "\<lbrakk>continuous_map X Y f; compact_space X; Hausdorff_space Y; inj_on f (topspace X)\<rbrakk>
         \<Longrightarrow> embedding_map X Y f"
   by (simp add: continuous_imp_closed_map injective_closed_imp_embedding_map)
 
diff -r e383580ffc35 -r ebd40fa4da8a src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Apr 26 19:00:02 2019 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Apr 26 19:00:44 2019 +0100
@@ -531,8 +531,8 @@
           SEQ(List(
             init,
             build_history_base,
+            build_release,
             PAR(
-              build_release ::
               List(remote_builds1, remote_builds2).map(remote_builds =>
               SEQ(List(
                 PAR(remote_builds.map(_.filter(_.active)).map(seq =>