# HG changeset patch
# User nipkow
# Date 1575550269 -3600
# Node ID da73ee7606437e997958e868123b5ba641871427
# Parent  d12c58e12c51863ae0001ab5d668c83cea0ef132# Parent  6c1ed478605ed701f8184417f23d2962ba333382
merged

diff -r d12c58e12c51 -r da73ee760643 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Dec 05 09:24:34 2019 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Dec 05 13:51:09 2019 +0100
@@ -5,7 +5,9 @@
 section \<open>Path-Connectedness\<close>
 
 theory Path_Connected
-  imports Starlike T1_Spaces
+imports
+  Starlike
+  T1_Spaces
 begin
 
 subsection \<open>Paths and Arcs\<close>
@@ -2081,6 +2083,48 @@
    "path_component_of X x y \<longleftrightarrow> path_component_of X y x"
   by (metis path_component_of_sym)
 
+lemma continuous_map_cases_le:
+  assumes contp: "continuous_map X euclideanreal p"
+    and contq: "continuous_map X euclideanreal q"
+    and contf: "continuous_map (subtopology X {x. x \<in> topspace X \<and> p x \<le> q x}) Y f"
+    and contg: "continuous_map (subtopology X {x. x \<in> topspace X \<and> q x \<le> p x}) Y g"
+    and fg: "\<And>x. \<lbrakk>x \<in> topspace X; p x = q x\<rbrakk> \<Longrightarrow> f x = g x"
+  shows "continuous_map X Y (\<lambda>x. if p x \<le> q x then f x else g x)"
+proof -
+  have "continuous_map X Y (\<lambda>x. if q x - p x \<in> {0..} then f x else g x)"
+  proof (rule continuous_map_cases_function)
+    show "continuous_map X euclideanreal (\<lambda>x. q x - p x)"
+      by (intro contp contq continuous_intros)
+    show "continuous_map (subtopology X {x \<in> topspace X. q x - p x \<in> euclideanreal closure_of {0..}}) Y f"
+      by (simp add: contf)
+    show "continuous_map (subtopology X {x \<in> topspace X. q x - p x \<in> euclideanreal closure_of (topspace euclideanreal - {0..})}) Y g"
+      by (simp add: contg flip: Compl_eq_Diff_UNIV)
+  qed (auto simp: fg)
+  then show ?thesis
+    by simp
+qed
+
+lemma continuous_map_cases_lt:
+  assumes contp: "continuous_map X euclideanreal p"
+    and contq: "continuous_map X euclideanreal q"
+    and contf: "continuous_map (subtopology X {x. x \<in> topspace X \<and> p x \<le> q x}) Y f"
+    and contg: "continuous_map (subtopology X {x. x \<in> topspace X \<and> q x \<le> p x}) Y g"
+    and fg: "\<And>x. \<lbrakk>x \<in> topspace X; p x = q x\<rbrakk> \<Longrightarrow> f x = g x"
+  shows "continuous_map X Y (\<lambda>x. if p x < q x then f x else g x)"
+proof -
+  have "continuous_map X Y (\<lambda>x. if q x - p x \<in> {0<..} then f x else g x)"
+  proof (rule continuous_map_cases_function)
+    show "continuous_map X euclideanreal (\<lambda>x. q x - p x)"
+      by (intro contp contq continuous_intros)
+    show "continuous_map (subtopology X {x \<in> topspace X. q x - p x \<in> euclideanreal closure_of {0<..}}) Y f"
+      by (simp add: contf)
+    show "continuous_map (subtopology X {x \<in> topspace X. q x - p x \<in> euclideanreal closure_of (topspace euclideanreal - {0<..})}) Y g"
+      by (simp add: contg flip: Compl_eq_Diff_UNIV)
+  qed (auto simp: fg)
+  then show ?thesis
+    by simp
+qed
+
 lemma path_component_of_trans:
   assumes "path_component_of X x y" and "path_component_of X y z"
   shows "path_component_of X x z"
diff -r d12c58e12c51 -r da73ee760643 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Dec 05 09:24:34 2019 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Thu Dec 05 13:51:09 2019 +0100
@@ -10,7 +10,6 @@
 theory Starlike
   imports
     Convex_Euclidean_Space
-    Abstract_Limits
     Line_Segment
 begin
 
@@ -6110,48 +6109,6 @@
     by (rule continuous_on_Un_local_open [OF opS opT])
 qed
 
-lemma continuous_map_cases_le:
-  assumes contp: "continuous_map X euclideanreal p"
-    and contq: "continuous_map X euclideanreal q"
-    and contf: "continuous_map (subtopology X {x. x \<in> topspace X \<and> p x \<le> q x}) Y f"
-    and contg: "continuous_map (subtopology X {x. x \<in> topspace X \<and> q x \<le> p x}) Y g"
-    and fg: "\<And>x. \<lbrakk>x \<in> topspace X; p x = q x\<rbrakk> \<Longrightarrow> f x = g x"
-  shows "continuous_map X Y (\<lambda>x. if p x \<le> q x then f x else g x)"
-proof -
-  have "continuous_map X Y (\<lambda>x. if q x - p x \<in> {0..} then f x else g x)"
-  proof (rule continuous_map_cases_function)
-    show "continuous_map X euclideanreal (\<lambda>x. q x - p x)"
-      by (intro contp contq continuous_intros)
-    show "continuous_map (subtopology X {x \<in> topspace X. q x - p x \<in> euclideanreal closure_of {0..}}) Y f"
-      by (simp add: contf)
-    show "continuous_map (subtopology X {x \<in> topspace X. q x - p x \<in> euclideanreal closure_of (topspace euclideanreal - {0..})}) Y g"
-      by (simp add: contg flip: Compl_eq_Diff_UNIV)
-  qed (auto simp: fg)
-  then show ?thesis
-    by simp
-qed
-
-lemma continuous_map_cases_lt:
-  assumes contp: "continuous_map X euclideanreal p"
-    and contq: "continuous_map X euclideanreal q"
-    and contf: "continuous_map (subtopology X {x. x \<in> topspace X \<and> p x \<le> q x}) Y f"
-    and contg: "continuous_map (subtopology X {x. x \<in> topspace X \<and> q x \<le> p x}) Y g"
-    and fg: "\<And>x. \<lbrakk>x \<in> topspace X; p x = q x\<rbrakk> \<Longrightarrow> f x = g x"
-  shows "continuous_map X Y (\<lambda>x. if p x < q x then f x else g x)"
-proof -
-  have "continuous_map X Y (\<lambda>x. if q x - p x \<in> {0<..} then f x else g x)"
-  proof (rule continuous_map_cases_function)
-    show "continuous_map X euclideanreal (\<lambda>x. q x - p x)"
-      by (intro contp contq continuous_intros)
-    show "continuous_map (subtopology X {x \<in> topspace X. q x - p x \<in> euclideanreal closure_of {0<..}}) Y f"
-      by (simp add: contf)
-    show "continuous_map (subtopology X {x \<in> topspace X. q x - p x \<in> euclideanreal closure_of (topspace euclideanreal - {0<..})}) Y g"
-      by (simp add: contg flip: Compl_eq_Diff_UNIV)
-  qed (auto simp: fg)
-  then show ?thesis
-    by simp
-qed
-
 subsection\<^marker>\<open>tag unimportant\<close>\<open>The union of two collinear segments is another segment\<close>
 
 proposition\<^marker>\<open>tag unimportant\<close> in_convex_hull_exchange: