# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1475150335 -3600
# Node ID 51a3d38d2281af1d54adcc0eabeebeac2eb208f3
# Parent  fb03766658f41b2b554623d0e38ac23ea3d5fa04
more new material

diff -r fb03766658f4 -r 51a3d38d2281 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Sep 29 11:24:36 2016 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Sep 29 12:58:55 2016 +0100
@@ -129,24 +129,28 @@
     have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b}" (is "?diff_fg")
     proof (cases x c rule: le_cases)
       case le show ?diff_fg
-        apply (rule differentiable_transform_within [where d = "dist x c" and f = f])
-        using x le st
-        apply (simp_all add: dist_real_def)
-        apply (rule differentiable_at_withinI)
-        apply (rule differentiable_within_open [where s = "{a<..<c} - s", THEN iffD1], simp_all)
-        apply (blast intro: open_greaterThanLessThan finite_imp_closed)
-        apply (force elim!: differentiable_subset)+
-        done
+      proof (rule differentiable_transform_within [where d = "dist x c" and f = f])
+        have "f differentiable at x within ({a<..<c} - s)"
+          apply (rule differentiable_at_withinI)
+          using x le st
+          by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost le st(3) x)
+        moreover have "open ({a<..<c} - s)"
+          by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed)
+        ultimately show "f differentiable at x within {a..b}"
+          using x le by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI) 
+      qed (use x le st dist_real_def in auto)
     next
       case ge show ?diff_fg
-        apply (rule differentiable_transform_within [where d = "dist x c" and f = g])
-        using x ge st
-        apply (simp_all add: dist_real_def)
-        apply (rule differentiable_at_withinI)
-        apply (rule differentiable_within_open [where s = "{c<..<b} - t", THEN iffD1], simp_all)
-        apply (blast intro: open_greaterThanLessThan finite_imp_closed)
-        apply (force elim!: differentiable_subset)+
-        done
+      proof (rule differentiable_transform_within [where d = "dist x c" and f = g])
+        have "g differentiable at x within ({c<..<b} - t)"
+          apply (rule differentiable_at_withinI)
+          using x ge st
+          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost)
+        moreover have "open ({c<..<b} - t)"
+          by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed)
+        ultimately show "g differentiable at x within {a..b}"
+          using x ge by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI) 
+      qed (use x ge st dist_real_def in auto)
     qed
   }
   then have "\<exists>s. finite s \<and>
@@ -3801,7 +3805,7 @@
   moreover have "{a<..<b} - k \<subseteq> {a..b} - k"
     by force
   ultimately have g_diff_at: "\<And>x. \<lbrakk>x \<notin> k; x \<in> {a<..<b}\<rbrakk> \<Longrightarrow> \<gamma> differentiable at x"
-    by (metis Diff_iff differentiable_on_subset C1_diff_imp_diff [OF g_C1_diff] differentiable_on_def differentiable_within_open)
+    by (metis Diff_iff differentiable_on_subset C1_diff_imp_diff [OF g_C1_diff] differentiable_on_def at_within_open)
   { fix w
     assume "w \<noteq> z"
     have "continuous_on (ball w (cmod (w - z))) (\<lambda>w. 1 / (w - z))"
@@ -7527,4 +7531,32 @@
 by (metis Cauchy_theorem_global assms winding_number_zero_in_outside valid_path_imp_path)
 
 
+lemma simply_connected_imp_winding_number_zero:
+  assumes "simply_connected s" "path g"
+           "path_image g \<subseteq> s" "pathfinish g = pathstart g" "z \<notin> s"
+    shows "winding_number g z = 0"
+proof -
+  have "winding_number g z = winding_number(linepath (pathstart g) (pathstart g)) z"
+    apply (rule winding_number_homotopic_paths)
+    apply (rule homotopic_loops_imp_homotopic_paths_null [where a = "pathstart g"])
+    apply (rule homotopic_loops_subset [of s])
+    using assms
+    apply (auto simp: homotopic_paths_imp_homotopic_loops path_defs simply_connected_eq_contractible_path)
+    done
+  also have "... = 0"
+    using assms by (force intro: winding_number_trivial)
+  finally show ?thesis .
+qed
+
+lemma Cauchy_theorem_simply_connected:
+  assumes "open s" "simply_connected s" "f holomorphic_on s" "valid_path g"
+           "path_image g \<subseteq> s" "pathfinish g = pathstart g"
+    shows "(f has_contour_integral 0) g"
+using assms
+apply (simp add: simply_connected_eq_contractible_path)
+apply (auto intro!: Cauchy_theorem_null_homotopic [where a = "pathstart g"]
+                         homotopic_paths_imp_homotopic_loops)
+using valid_path_imp_path by blast
+
+
 end
diff -r fb03766658f4 -r 51a3d38d2281 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Sep 29 11:24:36 2016 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Sep 29 12:58:55 2016 +0100
@@ -8697,6 +8697,59 @@
 apply (simp add: rel_frontier_def convex_affine_closure_Int frontier_def)
 by (metis Diff_Int_distrib2 Int_emptyI convex_affine_closure_Int convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen)
 
+lemma rel_interior_convex_Int_affine:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" "affine T" "interior S \<inter> T \<noteq> {}"
+    shows "rel_interior(S \<inter> T) = interior S \<inter> T"
+proof -
+  obtain a where aS: "a \<in> interior S" and aT:"a \<in> T"
+    using assms by force
+  have "rel_interior S = interior S"
+    by (metis (no_types) aS affine_hull_nonempty_interior equals0D rel_interior_interior)
+  then show ?thesis
+    by (metis (no_types) affine_imp_convex assms convex_rel_interior_inter_two hull_same rel_interior_affine_hull)
+qed
+
+lemma closure_convex_Int_affine:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" "affine T" "rel_interior S \<inter> T \<noteq> {}"
+  shows "closure(S \<inter> T) = closure S \<inter> T"
+proof
+  have "closure (S \<inter> T) \<subseteq> closure T"
+    by (simp add: closure_mono)
+  also have "... \<subseteq> T"
+    by (simp add: affine_closed assms)
+  finally show "closure(S \<inter> T) \<subseteq> closure S \<inter> T"
+    by (simp add: closure_mono)
+next
+  obtain a where "a \<in> rel_interior S" "a \<in> T"
+    using assms by auto
+  then have ssT: "subspace ((\<lambda>x. (-a)+x) ` T)" and "a \<in> S"
+    using affine_diffs_subspace rel_interior_subset assms by blast+
+  show "closure S \<inter> T \<subseteq> closure (S \<inter> T)"
+  proof
+    fix x  assume "x \<in> closure S \<inter> T"
+    show "x \<in> closure (S \<inter> T)"
+    proof (cases "x = a")
+      case True
+      then show ?thesis
+        using \<open>a \<in> S\<close> \<open>a \<in> T\<close> closure_subset by fastforce
+    next
+      case False
+      then have "x \<in> closure(open_segment a x)"
+        by auto
+      then show ?thesis
+        using \<open>x \<in> closure S \<inter> T\<close> assms convex_affine_closure_Int by blast
+    qed
+  qed
+qed
+
+lemma rel_frontier_convex_Int_affine:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" "affine T" "interior S \<inter> T \<noteq> {}"
+    shows "rel_frontier(S \<inter> T) = frontier S \<inter> T"
+by (simp add: assms convex_affine_rel_frontier_Int)
+
 lemma subset_rel_interior_convex:
   fixes S T :: "'n::euclidean_space set"
   assumes "convex S"
diff -r fb03766658f4 -r 51a3d38d2281 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Thu Sep 29 11:24:36 2016 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Thu Sep 29 12:58:55 2016 +0100
@@ -180,13 +180,6 @@
   shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
   by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
 
-lemma differentiable_within_open: (* TODO: delete *)
-  assumes "a \<in> s"
-    and "open s"
-  shows "f differentiable (at a within s) \<longleftrightarrow> f differentiable (at a)"
-  using assms
-  by (simp only: at_within_interior interior_open)
-
 lemma differentiable_on_eq_differentiable_at:
   "open s \<Longrightarrow> f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x)"
   unfolding differentiable_on_def
@@ -207,6 +200,15 @@
 lemma differentiable_on_id [simp, derivative_intros]: "id differentiable_on S"
   by (simp add: id_def)
 
+lemma differentiable_on_const [simp, derivative_intros]: "(\<lambda>z. c) differentiable_on S"
+  by (simp add: differentiable_on_def)
+
+lemma differentiable_on_mult [simp, derivative_intros]:
+  fixes f :: "'M::real_normed_vector \<Rightarrow> 'a::real_normed_algebra"
+  shows "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) differentiable_on S"
+  apply (simp add: differentiable_on_def differentiable_def)
+  using differentiable_def differentiable_mult by blast
+
 lemma differentiable_on_compose:
    "\<lbrakk>g differentiable_on S; f differentiable_on (g ` S)\<rbrakk> \<Longrightarrow> (\<lambda>x. f (g x)) differentiable_on S"
 by (simp add: differentiable_in_compose differentiable_on_def)
diff -r fb03766658f4 -r 51a3d38d2281 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Sep 29 11:24:36 2016 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Sep 29 12:58:55 2016 +0100
@@ -2315,10 +2315,10 @@
    "outside s \<inter> s = {}"
   by (auto simp: outside_def)
 
-lemma inside_inter_outside [simp]: "inside s \<inter> outside s = {}"
+lemma inside_Int_outside [simp]: "inside s \<inter> outside s = {}"
   by (auto simp: inside_def outside_def)
 
-lemma inside_union_outside [simp]: "inside s \<union> outside s = (- s)"
+lemma inside_Un_outside [simp]: "inside s \<union> outside s = (- s)"
   by (auto simp: inside_def outside_def)
 
 lemma inside_eq_outside:
@@ -2606,7 +2606,7 @@
   by (simp add: inside_def connected_component_UNIV)
 
 lemma outside_empty [simp]: "outside {} = (UNIV :: 'a :: {real_normed_vector, perfect_space} set)"
-using inside_empty inside_union_outside by blast
+using inside_empty inside_Un_outside by blast
 
 lemma inside_same_component:
    "\<lbrakk>connected_component (- s) x y; x \<in> inside s\<rbrakk> \<Longrightarrow> y \<in> inside s"
@@ -2666,7 +2666,7 @@
   fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   assumes "convex s"
     shows "outside s = - s"
-  by (metis ComplD assms convex_in_outside equalityI inside_union_outside subsetI sup.cobounded2)
+  by (metis ComplD assms convex_in_outside equalityI inside_Un_outside subsetI sup.cobounded2)
 
 lemma inside_convex:
   fixes s :: "'a :: {real_normed_vector, perfect_space} set"
@@ -2761,7 +2761,7 @@
   have "closure (inside s) \<inter> - inside s = closure (inside s) - interior (inside s)"
     by (metis (no_types) Diff_Compl assms closure_closed interior_closure open_closed open_inside)
   moreover have "- inside s \<inter> - outside s = s"
-    by (metis (no_types) compl_sup double_compl inside_union_outside)
+    by (metis (no_types) compl_sup double_compl inside_Un_outside)
   moreover have "closure (inside s) \<subseteq> - outside s"
     by (metis (no_types) assms closure_inside_subset union_with_inside)
   ultimately have "closure (inside s) - interior (inside s) \<subseteq> s"
@@ -5460,21 +5460,6 @@
 
 subsection\<open>Components, continuity, openin, closedin\<close>
 
-lemma continuous_openin_preimage_eq:
-   "continuous_on S f \<longleftrightarrow>
-    (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
-apply (auto simp: continuous_openin_preimage_gen)
-apply (fastforce simp add: continuous_on_open openin_open)
-done
-
-lemma continuous_closedin_preimage_eq:
-   "continuous_on S f \<longleftrightarrow>
-    (\<forall>t. closed t \<longrightarrow> closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
-apply safe
-apply (simp add: continuous_closedin_preimage)
-apply (fastforce simp add: continuous_on_closed closedin_closed)
-done
-
 lemma continuous_on_components_gen:
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   assumes "\<And>c. c \<in> components S \<Longrightarrow>
@@ -6108,7 +6093,6 @@
 apply (metis assms homotopy_eqv_homotopic_triviality_imp)
 by (metis (no_types) assms homotopy_eqv_homotopic_triviality_imp homotopy_eqv_sym)
 
-
 lemma homotopy_eqv_cohomotopic_triviality_null_imp:
   fixes S :: "'a::real_normed_vector set"
     and T :: "'b::real_normed_vector set"
@@ -6156,7 +6140,6 @@
 apply (metis assms homotopy_eqv_cohomotopic_triviality_null_imp)
 by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_eqv_sym)
 
-
 lemma homotopy_eqv_contractible_sets:
   fixes S :: "'a::real_normed_vector set"
     and T :: "'b::real_normed_vector set"
@@ -6215,6 +6198,50 @@
 lemma homeomorphic_contractible:
   fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
   shows "\<lbrakk>contractible S; S homeomorphic T\<rbrakk> \<Longrightarrow> contractible T"
-by (metis homeomorphic_contractible_eq)
+  by (metis homeomorphic_contractible_eq)
+
+subsection\<open>Misc other results\<close>
+
+lemma bounded_connected_Compl_real:
+  fixes S :: "real set"
+  assumes "bounded S" and conn: "connected(- S)"
+    shows "S = {}"
+proof -
+  obtain a b where "S \<subseteq> box a b"
+    by (meson assms bounded_subset_open_interval)
+  then have "a \<notin> S" "b \<notin> S"
+    by auto
+  then have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> - S"
+    by (meson Compl_iff conn connected_iff_interval)
+  then show ?thesis
+    using \<open>S \<subseteq> box a b\<close> by auto
+qed
+
+lemma bounded_connected_Compl_1:
+  fixes S :: "'a::{euclidean_space} set"
+  assumes "bounded S" and conn: "connected(- S)" and 1: "DIM('a) = 1"
+    shows "S = {}"
+proof -
+  have "DIM('a) = DIM(real)"
+    by (simp add: "1")
+  then obtain f::"'a \<Rightarrow> real" and g
+  where "linear f" "\<And>x. norm(f x) = norm x" "\<And>x. g(f x) = x" "\<And>y. f(g y) = y"
+    by (rule isomorphisms_UNIV_UNIV) blast
+  with \<open>bounded S\<close> have "bounded (f ` S)"
+    using bounded_linear_image linear_linear by blast
+  have "connected (f ` (-S))"
+    using connected_linear_image assms \<open>linear f\<close> by blast
+  moreover have "f ` (-S) = - (f ` S)"
+    apply (rule bij_image_Compl_eq)
+    apply (auto simp: bij_def)
+     apply (metis \<open>\<And>x. g (f x) = x\<close> injI)
+    by (metis UNIV_I \<open>\<And>y. f (g y) = y\<close> image_iff)
+  finally have "connected (- (f ` S))"
+    by simp
+  then have "f ` S = {}"
+    using \<open>bounded (f ` S)\<close> bounded_connected_Compl_real by blast
+  then show ?thesis
+    by blast
+qed
 
 end
diff -r fb03766658f4 -r 51a3d38d2281 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Sep 29 11:24:36 2016 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Sep 29 12:58:55 2016 +0100
@@ -550,6 +550,11 @@
 lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
   by auto
 
+lemma closedin_Union:
+  assumes "finite S" "\<And>T. T \<in> S \<Longrightarrow> closedin U T"
+    shows "closedin U (\<Union>S)"
+  using assms by induction auto
+
 lemma closedin_Inter[intro]:
   assumes Ke: "K \<noteq> {}"
     and Kc: "\<And>S. S \<in>K \<Longrightarrow> closedin U S"
@@ -6164,6 +6169,22 @@
     using * by auto
 qed
 
+lemma continuous_openin_preimage_eq:
+   "continuous_on S f \<longleftrightarrow>
+    (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+apply safe
+apply (simp add: continuous_openin_preimage_gen)
+apply (fastforce simp add: continuous_on_open openin_open)
+done
+
+lemma continuous_closedin_preimage_eq:
+   "continuous_on S f \<longleftrightarrow>
+    (\<forall>t. closed t \<longrightarrow> closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+apply safe
+apply (simp add: continuous_closedin_preimage)
+apply (fastforce simp add: continuous_on_closed closedin_closed)
+done
+
 lemma continuous_open_preimage:
   assumes "continuous_on s f"
     and "open s"
@@ -9893,6 +9914,101 @@
     by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
 qed
 
+subsection\<open>Pasting functions together\<close>
+
+subsubsection\<open>on open sets\<close>
+
+lemma pasting_lemma:
+  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
+      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+      and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
+    shows "continuous_on S g"
+proof (clarsimp simp: continuous_openin_preimage_eq)
+  fix U :: "'b set"
+  assume "open U"
+  have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
+    using clo openin_imp_subset by blast
+  have *: "{x \<in> S. g x \<in> U} = \<Union>{{x. x \<in> (T i) \<and> (f i x) \<in> U} |i. i \<in> I}"
+    apply (auto simp: dest: S)
+      apply (metis (no_types, lifting) g mem_Collect_eq)
+    using clo f g openin_imp_subset by fastforce
+  show "openin (subtopology euclidean S) {x \<in> S. g x \<in> U}"
+    apply (subst *)
+    apply (rule openin_Union, clarify)
+    apply (metis (full_types) \<open>open U\<close> cont clo openin_trans continuous_openin_preimage_gen)
+    done
+qed 
+
+lemma pasting_lemma_exists:
+  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes S: "S \<subseteq> (\<Union>i \<in> I. T i)"
+      and clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
+      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+    obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
+proof
+  show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
+    apply (rule pasting_lemma [OF clo cont])
+     apply (blast intro: f)+
+    apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
+    done
+next
+  fix x i
+  assume "i \<in> I" "x \<in> S \<inter> T i"
+  then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
+    by (metis (no_types, lifting) IntD2 IntI f someI_ex)
+qed
+
+subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close>
+
+lemma pasting_lemma_closed:
+  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes "finite I"
+      and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
+      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+      and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
+    shows "continuous_on S g"
+proof (clarsimp simp: continuous_closedin_preimage_eq)
+  fix U :: "'b set"
+  assume "closed U"
+  have *: "{x \<in> S. g x \<in> U} = \<Union>{{x. x \<in> (T i) \<and> (f i x) \<in> U} |i. i \<in> I}"
+    apply auto
+    apply (metis (no_types, lifting) g mem_Collect_eq)
+    using clo closedin_closed apply blast
+    apply (metis Int_iff f g clo closedin_limpt inf.absorb_iff2)
+    done
+  show "closedin (subtopology euclidean S) {x \<in> S. g x \<in> U}"
+    apply (subst *)
+    apply (rule closedin_Union)
+    using \<open>finite I\<close> apply simp
+    apply (blast intro: \<open>closed U\<close> continuous_closedin_preimage cont clo closedin_trans)
+    done
+qed
+
+lemma pasting_lemma_exists_closed:
+  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes "finite I"
+      and S: "S \<subseteq> (\<Union>i \<in> I. T i)"
+      and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
+      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+    obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
+proof
+  show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
+    apply (rule pasting_lemma_closed [OF \<open>finite I\<close> clo cont])
+     apply (blast intro: f)+
+    apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
+    done
+next
+  fix x i
+  assume "i \<in> I" "x \<in> S \<inter> T i"
+  then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
+    by (metis (no_types, lifting) IntD2 IntI f someI_ex)
+qed
+
 
 no_notation
   eucl_less (infix "<e" 50)