equal
deleted
inserted
replaced
6657 "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S" |
6657 "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S" |
6658 using aff_dim_sing connected_imp_perfect by blast |
6658 using aff_dim_sing connected_imp_perfect by blast |
6659 |
6659 |
6660 subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close> |
6660 subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close> |
6661 |
6661 |
6662 lemma is_interval_1: |
6662 lemma mem_is_interval_1_I: |
6663 "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)" |
6663 fixes a b c::real |
6664 unfolding is_interval_def by auto |
6664 assumes "is_interval S" |
|
6665 assumes "a \<in> S" "c \<in> S" |
|
6666 assumes "a \<le> b" "b \<le> c" |
|
6667 shows "b \<in> S" |
|
6668 using assms is_interval_1 by blast |
6665 |
6669 |
6666 lemma is_interval_connected_1: |
6670 lemma is_interval_connected_1: |
6667 fixes s :: "real set" |
6671 fixes s :: "real set" |
6668 shows "is_interval s \<longleftrightarrow> connected s" |
6672 shows "is_interval s \<longleftrightarrow> connected s" |
6669 apply rule |
6673 apply rule |
6706 lemma is_interval_convex_1: |
6710 lemma is_interval_convex_1: |
6707 fixes s :: "real set" |
6711 fixes s :: "real set" |
6708 shows "is_interval s \<longleftrightarrow> convex s" |
6712 shows "is_interval s \<longleftrightarrow> convex s" |
6709 by (metis is_interval_convex convex_connected is_interval_connected_1) |
6713 by (metis is_interval_convex convex_connected is_interval_connected_1) |
6710 |
6714 |
|
6715 lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real |
|
6716 by (metis connected_ball is_interval_connected_1) |
|
6717 |
6711 lemma connected_compact_interval_1: |
6718 lemma connected_compact_interval_1: |
6712 "connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})" |
6719 "connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})" |
6713 by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact) |
6720 by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact) |
6714 |
6721 |
6715 lemma connected_convex_1: |
6722 lemma connected_convex_1: |
6728 then have "f -` (f ` s) = s" |
6735 then have "f -` (f ` s) = s" |
6729 by (simp add: inj_vimage_image_eq) |
6736 by (simp add: inj_vimage_image_eq) |
6730 then show ?thesis |
6737 then show ?thesis |
6731 by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image) |
6738 by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image) |
6732 qed |
6739 qed |
|
6740 |
|
6741 lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real |
|
6742 by (auto simp: is_interval_convex_1 convex_cball) |
|
6743 |
6733 |
6744 |
6734 subsection \<open>Another intermediate value theorem formulation\<close> |
6745 subsection \<open>Another intermediate value theorem formulation\<close> |
6735 |
6746 |
6736 lemma ivt_increasing_component_on_1: |
6747 lemma ivt_increasing_component_on_1: |
6737 fixes f :: "real \<Rightarrow> 'a::euclidean_space" |
6748 fixes f :: "real \<Rightarrow> 'a::euclidean_space" |