# 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 \Path-Connectedness\ theory Path_Connected - imports Starlike T1_Spaces +imports + Starlike + T1_Spaces begin subsection \Paths and Arcs\ @@ -2081,6 +2083,48 @@ "path_component_of X x y \ 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 \ topspace X \ p x \ q x}) Y f" + and contg: "continuous_map (subtopology X {x. x \ topspace X \ q x \ p x}) Y g" + and fg: "\x. \x \ topspace X; p x = q x\ \ f x = g x" + shows "continuous_map X Y (\x. if p x \ q x then f x else g x)" +proof - + have "continuous_map X Y (\x. if q x - p x \ {0..} then f x else g x)" + proof (rule continuous_map_cases_function) + show "continuous_map X euclideanreal (\x. q x - p x)" + by (intro contp contq continuous_intros) + show "continuous_map (subtopology X {x \ topspace X. q x - p x \ euclideanreal closure_of {0..}}) Y f" + by (simp add: contf) + show "continuous_map (subtopology X {x \ topspace X. q x - p x \ 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 \ topspace X \ p x \ q x}) Y f" + and contg: "continuous_map (subtopology X {x. x \ topspace X \ q x \ p x}) Y g" + and fg: "\x. \x \ topspace X; p x = q x\ \ f x = g x" + shows "continuous_map X Y (\x. if p x < q x then f x else g x)" +proof - + have "continuous_map X Y (\x. if q x - p x \ {0<..} then f x else g x)" + proof (rule continuous_map_cases_function) + show "continuous_map X euclideanreal (\x. q x - p x)" + by (intro contp contq continuous_intros) + show "continuous_map (subtopology X {x \ topspace X. q x - p x \ euclideanreal closure_of {0<..}}) Y f" + by (simp add: contf) + show "continuous_map (subtopology X {x \ topspace X. q x - p x \ 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 \ topspace X \ p x \ q x}) Y f" - and contg: "continuous_map (subtopology X {x. x \ topspace X \ q x \ p x}) Y g" - and fg: "\x. \x \ topspace X; p x = q x\ \ f x = g x" - shows "continuous_map X Y (\x. if p x \ q x then f x else g x)" -proof - - have "continuous_map X Y (\x. if q x - p x \ {0..} then f x else g x)" - proof (rule continuous_map_cases_function) - show "continuous_map X euclideanreal (\x. q x - p x)" - by (intro contp contq continuous_intros) - show "continuous_map (subtopology X {x \ topspace X. q x - p x \ euclideanreal closure_of {0..}}) Y f" - by (simp add: contf) - show "continuous_map (subtopology X {x \ topspace X. q x - p x \ 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 \ topspace X \ p x \ q x}) Y f" - and contg: "continuous_map (subtopology X {x. x \ topspace X \ q x \ p x}) Y g" - and fg: "\x. \x \ topspace X; p x = q x\ \ f x = g x" - shows "continuous_map X Y (\x. if p x < q x then f x else g x)" -proof - - have "continuous_map X Y (\x. if q x - p x \ {0<..} then f x else g x)" - proof (rule continuous_map_cases_function) - show "continuous_map X euclideanreal (\x. q x - p x)" - by (intro contp contq continuous_intros) - show "continuous_map (subtopology X {x \ topspace X. q x - p x \ euclideanreal closure_of {0<..}}) Y f" - by (simp add: contf) - show "continuous_map (subtopology X {x \ topspace X. q x - p x \ 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>\tag unimportant\\The union of two collinear segments is another segment\ proposition\<^marker>\tag unimportant\ in_convex_hull_exchange: