--- a/src/HOL/Analysis/Connected.thy Sat Aug 29 16:30:33 2020 +0100
+++ b/src/HOL/Analysis/Connected.thy Sun Aug 30 19:45:46 2020 +0100
@@ -68,94 +68,94 @@
subsection \<open>Connected components, considered as a connectedness relation or a set\<close>
-definition\<^marker>\<open>tag important\<close> "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
+definition\<^marker>\<open>tag important\<close> "connected_component S x y \<equiv> \<exists>T. connected T \<and> T \<subseteq> S \<and> x \<in> T \<and> y \<in> T"
-abbreviation "connected_component_set s x \<equiv> Collect (connected_component s x)"
+abbreviation "connected_component_set S x \<equiv> Collect (connected_component S x)"
lemma connected_componentI:
- "connected t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> t \<Longrightarrow> y \<in> t \<Longrightarrow> connected_component s x y"
+ "connected T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> x \<in> T \<Longrightarrow> y \<in> T \<Longrightarrow> connected_component S x y"
by (auto simp: connected_component_def)
-lemma connected_component_in: "connected_component s x y \<Longrightarrow> x \<in> s \<and> y \<in> s"
+lemma connected_component_in: "connected_component S x y \<Longrightarrow> x \<in> S \<and> y \<in> S"
by (auto simp: connected_component_def)
-lemma connected_component_refl: "x \<in> s \<Longrightarrow> connected_component s x x"
+lemma connected_component_refl: "x \<in> S \<Longrightarrow> connected_component S x x"
by (auto simp: connected_component_def) (use connected_sing in blast)
-lemma connected_component_refl_eq [simp]: "connected_component s x x \<longleftrightarrow> x \<in> s"
+lemma connected_component_refl_eq [simp]: "connected_component S x x \<longleftrightarrow> x \<in> S"
by (auto simp: connected_component_refl) (auto simp: connected_component_def)
-lemma connected_component_sym: "connected_component s x y \<Longrightarrow> connected_component s y x"
+lemma connected_component_sym: "connected_component S x y \<Longrightarrow> connected_component S y x"
by (auto simp: connected_component_def)
lemma connected_component_trans:
- "connected_component s x y \<Longrightarrow> connected_component s y z \<Longrightarrow> connected_component s x z"
+ "connected_component S x y \<Longrightarrow> connected_component S y z \<Longrightarrow> connected_component S x z"
unfolding connected_component_def
by (metis Int_iff Un_iff Un_subset_iff equals0D connected_Un)
lemma connected_component_of_subset:
- "connected_component s x y \<Longrightarrow> s \<subseteq> t \<Longrightarrow> connected_component t x y"
+ "connected_component S x y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> connected_component T x y"
by (auto simp: connected_component_def)
-lemma connected_component_Union: "connected_component_set s x = \<Union>{t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
+lemma connected_component_Union: "connected_component_set S x = \<Union>{T. connected T \<and> x \<in> T \<and> T \<subseteq> S}"
by (auto simp: connected_component_def)
-lemma connected_connected_component [iff]: "connected (connected_component_set s x)"
+lemma connected_connected_component [iff]: "connected (connected_component_set S x)"
by (auto simp: connected_component_Union intro: connected_Union)
lemma connected_iff_eq_connected_component_set:
- "connected s \<longleftrightarrow> (\<forall>x \<in> s. connected_component_set s x = s)"
-proof (cases "s = {}")
+ "connected S \<longleftrightarrow> (\<forall>x \<in> S. connected_component_set S x = S)"
+proof (cases "S = {}")
case True
then show ?thesis by simp
next
case False
- then obtain x where "x \<in> s" by auto
+ then obtain x where "x \<in> S" by auto
show ?thesis
proof
- assume "connected s"
- then show "\<forall>x \<in> s. connected_component_set s x = s"
+ assume "connected S"
+ then show "\<forall>x \<in> S. connected_component_set S x = S"
by (force simp: connected_component_def)
next
- assume "\<forall>x \<in> s. connected_component_set s x = s"
- then show "connected s"
- by (metis \<open>x \<in> s\<close> connected_connected_component)
+ assume "\<forall>x \<in> S. connected_component_set S x = S"
+ then show "connected S"
+ by (metis \<open>x \<in> S\<close> connected_connected_component)
qed
qed
-lemma connected_component_subset: "connected_component_set s x \<subseteq> s"
+lemma connected_component_subset: "connected_component_set S x \<subseteq> S"
using connected_component_in by blast
-lemma connected_component_eq_self: "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> connected_component_set s x = s"
+lemma connected_component_eq_self: "connected S \<Longrightarrow> x \<in> S \<Longrightarrow> connected_component_set S x = S"
by (simp add: connected_iff_eq_connected_component_set)
lemma connected_iff_connected_component:
- "connected s \<longleftrightarrow> (\<forall>x \<in> s. \<forall>y \<in> s. connected_component s x y)"
+ "connected S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. connected_component S x y)"
using connected_component_in by (auto simp: connected_iff_eq_connected_component_set)
lemma connected_component_maximal:
- "x \<in> t \<Longrightarrow> connected t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> t \<subseteq> (connected_component_set s x)"
+ "x \<in> T \<Longrightarrow> connected T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> T \<subseteq> (connected_component_set S x)"
using connected_component_eq_self connected_component_of_subset by blast
lemma connected_component_mono:
- "s \<subseteq> t \<Longrightarrow> connected_component_set s x \<subseteq> connected_component_set t x"
+ "S \<subseteq> T \<Longrightarrow> connected_component_set S x \<subseteq> connected_component_set T x"
by (simp add: Collect_mono connected_component_of_subset)
-lemma connected_component_eq_empty [simp]: "connected_component_set s x = {} \<longleftrightarrow> x \<notin> s"
+lemma connected_component_eq_empty [simp]: "connected_component_set S x = {} \<longleftrightarrow> x \<notin> S"
using connected_component_refl by (fastforce simp: connected_component_in)
lemma connected_component_set_empty [simp]: "connected_component_set {} x = {}"
using connected_component_eq_empty by blast
lemma connected_component_eq:
- "y \<in> connected_component_set s x \<Longrightarrow> (connected_component_set s y = connected_component_set s x)"
+ "y \<in> connected_component_set S x \<Longrightarrow> (connected_component_set S y = connected_component_set S x)"
by (metis (no_types, lifting)
Collect_cong connected_component_sym connected_component_trans mem_Collect_eq)
lemma closed_connected_component:
- assumes s: "closed s"
- shows "closed (connected_component_set s x)"
-proof (cases "x \<in> s")
+ assumes S: "closed S"
+ shows "closed (connected_component_set S x)"
+proof (cases "x \<in> S")
case False
then show ?thesis
by (metis connected_component_eq_empty closed_empty)
@@ -164,29 +164,29 @@
show ?thesis
unfolding closure_eq [symmetric]
proof
- show "closure (connected_component_set s x) \<subseteq> connected_component_set s x"
+ show "closure (connected_component_set S x) \<subseteq> connected_component_set S x"
apply (rule connected_component_maximal)
apply (simp add: closure_def True)
apply (simp add: connected_imp_connected_closure)
- apply (simp add: s closure_minimal connected_component_subset)
+ apply (simp add: S closure_minimal connected_component_subset)
done
next
- show "connected_component_set s x \<subseteq> closure (connected_component_set s x)"
+ show "connected_component_set S x \<subseteq> closure (connected_component_set S x)"
by (simp add: closure_subset)
qed
qed
lemma connected_component_disjoint:
- "connected_component_set s a \<inter> connected_component_set s b = {} \<longleftrightarrow>
- a \<notin> connected_component_set s b"
+ "connected_component_set S a \<inter> connected_component_set S b = {} \<longleftrightarrow>
+ a \<notin> connected_component_set S b"
apply (auto simp: connected_component_eq)
using connected_component_eq connected_component_sym
apply blast
done
lemma connected_component_nonoverlap:
- "connected_component_set s a \<inter> connected_component_set s b = {} \<longleftrightarrow>
- a \<notin> s \<or> b \<notin> s \<or> connected_component_set s a \<noteq> connected_component_set s b"
+ "connected_component_set S a \<inter> connected_component_set S b = {} \<longleftrightarrow>
+ a \<notin> S \<or> b \<notin> S \<or> connected_component_set S a \<noteq> connected_component_set S b"
apply (auto simp: connected_component_in)
using connected_component_refl_eq
apply blast
@@ -195,30 +195,30 @@
done
lemma connected_component_overlap:
- "connected_component_set s a \<inter> connected_component_set s b \<noteq> {} \<longleftrightarrow>
- a \<in> s \<and> b \<in> s \<and> connected_component_set s a = connected_component_set s b"
+ "connected_component_set S a \<inter> connected_component_set S b \<noteq> {} \<longleftrightarrow>
+ a \<in> S \<and> b \<in> S \<and> connected_component_set S a = connected_component_set S b"
by (auto simp: connected_component_nonoverlap)
-lemma connected_component_sym_eq: "connected_component s x y \<longleftrightarrow> connected_component s y x"
+lemma connected_component_sym_eq: "connected_component S x y \<longleftrightarrow> connected_component S y x"
using connected_component_sym by blast
lemma connected_component_eq_eq:
- "connected_component_set s x = connected_component_set s y \<longleftrightarrow>
- x \<notin> s \<and> y \<notin> s \<or> x \<in> s \<and> y \<in> s \<and> connected_component s x y"
- apply (cases "y \<in> s", simp)
+ "connected_component_set S x = connected_component_set S y \<longleftrightarrow>
+ x \<notin> S \<and> y \<notin> S \<or> x \<in> S \<and> y \<in> S \<and> connected_component S x y"
+ apply (cases "y \<in> S", simp)
apply (metis connected_component_eq connected_component_eq_empty connected_component_refl_eq mem_Collect_eq)
- apply (cases "x \<in> s", simp)
+ apply (cases "x \<in> S", simp)
apply (metis connected_component_eq_empty)
using connected_component_eq_empty
apply blast
done
lemma connected_iff_connected_component_eq:
- "connected s \<longleftrightarrow> (\<forall>x \<in> s. \<forall>y \<in> s. connected_component_set s x = connected_component_set s y)"
+ "connected S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. connected_component_set S x = connected_component_set S y)"
by (simp add: connected_component_eq_eq connected_iff_connected_component)
lemma connected_component_idemp:
- "connected_component_set (connected_component_set s x) x = connected_component_set s x"
+ "connected_component_set (connected_component_set S x) x = connected_component_set S x"
apply (rule subset_antisym)
apply (simp add: connected_component_subset)
apply (metis connected_component_eq_empty connected_component_maximal
@@ -226,25 +226,24 @@
done
lemma connected_component_unique:
- "\<lbrakk>x \<in> c; c \<subseteq> s; connected c;
- \<And>c'. x \<in> c' \<and> c' \<subseteq> s \<and> connected c'
- \<Longrightarrow> c' \<subseteq> c\<rbrakk>
- \<Longrightarrow> connected_component_set s x = c"
-apply (rule subset_antisym)
-apply (meson connected_component_maximal connected_component_subset connected_connected_component contra_subsetD)
-by (simp add: connected_component_maximal)
+ "\<lbrakk>x \<in> c; c \<subseteq> S; connected c;
+ \<And>c'. \<lbrakk>x \<in> c'; c' \<subseteq> S; connected c'\<rbrakk> \<Longrightarrow> c' \<subseteq> c\<rbrakk>
+ \<Longrightarrow> connected_component_set S x = c"
+ apply (rule subset_antisym)
+ apply (meson connected_component_maximal connected_component_subset connected_connected_component contra_subsetD)
+ by (simp add: connected_component_maximal)
lemma joinable_connected_component_eq:
- "\<lbrakk>connected t; t \<subseteq> s;
- connected_component_set s x \<inter> t \<noteq> {};
- connected_component_set s y \<inter> t \<noteq> {}\<rbrakk>
- \<Longrightarrow> connected_component_set s x = connected_component_set s y"
+ "\<lbrakk>connected T; T \<subseteq> S;
+ connected_component_set S x \<inter> T \<noteq> {};
+ connected_component_set S y \<inter> T \<noteq> {}\<rbrakk>
+ \<Longrightarrow> connected_component_set S x = connected_component_set S y"
apply (simp add: ex_in_conv [symmetric])
apply (rule connected_component_eq)
by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
-lemma Union_connected_component: "\<Union>(connected_component_set s ` s) = s"
+lemma Union_connected_component: "\<Union>(connected_component_set S ` S) = S"
apply (rule subset_antisym)
apply (simp add: SUP_least connected_component_subset)
using connected_component_refl_eq
@@ -252,16 +251,16 @@
lemma complement_connected_component_unions:
- "s - connected_component_set s x =
- \<Union>(connected_component_set s ` s - {connected_component_set s x})"
+ "S - connected_component_set S x =
+ \<Union>(connected_component_set S ` S - {connected_component_set S x})"
apply (subst Union_connected_component [symmetric], auto)
apply (metis connected_component_eq_eq connected_component_in)
by (metis connected_component_eq mem_Collect_eq)
lemma connected_component_intermediate_subset:
- "\<lbrakk>connected_component_set u a \<subseteq> t; t \<subseteq> u\<rbrakk>
- \<Longrightarrow> connected_component_set t a = connected_component_set u a"
- apply (case_tac "a \<in> u")
+ "\<lbrakk>connected_component_set U a \<subseteq> T; T \<subseteq> U\<rbrakk>
+ \<Longrightarrow> connected_component_set T a = connected_component_set U a"
+ apply (case_tac "a \<in> U")
apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
using connected_component_eq_empty by blast
@@ -269,17 +268,17 @@
subsection \<open>The set of connected components of a set\<close>
definition\<^marker>\<open>tag important\<close> components:: "'a::topological_space set \<Rightarrow> 'a set set"
- where "components s \<equiv> connected_component_set s ` s"
+ where "components S \<equiv> connected_component_set S ` S"
-lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
+lemma components_iff: "S \<in> components U \<longleftrightarrow> (\<exists>x. x \<in> U \<and> S = connected_component_set U x)"
by (auto simp: components_def)
-lemma componentsI: "x \<in> u \<Longrightarrow> connected_component_set u x \<in> components u"
+lemma componentsI: "x \<in> U \<Longrightarrow> connected_component_set U x \<in> components U"
by (auto simp: components_def)
lemma componentsE:
- assumes "s \<in> components u"
- obtains x where "x \<in> u" "s = connected_component_set u x"
+ assumes "S \<in> components U"
+ obtains x where "x \<in> U" "S = connected_component_set U x"
using assms by (auto simp: components_def)
lemma Union_components [simp]: "\<Union>(components u) = u"
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Sat Aug 29 16:30:33 2020 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Sun Aug 30 19:45:46 2020 +0100
@@ -61,7 +61,7 @@
by (simp add: subset_eq)
lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"
- by (auto)
+ by auto
lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
by force
@@ -70,34 +70,34 @@
by auto
lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
- by (simp add: subset_eq)
+ by auto
lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e"
- by (simp add: subset_eq)
+ by auto
lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"
- by (auto)
+ by auto
lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
- by (auto)
+ by auto
lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
by metric
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
- by (simp add: set_eq_iff) arith
+ by auto
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
- by (simp add: set_eq_iff)
+ by auto
lemma cball_max_Un: "cball a (max r s) = cball a r \<union> cball a s"
- by (simp add: set_eq_iff) arith
+ by auto
lemma cball_min_Int: "cball a (min r s) = cball a r \<inter> cball a s"
- by (simp add: set_eq_iff)
+ by auto
lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r"
- by (auto simp: cball_def ball_def dist_commute)
+ by auto
lemma open_ball [intro, simp]: "open (ball x e)"
proof -
@@ -126,7 +126,8 @@
unfolding mem_ball set_eq_iff
by (simp add: not_less) metric
-lemma ball_empty: "e \<le> 0 \<Longrightarrow> ball x e = {}" by simp
+lemma ball_empty: "e \<le> 0 \<Longrightarrow> ball x e = {}"
+ by simp
lemma closed_cball [iff]: "closed (cball x e)"
proof -
@@ -142,16 +143,15 @@
{
fix x and e::real
assume "x\<in>S" "e>0" "ball x e \<subseteq> S"
- then have "\<exists>d>0. cball x d \<subseteq> S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto)
+ then have "\<exists>d>0. cball x d \<subseteq> S"
+ unfolding subset_eq by (rule_tac x="e/2" in exI, auto)
}
moreover
{
fix x and e::real
assume "x\<in>S" "e>0" "cball x e \<subseteq> S"
then have "\<exists>d>0. ball x d \<subseteq> S"
- unfolding subset_eq
- apply (rule_tac x="e/2" in exI, auto)
- done
+ using mem_ball_imp_mem_cball by blast
}
ultimately show ?thesis
unfolding open_contains_ball by auto
@@ -206,24 +206,17 @@
lemma cball_sing:
fixes x :: "'a::metric_space"
shows "e = 0 \<Longrightarrow> cball x e = {x}"
- by (auto simp: set_eq_iff)
+ by simp
lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"
- apply (cases "e \<le> 0")
- apply (simp add: ball_empty field_split_simps)
- apply (rule subset_ball)
- apply (simp add: field_split_simps)
- done
+ by (metis ball_eq_empty div_by_1 frac_le linear subset_ball zero_less_one)
lemma ball_divide_subset_numeral: "ball x (e / numeral w) \<subseteq> ball x e"
using ball_divide_subset one_le_numeral by blast
lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"
- apply (cases "e < 0")
- apply (simp add: field_split_simps)
- apply (rule subset_cball)
- apply (metis div_by_1 frac_le not_le order_refl zero_less_one)
- done
+ apply (cases "e < 0", simp add: field_split_simps)
+ by (metis div_by_1 frac_le less_numeral_extra(1) not_le order_refl subset_cball)
lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
using cball_divide_subset one_le_numeral by blast
@@ -2141,7 +2134,7 @@
then have D: "T \<subseteq> V" unfolding V_def by auto
have "(ball x ((infdist x T)/2)) \<inter> (ball y ((infdist y S)/2)) = {}" if "x \<in> S" "y \<in> T" for x y
- proof (auto)
+ proof auto
fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"
have "2 * dist x y \<le> 2 * dist x z + 2 * dist y z"
by metric
@@ -2728,8 +2721,8 @@
subsection \<open>With Abstract Topology (TODO: move and remove dependency?)\<close>
lemma openin_contains_ball:
- "openin (top_of_set t) s \<longleftrightarrow>
- s \<subseteq> t \<and> (\<forall>x \<in> s. \<exists>e. 0 < e \<and> ball x e \<inter> t \<subseteq> s)"
+ "openin (top_of_set T) S \<longleftrightarrow>
+ S \<subseteq> T \<and> (\<forall>x \<in> S. \<exists>e. 0 < e \<and> ball x e \<inter> T \<subseteq> S)"
(is "?lhs = ?rhs")
proof
assume ?lhs
@@ -2745,14 +2738,18 @@
qed
lemma openin_contains_cball:
- "openin (top_of_set t) s \<longleftrightarrow>
- s \<subseteq> t \<and>
- (\<forall>x \<in> s. \<exists>e. 0 < e \<and> cball x e \<inter> t \<subseteq> s)"
- apply (simp add: openin_contains_ball)
- apply (rule iffI)
- apply (auto dest!: bspec)
- apply (rule_tac x="e/2" in exI, force+)
- done
+ "openin (top_of_set T) S \<longleftrightarrow>
+ S \<subseteq> T \<and> (\<forall>x \<in> S. \<exists>e. 0 < e \<and> cball x e \<inter> T \<subseteq> S)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ by (force simp add: openin_contains_ball intro: exI [where x="_/2"])
+next
+ assume ?rhs
+ then show ?lhs
+ by (force simp add: openin_contains_ball)
+qed
subsection \<open>Closed Nest\<close>
@@ -3086,9 +3083,9 @@
by (auto intro!: bdd_belowI [where m=0] cInf_lower)
lemma le_setdist_iff:
- "d \<le> setdist s t \<longleftrightarrow>
- (\<forall>x \<in> s. \<forall>y \<in> t. d \<le> dist x y) \<and> (s = {} \<or> t = {} \<longrightarrow> d \<le> 0)"
- apply (cases "s = {} \<or> t = {}")
+ "d \<le> setdist S T \<longleftrightarrow>
+ (\<forall>x \<in> S. \<forall>y \<in> T. d \<le> dist x y) \<and> (S = {} \<or> T = {} \<longrightarrow> d \<le> 0)"
+ apply (cases "S = {} \<or> T = {}")
apply (force simp add: setdist_def)
apply (intro iffI conjI)
using setdist_le_dist apply fastforce
@@ -3096,34 +3093,33 @@
done
lemma setdist_ltE:
- assumes "setdist s t < b" "s \<noteq> {}" "t \<noteq> {}"
- obtains x y where "x \<in> s" "y \<in> t" "dist x y < b"
+ assumes "setdist S T < b" "S \<noteq> {}" "T \<noteq> {}"
+ obtains x y where "x \<in> S" "y \<in> T" "dist x y < b"
using assms
by (auto simp: not_le [symmetric] le_setdist_iff)
-lemma setdist_refl: "setdist s s = 0"
- apply (cases "s = {}")
+lemma setdist_refl: "setdist S S = 0"
+ apply (cases "S = {}")
apply (force simp add: setdist_def)
apply (rule antisym [OF _ setdist_pos_le])
apply (metis all_not_in_conv dist_self setdist_le_dist)
done
-lemma setdist_sym: "setdist s t = setdist t s"
+lemma setdist_sym: "setdist S T = setdist T S"
by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])
-lemma setdist_triangle: "setdist s t \<le> setdist s {a} + setdist {a} t"
-proof (cases "s = {} \<or> t = {}")
+lemma setdist_triangle: "setdist S T \<le> setdist S {a} + setdist {a} T"
+proof (cases "S = {} \<or> T = {}")
case True then show ?thesis
using setdist_pos_le by fastforce
next
case False
- have "\<And>x. x \<in> s \<Longrightarrow> setdist s t - dist x a \<le> setdist {a} t"
- apply (rule le_setdistI, blast)
- using False apply (fastforce intro: le_setdistI)
- apply (simp add: algebra_simps)
+ then have "\<And>x. x \<in> S \<Longrightarrow> setdist S T - dist x a \<le> setdist {a} T"
+ apply (intro le_setdistI)
+ apply (simp_all add: algebra_simps)
apply (metis dist_commute dist_triangle3 order_trans [OF setdist_le_dist])
done
- then have "setdist s t - setdist {a} t \<le> setdist s {a}"
+ then have "setdist S T - setdist {a} T \<le> setdist S {a}"
using False by (fastforce intro: le_setdistI)
then show ?thesis
by (simp add: algebra_simps)
@@ -3132,52 +3128,48 @@
lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
by (simp add: setdist_def)
-lemma setdist_Lipschitz: "\<bar>setdist {x} s - setdist {y} s\<bar> \<le> dist x y"
+lemma setdist_Lipschitz: "\<bar>setdist {x} S - setdist {y} S\<bar> \<le> dist x y"
apply (subst setdist_singletons [symmetric])
by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
-lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\<lambda>y. (setdist {y} s))"
+lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\<lambda>y. (setdist {y} S))"
by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
-lemma continuous_on_setdist [continuous_intros]: "continuous_on t (\<lambda>y. (setdist {y} s))"
+lemma continuous_on_setdist [continuous_intros]: "continuous_on T (\<lambda>y. (setdist {y} S))"
by (metis continuous_at_setdist continuous_at_imp_continuous_on)
-lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\<lambda>y. (setdist {y} s))"
+lemma uniformly_continuous_on_setdist: "uniformly_continuous_on T (\<lambda>y. (setdist {y} S))"
by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
-lemma setdist_subset_right: "\<lbrakk>t \<noteq> {}; t \<subseteq> u\<rbrakk> \<Longrightarrow> setdist s u \<le> setdist s t"
- apply (cases "s = {} \<or> u = {}", force)
+lemma setdist_subset_right: "\<lbrakk>T \<noteq> {}; T \<subseteq> u\<rbrakk> \<Longrightarrow> setdist S u \<le> setdist S T"
+ apply (cases "S = {} \<or> u = {}", force)
apply (auto simp: setdist_def intro!: bdd_belowI [where m=0] cInf_superset_mono)
done
-lemma setdist_subset_left: "\<lbrakk>s \<noteq> {}; s \<subseteq> t\<rbrakk> \<Longrightarrow> setdist t u \<le> setdist s u"
+lemma setdist_subset_left: "\<lbrakk>S \<noteq> {}; S \<subseteq> T\<rbrakk> \<Longrightarrow> setdist T u \<le> setdist S u"
by (metis setdist_subset_right setdist_sym)
-lemma setdist_closure_1 [simp]: "setdist (closure s) t = setdist s t"
-proof (cases "s = {} \<or> t = {}")
+lemma setdist_closure_1 [simp]: "setdist (closure S) T = setdist S T"
+proof (cases "S = {} \<or> T = {}")
case True then show ?thesis by force
next
case False
{ fix y
- assume "y \<in> t"
- have "continuous_on (closure s) (\<lambda>a. dist a y)"
+ assume "y \<in> T"
+ have "continuous_on (closure S) (\<lambda>a. dist a y)"
by (auto simp: continuous_intros dist_norm)
- then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"
- apply (rule continuous_ge_on_closure)
- apply assumption
- apply (blast intro: setdist_le_dist \<open>y \<in> t\<close> )
- done
+ then have *: "\<And>x. x \<in> closure S \<Longrightarrow> setdist S T \<le> dist x y"
+ by (fast intro: setdist_le_dist \<open>y \<in> T\<close> continuous_ge_on_closure)
} note * = this
show ?thesis
apply (rule antisym)
using False closure_subset apply (blast intro: setdist_subset_left)
- using False *
- apply (force intro!: le_setdistI)
+ using False * apply (force intro!: le_setdistI)
done
qed
-lemma setdist_closure_2 [simp]: "setdist t (closure s) = setdist t s"
-by (metis setdist_closure_1 setdist_sym)
+lemma setdist_closure_2 [simp]: "setdist T (closure S) = setdist T S"
+ by (metis setdist_closure_1 setdist_sym)
lemma setdist_eq_0I: "\<lbrakk>x \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> setdist S T = 0"
by (metis antisym dist_self setdist_le_dist setdist_pos_le)
--- a/src/HOL/Analysis/Elementary_Topology.thy Sat Aug 29 16:30:33 2020 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Sun Aug 30 19:45:46 2020 +0100
@@ -482,7 +482,8 @@
define U where "U = {x<..<y}"
then have "open U" by simp
moreover have "z \<in> U" using z U_def by simp
- ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+ ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U"
+ using topological_basisE[OF \<open>topological_basis A\<close>] by auto
define w where "w = (SOME x. x \<in> V)"
then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
then have "x < w \<and> w \<le> y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
@@ -494,7 +495,8 @@
define U where "U = {x<..}"
then have "open U" by simp
moreover have "y \<in> U" using \<open>x < y\<close> U_def by simp
- ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+ ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U"
+ using topological_basisE[OF \<open>topological_basis A\<close>] by auto
have "U = {y..}" unfolding U_def using * \<open>x < y\<close> by auto
then have "V \<subseteq> {y..}" using \<open>V \<subseteq> U\<close> by simp
then have "(LEAST w. w \<in> V) = y" using \<open>y \<in> V\<close> by (meson Least_equality atLeast_iff subsetCE)
@@ -521,7 +523,8 @@
define U where "U = {x<..<y}"
then have "open U" by simp
moreover have "z \<in> U" using z U_def by simp
- ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+ ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U"
+ using topological_basisE[OF \<open>topological_basis A\<close>] by auto
define w where "w = (SOME x. x \<in> V)"
then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
then have "x \<le> w \<and> w < y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
@@ -533,7 +536,8 @@
define U where "U = {..<y}"
then have "open U" by simp
moreover have "x \<in> U" using \<open>x < y\<close> U_def by simp
- ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+ ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U"
+ using topological_basisE[OF \<open>topological_basis A\<close>] by auto
have "U = {..x}" unfolding U_def using * \<open>x < y\<close> by auto
then have "V \<subseteq> {..x}" using \<open>V \<subseteq> U\<close> by simp
then have "(GREATEST x. x \<in> V) = x" using \<open>x \<in> V\<close> by (meson Greatest_equality atMost_iff subsetCE)
@@ -1556,18 +1560,12 @@
shows "infinite (range f)"
proof
assume "finite (range f)"
- then have "closed (range f)"
- by (rule finite_imp_closed)
- then have "open (- range f)"
- by (rule open_Compl)
- from assms(1) have "l \<in> - range f"
- by auto
- from assms(2) have "eventually (\<lambda>n. f n \<in> - range f) sequentially"
- using \<open>open (- range f)\<close> \<open>l \<in> - range f\<close>
- by (rule topological_tendstoD)
+ then have "l \<notin> range f \<and> closed (range f)"
+ using \<open>finite (range f)\<close> assms(1) finite_imp_closed by blast
+ then have "eventually (\<lambda>n. f n \<in> - range f) sequentially"
+ by (metis Compl_iff assms(2) open_Compl topological_tendstoD)
then show False
- unfolding eventually_sequentially
- by auto
+ unfolding eventually_sequentially by auto
qed
lemma Bolzano_Weierstrass_imp_closed:
--- a/src/HOL/Analysis/Path_Connected.thy Sat Aug 29 16:30:33 2020 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Sun Aug 30 19:45:46 2020 +0100
@@ -1629,8 +1629,7 @@
then have "y \<in> S"
by (simp add: path_component_mem(2))
then obtain e where e: "e > 0" "ball y e \<subseteq> S"
- using assms[unfolded open_contains_ball]
- by auto
+ using assms openE by blast
have "\<And>u. dist y u < e \<Longrightarrow> path_component S x u"
by (metis (full_types) as centre_in_ball convex_ball convex_imp_path_connected e mem_Collect_eq mem_ball path_component_eq path_component_of_subset path_connected_component)
then show "\<exists>e > 0. ball y e \<subseteq> path_component_set S x"
@@ -2863,30 +2862,33 @@
subsection\<^marker>\<open>tag unimportant\<close>\<open>Relations between components and path components\<close>
lemma open_connected_component:
- fixes s :: "'a::real_normed_vector set"
- shows "open s \<Longrightarrow> open (connected_component_set s x)"
- apply (simp add: open_contains_ball, clarify)
- apply (rename_tac y)
- apply (drule_tac x=y in bspec)
- apply (simp add: connected_component_in, clarify)
- apply (rule_tac x=e in exI)
- by (metis mem_Collect_eq connected_component_eq connected_component_maximal centre_in_ball connected_ball)
+ fixes S :: "'a::real_normed_vector set"
+ assumes "open S"
+ shows "open (connected_component_set S x)"
+proof (clarsimp simp: open_contains_ball)
+ fix y
+ assume xy: "connected_component S x y"
+ then obtain e where "e>0" "ball y e \<subseteq> S"
+ using assms connected_component_in openE by blast
+ then show "\<exists>e>0. ball y e \<subseteq> connected_component_set S x"
+ by (metis xy centre_in_ball connected_ball connected_component_eq_eq connected_component_in connected_component_maximal)
+qed
corollary open_components:
- fixes s :: "'a::real_normed_vector set"
- shows "\<lbrakk>open u; s \<in> components u\<rbrakk> \<Longrightarrow> open s"
+ fixes S :: "'a::real_normed_vector set"
+ shows "\<lbrakk>open u; S \<in> components u\<rbrakk> \<Longrightarrow> open S"
by (simp add: components_iff) (metis open_connected_component)
lemma in_closure_connected_component:
- fixes s :: "'a::real_normed_vector set"
- assumes x: "x \<in> s" and s: "open s"
- shows "x \<in> closure (connected_component_set s y) \<longleftrightarrow> x \<in> connected_component_set s y"
+ fixes S :: "'a::real_normed_vector set"
+ assumes x: "x \<in> S" and S: "open S"
+ shows "x \<in> closure (connected_component_set S y) \<longleftrightarrow> x \<in> connected_component_set S y"
proof -
- { assume "x \<in> closure (connected_component_set s y)"
- moreover have "x \<in> connected_component_set s x"
+ { assume "x \<in> closure (connected_component_set S y)"
+ moreover have "x \<in> connected_component_set S x"
using x by simp
- ultimately have "x \<in> connected_component_set s y"
- using s by (meson Compl_disjoint closure_iff_nhds_not_empty connected_component_disjoint disjoint_eq_subset_Compl open_connected_component)
+ ultimately have "x \<in> connected_component_set S y"
+ using S by (meson Compl_disjoint closure_iff_nhds_not_empty connected_component_disjoint disjoint_eq_subset_Compl open_connected_component)
}
then show ?thesis
by (auto simp: closure_def)
@@ -2957,76 +2959,72 @@
proof -
have "open S" using assms by blast
show ?thesis
- apply (rule connected_disjoint_Union_open_unique)
- apply (simp add: components_eq disjnt_def pairwise_def)
- using \<open>open S\<close>
- apply (simp_all add: assms open_components in_components_connected in_components_nonempty)
- done
+ proof (rule connected_disjoint_Union_open_unique)
+ show "disjoint (components S)"
+ by (simp add: components_eq disjnt_def pairwise_def)
+ qed (use \<open>open S\<close> in \<open>simp_all add: assms open_components in_components_connected in_components_nonempty\<close>)
qed
subsection\<^marker>\<open>tag unimportant\<close>\<open>Existence of unbounded components\<close>
lemma cobounded_unbounded_component:
- fixes s :: "'a :: euclidean_space set"
- assumes "bounded (-s)"
- shows "\<exists>x. x \<in> s \<and> \<not> bounded (connected_component_set s x)"
+ fixes S :: "'a :: euclidean_space set"
+ assumes "bounded (-S)"
+ shows "\<exists>x. x \<in> S \<and> \<not> bounded (connected_component_set S x)"
proof -
obtain i::'a where i: "i \<in> Basis"
using nonempty_Basis by blast
- obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
+ obtain B where B: "B>0" "-S \<subseteq> ball 0 B"
using bounded_subset_ballD [OF assms, of 0] by auto
- then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
+ then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> S"
by (force simp: ball_def dist_norm)
have unbounded_inner: "\<not> bounded {x. inner i x \<ge> B}"
- apply (auto simp: bounded_def dist_norm)
+ proof (clarsimp simp: bounded_def dist_norm)
+ fix e x
+ show "\<exists>y. B \<le> i \<bullet> y \<and> \<not> norm (x - y) \<le> e"
apply (rule_tac x="x + (max B e + 1 + \<bar>i \<bullet> x\<bar>) *\<^sub>R i" in exI)
- apply simp
- using i
- apply (auto simp: algebra_simps)
- done
- have **: "{x. B \<le> i \<bullet> x} \<subseteq> connected_component_set s (B *\<^sub>R i)"
+ using i by (auto simp: inner_right_distrib)
+ qed
+ have \<section>: "\<And>x. B \<le> i \<bullet> x \<Longrightarrow> x \<in> S"
+ using * Basis_le_norm [OF i] by (metis abs_ge_self inner_commute order_trans)
+ have "{x. B \<le> i \<bullet> x} \<subseteq> connected_component_set S (B *\<^sub>R i)"
apply (rule connected_component_maximal)
- apply (auto simp: i intro: convex_connected convex_halfspace_ge [of B])
- apply (rule *)
- apply (rule order_trans [OF _ Basis_le_norm [OF i]])
- by (simp add: inner_commute)
- have "B *\<^sub>R i \<in> s"
+ apply (auto simp: i intro: convex_connected convex_halfspace_ge [of B] \<section>)
+ done
+ then have "\<not> bounded (connected_component_set S (B *\<^sub>R i))"
+ using bounded_subset unbounded_inner by blast
+ moreover have "B *\<^sub>R i \<in> S"
by (rule *) (simp add: norm_Basis [OF i])
- then show ?thesis
- apply (rule_tac x="B *\<^sub>R i" in exI, clarify)
- apply (frule bounded_subset [of _ "{x. B \<le> i \<bullet> x}", OF _ **])
- using unbounded_inner apply blast
- done
+ ultimately show ?thesis
+ by blast
qed
lemma cobounded_unique_unbounded_component:
- fixes s :: "'a :: euclidean_space set"
- assumes bs: "bounded (-s)" and "2 \<le> DIM('a)"
- and bo: "\<not> bounded(connected_component_set s x)"
- "\<not> bounded(connected_component_set s y)"
- shows "connected_component_set s x = connected_component_set s y"
+ fixes S :: "'a :: euclidean_space set"
+ assumes bs: "bounded (-S)" and "2 \<le> DIM('a)"
+ and bo: "\<not> bounded(connected_component_set S x)"
+ "\<not> bounded(connected_component_set S y)"
+ shows "connected_component_set S x = connected_component_set S y"
proof -
obtain i::'a where i: "i \<in> Basis"
using nonempty_Basis by blast
- obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
+ obtain B where B: "B>0" "-S \<subseteq> ball 0 B"
using bounded_subset_ballD [OF bs, of 0] by auto
- then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
+ then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> S"
by (force simp: ball_def dist_norm)
- have ccb: "connected (- ball 0 B :: 'a set)"
- using assms by (auto intro: connected_complement_bounded_convex)
- obtain x' where x': "connected_component s x x'" "norm x' > B"
+ obtain x' where x': "connected_component S x x'" "norm x' > B"
using bo [unfolded bounded_def dist_norm, simplified, rule_format]
by (metis diff_zero norm_minus_commute not_less)
- obtain y' where y': "connected_component s y y'" "norm y' > B"
+ obtain y' where y': "connected_component S y y'" "norm y' > B"
using bo [unfolded bounded_def dist_norm, simplified, rule_format]
by (metis diff_zero norm_minus_commute not_less)
- have x'y': "connected_component s x' y'"
- apply (simp add: connected_component_def)
- apply (rule_tac x="- ball 0 B" in exI)
- using x' y'
- apply (auto simp: ccb dist_norm *)
- done
+ have x'y': "connected_component S x' y'"
+ unfolding connected_component_def
+ proof (intro exI conjI)
+ show "connected (- ball 0 B :: 'a set)"
+ using assms by (auto intro: connected_complement_bounded_convex)
+ qed (use x' y' dist_norm * in auto)
show ?thesis
apply (rule connected_component_eq)
using x' y' x'y'
@@ -3034,13 +3032,13 @@
qed
lemma cobounded_unbounded_components:
- fixes s :: "'a :: euclidean_space set"
- shows "bounded (-s) \<Longrightarrow> \<exists>c. c \<in> components s \<and> \<not>bounded c"
+ fixes S :: "'a :: euclidean_space set"
+ shows "bounded (-S) \<Longrightarrow> \<exists>c. c \<in> components S \<and> \<not>bounded c"
by (metis cobounded_unbounded_component components_def imageI)
lemma cobounded_unique_unbounded_components:
- fixes s :: "'a :: euclidean_space set"
- shows "\<lbrakk>bounded (- s); c \<in> components s; \<not> bounded c; c' \<in> components s; \<not> bounded c'; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> c' = c"
+ fixes S :: "'a :: euclidean_space set"
+ shows "\<lbrakk>bounded (- S); c \<in> components S; \<not> bounded c; c' \<in> components S; \<not> bounded c'; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> c' = c"
unfolding components_iff
by (metis cobounded_unique_unbounded_component)
@@ -3169,25 +3167,23 @@
assumes "bounded S" "2 \<le> DIM('a)"
shows "connected(outside S)"
apply (clarsimp simp add: connected_iff_connected_component outside)
- apply (rule_tac s="connected_component_set (- S) x" in connected_component_of_subset)
+ apply (rule_tac S="connected_component_set (- S) x" in connected_component_of_subset)
apply (metis (no_types) assms cobounded_unbounded_component cobounded_unique_unbounded_component connected_component_eq_eq connected_component_idemp double_complement mem_Collect_eq)
apply clarify
apply (metis connected_component_eq_eq connected_component_in)
done
lemma outside_connected_component_lt:
- "outside S = {x. \<forall>B. \<exists>y. B < norm(y) \<and> connected_component (- S) x y}"
-apply (auto simp: outside bounded_def dist_norm)
-apply (metis diff_0 norm_minus_cancel not_less)
-by (metis less_diff_eq norm_minus_commute norm_triangle_ineq2 order.trans pinf(6))
+ "outside S = {x. \<forall>B. \<exists>y. B < norm(y) \<and> connected_component (- S) x y}"
+ apply (auto simp: outside bounded_def dist_norm)
+ apply (metis diff_0 norm_minus_cancel not_less)
+ by (metis less_diff_eq norm_minus_commute norm_triangle_ineq2 order.trans pinf(6))
lemma outside_connected_component_le:
- "outside S =
- {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and>
- connected_component (- S) x y}"
-apply (simp add: outside_connected_component_lt)
-apply (simp add: Set.set_eq_iff)
-by (meson gt_ex leD le_less_linear less_imp_le order.trans)
+ "outside S =
+ {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> connected_component (- S) x y}"
+ apply (simp add: outside_connected_component_lt Set.set_eq_iff)
+ by (meson gt_ex leD le_less_linear less_imp_le order.trans)
lemma not_outside_connected_component_lt:
fixes S :: "'a::euclidean_space set"
@@ -3199,28 +3195,23 @@
{ fix y::'a and z::'a
assume yz: "B < norm z" "B < norm y"
have "connected_component (- cball 0 B) y z"
- apply (rule connected_componentI [OF _ subset_refl])
- apply (rule connected_complement_bounded_convex)
- using assms yz
- by (auto simp: dist_norm)
+ apply (intro connected_componentI [OF _ subset_refl] connected_complement_bounded_convex)
+ using assms yz by (auto simp: dist_norm)
then have "connected_component (- S) y z"
- apply (rule connected_component_of_subset)
- apply (metis Bno Compl_anti_mono mem_cball_0 subset_iff)
- done
+ by (metis connected_component_of_subset Bno Compl_anti_mono mem_cball_0 subset_iff)
} note cyz = this
show ?thesis
- apply (auto simp: outside)
+ apply (auto simp: outside bounded_pos)
apply (metis Compl_iff bounded_iff cobounded_imp_unbounded mem_Collect_eq not_le)
- apply (simp add: bounded_pos)
by (metis B connected_component_trans cyz not_le)
qed
lemma not_outside_connected_component_le:
- fixes S :: "'a::euclidean_space set"
- assumes S: "bounded S" "2 \<le> DIM('a)"
- shows "- (outside S) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> \<not> connected_component (- S) x y}"
-apply (auto intro: less_imp_le simp: not_outside_connected_component_lt [OF assms])
-by (meson gt_ex less_le_trans)
+ fixes S :: "'a::euclidean_space set"
+ assumes S: "bounded S" "2 \<le> DIM('a)"
+ shows "- (outside S) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> \<not> connected_component (- S) x y}"
+ apply (auto intro: less_imp_le simp: not_outside_connected_component_lt [OF assms])
+ by (meson gt_ex less_le_trans)
lemma inside_connected_component_lt:
fixes S :: "'a::euclidean_space set"
@@ -3237,9 +3228,9 @@
lemma inside_subset:
assumes "connected U" and "\<not> bounded U" and "T \<union> U = - S"
shows "inside S \<subseteq> T"
-apply (auto simp: inside_def)
-by (metis bounded_subset [of "connected_component_set (- S) _"] connected_component_maximal
- Compl_iff Un_iff assms subsetI)
+ apply (auto simp: inside_def)
+ by (metis bounded_subset [of "connected_component_set (- S) _"] connected_component_maximal
+ Compl_iff Un_iff assms subsetI)
lemma frontier_not_empty:
fixes S :: "'a :: real_normed_vector set"
@@ -3384,10 +3375,9 @@
assume x: "x \<in> interior s" and y: "y \<notin> s"
and cc: "connected_component (- frontier s) x y"
have "connected_component_set (- frontier s) x \<inter> frontier s \<noteq> {}"
- apply (rule connected_Int_frontier, simp)
- apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq rev_subsetD x)
- using y cc
- by blast
+ apply (rule connected_Int_frontier; simp add: set_eq_iff)
+ apply (meson cc connected_component_in connected_component_refl_eq interior_subset subsetD x)
+ using y cc by blast
then have "bounded (connected_component_set (- frontier s) x)"
using connected_component_in by auto
}
@@ -3402,29 +3392,29 @@
by (simp add: inside_def)
lemma outside_empty [simp]: "outside {} = (UNIV :: 'a :: {real_normed_vector, perfect_space} set)"
-using inside_empty inside_Un_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"
+ "\<lbrakk>connected_component (- S) x y; x \<in> inside S\<rbrakk> \<Longrightarrow> y \<in> inside S"
using connected_component_eq connected_component_in
by (fastforce simp add: inside_def)
lemma outside_same_component:
- "\<lbrakk>connected_component (- s) x y; x \<in> outside s\<rbrakk> \<Longrightarrow> y \<in> outside s"
+ "\<lbrakk>connected_component (- S) x y; x \<in> outside S\<rbrakk> \<Longrightarrow> y \<in> outside S"
using connected_component_eq connected_component_in
by (fastforce simp add: outside_def)
lemma convex_in_outside:
- fixes s :: "'a :: {real_normed_vector, perfect_space} set"
- assumes s: "convex s" and z: "z \<notin> s"
- shows "z \<in> outside s"
-proof (cases "s={}")
+ fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+ assumes S: "convex S" and z: "z \<notin> S"
+ shows "z \<in> outside S"
+proof (cases "S={}")
case True then show ?thesis by simp
next
- case False then obtain a where "a \<in> s" by blast
+ case False then obtain a where "a \<in> S" by blast
with z have zna: "z \<noteq> a" by auto
- { assume "bounded (connected_component_set (- s) z)"
- with bounded_pos_less obtain B where "B>0" and B: "\<And>x. connected_component (- s) z x \<Longrightarrow> norm x < B"
+ { assume "bounded (connected_component_set (- S) z)"
+ with bounded_pos_less obtain B where "B>0" and B: "\<And>x. connected_component (- S) z x \<Longrightarrow> norm x < B"
by (metis mem_Collect_eq)
define C where "C = (B + 1 + norm z) / norm (z-a)"
have "C > 0"
@@ -3435,16 +3425,16 @@
using zna \<open>B>0\<close> by (simp add: C_def le_max_iff_disj)
ultimately have C: "norm (z + C *\<^sub>R (z-a)) > B" by linarith
{ fix u::real
- assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> s"
+ assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> S"
then have Cpos: "1 + u * C > 0"
by (meson \<open>0 < C\<close> add_pos_nonneg less_eq_real_def zero_le_mult_iff zero_less_one)
then have *: "(1 / (1 + u * C)) *\<^sub>R z + (u * C / (1 + u * C)) *\<^sub>R z = z"
by (simp add: scaleR_add_left [symmetric] field_split_simps)
then have False
- using convexD_alt [OF s \<open>a \<in> s\<close> ins, of "1/(u*C + 1)"] \<open>C>0\<close> \<open>z \<notin> s\<close> Cpos u
+ using convexD_alt [OF S \<open>a \<in> S\<close> ins, of "1/(u*C + 1)"] \<open>C>0\<close> \<open>z \<notin> S\<close> Cpos u
by (simp add: * field_split_simps)
} note contra = this
- have "connected_component (- s) z (z + C *\<^sub>R (z-a))"
+ have "connected_component (- S) z (z + C *\<^sub>R (z-a))"
apply (rule connected_componentI [OF connected_segment [of z "z + C *\<^sub>R (z-a)"]])
apply (simp add: closed_segment_def)
using contra
@@ -3459,9 +3449,9 @@
qed
lemma outside_convex:
- fixes s :: "'a :: {real_normed_vector, perfect_space} set"
- assumes "convex s"
- shows "outside s = - s"
+ 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_Un_outside subsetI sup.cobounded2)
lemma outside_singleton [simp]:
@@ -3470,8 +3460,8 @@
by (auto simp: outside_convex)
lemma inside_convex:
- fixes s :: "'a :: {real_normed_vector, perfect_space} set"
- shows "convex s \<Longrightarrow> inside s = {}"
+ fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+ shows "convex S \<Longrightarrow> inside S = {}"
by (simp add: inside_outside outside_convex)
lemma inside_singleton [simp]:
@@ -3480,8 +3470,8 @@
by (auto simp: inside_convex)
lemma outside_subset_convex:
- fixes s :: "'a :: {real_normed_vector, perfect_space} set"
- shows "\<lbrakk>convex t; s \<subseteq> t\<rbrakk> \<Longrightarrow> - t \<subseteq> outside s"
+ fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+ shows "\<lbrakk>convex T; S \<subseteq> T\<rbrakk> \<Longrightarrow> - T \<subseteq> outside S"
using outside_convex outside_mono by blast
lemma outside_Un_outside_Un:
@@ -3505,49 +3495,49 @@
qed
lemma outside_frontier_misses_closure:
- fixes s :: "'a::real_normed_vector set"
- assumes "bounded s"
- shows "outside(frontier s) \<subseteq> - closure s"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "bounded S"
+ shows "outside(frontier S) \<subseteq> - closure S"
unfolding outside_inside Lattices.boolean_algebra_class.compl_le_compl_iff
proof -
- { assume "interior s \<subseteq> inside (frontier s)"
- hence "interior s \<union> inside (frontier s) = inside (frontier s)"
+ { assume "interior S \<subseteq> inside (frontier S)"
+ hence "interior S \<union> inside (frontier S) = inside (frontier S)"
by (simp add: subset_Un_eq)
- then have "closure s \<subseteq> frontier s \<union> inside (frontier s)"
+ then have "closure S \<subseteq> frontier S \<union> inside (frontier S)"
using frontier_def by auto
}
- then show "closure s \<subseteq> frontier s \<union> inside (frontier s)"
+ then show "closure S \<subseteq> frontier S \<union> inside (frontier S)"
using interior_inside_frontier [OF assms] by blast
qed
lemma outside_frontier_eq_complement_closure:
- fixes s :: "'a :: {real_normed_vector, perfect_space} set"
- assumes "bounded s" "convex s"
- shows "outside(frontier s) = - closure s"
+ fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+ assumes "bounded S" "convex S"
+ shows "outside(frontier S) = - closure S"
by (metis Diff_subset assms convex_closure frontier_def outside_frontier_misses_closure
outside_subset_convex subset_antisym)
lemma inside_frontier_eq_interior:
- fixes s :: "'a :: {real_normed_vector, perfect_space} set"
- shows "\<lbrakk>bounded s; convex s\<rbrakk> \<Longrightarrow> inside(frontier s) = interior s"
+ fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+ shows "\<lbrakk>bounded S; convex S\<rbrakk> \<Longrightarrow> inside(frontier S) = interior S"
apply (simp add: inside_outside outside_frontier_eq_complement_closure)
using closure_subset interior_subset
apply (auto simp: frontier_def)
done
lemma open_inside:
- fixes s :: "'a::real_normed_vector set"
- assumes "closed s"
- shows "open (inside s)"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "closed S"
+ shows "open (inside S)"
proof -
- { fix x assume x: "x \<in> inside s"
- have "open (connected_component_set (- s) x)"
+ { fix x assume x: "x \<in> inside S"
+ have "open (connected_component_set (- S) x)"
using assms open_connected_component by blast
- then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- s) x y"
+ then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- S) x y"
using dist_not_less_zero
apply (simp add: open_dist)
by (metis (no_types, lifting) Compl_iff connected_component_refl_eq inside_def mem_Collect_eq x)
- then have "\<exists>e>0. ball x e \<subseteq> inside s"
+ then have "\<exists>e>0. ball x e \<subseteq> inside S"
by (metis e dist_commute inside_same_component mem_ball subsetI x)
}
then show ?thesis
@@ -3555,18 +3545,18 @@
qed
lemma open_outside:
- fixes s :: "'a::real_normed_vector set"
- assumes "closed s"
- shows "open (outside s)"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "closed S"
+ shows "open (outside S)"
proof -
- { fix x assume x: "x \<in> outside s"
- have "open (connected_component_set (- s) x)"
+ { fix x assume x: "x \<in> outside S"
+ have "open (connected_component_set (- S) x)"
using assms open_connected_component by blast
- then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- s) x y"
+ then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- S) x y"
using dist_not_less_zero
apply (simp add: open_dist)
by (metis Int_iff outside_def connected_component_refl_eq x)
- then have "\<exists>e>0. ball x e \<subseteq> outside s"
+ then have "\<exists>e>0. ball x e \<subseteq> outside S"
by (metis e dist_commute outside_same_component mem_ball subsetI x)
}
then show ?thesis
@@ -3574,61 +3564,61 @@
qed
lemma closure_inside_subset:
- fixes s :: "'a::real_normed_vector set"
- assumes "closed s"
- shows "closure(inside s) \<subseteq> s \<union> inside s"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "closed S"
+ shows "closure(inside S) \<subseteq> S \<union> inside S"
by (metis assms closure_minimal open_closed open_outside sup.cobounded2 union_with_inside)
lemma frontier_inside_subset:
- fixes s :: "'a::real_normed_vector set"
- assumes "closed s"
- shows "frontier(inside s) \<subseteq> s"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "closed S"
+ shows "frontier(inside S) \<subseteq> S"
proof -
- have "closure (inside s) \<inter> - inside s = closure (inside s) - interior (inside s)"
+ 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"
+ moreover have "- inside S \<inter> - outside S = S"
by (metis (no_types) compl_sup double_compl inside_Un_outside)
- moreover have "closure (inside s) \<subseteq> - outside s"
+ 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"
+ ultimately have "closure (inside S) - interior (inside S) \<subseteq> S"
by blast
then show ?thesis
by (simp add: frontier_def open_inside interior_open)
qed
lemma closure_outside_subset:
- fixes s :: "'a::real_normed_vector set"
- assumes "closed s"
- shows "closure(outside s) \<subseteq> s \<union> outside s"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "closed S"
+ shows "closure(outside S) \<subseteq> S \<union> outside S"
apply (rule closure_minimal, simp)
by (metis assms closed_open inside_outside open_inside)
lemma frontier_outside_subset:
- fixes s :: "'a::real_normed_vector set"
- assumes "closed s"
- shows "frontier(outside s) \<subseteq> s"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "closed S"
+ shows "frontier(outside S) \<subseteq> S"
apply (simp add: frontier_def open_outside interior_open)
by (metis Diff_subset_conv assms closure_outside_subset interior_eq open_outside sup.commute)
lemma inside_complement_unbounded_connected_empty:
- "\<lbrakk>connected (- s); \<not> bounded (- s)\<rbrakk> \<Longrightarrow> inside s = {}"
+ "\<lbrakk>connected (- S); \<not> bounded (- S)\<rbrakk> \<Longrightarrow> inside S = {}"
apply (simp add: inside_def)
by (meson Compl_iff bounded_subset connected_component_maximal order_refl)
lemma inside_bounded_complement_connected_empty:
- fixes s :: "'a::{real_normed_vector, perfect_space} set"
- shows "\<lbrakk>connected (- s); bounded s\<rbrakk> \<Longrightarrow> inside s = {}"
+ fixes S :: "'a::{real_normed_vector, perfect_space} set"
+ shows "\<lbrakk>connected (- S); bounded S\<rbrakk> \<Longrightarrow> inside S = {}"
by (metis inside_complement_unbounded_connected_empty cobounded_imp_unbounded)
lemma inside_inside:
- assumes "s \<subseteq> inside t"
- shows "inside s - t \<subseteq> inside t"
+ assumes "S \<subseteq> inside T"
+ shows "inside S - T \<subseteq> inside T"
unfolding inside_def
proof clarify
fix x
- assume x: "x \<notin> t" "x \<notin> s" and bo: "bounded (connected_component_set (- s) x)"
- show "bounded (connected_component_set (- t) x)"
- proof (cases "s \<inter> connected_component_set (- t) x = {}")
+ assume x: "x \<notin> T" "x \<notin> S" and bo: "bounded (connected_component_set (- S) x)"
+ show "bounded (connected_component_set (- T) x)"
+ proof (cases "S \<inter> connected_component_set (- T) x = {}")
case True show ?thesis
apply (rule bounded_subset [OF bo])
apply (rule connected_component_maximal)
@@ -3643,68 +3633,68 @@
qed
qed
-lemma inside_inside_subset: "inside(inside s) \<subseteq> s"
+lemma inside_inside_subset: "inside(inside S) \<subseteq> S"
using inside_inside union_with_outside by fastforce
lemma inside_outside_intersect_connected:
- "\<lbrakk>connected t; inside s \<inter> t \<noteq> {}; outside s \<inter> t \<noteq> {}\<rbrakk> \<Longrightarrow> s \<inter> t \<noteq> {}"
+ "\<lbrakk>connected T; inside S \<inter> T \<noteq> {}; outside S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> S \<inter> T \<noteq> {}"
apply (simp add: inside_def outside_def ex_in_conv [symmetric] disjoint_eq_subset_Compl, clarify)
by (metis (no_types, hide_lams) Compl_anti_mono connected_component_eq connected_component_maximal contra_subsetD double_compl)
lemma outside_bounded_nonempty:
- fixes s :: "'a :: {real_normed_vector, perfect_space} set"
- assumes "bounded s" shows "outside s \<noteq> {}"
+ fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+ assumes "bounded S" shows "outside S \<noteq> {}"
by (metis (no_types, lifting) Collect_empty_eq Collect_mem_eq Compl_eq_Diff_UNIV Diff_cancel
Diff_disjoint UNIV_I assms ball_eq_empty bounded_diff cobounded_outside convex_ball
double_complement order_refl outside_convex outside_def)
lemma outside_compact_in_open:
- fixes s :: "'a :: {real_normed_vector,perfect_space} set"
- assumes s: "compact s" and t: "open t" and "s \<subseteq> t" "t \<noteq> {}"
- shows "outside s \<inter> t \<noteq> {}"
+ fixes S :: "'a :: {real_normed_vector,perfect_space} set"
+ assumes S: "compact S" and T: "open T" and "S \<subseteq> T" "T \<noteq> {}"
+ shows "outside S \<inter> T \<noteq> {}"
proof -
- have "outside s \<noteq> {}"
- by (simp add: compact_imp_bounded outside_bounded_nonempty s)
- with assms obtain a b where a: "a \<in> outside s" and b: "b \<in> t" by auto
+ have "outside S \<noteq> {}"
+ by (simp add: compact_imp_bounded outside_bounded_nonempty S)
+ with assms obtain a b where a: "a \<in> outside S" and b: "b \<in> T" by auto
show ?thesis
- proof (cases "a \<in> t")
+ proof (cases "a \<in> T")
case True with a show ?thesis by blast
next
case False
- have front: "frontier t \<subseteq> - s"
- using \<open>s \<subseteq> t\<close> frontier_disjoint_eq t by auto
+ have front: "frontier T \<subseteq> - S"
+ using \<open>S \<subseteq> T\<close> frontier_disjoint_eq T by auto
{ fix \<gamma>
- assume "path \<gamma>" and pimg_sbs: "path_image \<gamma> - {pathfinish \<gamma>} \<subseteq> interior (- t)"
- and pf: "pathfinish \<gamma> \<in> frontier t" and ps: "pathstart \<gamma> = a"
+ assume "path \<gamma>" and pimg_sbs: "path_image \<gamma> - {pathfinish \<gamma>} \<subseteq> interior (- T)"
+ and pf: "pathfinish \<gamma> \<in> frontier T" and ps: "pathstart \<gamma> = a"
define c where "c = pathfinish \<gamma>"
- have "c \<in> -s" unfolding c_def using front pf by blast
- moreover have "open (-s)" using s compact_imp_closed by blast
- ultimately obtain \<epsilon>::real where "\<epsilon> > 0" and \<epsilon>: "cball c \<epsilon> \<subseteq> -s"
- using open_contains_cball[of "-s"] s by blast
- then obtain d where "d \<in> t" and d: "dist d c < \<epsilon>"
- using closure_approachable [of c t] pf unfolding c_def
+ have "c \<in> -S" unfolding c_def using front pf by blast
+ moreover have "open (-S)" using S compact_imp_closed by blast
+ ultimately obtain \<epsilon>::real where "\<epsilon> > 0" and \<epsilon>: "cball c \<epsilon> \<subseteq> -S"
+ using open_contains_cball[of "-S"] S by blast
+ then obtain d where "d \<in> T" and d: "dist d c < \<epsilon>"
+ using closure_approachable [of c T] pf unfolding c_def
by (metis Diff_iff frontier_def)
- then have "d \<in> -s" using \<epsilon>
+ then have "d \<in> -S" using \<epsilon>
using dist_commute by (metis contra_subsetD mem_cball not_le not_less_iff_gr_or_eq)
- have pimg_sbs_cos: "path_image \<gamma> \<subseteq> -s"
+ have pimg_sbs_cos: "path_image \<gamma> \<subseteq> -S"
using pimg_sbs apply (auto simp: path_image_def)
apply (drule subsetD)
- using \<open>c \<in> - s\<close> \<open>s \<subseteq> t\<close> interior_subset apply (auto simp: c_def)
+ using \<open>c \<in> - S\<close> \<open>S \<subseteq> T\<close> interior_subset apply (auto simp: c_def)
done
have "closed_segment c d \<le> cball c \<epsilon>"
apply (simp add: segment_convex_hull)
apply (rule hull_minimal)
using \<open>\<epsilon> > 0\<close> d apply (auto simp: dist_commute)
done
- with \<epsilon> have "closed_segment c d \<subseteq> -s" by blast
+ with \<epsilon> have "closed_segment c d \<subseteq> -S" by blast
moreover have con_gcd: "connected (path_image \<gamma> \<union> closed_segment c d)"
by (rule connected_Un) (auto simp: c_def \<open>path \<gamma>\<close> connected_path_image)
- ultimately have "connected_component (- s) a d"
+ ultimately have "connected_component (- S) a d"
unfolding connected_component_def using pimg_sbs_cos ps by blast
- then have "outside s \<inter> t \<noteq> {}"
- using outside_same_component [OF _ a] by (metis IntI \<open>d \<in> t\<close> empty_iff)
+ then have "outside S \<inter> T \<noteq> {}"
+ using outside_same_component [OF _ a] by (metis IntI \<open>d \<in> T\<close> empty_iff)
} note * = this
- have pal: "pathstart (linepath a b) \<in> closure (- t)"
+ have pal: "pathstart (linepath a b) \<in> closure (- T)"
by (auto simp: False closure_def)
show ?thesis
by (rule exists_path_subpath_to_frontier [OF path_linepath pal _ *]) (auto simp: b)
@@ -3712,10 +3702,10 @@
qed
lemma inside_inside_compact_connected:
- fixes s :: "'a :: euclidean_space set"
- assumes s: "closed s" and t: "compact t" and "connected t" "s \<subseteq> inside t"
- shows "inside s \<subseteq> inside t"
-proof (cases "inside t = {}")
+ fixes S :: "'a :: euclidean_space set"
+ assumes S: "closed S" and T: "compact T" and "connected T" "S \<subseteq> inside T"
+ shows "inside S \<subseteq> inside T"
+proof (cases "inside T = {}")
case True with assms show ?thesis by auto
next
case False
@@ -3727,120 +3717,120 @@
using connected_convex_1_gen assms False inside_convex by blast
next
case 2
- have coms: "compact s"
- using assms apply (simp add: s compact_eq_bounded_closed)
+ have coms: "compact S"
+ using assms apply (simp add: S compact_eq_bounded_closed)
by (meson bounded_inside bounded_subset compact_imp_bounded)
- then have bst: "bounded (s \<union> t)"
- by (simp add: compact_imp_bounded t)
- then obtain r where "0 < r" and r: "s \<union> t \<subseteq> ball 0 r"
+ then have bst: "bounded (S \<union> T)"
+ by (simp add: compact_imp_bounded T)
+ then obtain r where "0 < r" and r: "S \<union> T \<subseteq> ball 0 r"
using bounded_subset_ballD by blast
- have outst: "outside s \<inter> outside t \<noteq> {}"
+ have outst: "outside S \<inter> outside T \<noteq> {}"
proof -
- have "- ball 0 r \<subseteq> outside s"
+ have "- ball 0 r \<subseteq> outside S"
apply (rule outside_subset_convex)
using r by auto
- moreover have "- ball 0 r \<subseteq> outside t"
+ moreover have "- ball 0 r \<subseteq> outside T"
apply (rule outside_subset_convex)
using r by auto
ultimately show ?thesis
by (metis Compl_subset_Compl_iff Int_subset_iff bounded_ball inf.orderE outside_bounded_nonempty outside_no_overlap)
qed
- have "s \<inter> t = {}" using assms
+ have "S \<inter> T = {}" using assms
by (metis disjoint_iff_not_equal inside_no_overlap subsetCE)
- moreover have "outside s \<inter> inside t \<noteq> {}"
- by (meson False assms(4) compact_eq_bounded_closed coms open_inside outside_compact_in_open t)
- ultimately have "inside s \<inter> t = {}"
- using inside_outside_intersect_connected [OF \<open>connected t\<close>, of s]
+ moreover have "outside S \<inter> inside T \<noteq> {}"
+ by (meson False assms(4) compact_eq_bounded_closed coms open_inside outside_compact_in_open T)
+ ultimately have "inside S \<inter> T = {}"
+ using inside_outside_intersect_connected [OF \<open>connected T\<close>, of S]
by (metis "2" compact_eq_bounded_closed coms connected_outside inf.commute inside_outside_intersect_connected outst)
then show ?thesis
- using inside_inside [OF \<open>s \<subseteq> inside t\<close>] by blast
+ using inside_inside [OF \<open>S \<subseteq> inside T\<close>] by blast
qed
qed
lemma connected_with_inside:
- fixes s :: "'a :: real_normed_vector set"
- assumes s: "closed s" and cons: "connected s"
- shows "connected(s \<union> inside s)"
-proof (cases "s \<union> inside s = UNIV")
+ fixes S :: "'a :: real_normed_vector set"
+ assumes S: "closed S" and cons: "connected S"
+ shows "connected(S \<union> inside S)"
+proof (cases "S \<union> inside S = UNIV")
case True with assms show ?thesis by auto
next
case False
- then obtain b where b: "b \<notin> s" "b \<notin> inside s" by blast
- have *: "\<exists>y t. y \<in> s \<and> connected t \<and> a \<in> t \<and> y \<in> t \<and> t \<subseteq> (s \<union> inside s)" if "a \<in> (s \<union> inside s)" for a
+ then obtain b where b: "b \<notin> S" "b \<notin> inside S" by blast
+ have *: "\<exists>y T. y \<in> S \<and> connected T \<and> a \<in> T \<and> y \<in> T \<and> T \<subseteq> (S \<union> inside S)" if "a \<in> (S \<union> inside S)" for a
using that proof
- assume "a \<in> s" then show ?thesis
+ assume "a \<in> S" then show ?thesis
apply (rule_tac x=a in exI)
apply (rule_tac x="{a}" in exI, simp)
done
next
- assume a: "a \<in> inside s"
+ assume a: "a \<in> inside S"
show ?thesis
- apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "inside s"])
+ apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "inside S"])
using a apply (simp add: closure_def)
apply (simp add: b)
apply (rule_tac x="pathfinish h" in exI)
apply (rule_tac x="path_image h" in exI)
apply (simp add: pathfinish_in_path_image connected_path_image, auto)
- using frontier_inside_subset s apply fastforce
- by (metis (no_types, lifting) frontier_inside_subset insertE insert_Diff interior_eq open_inside pathfinish_in_path_image s subsetCE)
+ using frontier_inside_subset S apply fastforce
+ by (metis (no_types, lifting) frontier_inside_subset insertE insert_Diff interior_eq open_inside pathfinish_in_path_image S subsetCE)
qed
show ?thesis
apply (simp add: connected_iff_connected_component)
apply (simp add: connected_component_def)
apply (clarify dest!: *)
- apply (rename_tac u u' t t')
- apply (rule_tac x="(s \<union> t \<union> t')" in exI)
- apply (auto simp: intro!: connected_Un cons)
+ apply (rename_tac u u' T t')
+ apply (rule_tac x="(S \<union> T \<union> t')" in exI)
+ apply (auto intro!: connected_Un cons)
done
qed
text\<open>The proof is virtually the same as that above.\<close>
lemma connected_with_outside:
- fixes s :: "'a :: real_normed_vector set"
- assumes s: "closed s" and cons: "connected s"
- shows "connected(s \<union> outside s)"
-proof (cases "s \<union> outside s = UNIV")
+ fixes S :: "'a :: real_normed_vector set"
+ assumes S: "closed S" and cons: "connected S"
+ shows "connected(S \<union> outside S)"
+proof (cases "S \<union> outside S = UNIV")
case True with assms show ?thesis by auto
next
case False
- then obtain b where b: "b \<notin> s" "b \<notin> outside s" by blast
- have *: "\<exists>y t. y \<in> s \<and> connected t \<and> a \<in> t \<and> y \<in> t \<and> t \<subseteq> (s \<union> outside s)" if "a \<in> (s \<union> outside s)" for a
+ then obtain b where b: "b \<notin> S" "b \<notin> outside S" by blast
+ have *: "\<exists>y T. y \<in> S \<and> connected T \<and> a \<in> T \<and> y \<in> T \<and> T \<subseteq> (S \<union> outside S)" if "a \<in> (S \<union> outside S)" for a
using that proof
- assume "a \<in> s" then show ?thesis
+ assume "a \<in> S" then show ?thesis
apply (rule_tac x=a in exI)
apply (rule_tac x="{a}" in exI, simp)
done
next
- assume a: "a \<in> outside s"
+ assume a: "a \<in> outside S"
show ?thesis
- apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "outside s"])
+ apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "outside S"])
using a apply (simp add: closure_def)
apply (simp add: b)
apply (rule_tac x="pathfinish h" in exI)
apply (rule_tac x="path_image h" in exI)
apply (simp add: pathfinish_in_path_image connected_path_image, auto)
- using frontier_outside_subset s apply fastforce
- by (metis (no_types, lifting) frontier_outside_subset insertE insert_Diff interior_eq open_outside pathfinish_in_path_image s subsetCE)
+ using frontier_outside_subset S apply fastforce
+ by (metis (no_types, lifting) frontier_outside_subset insertE insert_Diff interior_eq open_outside pathfinish_in_path_image S subsetCE)
qed
show ?thesis
apply (simp add: connected_iff_connected_component)
apply (simp add: connected_component_def)
apply (clarify dest!: *)
- apply (rename_tac u u' t t')
- apply (rule_tac x="(s \<union> t \<union> t')" in exI)
+ apply (rename_tac u u' T t')
+ apply (rule_tac x="(S \<union> T \<union> t')" in exI)
apply (auto simp: intro!: connected_Un cons)
done
qed
lemma inside_inside_eq_empty [simp]:
- fixes s :: "'a :: {real_normed_vector, perfect_space} set"
- assumes s: "closed s" and cons: "connected s"
- shows "inside (inside s) = {}"
+ fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+ assumes S: "closed S" and cons: "connected S"
+ shows "inside (inside S) = {}"
by (metis (no_types) unbounded_outside connected_with_outside [OF assms] bounded_Un
inside_complement_unbounded_connected_empty unbounded_outside union_with_outside)
lemma inside_in_components:
- "inside s \<in> components (- s) \<longleftrightarrow> connected(inside s) \<and> inside s \<noteq> {}"
+ "inside S \<in> components (- S) \<longleftrightarrow> connected(inside S) \<and> inside S \<noteq> {}"
apply (simp add: in_components_maximal)
apply (auto intro: inside_same_component connected_componentI)
apply (metis IntI empty_iff inside_no_overlap)
@@ -3848,15 +3838,15 @@
text\<open>The proof is virtually the same as that above.\<close>
lemma outside_in_components:
- "outside s \<in> components (- s) \<longleftrightarrow> connected(outside s) \<and> outside s \<noteq> {}"
+ "outside S \<in> components (- S) \<longleftrightarrow> connected(outside S) \<and> outside S \<noteq> {}"
apply (simp add: in_components_maximal)
apply (auto intro: outside_same_component connected_componentI)
apply (metis IntI empty_iff outside_no_overlap)
done
lemma bounded_unique_outside:
- fixes s :: "'a :: euclidean_space set"
- shows "\<lbrakk>bounded s; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- s) \<and> \<not> bounded c \<longleftrightarrow> c = outside s)"
+ fixes S :: "'a :: euclidean_space set"
+ shows "\<lbrakk>bounded S; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- S) \<and> \<not> bounded c \<longleftrightarrow> c = outside S)"
apply (rule iffI)
apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
@@ -3900,19 +3890,22 @@
by (metis (no_types) Klim zKs y contf comp_assoc continuous_on_closure_sequentially)
with fz have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
have rle: "r \<le> norm (f y - f a)"
- apply (rule le_no)
- using w wy oint
- by (force simp: imageI image_mono interiorI interior_subset frontier_def y)
+ proof (rule le_no)
+ show "y \<in> frontier S"
+ using w wy oint by (force simp: imageI image_mono interiorI interior_subset frontier_def y)
+ qed
have **: "(b \<inter> (- S) \<noteq> {} \<and> b - (- S) \<noteq> {} \<Longrightarrow> b \<inter> f \<noteq> {})
- \<Longrightarrow> (b \<inter> S \<noteq> {}) \<Longrightarrow> b \<inter> f = {} \<Longrightarrow>
- b \<subseteq> S" for b f and S :: "'b set"
+ \<Longrightarrow> (b \<inter> S \<noteq> {}) \<Longrightarrow> b \<inter> f = {} \<Longrightarrow> b \<subseteq> S"
+ for b f and S :: "'b set"
by blast
+ have \<section>: "\<And>y. \<lbrakk>norm (f a - y) < r; y \<in> frontier (f ` S)\<rbrakk> \<Longrightarrow> False"
+ by (metis dw_le norm_minus_commute not_less order_trans rle wy)
show ?thesis
apply (rule **) (*such a horrible mess*)
apply (rule connected_Int_frontier [where t = "f`S", OF connected_ball])
using \<open>a \<in> S\<close> \<open>0 < r\<close>
- apply (auto simp: disjoint_iff_not_equal dist_norm)
- by (metis dw_le norm_minus_commute not_less order_trans rle wy)
+ apply (auto simp: disjoint_iff_not_equal dist_norm dest: \<section>)
+ done
qed
--- a/src/HOL/Analysis/Starlike.thy Sat Aug 29 16:30:33 2020 +0100
+++ b/src/HOL/Analysis/Starlike.thy Sun Aug 30 19:45:46 2020 +0100
@@ -2823,14 +2823,11 @@
by (auto simp: dist_real_def field_simps split: split_min)
with \<open>x \<in> interior I\<close> e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
- have "open (interior I)" by auto
- from openE[OF this \<open>x \<in> interior I\<close>]
- obtain e where "0 < e" "ball x e \<subseteq> interior I" .
- moreover define K where "K = x - e / 2"
+ define K where "K = x - e / 2"
with \<open>0 < e\<close> have "K \<in> ball x e" "K < x"
by (auto simp: dist_real_def)
- ultimately have "K \<in> I" "K < x" "x \<in> I"
- using interior_subset[of I] \<open>x \<in> interior I\<close> by auto
+ then have "K \<in> I"
+ using \<open>interior I \<subseteq> I\<close> e(2) by blast
have "Inf (?F x) \<le> (f x - f y) / (x - y)"
proof (intro bdd_belowI cInf_lower2)
@@ -2870,11 +2867,8 @@
by auto
finally show "(f x - f y) / (x - y) \<le> z" .
next
- have "open (interior I)" by auto
- from openE[OF this \<open>x \<in> interior I\<close>]
- obtain e where e: "0 < e" "ball x e \<subseteq> interior I" .
- then have "x + e / 2 \<in> ball x e"
- by (auto simp: dist_real_def)
+ have "x + e / 2 \<in> ball x e"
+ using e by (auto simp: dist_real_def)
with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I"
by auto
then show "?F x \<noteq> {}"
@@ -2897,58 +2891,59 @@
qed
lemma affine_independent_convex_affine_hull:
- fixes s :: "'a::euclidean_space set"
- assumes "\<not> affine_dependent s" "t \<subseteq> s"
- shows "convex hull t = affine hull t \<inter> convex hull s"
+ fixes S :: "'a::euclidean_space set"
+ assumes "\<not> affine_dependent S" "T \<subseteq> S"
+ shows "convex hull T = affine hull T \<inter> convex hull S"
proof -
- have fin: "finite s" "finite t" using assms aff_independent_finite finite_subset by auto
+ have fin: "finite S" "finite T" using assms aff_independent_finite finite_subset by auto
{ fix u v x
- assume uv: "sum u t = 1" "\<forall>x\<in>s. 0 \<le> v x" "sum v s = 1"
- "(\<Sum>x\<in>s. v x *\<^sub>R x) = (\<Sum>v\<in>t. u v *\<^sub>R v)" "x \<in> t"
- then have s: "s = (s - t) \<union> t" \<comment> \<open>split into separate cases\<close>
+ assume uv: "sum u T = 1" "\<forall>x\<in>S. 0 \<le> v x" "sum v S = 1"
+ "(\<Sum>x\<in>S. v x *\<^sub>R x) = (\<Sum>v\<in>T. u v *\<^sub>R v)" "x \<in> T"
+ then have S: "S = (S - T) \<union> T" \<comment> \<open>split into separate cases\<close>
using assms by auto
- have [simp]: "(\<Sum>x\<in>t. v x *\<^sub>R x) + (\<Sum>x\<in>s - t. v x *\<^sub>R x) = (\<Sum>x\<in>t. u x *\<^sub>R x)"
- "sum v t + sum v (s - t) = 1"
- using uv fin s
+ have [simp]: "(\<Sum>x\<in>T. v x *\<^sub>R x) + (\<Sum>x\<in>S - T. v x *\<^sub>R x) = (\<Sum>x\<in>T. u x *\<^sub>R x)"
+ "sum v T + sum v (S - T) = 1"
+ using uv fin S
by (auto simp: sum.union_disjoint [symmetric] Un_commute)
- have "(\<Sum>x\<in>s. if x \<in> t then v x - u x else v x) = 0"
- "(\<Sum>x\<in>s. (if x \<in> t then v x - u x else v x) *\<^sub>R x) = 0"
+ have "(\<Sum>x\<in>S. if x \<in> T then v x - u x else v x) = 0"
+ "(\<Sum>x\<in>S. (if x \<in> T then v x - u x else v x) *\<^sub>R x) = 0"
using uv fin
- by (subst s, subst sum.union_disjoint, auto simp: algebra_simps sum_subtractf)+
+ by (subst S, subst sum.union_disjoint, auto simp: algebra_simps sum_subtractf)+
} note [simp] = this
- have "convex hull t \<subseteq> affine hull t"
+ have "convex hull T \<subseteq> affine hull T"
using convex_hull_subset_affine_hull by blast
- moreover have "convex hull t \<subseteq> convex hull s"
+ moreover have "convex hull T \<subseteq> convex hull S"
using assms hull_mono by blast
- moreover have "affine hull t \<inter> convex hull s \<subseteq> convex hull t"
- using assms
- apply (simp add: convex_hull_finite affine_hull_finite fin affine_dependent_explicit)
- apply (drule_tac x=s in spec)
- apply (auto simp: fin)
- apply (rule_tac x=u in exI)
- apply (rename_tac v)
- apply (drule_tac x="\<lambda>x. if x \<in> t then v x - u x else v x" in spec)
- apply (force)+
- done
+ moreover have "affine hull T \<inter> convex hull S \<subseteq> convex hull T"
+ proof -
+ have 0: "\<And>u. sum u S = 0 \<Longrightarrow> (\<forall>v\<in>S. u v = 0) \<or> (\<Sum>v\<in>S. u v *\<^sub>R v) \<noteq> 0"
+ using affine_dependent_explicit_finite assms(1) fin(1) by auto
+ show ?thesis
+ apply (clarsimp simp add: convex_hull_finite affine_hull_finite fin )
+ apply (rule_tac x=u in exI)
+ subgoal for u v
+ using 0 [of "\<lambda>x. if x \<in> T then v x - u x else v x"] \<open>T \<subseteq> S\<close> by force
+ done
+ qed
ultimately show ?thesis
by blast
qed
lemma affine_independent_span_eq:
- fixes s :: "'a::euclidean_space set"
- assumes "\<not> affine_dependent s" "card s = Suc (DIM ('a))"
- shows "affine hull s = UNIV"
-proof (cases "s = {}")
+ fixes S :: "'a::euclidean_space set"
+ assumes "\<not> affine_dependent S" "card S = Suc (DIM ('a))"
+ shows "affine hull S = UNIV"
+proof (cases "S = {}")
case True then show ?thesis
using assms by simp
next
case False
- then obtain a t where t: "a \<notin> t" "s = insert a t"
+ then obtain a T where T: "a \<notin> T" "S = insert a T"
by blast
- then have fin: "finite t" using assms
+ then have fin: "finite T" using assms
by (metis finite_insert aff_independent_finite)
show ?thesis
- using assms t fin
+ using assms T fin
apply (simp add: affine_dependent_iff_dependent affine_hull_insert_span_gen)
apply (rule subset_antisym)
apply force
@@ -2960,9 +2955,9 @@
qed
lemma affine_independent_span_gt:
- fixes s :: "'a::euclidean_space set"
- assumes ind: "\<not> affine_dependent s" and dim: "DIM ('a) < card s"
- shows "affine hull s = UNIV"
+ fixes S :: "'a::euclidean_space set"
+ assumes ind: "\<not> affine_dependent S" and dim: "DIM ('a) < card S"
+ shows "affine hull S = UNIV"
apply (rule affine_independent_span_eq [OF ind])
apply (rule antisym)
using assms
@@ -2971,35 +2966,35 @@
done
lemma empty_interior_affine_hull:
- fixes s :: "'a::euclidean_space set"
- assumes "finite s" and dim: "card s \<le> DIM ('a)"
- shows "interior(affine hull s) = {}"
+ fixes S :: "'a::euclidean_space set"
+ assumes "finite S" and dim: "card S \<le> DIM ('a)"
+ shows "interior(affine hull S) = {}"
using assms
- apply (induct s rule: finite_induct)
+ apply (induct S rule: finite_induct)
apply (simp_all add: affine_dependent_iff_dependent affine_hull_insert_span_gen interior_translation)
apply (rule empty_interior_lowdim)
by (auto simp: Suc_le_lessD card_image_le dual_order.trans intro!: dim_le_card'[THEN le_less_trans])
lemma empty_interior_convex_hull:
- fixes s :: "'a::euclidean_space set"
- assumes "finite s" and dim: "card s \<le> DIM ('a)"
- shows "interior(convex hull s) = {}"
+ fixes S :: "'a::euclidean_space set"
+ assumes "finite S" and dim: "card S \<le> DIM ('a)"
+ shows "interior(convex hull S) = {}"
by (metis Diff_empty Diff_eq_empty_iff convex_hull_subset_affine_hull
interior_mono empty_interior_affine_hull [OF assms])
lemma explicit_subset_rel_interior_convex_hull:
- fixes s :: "'a::euclidean_space set"
- shows "finite s
- \<Longrightarrow> {y. \<exists>u. (\<forall>x \<in> s. 0 < u x \<and> u x < 1) \<and> sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}
- \<subseteq> rel_interior (convex hull s)"
- by (force simp add: rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=s, simplified])
+ fixes S :: "'a::euclidean_space set"
+ shows "finite S
+ \<Longrightarrow> {y. \<exists>u. (\<forall>x \<in> S. 0 < u x \<and> u x < 1) \<and> sum u S = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y}
+ \<subseteq> rel_interior (convex hull S)"
+ by (force simp add: rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=S, simplified])
lemma explicit_subset_rel_interior_convex_hull_minimal:
- fixes s :: "'a::euclidean_space set"
- shows "finite s
- \<Longrightarrow> {y. \<exists>u. (\<forall>x \<in> s. 0 < u x) \<and> sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}
- \<subseteq> rel_interior (convex hull s)"
- by (force simp add: rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=s, simplified])
+ fixes S :: "'a::euclidean_space set"
+ shows "finite S
+ \<Longrightarrow> {y. \<exists>u. (\<forall>x \<in> S. 0 < u x) \<and> sum u S = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y}
+ \<subseteq> rel_interior (convex hull S)"
+ by (force simp add: rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=S, simplified])
lemma rel_interior_convex_hull_explicit:
fixes s :: "'a::euclidean_space set"
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy Sat Aug 29 16:30:33 2020 +0100
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy Sun Aug 30 19:45:46 2020 +0100
@@ -1024,12 +1024,9 @@
by (meson open_ball centre_in_ball)
define U where "U = (\<lambda>w. (w - \<xi>) * g w) ` T"
have "open U" by (metis oimT U_def)
- have "0 \<in> U"
- apply (auto simp: U_def)
- apply (rule image_eqI [where x = \<xi>])
- apply (auto simp: \<open>\<xi> \<in> T\<close>)
- done
- then obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "cball 0 \<epsilon> \<subseteq> U"
+ moreover have "0 \<in> U"
+ using \<open>\<xi> \<in> T\<close> by (auto simp: U_def intro: image_eqI [where x = \<xi>])
+ ultimately obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "cball 0 \<epsilon> \<subseteq> U"
using \<open>open U\<close> open_contains_cball by blast
then have "\<epsilon> * exp(2 * of_real pi * \<i> * (0/n)) \<in> cball 0 \<epsilon>"
"\<epsilon> * exp(2 * of_real pi * \<i> * (1/n)) \<in> cball 0 \<epsilon>"