New results about paths, segments, etc. The notion of simply_connected.
--- a/src/HOL/Complex.thy Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Complex.thy Mon Mar 14 15:58:02 2016 +0000
@@ -673,9 +673,10 @@
subsection\<open>Polar Form for Complex Numbers\<close>
-lemma complex_unimodular_polar: "(norm z = 1) \<Longrightarrow> \<exists>x. z = Complex (cos x) (sin x)"
- using sincos_total_2pi [of "Re z" "Im z"]
- by auto (metis cmod_power2 complex_eq power_one)
+lemma complex_unimodular_polar:
+ assumes "(norm z = 1)"
+ obtains t where "0 \<le> t" "t < 2*pi" "z = Complex (cos t) (sin t)"
+by (metis cmod_power2 one_power2 complex_surj sincos_total_2pi [of "Re z" "Im z"] assms)
subsubsection \<open>$\cos \theta + i \sin \theta$\<close>
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 14 15:58:02 2016 +0000
@@ -6,6 +6,38 @@
imports Complex_Transcendental Weierstrass Ordered_Euclidean_Space
begin
+subsection\<open>Homeomorphisms of arc images\<close>
+
+lemma homeomorphism_arc:
+ fixes g :: "real \<Rightarrow> 'a::t2_space"
+ assumes "arc g"
+ obtains h where "homeomorphism {0..1} (path_image g) g h"
+using assms by (force simp add: arc_def homeomorphism_compact path_def path_image_def)
+
+lemma homeomorphic_arc_image_interval:
+ fixes g :: "real \<Rightarrow> 'a::t2_space" and a::real
+ assumes "arc g" "a < b"
+ shows "(path_image g) homeomorphic {a..b}"
+proof -
+ have "(path_image g) homeomorphic {0..1::real}"
+ by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc)
+ also have "... homeomorphic {a..b}"
+ using assms by (force intro: homeomorphic_closed_intervals_real)
+ finally show ?thesis .
+qed
+
+lemma homeomorphic_arc_images:
+ fixes g :: "real \<Rightarrow> 'a::t2_space" and h :: "real \<Rightarrow> 'b::t2_space"
+ assumes "arc g" "arc h"
+ shows "(path_image g) homeomorphic (path_image h)"
+proof -
+ have "(path_image g) homeomorphic {0..1::real}"
+ by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc)
+ also have "... homeomorphic (path_image h)"
+ by (meson assms homeomorphic_def homeomorphism_arc)
+ finally show ?thesis .
+qed
+
subsection \<open>Piecewise differentiable functions\<close>
definition piecewise_differentiable_on
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Mar 14 15:58:02 2016 +0000
@@ -3661,6 +3661,14 @@
then show ?thesis using * by auto
qed
+lemma rel_interior_eq:
+ "rel_interior s = s \<longleftrightarrow> openin(subtopology euclidean (affine hull s)) s"
+using rel_open rel_open_def by blast
+
+lemma rel_interior_openin:
+ "openin(subtopology euclidean (affine hull s)) s \<Longrightarrow> rel_interior s = s"
+by (simp add: rel_interior_eq)
+
subsubsection\<open>Relative interior preserves under linear transformations\<close>
@@ -6678,6 +6686,226 @@
by (auto intro: rel_interior_closure_convex_shrink)
qed
+subsection\<open>More results about segments\<close>
+
+lemma dist_half_times2:
+ fixes a :: "'a :: real_normed_vector"
+ shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
+proof -
+ have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
+ by simp
+ also have "... = norm ((a + b) - 2 *\<^sub>R x)"
+ by (simp add: real_vector.scale_right_diff_distrib)
+ finally show ?thesis
+ by (simp only: dist_norm)
+qed
+
+lemma closed_segment_as_ball:
+ "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
+proof (cases "b = a")
+ case True then show ?thesis by (auto simp: hull_inc)
+next
+ case False
+ then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
+ (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
+ proof -
+ have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
+ ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
+ unfolding eq_diff_eq [symmetric] by simp
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
+ by (simp add: dist_half_times2) (simp add: dist_norm)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
+ by auto
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
+ by (simp add: algebra_simps scaleR_2)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
+ by simp
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
+ by (simp add: mult_le_cancel_right2 False)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
+ by auto
+ finally show ?thesis .
+ qed
+ show ?thesis
+ by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
+qed
+
+lemma open_segment_as_ball:
+ "open_segment a b =
+ affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
+proof (cases "b = a")
+ case True then show ?thesis by (auto simp: hull_inc)
+next
+ case False
+ then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
+ (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
+ proof -
+ have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
+ ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
+ unfolding eq_diff_eq [symmetric] by simp
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
+ by (simp add: dist_half_times2) (simp add: dist_norm)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
+ by auto
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
+ by (simp add: algebra_simps scaleR_2)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
+ by simp
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
+ by (simp add: mult_le_cancel_right2 False)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
+ by auto
+ finally show ?thesis .
+ qed
+ show ?thesis
+ using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
+qed
+
+lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
+
+lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
+ by auto
+
+lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
+proof -
+ { assume a1: "open_segment a b = {}"
+ have "{} \<noteq> {0::real<..<1}"
+ by simp
+ then have "a = b"
+ using a1 open_segment_image_interval by fastforce
+ } then show ?thesis by auto
+qed
+
+lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
+ using open_segment_eq_empty by blast
+
+lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
+
+lemma inj_segment:
+ fixes a :: "'a :: real_vector"
+ assumes "a \<noteq> b"
+ shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
+proof
+ fix x y
+ assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
+ then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
+ by (simp add: algebra_simps)
+ with assms show "x = y"
+ by (simp add: real_vector.scale_right_imp_eq)
+qed
+
+lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
+ apply auto
+ apply (rule ccontr)
+ apply (simp add: segment_image_interval)
+ using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
+ done
+
+lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
+ by (auto simp: open_segment_def)
+
+lemmas finite_segment = finite_closed_segment finite_open_segment
+
+lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
+ by auto
+
+lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
+ by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
+
+lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
+
+lemma subset_closed_segment:
+ "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
+ a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+ by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
+
+lemma subset_co_segment:
+ "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
+ a \<in> open_segment c d \<and> b \<in> open_segment c d"
+using closed_segment_subset by blast
+
+lemma subset_open_segment:
+ fixes a :: "'a::euclidean_space"
+ shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
+ a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+ (is "?lhs = ?rhs")
+proof (cases "a = b")
+ case True then show ?thesis by simp
+next
+ case False show ?thesis
+ proof
+ assume rhs: ?rhs
+ with \<open>a \<noteq> b\<close> have "c \<noteq> d"
+ using closed_segment_idem singleton_iff by auto
+ have "\<exists>uc. (1 - u) *\<^sub>R ((1 - ua) *\<^sub>R c + ua *\<^sub>R d) + u *\<^sub>R ((1 - ub) *\<^sub>R c + ub *\<^sub>R d) =
+ (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
+ if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
+ and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
+ and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
+ for u ua ub
+ proof -
+ have "ua \<noteq> ub"
+ using neq by auto
+ moreover have "(u - 1) * ua \<le> 0" using u uab
+ by (simp add: mult_nonpos_nonneg)
+ ultimately have lt: "(u - 1) * ua < u * ub" using u uab
+ by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
+ have "p * ua + q * ub < p+q" if p: "0 < p" and q: "0 < q" for p q
+ proof -
+ have "\<not> p \<le> 0" "\<not> q \<le> 0"
+ using p q not_less by blast+
+ then show ?thesis
+ by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
+ less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
+ qed
+ then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
+ by (metis diff_add_cancel diff_gt_0_iff_gt)
+ with lt show ?thesis
+ by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
+ qed
+ with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
+ unfolding open_segment_image_interval closed_segment_def
+ by (fastforce simp add:)
+ next
+ assume lhs: ?lhs
+ with \<open>a \<noteq> b\<close> have "c \<noteq> d"
+ by (meson finite_open_segment rev_finite_subset)
+ have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
+ using lhs closure_mono by blast
+ then have "closed_segment a b \<subseteq> closed_segment c d"
+ by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
+ then show ?rhs
+ by (force simp: \<open>a \<noteq> b\<close>)
+ qed
+qed
+
+lemma subset_oc_segment:
+ fixes a :: "'a::euclidean_space"
+ shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
+ a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+apply (simp add: subset_open_segment [symmetric])
+apply (rule iffI)
+ apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
+apply (meson dual_order.trans segment_open_subset_closed)
+done
+
+lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
+
+
subsection\<open>Betweenness\<close>
lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
@@ -7647,6 +7875,35 @@
shows "A \<inter> closure S = {} \<longleftrightarrow> A \<inter> rel_interior S = {}"
by (metis assms convex_closure_rel_interior open_inter_closure_eq_empty)
+lemma rel_interior_open_segment:
+ fixes a :: "'a :: euclidean_space"
+ shows "rel_interior(open_segment a b) = open_segment a b"
+proof (cases "a = b")
+ case True then show ?thesis by auto
+next
+ case False then show ?thesis
+ apply (simp add: rel_interior_eq openin_open)
+ apply (rule_tac x="ball (inverse 2 *\<^sub>R (a + b)) (norm(b - a) / 2)" in exI)
+ apply (simp add: open_segment_as_ball)
+ done
+qed
+
+lemma rel_interior_closed_segment:
+ fixes a :: "'a :: euclidean_space"
+ shows "rel_interior(closed_segment a b) =
+ (if a = b then {a} else open_segment a b)"
+proof (cases "a = b")
+ case True then show ?thesis by auto
+next
+ case False then show ?thesis
+ by simp
+ (metis closure_open_segment convex_open_segment convex_rel_interior_closure
+ rel_interior_open_segment)
+qed
+
+lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment
+
+
definition "rel_frontier S = closure S - rel_interior S"
lemma closed_affine_hull:
@@ -8037,7 +8294,6 @@
then show ?thesis by auto
qed
-
lemma convex_closure_inter:
assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
@@ -8172,6 +8428,19 @@
using convex_closure_inter_two[of S T] assms affine_imp_convex by auto
qed
+lemma connected_component_1_gen:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "DIM('a) = 1"
+ shows "connected_component S a b \<longleftrightarrow> closed_segment a b \<subseteq> S"
+unfolding connected_component_def
+by (metis (no_types, lifting) assms subsetD subsetI convex_contains_segment convex_segment(1)
+ ends_in_segment connected_convex_1_gen)
+
+lemma connected_component_1:
+ fixes S :: "real set"
+ shows "connected_component S a b \<longleftrightarrow> closed_segment a b \<subseteq> S"
+by (simp add: connected_component_1_gen)
+
lemma convex_affine_rel_interior_inter:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
@@ -9448,6 +9717,126 @@
done
qed
+lemma interior_closed_segment_ge2:
+ fixes a :: "'a::euclidean_space"
+ assumes "2 \<le> DIM('a)"
+ shows "interior(closed_segment a b) = {}"
+using assms unfolding segment_convex_hull
+proof -
+ have "card {a, b} \<le> DIM('a)"
+ using assms
+ by (simp add: card_insert_if linear not_less_eq_eq numeral_2_eq_2)
+ then show "interior (convex hull {a, b}) = {}"
+ by (metis empty_interior_convex_hull finite.insertI finite.emptyI)
+qed
+
+lemma interior_open_segment:
+ fixes a :: "'a::euclidean_space"
+ shows "interior(open_segment a b) =
+ (if 2 \<le> DIM('a) then {} else open_segment a b)"
+proof (simp add: not_le, intro conjI impI)
+ assume "2 \<le> DIM('a)"
+ then show "interior (open_segment a b) = {}"
+ apply (simp add: segment_convex_hull open_segment_def)
+ apply (metis Diff_subset interior_mono segment_convex_hull subset_empty interior_closed_segment_ge2)
+ done
+next
+ assume le2: "DIM('a) < 2"
+ show "interior (open_segment a b) = open_segment a b"
+ proof (cases "a = b")
+ case True then show ?thesis by auto
+ next
+ case False
+ with le2 have "affine hull (open_segment a b) = UNIV"
+ apply simp
+ apply (rule affine_independent_span_gt)
+ apply (simp_all add: affine_dependent_def insert_Diff_if)
+ done
+ then show "interior (open_segment a b) = open_segment a b"
+ using rel_interior_interior rel_interior_open_segment by blast
+ qed
+qed
+
+lemma interior_closed_segment:
+ fixes a :: "'a::euclidean_space"
+ shows "interior(closed_segment a b) =
+ (if 2 \<le> DIM('a) then {} else open_segment a b)"
+proof (cases "a = b")
+ case True then show ?thesis by simp
+next
+ case False
+ then have "closure (open_segment a b) = closed_segment a b"
+ by simp
+ then show ?thesis
+ by (metis (no_types) convex_interior_closure convex_open_segment interior_open_segment)
+qed
+
+lemmas interior_segment = interior_closed_segment interior_open_segment
+
+lemma closed_segment_eq [simp]:
+ fixes a :: "'a::euclidean_space"
+ shows "closed_segment a b = closed_segment c d \<longleftrightarrow> {a,b} = {c,d}"
+proof
+ assume abcd: "closed_segment a b = closed_segment c d"
+ show "{a,b} = {c,d}"
+ proof (cases "a=b \<or> c=d")
+ case True with abcd show ?thesis by force
+ next
+ case False
+ then have neq: "a \<noteq> b \<and> c \<noteq> d" by force
+ have *: "closed_segment c d - {a, b} = rel_interior (closed_segment c d)"
+ using neq abcd by (metis (no_types) open_segment_def rel_interior_closed_segment)
+ have "b \<in> {c, d}"
+ proof -
+ have "insert b (closed_segment c d) = closed_segment c d"
+ using abcd by blast
+ then show ?thesis
+ by (metis DiffD2 Diff_insert2 False * insertI1 insert_Diff_if open_segment_def rel_interior_closed_segment)
+ qed
+ moreover have "a \<in> {c, d}"
+ by (metis Diff_iff False * abcd ends_in_segment(1) insertI1 open_segment_def rel_interior_closed_segment)
+ ultimately show "{a, b} = {c, d}"
+ using neq by fastforce
+ qed
+next
+ assume "{a,b} = {c,d}"
+ then show "closed_segment a b = closed_segment c d"
+ by (simp add: segment_convex_hull)
+qed
+
+lemma closed_open_segment_eq [simp]:
+ fixes a :: "'a::euclidean_space"
+ shows "closed_segment a b \<noteq> open_segment c d"
+by (metis DiffE closed_segment_neq_empty closure_closed_segment closure_open_segment ends_in_segment(1) insertI1 open_segment_def)
+
+lemma open_closed_segment_eq [simp]:
+ fixes a :: "'a::euclidean_space"
+ shows "open_segment a b \<noteq> closed_segment c d"
+using closed_open_segment_eq by blast
+
+lemma open_segment_eq [simp]:
+ fixes a :: "'a::euclidean_space"
+ shows "open_segment a b = open_segment c d \<longleftrightarrow> a = b \<and> c = d \<or> {a,b} = {c,d}"
+ (is "?lhs = ?rhs")
+proof
+ assume abcd: ?lhs
+ show ?rhs
+ proof (cases "a=b \<or> c=d")
+ case True with abcd show ?thesis
+ using finite_open_segment by fastforce
+ next
+ case False
+ then have a2: "a \<noteq> b \<and> c \<noteq> d" by force
+ with abcd show ?rhs
+ unfolding open_segment_def
+ by (metis (no_types) abcd closed_segment_eq closure_open_segment)
+ qed
+next
+ assume ?rhs
+ then show ?lhs
+ by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
+qed
+
subsection\<open>Similar results for closure and (relative or absolute) frontier.\<close>
lemma closure_convex_hull [simp]:
@@ -9646,6 +10035,21 @@
by blast
qed
+lemma collinear_closed_segment [simp]: "collinear (closed_segment a b)"
+by (metis affine_hull_convex_hull collinear_affine_hull hull_subset segment_convex_hull)
+
+lemma collinear_open_segment [simp]: "collinear (open_segment a b)"
+ unfolding open_segment_def
+ by (metis convex_hull_subset_affine_hull segment_convex_hull dual_order.trans
+ convex_hull_subset_affine_hull Diff_subset collinear_affine_hull)
+
+lemma subset_continuous_image_segment_1:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes "continuous_on (closed_segment a b) f"
+ shows "closed_segment (f a) (f b) \<subseteq> image f (closed_segment a b)"
+by (metis connected_segment convex_contains_segment ends_in_segment imageI
+ is_interval_connected_1 is_interval_convex connected_continuous_image [OF assms])
+
lemma collinear_imp_coplanar:
"collinear s ==> coplanar s"
by (metis collinear_affine_hull coplanar_def insert_absorb2)
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Mon Mar 14 15:58:02 2016 +0000
@@ -223,6 +223,20 @@
shows "compact {a .. b}"
by (metis compact_cbox interval_cbox)
+lemma homeomorphic_closed_intervals:
+ fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
+ assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
+ shows "(cbox a b) homeomorphic (cbox c d)"
+apply (rule homeomorphic_convex_compact)
+using assms apply auto
+done
+
+lemma homeomorphic_closed_intervals_real:
+ fixes a::real and b and c::real and d
+ assumes "a<b" and "c<d"
+ shows "{a..b} homeomorphic {c..d}"
+by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt)
+
no_notation
eucl_less (infix "<e" 50)
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Mar 14 15:58:02 2016 +0000
@@ -739,6 +739,22 @@
\<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
by (simp add: arc_simple_path simple_path_assoc)
+subsubsection\<open>Symmetry and loops\<close>
+
+lemma path_sym:
+ "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
+ by auto
+
+lemma simple_path_sym:
+ "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
+ \<Longrightarrow> simple_path(p +++ q) \<longleftrightarrow> simple_path(q +++ p)"
+by (metis (full_types) inf_commute insert_commute simple_path_joinE simple_path_join_loop)
+
+lemma path_image_sym:
+ "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
+ \<Longrightarrow> path_image(p +++ q) = path_image(q +++ p)"
+by (simp add: path_image_join sup_commute)
+
section\<open>Choosing a subpath of an existing path\<close>
@@ -1334,7 +1350,7 @@
done
-text \<open>Can also consider it as a set, as the name suggests.\<close>
+subsubsection \<open>Path components as sets\<close>
lemma path_component_set:
"path_component_set s x =
@@ -1372,7 +1388,7 @@
"\<lbrakk>x \<in> t; path_connected t; t \<subseteq> s\<rbrakk> \<Longrightarrow> t \<subseteq> (path_component_set s x)"
by (metis path_component_mono path_connected_component_set)
-subsection \<open>Some useful lemmas about path-connectedness\<close>
+subsection \<open>More about path-connectedness\<close>
lemma convex_imp_path_connected:
fixes s :: "'a::real_normed_vector set"
@@ -1387,6 +1403,12 @@
apply auto
done
+lemma path_connected_UNIV [iff]: "path_connected (UNIV :: 'a::real_normed_vector set)"
+ by (simp add: convex_imp_path_connected)
+
+lemma path_component_UNIV: "path_component_set UNIV x = (UNIV :: 'a::real_normed_vector set)"
+ using path_connected_component_set by auto
+
lemma path_connected_imp_connected:
assumes "path_connected s"
shows "connected s"
@@ -1679,6 +1701,72 @@
using path_component_eq_empty by auto
qed
+subsection\<open>Lemmas about path-connectedness\<close>
+
+lemma path_connected_linear_image:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+ assumes "path_connected s" "bounded_linear f"
+ shows "path_connected(f ` s)"
+by (auto simp: linear_continuous_on assms path_connected_continuous_image)
+
+lemma is_interval_path_connected: "is_interval s \<Longrightarrow> path_connected s"
+ by (simp add: convex_imp_path_connected is_interval_convex)
+
+lemma linear_homeomorphic_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+ assumes "linear f" "inj f"
+ shows "s homeomorphic f ` s"
+ using assms unfolding homeomorphic_def homeomorphism_def
+ apply (rule_tac x=f in exI)
+ apply (rule_tac x="inv f" in exI)
+ using inj_linear_imp_inv_linear linear_continuous_on
+ apply (auto simp: linear_conv_bounded_linear)
+ done
+
+lemma path_connected_Times:
+ assumes "path_connected s" "path_connected t"
+ shows "path_connected (s \<times> t)"
+proof (simp add: path_connected_def Sigma_def, clarify)
+ fix x1 y1 x2 y2
+ assume "x1 \<in> s" "y1 \<in> t" "x2 \<in> s" "y2 \<in> t"
+ obtain g where "path g" and g: "path_image g \<subseteq> s" and gs: "pathstart g = x1" and gf: "pathfinish g = x2"
+ using \<open>x1 \<in> s\<close> \<open>x2 \<in> s\<close> assms by (force simp: path_connected_def)
+ obtain h where "path h" and h: "path_image h \<subseteq> t" and hs: "pathstart h = y1" and hf: "pathfinish h = y2"
+ using \<open>y1 \<in> t\<close> \<open>y2 \<in> t\<close> assms by (force simp: path_connected_def)
+ have "path (\<lambda>z. (x1, h z))"
+ using \<open>path h\<close>
+ apply (simp add: path_def)
+ apply (rule continuous_on_compose2 [where f = h])
+ apply (rule continuous_intros | force)+
+ done
+ moreover have "path (\<lambda>z. (g z, y2))"
+ using \<open>path g\<close>
+ apply (simp add: path_def)
+ apply (rule continuous_on_compose2 [where f = g])
+ apply (rule continuous_intros | force)+
+ done
+ ultimately have 1: "path ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2)))"
+ by (metis hf gs path_join_imp pathstart_def pathfinish_def)
+ have "path_image ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2))) \<subseteq> path_image (\<lambda>z. (x1, h z)) \<union> path_image (\<lambda>z. (g z, y2))"
+ by (rule Path_Connected.path_image_join_subset)
+ also have "... \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})"
+ using g h \<open>x1 \<in> s\<close> \<open>y2 \<in> t\<close> by (force simp: path_image_def)
+ finally have 2: "path_image ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2))) \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})" .
+ show "\<exists>g. path g \<and> path_image g \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)}) \<and>
+ pathstart g = (x1, y1) \<and> pathfinish g = (x2, y2)"
+ apply (intro exI conjI)
+ apply (rule 1)
+ apply (rule 2)
+ apply (metis hs pathstart_def pathstart_join)
+ by (metis gf pathfinish_def pathfinish_join)
+qed
+
+lemma is_interval_path_connected_1:
+ fixes s :: "real set"
+ shows "is_interval s \<longleftrightarrow> path_connected s"
+using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
+
+
subsection \<open>Sphere is path-connected\<close>
lemma path_connected_punctured_universe:
@@ -2285,6 +2373,45 @@
then show ?thesis by (auto simp: frontier_def)
qed
+lemma frontier_Union_subset_closure:
+ fixes F :: "'a::real_normed_vector set set"
+ shows "frontier(\<Union>F) \<subseteq> closure(\<Union>t \<in> F. frontier t)"
+proof -
+ have "\<exists>y\<in>F. \<exists>y\<in>frontier y. dist y x < e"
+ if "T \<in> F" "y \<in> T" "dist y x < e"
+ "x \<notin> interior (\<Union>F)" "0 < e" for x y e T
+ proof (cases "x \<in> T")
+ case True with that show ?thesis
+ by (metis Diff_iff Sup_upper closure_subset contra_subsetD dist_self frontier_def interior_mono)
+ next
+ case False
+ have 1: "closed_segment x y \<inter> T \<noteq> {}" using \<open>y \<in> T\<close> by blast
+ have 2: "closed_segment x y - T \<noteq> {}"
+ using False by blast
+ obtain c where "c \<in> closed_segment x y" "c \<in> frontier T"
+ using False connected_Int_frontier [OF connected_segment 1 2] by auto
+ then show ?thesis
+ proof -
+ have "norm (y - x) < e"
+ by (metis dist_norm \<open>dist y x < e\<close>)
+ moreover have "norm (c - x) \<le> norm (y - x)"
+ by (simp add: \<open>c \<in> closed_segment x y\<close> segment_bound(1))
+ ultimately have "norm (c - x) < e"
+ by linarith
+ then show ?thesis
+ by (metis (no_types) \<open>c \<in> frontier T\<close> dist_norm that(1))
+ qed
+ qed
+ then show ?thesis
+ by (fastforce simp add: frontier_def closure_approachable)
+qed
+
+lemma frontier_Union_subset:
+ fixes F :: "'a::real_normed_vector set set"
+ shows "finite F \<Longrightarrow> frontier(\<Union>F) \<subseteq> (\<Union>t \<in> F. frontier t)"
+by (rule order_trans [OF frontier_Union_subset_closure])
+ (auto simp: closure_subset_eq)
+
lemma connected_component_UNIV:
fixes x :: "'a::real_normed_vector"
shows "connected_component_set UNIV x = UNIV"
@@ -3710,4 +3837,220 @@
apply (rule le_cases3 [of u v w])
using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
+text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
+
+lemma path_component_imp_homotopic_points:
+ "path_component S a b \<Longrightarrow> homotopic_loops S (linepath a a) (linepath b b)"
+apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
+ pathstart_def pathfinish_def path_image_def path_def, clarify)
+apply (rule_tac x="g o fst" in exI)
+apply (intro conjI continuous_intros continuous_on_compose)+
+apply (auto elim!: continuous_on_subset)
+done
+
+lemma homotopic_loops_imp_path_component_value:
+ "\<lbrakk>homotopic_loops S p q; 0 \<le> t; t \<le> 1\<rbrakk>
+ \<Longrightarrow> path_component S (p t) (q t)"
+apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
+ pathstart_def pathfinish_def path_image_def path_def, clarify)
+apply (rule_tac x="h o (\<lambda>u. (u, t))" in exI)
+apply (intro conjI continuous_intros continuous_on_compose)+
+apply (auto elim!: continuous_on_subset)
+done
+
+lemma homotopic_points_eq_path_component:
+ "homotopic_loops S (linepath a a) (linepath b b) \<longleftrightarrow>
+ path_component S a b"
+by (auto simp: path_component_imp_homotopic_points
+ dest: homotopic_loops_imp_path_component_value [where t=1])
+
+lemma path_connected_eq_homotopic_points:
+ "path_connected S \<longleftrightarrow>
+ (\<forall>a b. a \<in> S \<and> b \<in> S \<longrightarrow> homotopic_loops S (linepath a a) (linepath b b))"
+by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
+
+
+subsection\<open>Simply connected sets\<close>
+
+text\<open>defined as "all loops are homotopic (as loops)\<close>
+
+definition simply_connected where
+ "simply_connected S \<equiv>
+ \<forall>p q. path p \<and> pathfinish p = pathstart p \<and> path_image p \<subseteq> S \<and>
+ path q \<and> pathfinish q = pathstart q \<and> path_image q \<subseteq> S
+ \<longrightarrow> homotopic_loops S p q"
+
+lemma simply_connected_empty [iff]: "simply_connected {}"
+ by (simp add: simply_connected_def)
+
+lemma simply_connected_imp_path_connected:
+ fixes S :: "_::real_normed_vector set"
+ shows "simply_connected S \<Longrightarrow> path_connected S"
+by (simp add: simply_connected_def path_connected_eq_homotopic_points)
+
+lemma simply_connected_imp_connected:
+ fixes S :: "_::real_normed_vector set"
+ shows "simply_connected S \<Longrightarrow> connected S"
+by (simp add: path_connected_imp_connected simply_connected_imp_path_connected)
+
+lemma simply_connected_eq_contractible_loop_any:
+ fixes S :: "_::real_normed_vector set"
+ shows "simply_connected S \<longleftrightarrow>
+ (\<forall>p a. path p \<and> path_image p \<subseteq> S \<and>
+ pathfinish p = pathstart p \<and> a \<in> S
+ \<longrightarrow> homotopic_loops S p (linepath a a))"
+apply (simp add: simply_connected_def)
+apply (rule iffI, force, clarify)
+apply (rule_tac q = "linepath (pathstart p) (pathstart p)" in homotopic_loops_trans)
+apply (fastforce simp add:)
+using homotopic_loops_sym apply blast
+done
+
+lemma simply_connected_eq_contractible_loop_some:
+ fixes S :: "_::real_normed_vector set"
+ shows "simply_connected S \<longleftrightarrow>
+ path_connected S \<and>
+ (\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
+ \<longrightarrow> (\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)))"
+apply (rule iffI)
+ apply (fastforce simp: simply_connected_imp_path_connected simply_connected_eq_contractible_loop_any)
+apply (clarsimp simp add: simply_connected_eq_contractible_loop_any)
+apply (drule_tac x=p in spec)
+using homotopic_loops_trans path_connected_eq_homotopic_points
+ apply blast
+done
+
+lemma simply_connected_eq_contractible_loop_all:
+ fixes S :: "_::real_normed_vector set"
+ shows "simply_connected S \<longleftrightarrow>
+ S = {} \<or>
+ (\<exists>a \<in> S. \<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
+ \<longrightarrow> homotopic_loops S p (linepath a a))"
+ (is "?lhs = ?rhs")
+proof (cases "S = {}")
+ case True then show ?thesis by force
+next
+ case False
+ then obtain a where "a \<in> S" by blast
+ show ?thesis
+ proof
+ assume "simply_connected S"
+ then show ?rhs
+ using \<open>a \<in> S\<close> \<open>simply_connected S\<close> simply_connected_eq_contractible_loop_any
+ by blast
+ next
+ assume ?rhs
+ then show "simply_connected S"
+ apply (simp add: simply_connected_eq_contractible_loop_any False)
+ by (meson homotopic_loops_refl homotopic_loops_sym homotopic_loops_trans
+ path_component_imp_homotopic_points path_component_refl)
+ qed
+qed
+
+lemma simply_connected_eq_contractible_path:
+ fixes S :: "_::real_normed_vector set"
+ shows "simply_connected S \<longleftrightarrow>
+ path_connected S \<and>
+ (\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
+ \<longrightarrow> homotopic_paths S p (linepath (pathstart p) (pathstart p)))"
+apply (rule iffI)
+ apply (simp add: simply_connected_imp_path_connected)
+ apply (metis simply_connected_eq_contractible_loop_some homotopic_loops_imp_homotopic_paths_null)
+by (meson homotopic_paths_imp_homotopic_loops pathfinish_linepath pathstart_in_path_image
+ simply_connected_eq_contractible_loop_some subset_iff)
+
+lemma simply_connected_eq_homotopic_paths:
+ fixes S :: "_::real_normed_vector set"
+ shows "simply_connected S \<longleftrightarrow>
+ path_connected S \<and>
+ (\<forall>p q. path p \<and> path_image p \<subseteq> S \<and>
+ path q \<and> path_image q \<subseteq> S \<and>
+ pathstart q = pathstart p \<and> pathfinish q = pathfinish p
+ \<longrightarrow> homotopic_paths S p q)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have pc: "path_connected S"
+ and *: "\<And>p. \<lbrakk>path p; path_image p \<subseteq> S;
+ pathfinish p = pathstart p\<rbrakk>
+ \<Longrightarrow> homotopic_paths S p (linepath (pathstart p) (pathstart p))"
+ by (auto simp: simply_connected_eq_contractible_path)
+ have "homotopic_paths S p q"
+ if "path p" "path_image p \<subseteq> S" "path q"
+ "path_image q \<subseteq> S" "pathstart q = pathstart p"
+ "pathfinish q = pathfinish p" for p q
+ proof -
+ have "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))"
+ by (simp add: homotopic_paths_rid homotopic_paths_sym that)
+ also have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p))
+ (p +++ reversepath q +++ q)"
+ using that
+ by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl homotopic_paths_sym_eq pathstart_linepath)
+ also have "homotopic_paths S (p +++ reversepath q +++ q)
+ ((p +++ reversepath q) +++ q)"
+ by (simp add: that homotopic_paths_assoc)
+ also have "homotopic_paths S ((p +++ reversepath q) +++ q)
+ (linepath (pathstart q) (pathstart q) +++ q)"
+ using * [of "p +++ reversepath q"] that
+ by (simp add: homotopic_paths_join path_image_join)
+ also have "homotopic_paths S (linepath (pathstart q) (pathstart q) +++ q) q"
+ using that homotopic_paths_lid by blast
+ finally show ?thesis .
+ qed
+ then show ?rhs
+ by (blast intro: pc *)
+next
+ assume ?rhs
+ then show ?lhs
+ by (force simp: simply_connected_eq_contractible_path)
+qed
+
+proposition simply_connected_Times:
+ fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
+ assumes S: "simply_connected S" and T: "simply_connected T"
+ shows "simply_connected(S \<times> T)"
+proof -
+ have "homotopic_loops (S \<times> T) p (linepath (a, b) (a, b))"
+ if "path p" "path_image p \<subseteq> S \<times> T" "p 1 = p 0" "a \<in> S" "b \<in> T"
+ for p a b
+ proof -
+ have "path (fst \<circ> p)"
+ apply (rule Path_Connected.path_continuous_image [OF \<open>path p\<close>])
+ apply (rule continuous_intros)+
+ done
+ moreover have "path_image (fst \<circ> p) \<subseteq> S"
+ using that apply (simp add: path_image_def) by force
+ ultimately have p1: "homotopic_loops S (fst o p) (linepath a a)"
+ using S that
+ apply (simp add: simply_connected_eq_contractible_loop_any)
+ apply (drule_tac x="fst o p" in spec)
+ apply (drule_tac x=a in spec)
+ apply (auto simp: pathstart_def pathfinish_def)
+ done
+ have "path (snd \<circ> p)"
+ apply (rule Path_Connected.path_continuous_image [OF \<open>path p\<close>])
+ apply (rule continuous_intros)+
+ done
+ moreover have "path_image (snd \<circ> p) \<subseteq> T"
+ using that apply (simp add: path_image_def) by force
+ ultimately have p2: "homotopic_loops T (snd o p) (linepath b b)"
+ using T that
+ apply (simp add: simply_connected_eq_contractible_loop_any)
+ apply (drule_tac x="snd o p" in spec)
+ apply (drule_tac x=b in spec)
+ apply (auto simp: pathstart_def pathfinish_def)
+ done
+ show ?thesis
+ using p1 p2
+ apply (simp add: homotopic_loops, clarify)
+ apply (rename_tac h k)
+ apply (rule_tac x="\<lambda>z. Pair (h z) (k z)" in exI)
+ apply (intro conjI continuous_intros | assumption)+
+ apply (auto simp: pathstart_def pathfinish_def)
+ done
+ qed
+ with assms show ?thesis
+ by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
+qed
+
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 14 15:58:02 2016 +0000
@@ -7792,10 +7792,10 @@
unfolding homeomorphism_def
by blast
-lemma homeomorphic_trans:
+lemma homeomorphic_trans [trans]:
assumes "s homeomorphic t"
- and "t homeomorphic u"
- shows "s homeomorphic u"
+ and "t homeomorphic u"
+ shows "s homeomorphic u"
proof -
obtain f1 g1 where fg1: "\<forall>x\<in>s. g1 (f1 x) = x" "f1 ` s = t"
"continuous_on s f1" "\<forall>y\<in>t. f1 (g1 y) = y" "g1 ` t = s" "continuous_on t g1"