--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Oct 19 17:16:01 2017 +0100
@@ -2279,7 +2279,7 @@
lemma retraction_imp_quotient_map:
"retraction s t r
\<Longrightarrow> u \<subseteq> t
- \<Longrightarrow> (openin (subtopology euclidean s) {x. x \<in> s \<and> r x \<in> u} \<longleftrightarrow>
+ \<Longrightarrow> (openin (subtopology euclidean s) (s \<inter> r -` u) \<longleftrightarrow>
openin (subtopology euclidean t) u)"
apply (clarsimp simp add: retraction)
apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
@@ -2941,21 +2941,21 @@
and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
by (metis Dugundji [OF C cloUT contgf gfTC])
show ?thesis
- proof (rule_tac V = "{x \<in> U. f' x \<in> D}" and g = "h o r o f'" in that)
- show "T \<subseteq> {x \<in> U. f' x \<in> D}"
+ proof (rule_tac V = "U \<inter> f' -` D" and g = "h o r o f'" in that)
+ show "T \<subseteq> U \<inter> f' -` D"
using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
by fastforce
- show ope: "openin (subtopology euclidean U) {x \<in> U. f' x \<in> D}"
+ show ope: "openin (subtopology euclidean U) (U \<inter> f' -` D)"
using \<open>f' ` U \<subseteq> C\<close> by (auto simp: opD contf' continuous_openin_preimage)
- have conth: "continuous_on (r ` f' ` {x \<in> U. f' x \<in> D}) h"
+ have conth: "continuous_on (r ` f' ` (U \<inter> f' -` D)) h"
apply (rule continuous_on_subset [of S'])
using homeomorphism_def homgh apply blast
using \<open>r ` D \<subseteq> S'\<close> by blast
- show "continuous_on {x \<in> U. f' x \<in> D} (h \<circ> r \<circ> f')"
+ show "continuous_on (U \<inter> f' -` D) (h \<circ> r \<circ> f')"
apply (intro continuous_on_compose conth
continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto)
done
- show "(h \<circ> r \<circ> f') ` {x \<in> U. f' x \<in> D} \<subseteq> S"
+ show "(h \<circ> r \<circ> f') ` (U \<inter> f' -` D) \<subseteq> S"
using \<open>homeomorphism S S' g h\<close> \<open>f' ` U \<subseteq> C\<close> \<open>r ` D \<subseteq> S'\<close>
by (auto simp: homeomorphism_def)
show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
@@ -3150,36 +3150,36 @@
have "S' \<subseteq> W" using WS' closedin_closed by auto
have him: "\<And>x. x \<in> S' \<Longrightarrow> h x \<in> X"
by (metis (no_types) \<open>S retract_of X\<close> hg hom homeomorphism_def image_insert insert_absorb insert_iff retract_of_imp_subset subset_eq)
- have "S' retract_of {x \<in> W. h x \<in> X}"
+ have "S' retract_of (W \<inter> h -` X)"
proof (simp add: retraction_def retract_of_def, intro exI conjI)
- show "S' \<subseteq> {x \<in> W. h x \<in> X}"
- using him WS' closedin_imp_subset by blast
- show "continuous_on {x \<in> W. h x \<in> X} (f o r o h)"
+ show "S' \<subseteq> W" "S' \<subseteq> h -` X"
+ using him WS' closedin_imp_subset by blast+
+ show "continuous_on (W \<inter> h -` X) (f o r o h)"
proof (intro continuous_on_compose)
- show "continuous_on {x \<in> W. h x \<in> X} h"
- by (metis (no_types) Collect_restrict conth continuous_on_subset)
- show "continuous_on (h ` {x \<in> W. h x \<in> X}) r"
+ show "continuous_on (W \<inter> h -` X) h"
+ by (meson conth continuous_on_subset inf_le1)
+ show "continuous_on (h ` (W \<inter> h -` X)) r"
proof -
- have "h ` {b \<in> W. h b \<in> X} \<subseteq> X"
+ have "h ` (W \<inter> h -` X) \<subseteq> X"
by blast
- then show "continuous_on (h ` {b \<in> W. h b \<in> X}) r"
+ then show "continuous_on (h ` (W \<inter> h -` X)) r"
by (meson \<open>retraction X S r\<close> continuous_on_subset retraction)
qed
- show "continuous_on (r ` h ` {x \<in> W. h x \<in> X}) f"
+ show "continuous_on (r ` h ` (W \<inter> h -` X)) f"
apply (rule continuous_on_subset [of S])
using hom homeomorphism_def apply blast
apply clarify
apply (meson \<open>retraction X S r\<close> subsetD imageI retraction_def)
done
qed
- show "(f \<circ> r \<circ> h) ` {x \<in> W. h x \<in> X} \<subseteq> S'"
+ show "(f \<circ> r \<circ> h) ` (W \<inter> h -` X) \<subseteq> S'"
using \<open>retraction X S r\<close> hom
by (auto simp: retraction_def homeomorphism_def)
show "\<forall>x\<in>S'. (f \<circ> r \<circ> h) x = x"
using \<open>retraction X S r\<close> hom by (auto simp: retraction_def homeomorphism_def hg)
qed
then show ?thesis
- apply (rule_tac V = "{x. x \<in> W \<and> h x \<in> X}" in that)
+ apply (rule_tac V = "W \<inter> h -` X" in that)
apply (rule openin_trans [OF _ UW])
using \<open>continuous_on W h\<close> \<open>open X\<close> continuous_openin_preimage_eq apply blast+
done
@@ -3248,8 +3248,7 @@
using \<open>ANR S\<close>
apply (simp add: ANR_def)
apply (drule_tac x=UNIV in spec)
- apply (drule_tac x=T in spec)
- apply (auto simp: closed_closedin)
+ apply (drule_tac x=T in spec, clarsimp)
apply (meson ENR_def ENR_homeomorphic_ENR open_openin)
done
qed
@@ -3455,10 +3454,10 @@
define W where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
have US': "closedin (subtopology euclidean U) S'"
using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
- by (simp add: S'_def continuous_intros)
+ by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
have UT': "closedin (subtopology euclidean U) T'"
using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
- by (simp add: T'_def continuous_intros)
+ by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
have "S \<subseteq> S'"
using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
have "T \<subseteq> T'"
@@ -3543,19 +3542,19 @@
proof -
obtain f g where hom: "homeomorphism (S \<union> T) C f g"
using hom by (force simp: homeomorphic_def)
- have US: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> S}"
+ have US: "closedin (subtopology euclidean U) (C \<inter> g -` S)"
apply (rule closedin_trans [OF _ UC])
apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
using hom homeomorphism_def apply blast
apply (metis hom homeomorphism_def set_eq_subset)
done
- have UT: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> T}"
+ have UT: "closedin (subtopology euclidean U) (C \<inter> g -` T)"
apply (rule closedin_trans [OF _ UC])
apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
using hom homeomorphism_def apply blast
apply (metis hom homeomorphism_def set_eq_subset)
done
- have ARS: "AR {x \<in> C. g x \<in> S}"
+ have ARS: "AR (C \<inter> g -` S)"
apply (rule AR_homeomorphic_AR [OF \<open>AR S\<close>])
apply (simp add: homeomorphic_def)
apply (rule_tac x=g in exI)
@@ -3563,7 +3562,7 @@
using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
apply (rule_tac x="f x" in image_eqI, auto)
done
- have ART: "AR {x \<in> C. g x \<in> T}"
+ have ART: "AR (C \<inter> g -` T)"
apply (rule AR_homeomorphic_AR [OF \<open>AR T\<close>])
apply (simp add: homeomorphic_def)
apply (rule_tac x=g in exI)
@@ -3571,7 +3570,7 @@
using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
apply (rule_tac x="f x" in image_eqI, auto)
done
- have ARI: "AR ({x \<in> C. g x \<in> S} \<inter> {x \<in> C. g x \<in> T})"
+ have ARI: "AR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
apply (rule AR_homeomorphic_AR [OF \<open>AR (S \<inter> T)\<close>])
apply (simp add: homeomorphic_def)
apply (rule_tac x=g in exI)
@@ -3580,7 +3579,7 @@
apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
apply (rule_tac x="f x" in image_eqI, auto)
done
- have "C = {x \<in> C. g x \<in> S} \<union> {x \<in> C. g x \<in> T}"
+ have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
using hom by (auto simp: homeomorphism_def)
then show ?thesis
by (metis AR_closed_Un_local_aux [OF US UT ARS ART ARI])
@@ -3615,10 +3614,10 @@
define W where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
have cloUS': "closedin (subtopology euclidean U) S'"
using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
- by (simp add: S'_def continuous_intros)
+ by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
have cloUT': "closedin (subtopology euclidean U) T'"
using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
- by (simp add: T'_def continuous_intros)
+ by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
have "S \<subseteq> S'"
using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
have "T \<subseteq> T'"
@@ -3752,19 +3751,19 @@
proof -
obtain f g where hom: "homeomorphism (S \<union> T) C f g"
using hom by (force simp: homeomorphic_def)
- have US: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> S}"
+ have US: "closedin (subtopology euclidean U) (C \<inter> g -` S)"
apply (rule closedin_trans [OF _ UC])
apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
using hom [unfolded homeomorphism_def] apply blast
apply (metis hom homeomorphism_def set_eq_subset)
done
- have UT: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> T}"
+ have UT: "closedin (subtopology euclidean U) (C \<inter> g -` T)"
apply (rule closedin_trans [OF _ UC])
apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
using hom [unfolded homeomorphism_def] apply blast
apply (metis hom homeomorphism_def set_eq_subset)
done
- have ANRS: "ANR {x \<in> C. g x \<in> S}"
+ have ANRS: "ANR (C \<inter> g -` S)"
apply (rule ANR_homeomorphic_ANR [OF \<open>ANR S\<close>])
apply (simp add: homeomorphic_def)
apply (rule_tac x=g in exI)
@@ -3772,7 +3771,7 @@
using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
apply (rule_tac x="f x" in image_eqI, auto)
done
- have ANRT: "ANR {x \<in> C. g x \<in> T}"
+ have ANRT: "ANR (C \<inter> g -` T)"
apply (rule ANR_homeomorphic_ANR [OF \<open>ANR T\<close>])
apply (simp add: homeomorphic_def)
apply (rule_tac x=g in exI)
@@ -3780,7 +3779,7 @@
using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
apply (rule_tac x="f x" in image_eqI, auto)
done
- have ANRI: "ANR ({x \<in> C. g x \<in> S} \<inter> {x \<in> C. g x \<in> T})"
+ have ANRI: "ANR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
apply (rule ANR_homeomorphic_ANR [OF \<open>ANR (S \<inter> T)\<close>])
apply (simp add: homeomorphic_def)
apply (rule_tac x=g in exI)
@@ -3789,8 +3788,8 @@
apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
apply (rule_tac x="f x" in image_eqI, auto)
done
- have "C = {x. x \<in> C \<and> g x \<in> S} \<union> {x. x \<in> C \<and> g x \<in> T}"
- by auto (metis Un_iff hom homeomorphism_def imageI)
+ have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
+ using hom by (auto simp: homeomorphism_def)
then show ?thesis
by (metis ANR_closed_Un_local_aux [OF US UT ANRS ANRT ANRI])
qed
@@ -3822,13 +3821,13 @@
using fim by auto
show "\<exists>V g. C \<subseteq> V \<and> openin (subtopology euclidean U) V \<and> continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x\<in>C. g x = f x)"
proof (intro exI conjI)
- show "C \<subseteq> {x \<in> W. g x \<in> S}"
+ show "C \<subseteq> W \<inter> g -` S"
using \<open>C \<subseteq> W\<close> fim geq by blast
- show "openin (subtopology euclidean U) {x \<in> W. g x \<in> S}"
+ show "openin (subtopology euclidean U) (W \<inter> g -` S)"
by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans)
- show "continuous_on {x \<in> W. g x \<in> S} g"
+ show "continuous_on (W \<inter> g -` S) g"
by (blast intro: continuous_on_subset [OF contg])
- show "g ` {x \<in> W. g x \<in> S} \<subseteq> S"
+ show "g ` (W \<inter> g -` S) \<subseteq> S"
using gim by blast
show "\<forall>x\<in>C. g x = f x"
using geq by blast
@@ -4074,15 +4073,14 @@
apply (auto simp add: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point)
done
finally have "rel_frontier S retract_of {x. closest_point (affine hull S) x \<noteq> a}" .
- moreover have "openin (subtopology euclidean UNIV) {x \<in> UNIV. closest_point (affine hull S) x \<in> - {a}}"
+ moreover have "openin (subtopology euclidean UNIV) (UNIV \<inter> closest_point (affine hull S) -` (- {a}))"
apply (rule continuous_openin_preimage_gen)
apply (auto simp add: False affine_imp_convex continuous_on_closest_point)
done
ultimately show ?thesis
- apply (simp add: ENR_def)
- apply (rule_tac x = "{x. x \<in> UNIV \<and>
- closest_point (affine hull S) x \<in> (- {a})}" in exI)
- apply simp
+ unfolding ENR_def
+ apply (rule_tac x = "closest_point (affine hull S) -` (- {a})" in exI)
+ apply (simp add: vimage_def)
done
qed
@@ -4881,5 +4879,4 @@
using connected_complement_homeomorphic_convex_compact [OF assms]
using \<open>compact T\<close> compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast
-
end
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Oct 19 17:16:01 2017 +0100
@@ -4111,30 +4111,29 @@
subsection\<open>The winding number is constant on a connected region\<close>
lemma winding_number_constant:
- assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and cs: "connected s" and sg: "s \<inter> path_image \<gamma> = {}"
- obtains k where "\<And>z. z \<in> s \<Longrightarrow> winding_number \<gamma> z = k"
+ assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and cs: "connected S" and sg: "S \<inter> path_image \<gamma> = {}"
+ shows "winding_number \<gamma> constant_on S"
proof -
have *: "1 \<le> cmod (winding_number \<gamma> y - winding_number \<gamma> z)"
- if ne: "winding_number \<gamma> y \<noteq> winding_number \<gamma> z" and "y \<in> s" "z \<in> s" for y z
+ if ne: "winding_number \<gamma> y \<noteq> winding_number \<gamma> z" and "y \<in> S" "z \<in> S" for y z
proof -
have "winding_number \<gamma> y \<in> \<int>" "winding_number \<gamma> z \<in> \<int>"
- using that integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> s\<close> by auto
+ using that integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> S\<close> by auto
with ne show ?thesis
by (auto simp: Ints_def of_int_diff [symmetric] simp del: of_int_diff)
qed
- have cont: "continuous_on s (\<lambda>w. winding_number \<gamma> w)"
+ have cont: "continuous_on S (\<lambda>w. winding_number \<gamma> w)"
using continuous_on_winding_number [OF \<gamma>] sg
by (meson continuous_on_subset disjoint_eq_subset_Compl)
show ?thesis
- apply (rule continuous_discrete_range_constant [OF cs cont])
- using "*" zero_less_one apply blast
- by (simp add: that)
+ using "*" zero_less_one
+ by (blast intro: continuous_discrete_range_constant [OF cs cont])
qed
lemma winding_number_eq:
- "\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; w \<in> s; z \<in> s; connected s; s \<inter> path_image \<gamma> = {}\<rbrakk>
+ "\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; w \<in> S; z \<in> S; connected S; S \<inter> path_image \<gamma> = {}\<rbrakk>
\<Longrightarrow> winding_number \<gamma> w = winding_number \<gamma> z"
- using winding_number_constant by blast
+ using winding_number_constant by (metis constant_on_def)
lemma open_winding_number_levelsets:
assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
@@ -4149,7 +4148,7 @@
have "\<exists>e>0. \<forall>y. dist y z < e \<longrightarrow> y \<notin> path_image \<gamma> \<and> winding_number \<gamma> y = winding_number \<gamma> z"
apply (rule_tac x=e in exI)
using e apply (simp add: dist_norm ball_def norm_minus_commute)
- apply (auto simp: dist_norm norm_minus_commute intro!: winding_number_eq [OF assms, where s = "ball z e"])
+ apply (auto simp: dist_norm norm_minus_commute intro!: winding_number_eq [OF assms, where S = "ball z e"])
done
} then
show ?thesis
@@ -4171,11 +4170,11 @@
using B subset_ball by auto
then have wout: "w \<in> outside (path_image \<gamma>)"
using w by blast
- moreover obtain k where "\<And>z. z \<in> outside (path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = k"
+ moreover have "winding_number \<gamma> constant_on outside (path_image \<gamma>)"
using winding_number_constant [OF \<gamma> loop, of "outside(path_image \<gamma>)"] connected_outside
by (metis DIM_complex bounded_path_image dual_order.refl \<gamma> outside_no_overlap)
ultimately have "winding_number \<gamma> z = winding_number \<gamma> w"
- using z by blast
+ by (metis (no_types, hide_lams) constant_on_def z)
also have "... = 0"
proof -
have wnot: "w \<notin> path_image \<gamma>" using wout by (simp add: outside_def)
--- a/src/HOL/Analysis/Conformal_Mappings.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Thu Oct 19 17:16:01 2017 +0100
@@ -127,7 +127,7 @@
apply (rule Cauchy_inequality)
using holf holomorphic_on_subset apply force
using holf holomorphic_on_imp_continuous_on holomorphic_on_subset apply blast
- using \<open>w \<noteq> 0\<close> apply (simp add:)
+ using \<open>w \<noteq> 0\<close> apply simp
by (metis nof wgeA dist_0_norm dist_norm)
also have "... = fact k * (B * 1 / cmod w ^ (k-n))"
apply (simp only: mult_cancel_left times_divide_eq_right [symmetric])
@@ -327,7 +327,7 @@
ultimately obtain w where w: "w \<in> frontier(cball \<xi> r)"
and now: "\<And>x. x \<in> frontier(cball \<xi> r) \<Longrightarrow> norm (f w) \<le> norm (f x)"
apply (rule bexE [OF continuous_attains_inf [OF compact_frontier [OF compact_cball]]])
- apply (simp add:)
+ apply simp
done
then have fw: "0 < norm (f w)"
by (simp add: fnz')
@@ -336,7 +336,7 @@
then obtain v where v: "v \<in> frontier(cball \<xi> r)"
and nov: "\<And>x. x \<in> frontier(cball \<xi> r) \<Longrightarrow> norm (g v) \<ge> norm (g x)"
apply (rule bexE [OF continuous_attains_sup [OF compact_frontier [OF compact_cball] froc]])
- apply (simp add:)
+ apply simp
done
then have fv: "0 < norm (f v)"
by (simp add: fnz')
@@ -628,7 +628,7 @@
unfolding powf_def by (rule holomorphic_power_series [OF holfb w])
moreover have "(\<Sum>i<n. powf i) = f \<xi>"
apply (subst Groups_Big.comm_monoid_add_class.sum.setdiff_irrelevant [symmetric])
- apply (simp add:)
+ apply simp
apply (simp only: dfz sing)
apply (simp add: powf_def)
done
@@ -640,7 +640,7 @@
have "summable (\<lambda>i. (deriv ^^ (i + n)) f \<xi> * (w - \<xi>) ^ i / fact (i + n))"
proof (cases "w=\<xi>")
case False then show ?thesis
- using summable_mult [OF *, of "1 / (w - \<xi>) ^ n"] by (simp add:)
+ using summable_mult [OF *, of "1 / (w - \<xi>) ^ n"] by simp
next
case True then show ?thesis
by (auto simp: Power.semiring_1_class.power_0_left intro!: summable_finite [of "{0}"]
@@ -716,7 +716,7 @@
apply (rule holomorphic_intros)+
using h holomorphic_on_open apply blast
apply (rule holomorphic_intros)+
- using \<open>0 < n\<close> apply (simp add:)
+ using \<open>0 < n\<close> apply simp
apply (rule holomorphic_intros)+
done
show ?thesis
@@ -924,7 +924,7 @@
using \<open>0 < r\<close> by simp
have "\<exists>B. 0<B \<and> eventually (\<lambda>z. cmod ((inverse \<circ> f \<circ> inverse) z) \<le> B) (at 0)"
apply (rule exI [where x=1])
- apply (simp add:)
+ apply simp
using tendstoD [OF lim [unfolded lim_at_infinity_0] zero_less_one]
apply (rule eventually_mono)
apply (simp add: dist_norm)
@@ -969,8 +969,7 @@
qed
then show ?thesis
apply (rule_tac a = "\<lambda>k. (deriv ^^ k) f 0 / (fact k)" and n=n in that)
- apply (rule_tac A = "2/e" and B = "1/B" in Liouville_polynomial [OF holf])
- apply (simp add:)
+ apply (rule_tac A = "2/e" and B = "1/B" in Liouville_polynomial [OF holf], simp)
done
next
case False
@@ -1041,11 +1040,12 @@
have "bounded {z. (\<Sum>i\<le>n. c i * z ^ i) \<in> K}"
using polyfun_extremal [where c=c and B="B+1", OF c]
by (auto simp: bounded_pos eventually_at_infinity_pos *)
- moreover have "closed {z. (\<Sum>i\<le>n. c i * z ^ i) \<in> K}"
- apply (intro allI continuous_closed_preimage_univ continuous_intros)
+ moreover have "closed ((\<lambda>z. (\<Sum>i\<le>n. c i * z ^ i)) -` K)"
+ apply (intro allI continuous_closed_vimage continuous_intros)
using \<open>compact K\<close> compact_eq_bounded_closed by blast
ultimately show ?thesis
- using closed_Int_compact [OF \<open>closed S\<close>] compact_eq_bounded_closed by blast
+ using closed_Int_compact [OF \<open>closed S\<close>] compact_eq_bounded_closed
+ by (auto simp add: vimage_def)
qed
corollary proper_map_polyfun_univ:
@@ -1095,7 +1095,7 @@
fix e::real assume "0 < e"
with compf [of "cball 0 (inverse e)"]
show "\<exists>B. \<forall>x. B \<le> cmod x \<longrightarrow> dist ((inverse \<circ> f) x) 0 \<le> e"
- apply (simp add:)
+ apply simp
apply (clarsimp simp add: compact_eq_bounded_closed bounded_pos norm_inverse)
apply (rule_tac x="b+1" in exI)
apply (metis inverse_inverse_eq less_add_same_cancel2 less_imp_inverse_less add.commute not_le not_less_iff_gr_or_eq order_trans zero_less_one)
@@ -1134,7 +1134,7 @@
with \<open>\<delta>>0\<close> have "\<exists>\<delta>>0. \<forall>x. dist \<xi> x < \<delta> \<longrightarrow> onorm (\<lambda>v. deriv f x * v - deriv f \<xi> * v) \<le> e/2"
apply (rule_tac x="min \<delta> \<epsilon>" in exI)
apply (intro conjI allI impI Operator_Norm.onorm_le)
- apply (simp add:)
+ apply simp
apply (simp only: Rings.ring_class.left_diff_distrib [symmetric] norm_mult)
apply (rule mult_right_mono [OF \<delta>])
apply (auto simp: dist_commute Rings.ordered_semiring_class.mult_right_mono \<delta>)
--- a/src/HOL/Analysis/Connected.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Connected.thy Thu Oct 19 17:16:01 2017 +0100
@@ -395,29 +395,6 @@
by (simp add: th0 th1)
qed
-lemma connected_continuous_image:
- assumes "continuous_on s f"
- and "connected s"
- shows "connected(f ` s)"
-proof -
- {
- fix T
- assume as:
- "T \<noteq> {}"
- "T \<noteq> f ` s"
- "openin (subtopology euclidean (f ` s)) T"
- "closedin (subtopology euclidean (f ` s)) T"
- have "{x \<in> s. f x \<in> T} = {} \<or> {x \<in> s. f x \<in> T} = s"
- using assms(1)[unfolded continuous_on_open, THEN spec[where x=T]]
- using assms(1)[unfolded continuous_on_closed, THEN spec[where x=T]]
- using assms(2)[unfolded connected_clopen, THEN spec[where x="{x \<in> s. f x \<in> T}"]] as(3,4) by auto
- then have False using as(1,2)
- using as(4)[unfolded closedin_def topspace_euclidean_subtopology] by auto
- }
- then show ?thesis
- unfolding connected_clopen by auto
-qed
-
lemma connected_linear_image:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "linear f" and "connected s"
@@ -1442,13 +1419,13 @@
lemma continuous_closedin_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
- shows "continuous_on s f \<Longrightarrow> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
- using continuous_closedin_preimage[of s f "{a}"] by auto
+ shows "continuous_on S f \<Longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x = a}"
+ using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
lemma continuous_closed_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
- shows "continuous_on s f \<Longrightarrow> closed s \<Longrightarrow> closed {x \<in> s. f x = a}"
- using continuous_closed_preimage[of s f "{a}"] by auto
+ shows "continuous_on S f \<Longrightarrow> closed S \<Longrightarrow> closed {x \<in> S. f x = a}"
+ using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
lemma continuous_constant_on_closure:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -1462,17 +1439,17 @@
by auto
lemma image_closure_subset:
- assumes "continuous_on (closure s) f"
- and "closed t"
- and "(f ` s) \<subseteq> t"
- shows "f ` (closure s) \<subseteq> t"
+ assumes contf: "continuous_on (closure S) f"
+ and "closed T"
+ and "(f ` S) \<subseteq> T"
+ shows "f ` (closure S) \<subseteq> T"
proof -
- have "s \<subseteq> {x \<in> closure s. f x \<in> t}"
+ have "S \<subseteq> {x \<in> closure S. f x \<in> T}"
using assms(3) closure_subset by auto
- moreover have "closed {x \<in> closure s. f x \<in> t}"
- using continuous_closed_preimage[OF assms(1)] and assms(2) by auto
- ultimately have "closure s = {x \<in> closure s . f x \<in> t}"
- using closure_minimal[of s "{x \<in> closure s. f x \<in> t}"] by auto
+ moreover have "closed (closure S \<inter> f -` T)"
+ using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto
+ ultimately have "closure S = (closure S \<inter> f -` T)"
+ using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto
then show ?thesis by auto
qed
@@ -1967,7 +1944,7 @@
lemma bounded_uniformly_continuous_image:
fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
assumes "uniformly_continuous_on S f" "bounded S"
- shows "bounded(image f S)"
+ shows "bounded(f ` S)"
by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
subsection \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
@@ -2023,61 +2000,61 @@
subsection\<open>Quotient maps\<close>
lemma quotient_map_imp_continuous_open:
- assumes t: "f ` s \<subseteq> t"
- and ope: "\<And>u. u \<subseteq> t
- \<Longrightarrow> (openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
- openin (subtopology euclidean t) u)"
- shows "continuous_on s f"
+ assumes T: "f ` S \<subseteq> T"
+ and ope: "\<And>U. U \<subseteq> T
+ \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+ openin (subtopology euclidean T) U)"
+ shows "continuous_on S f"
proof -
- have [simp]: "{x \<in> s. f x \<in> f ` s} = s" by auto
+ have [simp]: "S \<inter> f -` f ` S = S" by auto
show ?thesis
- using ope [OF t]
+ using ope [OF T]
apply (simp add: continuous_on_open)
- by (metis (no_types, lifting) "ope" openin_imp_subset openin_trans)
+ by (meson ope openin_imp_subset openin_trans)
qed
lemma quotient_map_imp_continuous_closed:
- assumes t: "f ` s \<subseteq> t"
- and ope: "\<And>u. u \<subseteq> t
- \<Longrightarrow> (closedin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
- closedin (subtopology euclidean t) u)"
- shows "continuous_on s f"
+ assumes T: "f ` S \<subseteq> T"
+ and ope: "\<And>U. U \<subseteq> T
+ \<Longrightarrow> (closedin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+ closedin (subtopology euclidean T) U)"
+ shows "continuous_on S f"
proof -
- have [simp]: "{x \<in> s. f x \<in> f ` s} = s" by auto
+ have [simp]: "S \<inter> f -` f ` S = S" by auto
show ?thesis
- using ope [OF t]
+ using ope [OF T]
apply (simp add: continuous_on_closed)
- by (metis (no_types, lifting) "ope" closedin_imp_subset closedin_subtopology_refl closedin_trans openin_subtopology_refl openin_subtopology_self)
+ by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
qed
lemma open_map_imp_quotient_map:
- assumes contf: "continuous_on s f"
- and t: "t \<subseteq> f ` s"
- and ope: "\<And>t. openin (subtopology euclidean s) t
- \<Longrightarrow> openin (subtopology euclidean (f ` s)) (f ` t)"
- shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t} =
- openin (subtopology euclidean (f ` s)) t"
+ assumes contf: "continuous_on S f"
+ and T: "T \<subseteq> f ` S"
+ and ope: "\<And>T. openin (subtopology euclidean S) T
+ \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` T)"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` T) =
+ openin (subtopology euclidean (f ` S)) T"
proof -
- have "t = image f {x. x \<in> s \<and> f x \<in> t}"
- using t by blast
+ have "T = f ` (S \<inter> f -` T)"
+ using T by blast
then show ?thesis
- using "ope" contf continuous_on_open by fastforce
+ using "ope" contf continuous_on_open by metis
qed
lemma closed_map_imp_quotient_map:
- assumes contf: "continuous_on s f"
- and t: "t \<subseteq> f ` s"
- and ope: "\<And>t. closedin (subtopology euclidean s) t
- \<Longrightarrow> closedin (subtopology euclidean (f ` s)) (f ` t)"
- shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t} \<longleftrightarrow>
- openin (subtopology euclidean (f ` s)) t"
+ assumes contf: "continuous_on S f"
+ and T: "T \<subseteq> f ` S"
+ and ope: "\<And>T. closedin (subtopology euclidean S) T
+ \<Longrightarrow> closedin (subtopology euclidean (f ` S)) (f ` T)"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
+ openin (subtopology euclidean (f ` S)) T"
(is "?lhs = ?rhs")
proof
assume ?lhs
- then have *: "closedin (subtopology euclidean s) (s - {x \<in> s. f x \<in> t})"
+ then have *: "closedin (subtopology euclidean S) (S - (S \<inter> f -` T))"
using closedin_diff by fastforce
- have [simp]: "(f ` s - f ` (s - {x \<in> s. f x \<in> t})) = t"
- using t by blast
+ have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T"
+ using T by blast
show ?rhs
using ope [OF *, unfolded closedin_def] by auto
next
@@ -2087,51 +2064,50 @@
qed
lemma continuous_right_inverse_imp_quotient_map:
- assumes contf: "continuous_on s f" and imf: "f ` s \<subseteq> t"
- and contg: "continuous_on t g" and img: "g ` t \<subseteq> s"
- and fg [simp]: "\<And>y. y \<in> t \<Longrightarrow> f(g y) = y"
- and u: "u \<subseteq> t"
- shows "openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
- openin (subtopology euclidean t) u"
+ assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
+ and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
+ and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
+ and U: "U \<subseteq> T"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+ openin (subtopology euclidean T) U"
(is "?lhs = ?rhs")
proof -
- have f: "\<And>z. openin (subtopology euclidean (f ` s)) z \<Longrightarrow>
- openin (subtopology euclidean s) {x \<in> s. f x \<in> z}"
- and g: "\<And>z. openin (subtopology euclidean (g ` t)) z \<Longrightarrow>
- openin (subtopology euclidean t) {x \<in> t. g x \<in> z}"
+ have f: "\<And>Z. openin (subtopology euclidean (f ` S)) Z \<Longrightarrow>
+ openin (subtopology euclidean S) (S \<inter> f -` Z)"
+ and g: "\<And>Z. openin (subtopology euclidean (g ` T)) Z \<Longrightarrow>
+ openin (subtopology euclidean T) (T \<inter> g -` Z)"
using contf contg by (auto simp: continuous_on_open)
show ?thesis
proof
- have "{x \<in> t. g x \<in> g ` t \<and> g x \<in> s \<and> f (g x) \<in> u} = {x \<in> t. f (g x) \<in> u}"
+ have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}"
using imf img by blast
- also have "... = u"
- using u by auto
- finally have [simp]: "{x \<in> t. g x \<in> g ` t \<and> g x \<in> s \<and> f (g x) \<in> u} = u" .
+ also have "... = U"
+ using U by auto
+ finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
assume ?lhs
- then have *: "openin (subtopology euclidean (g ` t)) (g ` t \<inter> {x \<in> s. f x \<in> u})"
+ then have *: "openin (subtopology euclidean (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
show ?rhs
- using g [OF *] by simp
+ using g [OF *] eq by auto
next
assume rhs: ?rhs
show ?lhs
- apply (rule f)
- by (metis fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
+ by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
qed
qed
lemma continuous_left_inverse_imp_quotient_map:
- assumes "continuous_on s f"
- and "continuous_on (f ` s) g"
- and "\<And>x. x \<in> s \<Longrightarrow> g(f x) = x"
- and "u \<subseteq> f ` s"
- shows "openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
- openin (subtopology euclidean (f ` s)) u"
+ assumes "continuous_on S f"
+ and "continuous_on (f ` S) g"
+ and "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+ and "U \<subseteq> f ` S"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+ openin (subtopology euclidean (f ` S)) U"
apply (rule continuous_right_inverse_imp_quotient_map)
-using assms
-apply force+
+using assms apply force+
done
+
text \<open>Proving a function is constant by proving that a level set is open\<close>
lemma continuous_levelset_openin_cases:
@@ -3234,17 +3210,19 @@
and "\<And>t. \<lbrakk>t \<in> s; h t = a\<rbrakk> \<Longrightarrow> f t = g t"
shows "continuous_on s (\<lambda>t. if h t \<le> a then f(t) else g(t))"
proof -
- have s: "s = {t \<in> s. h t \<in> atMost a} \<union> {t \<in> s. h t \<in> atLeast a}"
+ have s: "s = (s \<inter> h -` atMost a) \<union> (s \<inter> h -` atLeast a)"
by force
- have 1: "closedin (subtopology euclidean s) {t \<in> s. h t \<in> atMost a}"
+ have 1: "closedin (subtopology euclidean s) (s \<inter> h -` atMost a)"
by (rule continuous_closedin_preimage [OF h closed_atMost])
- have 2: "closedin (subtopology euclidean s) {t \<in> s. h t \<in> atLeast a}"
+ have 2: "closedin (subtopology euclidean s) (s \<inter> h -` atLeast a)"
by (rule continuous_closedin_preimage [OF h closed_atLeast])
+ have eq: "s \<inter> h -` {..a} = {t \<in> s. h t \<le> a}" "s \<inter> h -` {a..} = {t \<in> s. a \<le> h t}"
+ by auto
show ?thesis
apply (rule continuous_on_subset [of s, OF _ order_refl])
apply (subst s)
apply (rule continuous_on_cases_local)
- using 1 2 s assms apply auto
+ using 1 2 s assms apply (auto simp: eq)
done
qed
@@ -3761,7 +3739,7 @@
proof -
from imf injf have gTS: "g ` T = S"
by force
- from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
+ from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U
by force
show ?thesis
by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo)
@@ -3776,7 +3754,7 @@
proof -
from imf injf have gTS: "g ` T = S"
by force
- from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
+ from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U
by force
show ?thesis
by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo)
@@ -3813,7 +3791,7 @@
and oo: "openin (subtopology euclidean S) U"
shows "openin (subtopology euclidean T) (f ` U)"
proof -
- from hom oo have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
+ from hom oo have [simp]: "f ` U = T \<inter> g -` U"
using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
from hom have "continuous_on T g"
unfolding homeomorphism_def by blast
@@ -3828,7 +3806,7 @@
and oo: "closedin (subtopology euclidean S) U"
shows "closedin (subtopology euclidean T) (f ` U)"
proof -
- from hom oo have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
+ from hom oo have [simp]: "f ` U = T \<inter> g -` U"
using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
from hom have "continuous_on T g"
unfolding homeomorphism_def by blast
@@ -4750,17 +4728,263 @@
lemma continuous_imp_closed_map:
fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
assumes "closedin (subtopology euclidean S) U"
- "continuous_on S f" "image f S = T" "compact S"
- shows "closedin (subtopology euclidean T) (image f U)"
+ "continuous_on S f" "f ` S = T" "compact S"
+ shows "closedin (subtopology euclidean T) (f ` U)"
by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
lemma continuous_imp_quotient_map:
fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
- assumes "continuous_on S f" "image f S = T" "compact S" "U \<subseteq> T"
- shows "openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> U} \<longleftrightarrow>
+ assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
openin (subtopology euclidean T) U"
- by (metis (no_types, lifting) Collect_cong assms closed_map_imp_quotient_map continuous_imp_closed_map)
-
+ by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
+
+
+lemma open_map_restrict:
+ assumes opeU: "openin (subtopology euclidean (S \<inter> f -` T')) U"
+ and oo: "\<And>U. openin (subtopology euclidean S) U \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
+ and "T' \<subseteq> T"
+ shows "openin (subtopology euclidean T') (f ` U)"
+proof -
+ obtain V where "open V" "U = S \<inter> f -` T' \<inter> V"
+ using opeU by (auto simp: openin_open)
+ with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
+ by (fastforce simp add: openin_open)
+qed
+
+lemma closed_map_restrict:
+ assumes cloU: "closedin (subtopology euclidean (S \<inter> f -` T')) U"
+ and cc: "\<And>U. closedin (subtopology euclidean S) U \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
+ and "T' \<subseteq> T"
+ shows "closedin (subtopology euclidean T') (f ` U)"
+proof -
+ obtain V where "closed V" "U = S \<inter> f -` T' \<inter> V"
+ using cloU by (auto simp: closedin_closed)
+ with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
+ by (fastforce simp add: closedin_closed)
+qed
+
+lemma connected_monotone_quotient_preimage:
+ assumes "connected T"
+ and contf: "continuous_on S f" and fim: "f ` S = T"
+ and opT: "\<And>U. U \<subseteq> T
+ \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+ openin (subtopology euclidean T) U"
+ and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
+ shows "connected S"
+proof (rule connectedI)
+ fix U V
+ assume "open U" and "open V" and "U \<inter> S \<noteq> {}" and "V \<inter> S \<noteq> {}"
+ and "U \<inter> V \<inter> S = {}" and "S \<subseteq> U \<union> V"
+ moreover
+ have disjoint: "f ` (S \<inter> U) \<inter> f ` (S \<inter> V) = {}"
+ proof -
+ have False if "y \<in> f ` (S \<inter> U) \<inter> f ` (S \<inter> V)" for y
+ proof -
+ have "y \<in> T"
+ using fim that by blast
+ show ?thesis
+ using connectedD [OF connT [OF \<open>y \<in> T\<close>] \<open>open U\<close> \<open>open V\<close>]
+ \<open>S \<subseteq> U \<union> V\<close> \<open>U \<inter> V \<inter> S = {}\<close> that by fastforce
+ qed
+ then show ?thesis by blast
+ qed
+ ultimately have UU: "(S \<inter> f -` f ` (S \<inter> U)) = S \<inter> U" and VV: "(S \<inter> f -` f ` (S \<inter> V)) = S \<inter> V"
+ by auto
+ have opeU: "openin (subtopology euclidean T) (f ` (S \<inter> U))"
+ by (metis UU \<open>open U\<close> fim image_Int_subset le_inf_iff opT openin_open_Int)
+ have opeV: "openin (subtopology euclidean T) (f ` (S \<inter> V))"
+ by (metis opT fim VV \<open>open V\<close> openin_open_Int image_Int_subset inf.bounded_iff)
+ have "T \<subseteq> f ` (S \<inter> U) \<union> f ` (S \<inter> V)"
+ using \<open>S \<subseteq> U \<union> V\<close> fim by auto
+ then show False
+ using \<open>connected T\<close> disjoint opeU opeV \<open>U \<inter> S \<noteq> {}\<close> \<open>V \<inter> S \<noteq> {}\<close>
+ by (auto simp: connected_openin)
+qed
+
+lemma connected_open_monotone_preimage:
+ assumes contf: "continuous_on S f" and fim: "f ` S = T"
+ and ST: "\<And>C. openin (subtopology euclidean S) C \<Longrightarrow> openin (subtopology euclidean T) (f ` C)"
+ and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
+ and "connected C" "C \<subseteq> T"
+ shows "connected (S \<inter> f -` C)"
+proof -
+ have contf': "continuous_on (S \<inter> f -` C) f"
+ by (meson contf continuous_on_subset inf_le1)
+ have eqC: "f ` (S \<inter> f -` C) = C"
+ using \<open>C \<subseteq> T\<close> fim by blast
+ show ?thesis
+ proof (rule connected_monotone_quotient_preimage [OF \<open>connected C\<close> contf' eqC])
+ show "connected (S \<inter> f -` C \<inter> f -` {y})" if "y \<in> C" for y
+ proof -
+ have "S \<inter> f -` C \<inter> f -` {y} = S \<inter> f -` {y}"
+ using that by blast
+ moreover have "connected (S \<inter> f -` {y})"
+ using \<open>C \<subseteq> T\<close> connT that by blast
+ ultimately show ?thesis
+ by metis
+ qed
+ have "\<And>U. openin (subtopology euclidean (S \<inter> f -` C)) U
+ \<Longrightarrow> openin (subtopology euclidean C) (f ` U)"
+ using open_map_restrict [OF _ ST \<open>C \<subseteq> T\<close>] by metis
+ then show "\<And>D. D \<subseteq> C
+ \<Longrightarrow> openin (subtopology euclidean (S \<inter> f -` C)) (S \<inter> f -` C \<inter> f -` D) =
+ openin (subtopology euclidean C) D"
+ using open_map_imp_quotient_map [of "(S \<inter> f -` C)" f] contf' by (simp add: eqC)
+ qed
+qed
+
+
+lemma connected_closed_monotone_preimage:
+ assumes contf: "continuous_on S f" and fim: "f ` S = T"
+ and ST: "\<And>C. closedin (subtopology euclidean S) C \<Longrightarrow> closedin (subtopology euclidean T) (f ` C)"
+ and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
+ and "connected C" "C \<subseteq> T"
+ shows "connected (S \<inter> f -` C)"
+proof -
+ have contf': "continuous_on (S \<inter> f -` C) f"
+ by (meson contf continuous_on_subset inf_le1)
+ have eqC: "f ` (S \<inter> f -` C) = C"
+ using \<open>C \<subseteq> T\<close> fim by blast
+ show ?thesis
+ proof (rule connected_monotone_quotient_preimage [OF \<open>connected C\<close> contf' eqC])
+ show "connected (S \<inter> f -` C \<inter> f -` {y})" if "y \<in> C" for y
+ proof -
+ have "S \<inter> f -` C \<inter> f -` {y} = S \<inter> f -` {y}"
+ using that by blast
+ moreover have "connected (S \<inter> f -` {y})"
+ using \<open>C \<subseteq> T\<close> connT that by blast
+ ultimately show ?thesis
+ by metis
+ qed
+ have "\<And>U. closedin (subtopology euclidean (S \<inter> f -` C)) U
+ \<Longrightarrow> closedin (subtopology euclidean C) (f ` U)"
+ using closed_map_restrict [OF _ ST \<open>C \<subseteq> T\<close>] by metis
+ then show "\<And>D. D \<subseteq> C
+ \<Longrightarrow> openin (subtopology euclidean (S \<inter> f -` C)) (S \<inter> f -` C \<inter> f -` D) =
+ openin (subtopology euclidean C) D"
+ using closed_map_imp_quotient_map [of "(S \<inter> f -` C)" f] contf' by (simp add: eqC)
+ qed
+qed
+
+
+
+subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4).\<close>
+
+
+lemma connected_Un_clopen_in_complement:
+ fixes S U :: "'a::metric_space set"
+ assumes "connected S" "connected U" "S \<subseteq> U"
+ and opeT: "openin (subtopology euclidean (U - S)) T"
+ and cloT: "closedin (subtopology euclidean (U - S)) T"
+ shows "connected (S \<union> T)"
+proof -
+ have *: "\<lbrakk>\<And>x y. P x y \<longleftrightarrow> P y x; \<And>x y. P x y \<Longrightarrow> S \<subseteq> x \<or> S \<subseteq> y;
+ \<And>x y. \<lbrakk>P x y; S \<subseteq> x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> ~(\<exists>x y. (P x y))" for P
+ by metis
+ show ?thesis
+ unfolding connected_closedin_eq
+ proof (rule *)
+ fix H1 H2
+ assume H: "closedin (subtopology euclidean (S \<union> T)) H1 \<and>
+ closedin (subtopology euclidean (S \<union> T)) H2 \<and>
+ H1 \<union> H2 = S \<union> T \<and> H1 \<inter> H2 = {} \<and> H1 \<noteq> {} \<and> H2 \<noteq> {}"
+ then have clo: "closedin (subtopology euclidean S) (S \<inter> H1)"
+ "closedin (subtopology euclidean S) (S \<inter> H2)"
+ by (metis Un_upper1 closedin_closed_subset inf_commute)+
+ have Seq: "S \<inter> (H1 \<union> H2) = S"
+ by (simp add: H)
+ have "S \<inter> ((S \<union> T) \<inter> H1) \<union> S \<inter> ((S \<union> T) \<inter> H2) = S"
+ using Seq by auto
+ moreover have "H1 \<inter> (S \<inter> ((S \<union> T) \<inter> H2)) = {}"
+ using H by blast
+ ultimately have "S \<inter> H1 = {} \<or> S \<inter> H2 = {}"
+ by (metis (no_types) H Int_assoc \<open>S \<inter> (H1 \<union> H2) = S\<close> \<open>connected S\<close>
+ clo Seq connected_closedin inf_bot_right inf_le1)
+ then show "S \<subseteq> H1 \<or> S \<subseteq> H2"
+ using H \<open>connected S\<close> unfolding connected_closedin by blast
+ next
+ fix H1 H2
+ assume H: "closedin (subtopology euclidean (S \<union> T)) H1 \<and>
+ closedin (subtopology euclidean (S \<union> T)) H2 \<and>
+ H1 \<union> H2 = S \<union> T \<and> H1 \<inter> H2 = {} \<and> H1 \<noteq> {} \<and> H2 \<noteq> {}"
+ and "S \<subseteq> H1"
+ then have H2T: "H2 \<subseteq> T"
+ by auto
+ have "T \<subseteq> U"
+ using Diff_iff opeT openin_imp_subset by auto
+ with \<open>S \<subseteq> U\<close> have Ueq: "U = (U - S) \<union> (S \<union> T)"
+ by auto
+ have "openin (subtopology euclidean ((U - S) \<union> (S \<union> T))) H2"
+ proof (rule openin_subtopology_Un)
+ show "openin (subtopology euclidean (S \<union> T)) H2"
+ using \<open>H2 \<subseteq> T\<close> apply (auto simp: openin_closedin_eq)
+ by (metis Diff_Diff_Int Diff_disjoint Diff_partition Diff_subset H Int_absorb1 Un_Diff)
+ then show "openin (subtopology euclidean (U - S)) H2"
+ by (meson H2T Un_upper2 opeT openin_subset_trans openin_trans)
+ qed
+ moreover have "closedin (subtopology euclidean ((U - S) \<union> (S \<union> T))) H2"
+ proof (rule closedin_subtopology_Un)
+ show "closedin (subtopology euclidean (U - S)) H2"
+ using H H2T cloT closedin_subset_trans
+ by (blast intro: closedin_subtopology_Un closedin_trans)
+ qed (simp add: H)
+ ultimately
+ have H2: "H2 = {} \<or> H2 = U"
+ using Ueq \<open>connected U\<close> unfolding connected_clopen by metis
+ then have "H2 \<subseteq> S"
+ by (metis Diff_partition H Un_Diff_cancel Un_subset_iff \<open>H2 \<subseteq> T\<close> assms(3) inf.orderE opeT openin_imp_subset)
+ moreover have "T \<subseteq> H2 - S"
+ by (metis (no_types) H2 H opeT openin_closedin_eq topspace_euclidean_subtopology)
+ ultimately show False
+ using H \<open>S \<subseteq> H1\<close> by blast
+ qed blast
+qed
+
+
+proposition component_complement_connected:
+ fixes S :: "'a::metric_space set"
+ assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
+ shows "connected(U - C)"
+ using \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
+proof clarify
+ fix H3 H4
+ assume clo3: "closedin (subtopology euclidean (U - C)) H3"
+ and clo4: "closedin (subtopology euclidean (U - C)) H4"
+ and "H3 \<union> H4 = U - C" and "H3 \<inter> H4 = {}" and "H3 \<noteq> {}" and "H4 \<noteq> {}"
+ and * [rule_format]:
+ "\<forall>H1 H2. \<not> closedin (subtopology euclidean S) H1 \<or>
+ \<not> closedin (subtopology euclidean S) H2 \<or>
+ H1 \<union> H2 \<noteq> S \<or> H1 \<inter> H2 \<noteq> {} \<or> \<not> H1 \<noteq> {} \<or> \<not> H2 \<noteq> {}"
+ then have "H3 \<subseteq> U-C" and ope3: "openin (subtopology euclidean (U - C)) (U - C - H3)"
+ and "H4 \<subseteq> U-C" and ope4: "openin (subtopology euclidean (U - C)) (U - C - H4)"
+ by (auto simp: closedin_def)
+ have "C \<noteq> {}" "C \<subseteq> U-S" "connected C"
+ using C in_components_nonempty in_components_subset in_components_maximal by blast+
+ have cCH3: "connected (C \<union> H3)"
+ proof (rule connected_Un_clopen_in_complement [OF \<open>connected C\<close> \<open>connected U\<close> _ _ clo3])
+ show "openin (subtopology euclidean (U - C)) H3"
+ apply (simp add: openin_closedin_eq \<open>H3 \<subseteq> U - C\<close>)
+ apply (simp add: closedin_subtopology)
+ by (metis Diff_cancel Diff_triv Un_Diff clo4 \<open>H3 \<inter> H4 = {}\<close> \<open>H3 \<union> H4 = U - C\<close> closedin_closed inf_commute sup_bot.left_neutral)
+ qed (use clo3 \<open>C \<subseteq> U - S\<close> in auto)
+ have cCH4: "connected (C \<union> H4)"
+ proof (rule connected_Un_clopen_in_complement [OF \<open>connected C\<close> \<open>connected U\<close> _ _ clo4])
+ show "openin (subtopology euclidean (U - C)) H4"
+ apply (simp add: openin_closedin_eq \<open>H4 \<subseteq> U - C\<close>)
+ apply (simp add: closedin_subtopology)
+ by (metis Diff_cancel Int_commute Un_Diff Un_Diff_Int \<open>H3 \<inter> H4 = {}\<close> \<open>H3 \<union> H4 = U - C\<close> clo3 closedin_closed)
+ qed (use clo4 \<open>C \<subseteq> U - S\<close> in auto)
+ have "closedin (subtopology euclidean S) (S \<inter> H3)" "closedin (subtopology euclidean S) (S \<inter> H4)"
+ using clo3 clo4 \<open>S \<subseteq> U\<close> \<open>C \<subseteq> U - S\<close> by (auto simp: closedin_closed)
+ moreover have "S \<inter> H3 \<noteq> {}"
+ using components_maximal [OF C cCH3] \<open>C \<noteq> {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H3 \<noteq> {}\<close> \<open>H3 \<subseteq> U - C\<close> by auto
+ moreover have "S \<inter> H4 \<noteq> {}"
+ using components_maximal [OF C cCH4] \<open>C \<noteq> {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H4 \<noteq> {}\<close> \<open>H4 \<subseteq> U - C\<close> by auto
+ ultimately show False
+ using * [of "S \<inter> H3" "S \<inter> H4"] \<open>H3 \<inter> H4 = {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H3 \<union> H4 = U - C\<close> \<open>S \<subseteq> U\<close>
+ by auto
+qed
subsection\<open> Finite intersection property\<close>
@@ -4952,15 +5176,12 @@
assume "open U"
have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
using clo openin_imp_subset by blast
- have *: "{x \<in> S. g x \<in> U} = \<Union>{{x. x \<in> (T i) \<and> (f i x) \<in> U} |i. i \<in> I}"
- apply (auto simp: dest: S)
- apply (metis (no_types, lifting) g mem_Collect_eq)
- using clo f g openin_imp_subset by fastforce
- show "openin (subtopology euclidean S) {x \<in> S. g x \<in> U}"
+ have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
+ using S f g by fastforce
+ show "openin (subtopology euclidean S) (S \<inter> g -` U)"
apply (subst *)
apply (rule openin_Union, clarify)
- apply (metis (full_types) \<open>open U\<close> cont clo openin_trans continuous_openin_preimage_gen)
- done
+ using \<open>open U\<close> clo cont continuous_openin_preimage_gen openin_trans by blast
qed
lemma pasting_lemma_exists:
@@ -4996,13 +5217,11 @@
proof (clarsimp simp: continuous_closedin_preimage_eq)
fix U :: "'b set"
assume "closed U"
- have *: "{x \<in> S. g x \<in> U} = \<Union>{{x. x \<in> (T i) \<and> (f i x) \<in> U} |i. i \<in> I}"
- apply auto
- apply (metis (no_types, lifting) g mem_Collect_eq)
- using clo closedin_closed apply blast
- apply (metis Int_iff f g clo closedin_limpt inf.absorb_iff2)
- done
- show "closedin (subtopology euclidean S) {x \<in> S. g x \<in> U}"
+ have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
+ using clo closedin_imp_subset by blast
+ have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
+ using S f g by fastforce
+ show "closedin (subtopology euclidean S) (S \<inter> g -` U)"
apply (subst *)
apply (rule closedin_Union)
using \<open>finite I\<close> apply simp
@@ -5119,9 +5338,10 @@
and conf: "continuous_on S f"
and fim: "f ` S \<subseteq> t"
and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
- shows "\<exists>a. \<forall>x \<in> S. f x = a"
+ shows "f constant_on S"
proof (cases "S = {}")
- case True then show ?thesis by force
+ case True then show ?thesis
+ by (simp add: constant_on_def)
next
case False
{ fix x assume "x \<in> S"
@@ -5129,7 +5349,7 @@
by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI S cct)
}
with False show ?thesis
- by blast
+ unfolding constant_on_def by blast
qed
lemma discrete_subset_disconnected:
@@ -5195,7 +5415,7 @@
text\<open>This proof requires the existence of two separate values of the range type.\<close>
lemma finite_range_constant_imp_connected:
assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
- \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> S. f x = a"
+ \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> f constant_on S"
shows "connected S"
proof -
{ fix t u
@@ -5212,7 +5432,7 @@
by (rule finite_subset [of _ "{0,1}"]) auto
have "t = {} \<or> u = {}"
using assms [OF conif fi] tus [symmetric]
- by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
+ by (auto simp: Ball_def constant_on_def) (metis IntI empty_iff one_neq_zero tue)
}
then show ?thesis
by (simp add: connected_closedin_eq)
@@ -5222,18 +5442,18 @@
"(connected S \<longleftrightarrow>
(\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
\<forall>t. continuous_on S f \<and> f ` S \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
- \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis1)
+ \<longrightarrow> f constant_on S))" (is ?thesis1)
and continuous_discrete_range_constant_eq:
"(connected S \<longleftrightarrow>
(\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
continuous_on S f \<and>
(\<forall>x \<in> S. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> S \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
- \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis2)
+ \<longrightarrow> f constant_on S))" (is ?thesis2)
and continuous_finite_range_constant_eq:
"(connected S \<longleftrightarrow>
(\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
continuous_on S f \<and> finite (f ` S)
- \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis3)
+ \<longrightarrow> f constant_on S))" (is ?thesis3)
proof -
have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
\<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
@@ -5255,18 +5475,16 @@
assumes S: "connected S"
and "continuous_on S f"
and "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
- obtains a where "\<And>x. x \<in> S \<Longrightarrow> f x = a"
- using continuous_discrete_range_constant_eq [THEN iffD1, OF S] assms
- by blast
+ shows "f constant_on S"
+ using continuous_discrete_range_constant_eq [THEN iffD1, OF S] assms by blast
lemma continuous_finite_range_constant:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
assumes "connected S"
and "continuous_on S f"
and "finite (f ` S)"
- obtains a where "\<And>x. x \<in> S \<Longrightarrow> f x = a"
- using assms continuous_finite_range_constant_eq
- by blast
+ shows "f constant_on S"
+ using assms continuous_finite_range_constant_eq by blast
--- a/src/HOL/Analysis/Continuous_Extension.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Continuous_Extension.thy Thu Oct 19 17:16:01 2017 +0100
@@ -281,10 +281,7 @@
"\<And>x. f x \<in> closed_segment a b"
"\<And>x. f x = a \<longleftrightarrow> x \<in> S"
"\<And>x. f x = b \<longleftrightarrow> x \<in> T"
-apply (rule Urysohn_local_strong [of UNIV S T])
-using assms
-apply (auto simp: closed_closedin)
-done
+using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
proposition Urysohn:
assumes US: "closed S"
@@ -295,10 +292,7 @@
"\<And>x. f x \<in> closed_segment a b"
"\<And>x. x \<in> S \<Longrightarrow> f x = a"
"\<And>x. x \<in> T \<Longrightarrow> f x = b"
-apply (rule Urysohn_local [of UNIV S T a b])
-using assms
-apply (auto simp: closed_closedin)
-done
+using assms by (auto intro: Urysohn_local [of UNIV S T a b])
subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close>
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Oct 19 17:16:01 2017 +0100
@@ -1271,15 +1271,17 @@
using g by (simp add: image_comp)
have cgf: "closed (g ` f ` S)"
by (simp add: \<open>g \<circ> f = id\<close> S image_comp)
- have [simp]: "{x \<in> range f. g x \<in> S} = f ` S"
- using g by (simp add: o_def id_def image_def) metis
+ have [simp]: "(range f \<inter> g -` S) = f ` S"
+ using g unfolding o_def id_def image_def by auto metis+
show ?thesis
- apply (rule closedin_closed_trans [of "range f"])
- apply (rule continuous_closedin_preimage [OF confg cgf, simplified])
- apply (rule closed_injective_image_subspace)
- using f
- apply (auto simp: linear_linear linear_injective_0)
- done
+ proof (rule closedin_closed_trans [of "range f"])
+ show "closedin (subtopology euclidean (range f)) (f ` S)"
+ using continuous_closedin_preimage [OF confg cgf] by simp
+ show "closed (range f)"
+ apply (rule closed_injective_image_subspace)
+ using f apply (auto simp: linear_linear linear_injective_0)
+ done
+ qed
qed
lemma closed_injective_linear_image_eq:
@@ -2374,16 +2376,13 @@
by(simp add: convex_connected)
proposition clopen:
- fixes s :: "'a :: real_normed_vector set"
- shows "closed s \<and> open s \<longleftrightarrow> s = {} \<or> s = UNIV"
-apply (rule iffI)
- apply (rule connected_UNIV [unfolded connected_clopen, rule_format])
- apply (force simp add: closed_closedin, force)
-done
+ fixes S :: "'a :: real_normed_vector set"
+ shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV"
+ by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format])
corollary compact_open:
- fixes s :: "'a :: euclidean_space set"
- shows "compact s \<and> open s \<longleftrightarrow> s = {}"
+ fixes S :: "'a :: euclidean_space set"
+ shows "compact S \<and> open S \<longleftrightarrow> S = {}"
by (auto simp: compact_eq_bounded_closed clopen)
corollary finite_imp_not_open:
--- a/src/HOL/Analysis/Further_Topology.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Thu Oct 19 17:16:01 2017 +0100
@@ -2318,9 +2318,9 @@
proof (clarsimp simp add: continuous_openin_preimage_eq)
fix T :: "'a set"
assume "open T"
- have eq: "{x. x \<in> f ` S \<and> g x \<in> T} = f ` (S \<inter> T)"
+ have eq: "f ` S \<inter> g -` T = f ` (S \<inter> T)"
by (auto simp: gf)
- show "openin (subtopology euclidean (f ` S)) {x \<in> f ` S. g x \<in> T}"
+ show "openin (subtopology euclidean (f ` S)) (f ` S \<inter> g -` T)"
apply (subst eq)
apply (rule open_openin_trans)
apply (rule invariance_of_domain_gen)
@@ -3173,7 +3173,7 @@
have zn2: "(\<lambda>z::complex. z^n) ` (- {0}) = - {0}"
using assms by (auto simp: image_def elim: exists_complex_root_nonzero [where n = n])
have zn3: "\<exists>T. z^n \<in> T \<and> open T \<and> 0 \<notin> T \<and>
- (\<exists>v. \<Union>v = {x. x \<noteq> 0 \<and> x^n \<in> T} \<and>
+ (\<exists>v. \<Union>v = -{0} \<inter> (\<lambda>z. z ^ n) -` T \<and>
(\<forall>u\<in>v. open u \<and> 0 \<notin> u) \<and>
pairwise disjnt v \<and>
(\<forall>u\<in>v. Ex (homeomorphism u T (\<lambda>z. z^n))))"
@@ -3216,8 +3216,6 @@
by (intro continuous_intros)
have noncon: "\<not> (\<lambda>w::complex. w^n) constant_on UNIV"
by (metis UNIV_I assms constant_on_def power_one zero_neq_one zero_power)
- have open_imball: "open ((\<lambda>w. w^n) ` ball z d)"
- by (rule invariance_of_domain [OF cont open_ball inj])
have im_eq: "(\<lambda>w. w^n) ` ball z' d = (\<lambda>w. w^n) ` ball z d"
if z': "z'^n = z^n" for z'
proof -
@@ -3262,6 +3260,7 @@
qed
then show ?thesis by blast
qed
+
have ex_ball: "\<exists>B. (\<exists>z'. B = ball z' d \<and> z'^n = z^n) \<and> x \<in> B"
if "x \<noteq> 0" and eq: "x^n = w^n" and dzw: "dist z w < d" for x w
proof -
@@ -3286,50 +3285,63 @@
apply (simp add: dist_norm)
done
qed
- have ball1: "\<Union>{ball z' d |z'. z'^n = z^n} = {x. x \<noteq> 0 \<and> x^n \<in> (\<lambda>w. w^n) ` ball z d}"
- apply (rule equalityI)
- prefer 2 apply (force simp: ex_ball, clarsimp)
- apply (subst im_eq [symmetric], assumption)
- using assms
- apply (force simp: dist_norm d_def min_mult_distrib_right dest: power_eq_imp_eq_norm)
- done
- have ball2: "pairwise disjnt {ball z' d |z'. z'^n = z^n}"
- proof (clarsimp simp add: pairwise_def disjnt_iff)
- fix \<xi> \<zeta> x
- assume "\<xi>^n = z^n" "\<zeta>^n = z^n" "ball \<xi> d \<noteq> ball \<zeta> d"
- and "dist \<xi> x < d" "dist \<zeta> x < d"
- then have "dist \<xi> \<zeta> < d+d"
- using dist_triangle_less_add by blast
- then have "cmod (\<xi> - \<zeta>) < 2*d"
- by (simp add: dist_norm)
- also have "... \<le> e * cmod z"
- using mult_right_mono \<open>0 < e\<close> that by (auto simp: d_def)
- finally have "cmod (\<xi> - \<zeta>) < e * cmod z" .
- with e have "\<xi> = \<zeta>"
- by (metis \<open>\<xi>^n = z^n\<close> \<open>\<zeta>^n = z^n\<close> assms power_eq_imp_eq_norm)
- then show "False"
- using \<open>ball \<xi> d \<noteq> ball \<zeta> d\<close> by blast
+
+ show ?thesis
+ proof (rule exI, intro conjI)
+ show "z ^ n \<in> (\<lambda>w. w ^ n) ` ball z d"
+ using \<open>d > 0\<close> by simp
+ show "open ((\<lambda>w. w ^ n) ` ball z d)"
+ by (rule invariance_of_domain [OF cont open_ball inj])
+ show "0 \<notin> (\<lambda>w. w ^ n) ` ball z d"
+ using \<open>z \<noteq> 0\<close> assms by (force simp: d_def)
+ show "\<exists>v. \<Union>v = - {0} \<inter> (\<lambda>z. z ^ n) -` (\<lambda>w. w ^ n) ` ball z d \<and>
+ (\<forall>u\<in>v. open u \<and> 0 \<notin> u) \<and>
+ disjoint v \<and>
+ (\<forall>u\<in>v. Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n)))"
+ proof (rule exI, intro ballI conjI)
+ show "\<Union>{ball z' d |z'. z'^n = z^n} = - {0} \<inter> (\<lambda>z. z ^ n) -` (\<lambda>w. w ^ n) ` ball z d" (is "?l = ?r")
+ proof
+ show "?l \<subseteq> ?r"
+ apply auto
+ apply (simp add: assms d_def power_eq_imp_eq_norm that)
+ by (metis im_eq image_eqI mem_ball)
+ show "?r \<subseteq> ?l"
+ by auto (meson ex_ball)
+ qed
+ show "\<And>u. u \<in> {ball z' d |z'. z' ^ n = z ^ n} \<Longrightarrow> 0 \<notin> u"
+ by (force simp add: assms d_def power_eq_imp_eq_norm that)
+
+ show "disjoint {ball z' d |z'. z' ^ n = z ^ n}"
+ proof (clarsimp simp add: pairwise_def disjnt_iff)
+ fix \<xi> \<zeta> x
+ assume "\<xi>^n = z^n" "\<zeta>^n = z^n" "ball \<xi> d \<noteq> ball \<zeta> d"
+ and "dist \<xi> x < d" "dist \<zeta> x < d"
+ then have "dist \<xi> \<zeta> < d+d"
+ using dist_triangle_less_add by blast
+ then have "cmod (\<xi> - \<zeta>) < 2*d"
+ by (simp add: dist_norm)
+ also have "... \<le> e * cmod z"
+ using mult_right_mono \<open>0 < e\<close> that by (auto simp: d_def)
+ finally have "cmod (\<xi> - \<zeta>) < e * cmod z" .
+ with e have "\<xi> = \<zeta>"
+ by (metis \<open>\<xi>^n = z^n\<close> \<open>\<zeta>^n = z^n\<close> assms power_eq_imp_eq_norm)
+ then show "False"
+ using \<open>ball \<xi> d \<noteq> ball \<zeta> d\<close> by blast
+ qed
+ show "Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n))"
+ if "u \<in> {ball z' d |z'. z' ^ n = z ^ n}" for u
+ proof (rule invariance_of_domain_homeomorphism [of "u" "\<lambda>z. z^n"])
+ show "open u"
+ using that by auto
+ show "continuous_on u (\<lambda>z. z ^ n)"
+ by (intro continuous_intros)
+ show "inj_on (\<lambda>z. z ^ n) u"
+ using that by (auto simp: iff_x_eq_y inj_on_def)
+ show "\<And>g. homeomorphism u ((\<lambda>z. z ^ n) ` u) (\<lambda>z. z ^ n) g \<Longrightarrow> Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n))"
+ using im_eq that by clarify metis
+ qed auto
+ qed auto
qed
- have ball3: "Ex (homeomorphism (ball z' d) ((\<lambda>w. w^n) ` ball z d) (\<lambda>z. z^n))"
- if zeq: "z'^n = z^n" for z'
- proof -
- have inj: "inj_on (\<lambda>z. z ^ n) (ball z' d)"
- by (meson iff_x_eq_y inj_onI zeq)
- show ?thesis
- apply (rule invariance_of_domain_homeomorphism [of "ball z' d" "\<lambda>z. z^n"])
- apply (rule open_ball continuous_intros order_refl inj)+
- apply (force simp: im_eq [OF zeq])
- done
- qed
- show ?thesis
- apply (rule_tac x = "(\<lambda>w. w^n) ` (ball z d)" in exI)
- apply (intro conjI open_imball)
- using \<open>d > 0\<close> apply simp
- using \<open>z \<noteq> 0\<close> assms apply (force simp: d_def)
- apply (rule_tac x="{ ball z' d |z'. z'^n = z^n}" in exI)
- apply (intro conjI ball1 ball2)
- apply (force simp: assms d_def power_eq_imp_eq_norm that, clarify)
- by (metis ball3)
qed
show ?thesis
using assms
@@ -3353,7 +3365,7 @@
show "range exp = - {0::complex}"
by auto (metis exp_Ln range_eqI)
show "\<exists>T. z \<in> T \<and> openin (subtopology euclidean (- {0})) T \<and>
- (\<exists>v. \<Union>v = {z. exp z \<in> T} \<and> (\<forall>u\<in>v. open u) \<and> disjoint v \<and>
+ (\<exists>v. \<Union>v = exp -` T \<and> (\<forall>u\<in>v. open u) \<and> disjoint v \<and>
(\<forall>u\<in>v. \<exists>q. homeomorphism u T exp q))"
if "z \<in> - {0::complex}" for z
proof -
@@ -3374,8 +3386,8 @@
using pi_ge_two by (simp add: ball_subset_ball_iff)
ultimately show "openin (subtopology euclidean (- {0})) (exp ` ball (Ln z) 1)"
by (auto simp: openin_open_eq invariance_of_domain continuous_on_exp [OF continuous_on_id])
- show "\<Union>\<V> = {w. exp w \<in> exp ` ball (Ln z) 1}"
- by (auto simp: \<V>_def Complex_Transcendental.exp_eq image_iff)
+ show "\<Union>\<V> = exp -` exp ` ball (Ln z) 1"
+ by (force simp: \<V>_def Complex_Transcendental.exp_eq image_iff)
show "\<forall>V\<in>\<V>. open V"
by (auto simp: \<V>_def inj_on_def continuous_intros invariance_of_domain)
have xy: "2 \<le> cmod (2 * of_int x * of_real pi * \<i> - 2 * of_int y * of_real pi * \<i>)"
@@ -4314,7 +4326,7 @@
qed
next
case False
- obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+ have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
proof (rule continuous_discrete_range_constant [OF ST])
show "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
apply (intro continuous_intros)
@@ -4338,7 +4350,9 @@
then show ?thesis
by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
qed
- qed blast
+ qed
+ then obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+ by (auto simp: constant_on_def)
with False have "exp a = 1"
by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
with a show ?thesis
@@ -4382,7 +4396,7 @@
qed
next
case False
- obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+ have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
proof (rule continuous_discrete_range_constant [OF ST])
show "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
apply (intro continuous_intros)
@@ -4406,7 +4420,9 @@
then show ?thesis
by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
qed
- qed blast
+ qed
+ then obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+ by (auto simp: constant_on_def)
with False have "exp a = 1"
by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
with a show ?thesis
@@ -4441,7 +4457,7 @@
using fim by auto
then obtain f' where f': "\<And>y. y \<in> T \<longrightarrow> f' y \<in> S \<and> f (f' y) = y"
by metis
- have *: "\<exists>a. \<forall>x \<in> {x. x \<in> S \<and> f x = y}. h x - h(f' y) = a" if "y \<in> T" for y
+ have *: "(\<lambda>x. h x - h(f' y)) constant_on {x. x \<in> S \<and> f x = y}" if "y \<in> T" for y
proof (rule continuous_discrete_range_constant [OF conn [OF that], of "\<lambda>x. h x - h (f' y)"], simp_all add: algebra_simps)
show "continuous_on {x \<in> S. f x = y} (\<lambda>x. h x - h (f' y))"
by (intro continuous_intros continuous_on_subset [OF conth]) auto
@@ -4462,13 +4478,12 @@
qed
qed
have "h x = h (f' (f x))" if "x \<in> S" for x
- using * [of "f x"] fim that apply clarsimp
- by (metis f' imageI right_minus_eq)
+ using * [of "f x"] fim that unfolding constant_on_def by clarsimp (metis f' imageI right_minus_eq)
moreover have "\<And>x. x \<in> T \<Longrightarrow> \<exists>u. u \<in> S \<and> x = f u \<and> h (f' x) = h u"
using f' by fastforce
ultimately
have eq: "((\<lambda>x. (x, (h \<circ> f') x)) ` T) =
- {p. \<exists>x. x \<in> S \<and> (x, p) \<in> {z \<in> S \<times> UNIV. snd z - ((f \<circ> fst) z, (h \<circ> fst) z) \<in> {0}}}"
+ {p. \<exists>x. x \<in> S \<and> (x, p) \<in> (S \<times> UNIV) \<inter> ((\<lambda>z. snd z - ((f \<circ> fst) z, (h \<circ> fst) z)) -` {0})}"
using fim by (auto simp: image_iff)
show "\<exists>h. continuous_on T h \<and> (\<forall>x\<in>T. g x = exp (h x))"
proof (intro exI conjI)
@@ -4513,9 +4528,10 @@
proof (rule compact_continuous_image)
show "continuous_on {x \<in> S. f x = y} h"
by (rule continuous_on_subset [OF conth]) auto
- have "compact {x \<in> S. f x \<in> {y}}"
+ have "compact (S \<inter> f -` {y})"
by (rule proper_map_from_compact [OF contf _ \<open>compact S\<close>, of T]) (simp_all add: fim that)
- then show "compact {x \<in> S. f x = y}" by simp
+ then show "compact {x \<in> S. f x = y}"
+ by (auto simp: vimage_def Int_def)
qed
have 2: "h ` {x \<in> S. f x = y} \<noteq> {}"
using fim that by auto
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Oct 19 17:16:01 2017 +0100
@@ -3187,17 +3187,15 @@
proof -
have "e * r > 0" using that \<open>0 < r\<close> by simp
with intfi[unfolded has_integral]
- obtain d where d: "gauge d"
- "\<And>p. p tagged_division_of cbox a b \<and> d fine p
+ obtain d where "gauge d"
+ and d: "\<And>p. p tagged_division_of cbox a b \<and> d fine p
\<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) < e * r"
by metis
- define d' where "d' x = {y. g y \<in> d (g x)}" for x
- have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
- unfolding d'_def ..
+ define d' where "d' x = g -` d (g x)" for x
show ?thesis
proof (rule_tac x=d' in exI, safe)
show "gauge d'"
- using d(1) continuous_open_preimage_univ[OF _ contg] by (auto simp: gauge_def d')
+ using \<open>gauge d\<close> continuous_open_vimage[OF _ contg] by (auto simp: gauge_def d'_def)
next
fix p
assume ptag: "p tagged_division_of h ` cbox a b" and finep: "d' fine p"
@@ -3211,7 +3209,7 @@
show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)"
using ptag by auto
show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
- using finep unfolding fine_def d' by auto
+ using finep unfolding fine_def d'_def by auto
next
fix x k
assume xk: "(x, k) \<in> p"
@@ -3259,7 +3257,7 @@
using \<open>0 < r\<close> by (auto simp: scaleR_diff_right)
finally have eq: "?l = ?r" .
show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
- using d(2)[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
+ using d[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
qed
qed
then show ?thesis
@@ -4229,7 +4227,7 @@
and "x \<in> S"
shows "f x = y"
proof -
- have xx: "\<exists>e>0. ball x e \<subseteq> {xa \<in> S. f xa \<in> {f x}}" if "x \<in> S" for x
+ have "\<exists>e>0. ball x e \<subseteq> (S \<inter> f -` {f x})" if "x \<in> S" for x
proof -
obtain e where "0 < e" and e: "ball x e \<subseteq> S"
using \<open>x \<in> S\<close> \<open>open S\<close> open_contains_ball by blast
@@ -4248,15 +4246,15 @@
by (metis Diff_iff contra_subsetD derf e has_derivative_within_subset that)
qed (use y e \<open>0 < e\<close> in auto)
qed
- then show "\<exists>e>0. ball x e \<subseteq> {xa \<in> S. f xa \<in> {f x}}"
+ then show "\<exists>e>0. ball x e \<subseteq> (S \<inter> f -` {f x})"
using \<open>0 < e\<close> by blast
qed
- then have "openin (subtopology euclidean S) {x \<in> S. f x \<in> {y}}"
+ then have "openin (subtopology euclidean S) (S \<inter> f -` {y})"
by (auto intro!: open_openin_trans[OF \<open>open S\<close>] simp: open_contains_ball)
- moreover have "closedin (subtopology euclidean S) {x \<in> S. f x \<in> {y}}"
+ moreover have "closedin (subtopology euclidean S) (S \<inter> f -` {y})"
by (force intro!: continuous_closedin_preimage [OF contf])
- ultimately have "{x \<in> S. f x \<in> {y}} = {} \<or> {x \<in> S. f x \<in> {y}} = S"
- using \<open>connected S\<close> connected_clopen by blast
+ ultimately have "(S \<inter> f -` {y}) = {} \<or> (S \<inter> f -` {y}) = S"
+ using \<open>connected S\<close> by (simp add: connected_clopen)
then show ?thesis
using \<open>x \<in> S\<close> \<open>f c = y\<close> \<open>c \<in> S\<close> by auto
qed
--- a/src/HOL/Analysis/Homeomorphism.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy Thu Oct 19 17:16:01 2017 +0100
@@ -1089,14 +1089,14 @@
by force
have *: "r *\<^sub>R b = One \<Longrightarrow> b = (1 / r) *\<^sub>R One" for r and b::'b
by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
- have "f ` U = {z. (setdist {fst z} (- U) *\<^sub>R snd z) \<in> {One}}"
+ have "f ` U = (\<lambda>z. (setdist {fst z} (- U) *\<^sub>R snd z)) -` {One}"
apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
apply (rule_tac x=a in image_eqI)
apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D)
done
then have clfU: "closed (f ` U)"
apply (rule ssubst)
- apply (rule continuous_closed_preimage_univ)
+ apply (rule continuous_closed_vimage)
apply (auto intro: continuous_intros cont [unfolded o_def])
done
have "closed (f ` S)"
@@ -1278,7 +1278,7 @@
"covering_space c p S \<equiv>
continuous_on c p \<and> p ` c = S \<and>
(\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (subtopology euclidean S) T \<and>
- (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> T} \<and>
+ (\<exists>v. \<Union>v = c \<inter> p -` T \<and>
(\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
pairwise disjnt v \<and>
(\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
@@ -1302,16 +1302,16 @@
"homeomorphism T u p q"
using assms
apply (simp add: covering_space_def, clarify)
-apply (drule_tac x="p x" in bspec, force)
-by (metis (no_types, lifting) Union_iff mem_Collect_eq)
+ apply (drule_tac x="p x" in bspec, force)
+ by (metis IntI UnionE vimage_eq)
lemma covering_space_local_homeomorphism_alt:
assumes p: "covering_space c p S" and "y \<in> S"
- obtains x T u q where "p x = y"
+ obtains x T U q where "p x = y"
"x \<in> T" "openin (subtopology euclidean c) T"
- "y \<in> u" "openin (subtopology euclidean S) u"
- "homeomorphism T u p q"
+ "y \<in> U" "openin (subtopology euclidean S) U"
+ "homeomorphism T U p q"
proof -
obtain x where "p x = y" "x \<in> c"
using assms covering_space_imp_surjective by blast
@@ -1329,7 +1329,7 @@
and covs:
"\<And>x. x \<in> S \<Longrightarrow>
\<exists>X VS. x \<in> X \<and> openin (subtopology euclidean S) X \<and>
- \<Union>VS = {x. x \<in> c \<and> p x \<in> X} \<and>
+ \<Union>VS = c \<inter> p -` X \<and>
(\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and>
pairwise disjnt VS \<and>
(\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
@@ -1340,7 +1340,7 @@
proof -
have "y \<in> S" using \<open>T \<subseteq> c\<close> pce that by blast
obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean S) U"
- and VS: "\<Union>VS = {x. x \<in> c \<and> p x \<in> U}"
+ and VS: "\<Union>VS = c \<inter> p -` U"
and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V"
and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
using covs [OF \<open>y \<in> S\<close>] by auto
@@ -1349,16 +1349,16 @@
using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast
with VS obtain V where "x \<in> V" "V \<in> VS" by auto
then obtain q where q: "homeomorphism V U p q" using homVS by blast
- then have ptV: "p ` (T \<inter> V) = U \<inter> {z. q z \<in> (T \<inter> V)}"
+ then have ptV: "p ` (T \<inter> V) = U \<inter> q -` (T \<inter> V)"
using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
have ocv: "openin (subtopology euclidean c) V"
by (simp add: \<open>V \<in> VS\<close> openVS)
- have "openin (subtopology euclidean U) {z \<in> U. q z \<in> T \<inter> V}"
+ have "openin (subtopology euclidean U) (U \<inter> q -` (T \<inter> V))"
apply (rule continuous_on_open [THEN iffD1, rule_format])
using homeomorphism_def q apply blast
using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def
by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
- then have os: "openin (subtopology euclidean S) (U \<inter> {z. q z \<in> T \<inter> V})"
+ then have os: "openin (subtopology euclidean S) (U \<inter> q -` (T \<inter> V))"
using openin_trans [of U] by (simp add: Collect_conj_eq U)
show ?thesis
apply (rule_tac x = "p ` (T \<inter> V)" in exI)
@@ -1400,20 +1400,19 @@
using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+
done
have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
- have gg: "{x \<in> U. g x \<in> v} = {x \<in> U. g x \<in> (v \<inter> g ` U)}" for g
+ have gg: "U \<inter> g -` v = U \<inter> g -` (v \<inter> g ` U)" for g
by auto
have "openin (subtopology euclidean (g1 ` U)) (v \<inter> g1 ` U)"
using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open)
- then have 1: "openin (subtopology euclidean U) {x \<in> U. g1 x \<in> v}"
+ then have 1: "openin (subtopology euclidean U) (U \<inter> g1 -` v)"
unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
have "openin (subtopology euclidean (g2 ` U)) (v \<inter> g2 ` U)"
using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open)
- then have 2: "openin (subtopology euclidean U) {x \<in> U. g2 x \<in> v}"
+ then have 2: "openin (subtopology euclidean U) (U \<inter> g2 -` v)"
unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
- show "\<exists>T. openin (subtopology euclidean U) T \<and>
- z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
+ show "\<exists>T. openin (subtopology euclidean U) T \<and> z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
using z
- apply (rule_tac x = "{x. x \<in> U \<and> g1 x \<in> v} \<inter> {x. x \<in> U \<and> g2 x \<in> v}" in exI)
+ apply (rule_tac x = "(U \<inter> g1 -` v) \<inter> (U \<inter> g2 -` v)" in exI)
apply (intro conjI)
apply (rule openin_Int [OF 1 2])
using \<open>g1 z \<in> v\<close> \<open>g2 z \<in> v\<close> apply (force simp:, clarify)
@@ -1475,7 +1474,7 @@
by (metis IntE V \<open>x \<in> V\<close> imageI openin_open)
then obtain T \<V> where "p x \<in> T"
and opeT: "openin (subtopology euclidean S) T"
- and veq: "\<Union>\<V> = {x \<in> C. p x \<in> T}"
+ and veq: "\<Union>\<V> = C \<inter> p -` T"
and ope: "\<forall>U\<in>\<V>. openin (subtopology euclidean C) U"
and hom: "\<forall>U\<in>\<V>. \<exists>q. homeomorphism U T p q"
using cov unfolding covering_space_def by (blast intro: that)
@@ -1583,7 +1582,7 @@
if "y \<in> U" for y
proof -
obtain UU where UU: "\<And>s. s \<in> S \<Longrightarrow> s \<in> (UU s) \<and> openin (subtopology euclidean S) (UU s) \<and>
- (\<exists>\<V>. \<Union>\<V> = {x. x \<in> C \<and> p x \<in> (UU s)} \<and>
+ (\<exists>\<V>. \<Union>\<V> = C \<inter> p -` UU s \<and>
(\<forall>U \<in> \<V>. openin (subtopology euclidean C) U) \<and>
pairwise disjnt \<V> \<and>
(\<forall>U \<in> \<V>. \<exists>q. homeomorphism U (UU s) p q))"
@@ -1595,13 +1594,13 @@
proof -
have hinS: "h (t, y) \<in> S"
using \<open>y \<in> U\<close> him that by blast
- then have "(t,y) \<in> {z \<in> {0..1} \<times> U. h z \<in> UU (h (t, y))}"
+ then have "(t,y) \<in> ({0..1} \<times> U) \<inter> h -` UU(h(t, y))"
using \<open>y \<in> U\<close> \<open>t \<in> {0..1}\<close> by (auto simp: ope)
- moreover have ope_01U: "openin (subtopology euclidean ({0..1} \<times> U)) {z. z \<in> ({0..1} \<times> U) \<and> h z \<in> UU(h(t, y))}"
+ moreover have ope_01U: "openin (subtopology euclidean ({0..1} \<times> U)) (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))"
using hinS ope continuous_on_open_gen [OF him] conth by blast
ultimately obtain V W where opeV: "open V" and "t \<in> {0..1} \<inter> V" "t \<in> {0..1} \<inter> V"
and opeW: "open W" and "y \<in> U" "y \<in> W"
- and VW: "({0..1} \<inter> V) \<times> (U \<inter> W) \<subseteq> {z. z \<in> ({0..1} \<times> U) \<and> h z \<in> UU(h(t, y))}"
+ and VW: "({0..1} \<inter> V) \<times> (U \<inter> W) \<subseteq> (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))"
by (rule Times_in_interior_subtopology) (auto simp: openin_open)
then show ?thesis
using hinS by blast
@@ -1677,7 +1676,7 @@
qed blast
have t01: "t \<in> {0..1}"
using \<open>t \<in> tk\<close> \<open>tk \<subseteq> {0..1}\<close> by blast
- obtain \<V> where "\<Union>\<V> = {x. x \<in> C \<and> p x \<in> (UU (X t))}"
+ obtain \<V> where \<V>: "\<Union>\<V> = C \<inter> p -` UU (X t)"
and opeC: "\<And>U. U \<in> \<V> \<Longrightarrow> openin (subtopology euclidean C) U"
and "pairwise disjnt \<V>"
and homuu: "\<And>U. U \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism U (UU (X t)) p q"
@@ -1686,7 +1685,7 @@
using N by (auto simp: divide_simps algebra_simps)
with t have nN_in_kkt: "real n / real N \<in> K t"
by blast
- have "k (real n / real N, y) \<in> {x. x \<in> C \<and> p x \<in> (UU (X t))}"
+ have "k (real n / real N, y) \<in> C \<inter> p -` UU (X t)"
proof (simp, rule conjI)
show "k (real n / real N, y) \<in> C"
using \<open>y \<in> V\<close> kim keq by force
@@ -1701,8 +1700,8 @@
using him t01 by blast
finally show "p (k (real n / real N, y)) \<in> UU (X t)" .
qed
- then have "k (real n / real N, y) \<in> \<Union>\<V>"
- using \<open>\<Union>\<V> = {x \<in> C. p x \<in> UU (X t)}\<close> by blast
+ with \<V> have "k (real n / real N, y) \<in> \<Union>\<V>"
+ by blast
then obtain W where W: "k (real n / real N, y) \<in> W" and "W \<in> \<V>"
by blast
then obtain p' where opeC': "openin (subtopology euclidean C) W"
@@ -1711,14 +1710,14 @@
then have "W \<subseteq> C"
using openin_imp_subset by blast
define W' where "W' = UU(X t)"
- have opeVW: "openin (subtopology euclidean V) {z \<in> V. (k \<circ> Pair (real n / real N)) z \<in> W}"
+ have opeVW: "openin (subtopology euclidean V) (V \<inter> (k \<circ> Pair (n / N)) -` W)"
apply (rule continuous_openin_preimage [OF _ _ opeC'])
apply (intro continuous_intros continuous_on_subset [OF contk])
using kim apply (auto simp: \<open>y \<in> V\<close> W)
done
obtain N' where opeUN': "openin (subtopology euclidean U) N'"
and "y \<in> N'" and kimw: "k ` ({(real n / real N)} \<times> N') \<subseteq> W"
- apply (rule_tac N' = "{z \<in> V. (k \<circ> Pair ((real n / real N))) z \<in> W}" in that)
+ apply (rule_tac N' = "(V \<inter> (k \<circ> Pair (n / N)) -` W)" in that)
apply (fastforce simp: \<open>y \<in> V\<close> W intro!: openin_trans [OF opeVW opeUV])+
done
obtain Q Q' where opeUQ: "openin (subtopology euclidean U) Q"
@@ -2283,7 +2282,7 @@
using l [of "linepath z z" z "linepath a a"] by (auto simp: assms)
show LC: "l ` U \<subseteq> C"
by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE)
- have "\<exists>T. openin (subtopology euclidean U) T \<and> y \<in> T \<and> T \<subseteq> {x \<in> U. l x \<in> X}"
+ have "\<exists>T. openin (subtopology euclidean U) T \<and> y \<in> T \<and> T \<subseteq> U \<inter> l -` X"
if X: "openin (subtopology euclidean C) X" and "y \<in> U" "l y \<in> X" for X y
proof -
have "X \<subseteq> C"
@@ -2292,7 +2291,7 @@
using fim \<open>y \<in> U\<close> by blast
then obtain W \<V>
where WV: "f y \<in> W \<and> openin (subtopology euclidean S) W \<and>
- (\<Union>\<V> = {x. x \<in> C \<and> p x \<in> W} \<and>
+ (\<Union>\<V> = C \<inter> p -` W \<and>
(\<forall>U \<in> \<V>. openin (subtopology euclidean C) U) \<and>
pairwise disjnt \<V> \<and>
(\<forall>U \<in> \<V>. \<exists>q. homeomorphism U W p q))"
@@ -2309,12 +2308,12 @@
obtain V where "y \<in> V" "y \<in> U" and fimW: "f ` V \<subseteq> W" "V \<subseteq> U"
and "path_connected V" and opeUV: "openin (subtopology euclidean U) V"
proof -
- have "openin (subtopology euclidean U) {c \<in> U. f c \<in> W}"
+ have "openin (subtopology euclidean U) (U \<inter> f -` W)"
using WV contf continuous_on_open_gen fim by auto
then show ?thesis
using U WV
apply (auto simp: locally_path_connected)
- apply (drule_tac x="{x. x \<in> U \<and> f x \<in> W}" in spec)
+ apply (drule_tac x="U \<inter> f -` W" in spec)
apply (drule_tac x=y in spec)
apply (auto simp: \<open>y \<in> U\<close> intro: that)
done
@@ -2325,23 +2324,23 @@
using homUW' homeomorphism_image2 by fastforce
show ?thesis
proof (intro exI conjI)
- have "openin (subtopology euclidean S) {x \<in> W. p' x \<in> W' \<inter> X}"
+ have "openin (subtopology euclidean S) (W \<inter> p' -` (W' \<inter> X))"
proof (rule openin_trans)
- show "openin (subtopology euclidean W) {x \<in> W. p' x \<in> W' \<inter> X}"
+ show "openin (subtopology euclidean W) (W \<inter> p' -` (W' \<inter> X))"
apply (rule continuous_openin_preimage [OF contp' p'im])
using X \<open>W' \<subseteq> C\<close> apply (auto simp: openin_open)
done
show "openin (subtopology euclidean S) W"
using WV by blast
qed
- then show "openin (subtopology euclidean U) (V \<inter> {x. x \<in> U \<and> f x \<in> {x. x \<in> W \<and> p' x \<in> W' \<inter> X}})"
- by (intro openin_Int opeUV continuous_openin_preimage [OF contf fim])
- have "p' (f y) \<in> X"
+ then show "openin (subtopology euclidean U) (V \<inter> (U \<inter> (f -` (W \<inter> (p' -` (W' \<inter> X))))))"
+ by (blast intro: opeUV openin_subtopology_self continuous_openin_preimage [OF contf fim])
+ have "p' (f y) \<in> X"
using \<open>l y \<in> W'\<close> homeomorphism_apply1 [OF homUW'] pleq \<open>y \<in> U\<close> \<open>l y \<in> X\<close> by fastforce
- then show "y \<in> V \<inter> {x \<in> U. f x \<in> {x \<in> W. p' x \<in> W' \<inter> X}}"
+ then show "y \<in> V \<inter> (U \<inter> f -` (W \<inter> p' -` (W' \<inter> X)))"
using \<open>y \<in> U\<close> \<open>y \<in> V\<close> WV p'im by auto
- show "V \<inter> {x \<in> U. f x \<in> {x \<in> W. p' x \<in> W' \<inter> X}} \<subseteq> {x \<in> U. l x \<in> X}"
- proof clarsimp
+ show "V \<inter> (U \<inter> f -` (W \<inter> p' -` (W' \<inter> X))) \<subseteq> U \<inter> l -` X"
+ proof (intro subsetI IntI; clarify)
fix y'
assume y': "y' \<in> V" "y' \<in> U" "f y' \<in> W" "p' (f y') \<in> W'" "p' (f y') \<in> X"
then obtain \<gamma> where "path \<gamma>" "path_image \<gamma> \<subseteq> V" "pathstart \<gamma> = y" "pathfinish \<gamma> = y'"
@@ -2354,7 +2353,7 @@
have finW: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> f (\<gamma> x) \<in> W"
using \<open>path_image \<gamma> \<subseteq> V\<close> by (auto simp: image_subset_iff path_image_def fimW [THEN subsetD])
have "pathfinish (qq +++ (p' \<circ> f \<circ> \<gamma>)) = l y'"
- proof (rule l [of "pp +++ \<gamma>" y' "qq +++ (p' \<circ> f \<circ> \<gamma>)" ])
+ proof (rule l [of "pp +++ \<gamma>" y' "qq +++ (p' \<circ> f \<circ> \<gamma>)"])
show "path (pp +++ \<gamma>)"
by (simp add: \<open>path \<gamma>\<close> \<open>path pp\<close> \<open>pathfinish pp = y\<close> \<open>pathstart \<gamma> = y\<close>)
show "path_image (pp +++ \<gamma>) \<subseteq> U"
@@ -2395,14 +2394,13 @@
using that \<xi> by auto
qed
qed
- with \<open>pathfinish \<gamma> = y'\<close> \<open>p' (f y') \<in> X\<close> show "l y' \<in> X"
+ with \<open>pathfinish \<gamma> = y'\<close> \<open>p' (f y') \<in> X\<close> show "y' \<in> l -` X"
unfolding pathfinish_join by (simp add: pathfinish_def)
qed
qed
qed
then show "continuous_on U l"
- using openin_subopen continuous_on_open_gen [OF LC]
- by (metis (no_types, lifting) mem_Collect_eq)
+ by (metis IntD1 IntD2 vimage_eq openin_subopen continuous_on_open_gen [OF LC])
qed
qed
--- a/src/HOL/Analysis/Jordan_Curve.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy Thu Oct 19 17:16:01 2017 +0100
@@ -88,8 +88,10 @@
then show ?thesis
by (rule_tac x="2*pi" in exI) auto
qed
- ultimately obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
+ ultimately have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
using continuous_discrete_range_constant [OF conST contgh] by blast
+ then obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
+ by (auto simp: constant_on_def)
obtain w where "exp(\<i> * of_real(h w)) = exp (\<i> * of_real(z + h w))"
using disc z False
by auto (metis diff_add_cancel g h of_real_add)
--- a/src/HOL/Analysis/Path_Connected.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Thu Oct 19 17:16:01 2017 +0100
@@ -1546,7 +1546,7 @@
by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl)
ultimately show False
using *[unfolded connected_local not_ex, rule_format,
- of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"]
+ of "{0..1} \<inter> g -` e1" "{0..1} \<inter> g -` e2"]
using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(1)]
using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(2)]
by auto
@@ -4946,58 +4946,57 @@
proposition homeomorphism_locally_imp:
fixes S :: "'a::metric_space set" and t :: "'b::t2_space set"
assumes S: "locally P S" and hom: "homeomorphism S t f g"
- and Q: "\<And>S t. \<lbrakk>P S; homeomorphism S t f g\<rbrakk> \<Longrightarrow> Q t"
+ and Q: "\<And>S S'. \<lbrakk>P S; homeomorphism S S' f g\<rbrakk> \<Longrightarrow> Q S'"
shows "locally Q t"
proof (clarsimp simp: locally_def)
- fix w y
- assume "y \<in> w" and "openin (subtopology euclidean t) w"
- then obtain T where T: "open T" "w = t \<inter> T"
+ fix W y
+ assume "y \<in> W" and "openin (subtopology euclidean t) W"
+ then obtain T where T: "open T" "W = t \<inter> T"
by (force simp: openin_open)
- then have "w \<subseteq> t" by auto
+ then have "W \<subseteq> t" by auto
have f: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "f ` S = t" "continuous_on S f"
and g: "\<And>y. y \<in> t \<Longrightarrow> f(g y) = y" "g ` t = S" "continuous_on t g"
using hom by (auto simp: homeomorphism_def)
- have gw: "g ` w = S \<inter> {x. f x \<in> w}"
- using \<open>w \<subseteq> t\<close>
+ have gw: "g ` W = S \<inter> f -` W"
+ using \<open>W \<subseteq> t\<close>
apply auto
- using \<open>g ` t = S\<close> \<open>w \<subseteq> t\<close> apply blast
- using g \<open>w \<subseteq> t\<close> apply auto[1]
+ using \<open>g ` t = S\<close> \<open>W \<subseteq> t\<close> apply blast
+ using g \<open>W \<subseteq> t\<close> apply auto[1]
by (simp add: f rev_image_eqI)
- have o: "openin (subtopology euclidean S) (g ` w)"
+ have o: "openin (subtopology euclidean S) (g ` W)"
proof -
have "continuous_on S f"
using f(3) by blast
- then show "openin (subtopology euclidean S) (g ` w)"
- by (simp add: gw Collect_conj_eq \<open>openin (subtopology euclidean t) w\<close> continuous_on_open f(2))
+ then show "openin (subtopology euclidean S) (g ` W)"
+ by (simp add: gw Collect_conj_eq \<open>openin (subtopology euclidean t) W\<close> continuous_on_open f(2))
qed
then obtain u v
- where osu: "openin (subtopology euclidean S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` w"
- using S [unfolded locally_def, rule_format, of "g ` w" "g y"] \<open>y \<in> w\<close> by force
+ where osu: "openin (subtopology euclidean S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` W"
+ using S [unfolded locally_def, rule_format, of "g ` W" "g y"] \<open>y \<in> W\<close> by force
have "v \<subseteq> S" using uv by (simp add: gw)
have fv: "f ` v = t \<inter> {x. g x \<in> v}"
using \<open>f ` S = t\<close> f \<open>v \<subseteq> S\<close> by auto
- have "f ` v \<subseteq> w"
+ have "f ` v \<subseteq> W"
using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto
have contvf: "continuous_on v f"
using \<open>v \<subseteq> S\<close> continuous_on_subset f(3) by blast
have contvg: "continuous_on (f ` v) g"
- using \<open>f ` v \<subseteq> w\<close> \<open>w \<subseteq> t\<close> continuous_on_subset g(3) by blast
+ using \<open>f ` v \<subseteq> W\<close> \<open>W \<subseteq> t\<close> continuous_on_subset g(3) by blast
have homv: "homeomorphism v (f ` v) f g"
- using \<open>v \<subseteq> S\<close> \<open>w \<subseteq> t\<close> f
+ using \<open>v \<subseteq> S\<close> \<open>W \<subseteq> t\<close> f
apply (simp add: homeomorphism_def contvf contvg, auto)
by (metis f(1) rev_image_eqI rev_subsetD)
- have 1: "openin (subtopology euclidean t) {x \<in> t. g x \<in> u}"
+ have 1: "openin (subtopology euclidean t) (t \<inter> g -` u)"
apply (rule continuous_on_open [THEN iffD1, rule_format])
apply (rule \<open>continuous_on t g\<close>)
using \<open>g ` t = S\<close> apply (simp add: osu)
done
- have 2: "\<exists>v. Q v \<and> y \<in> {x \<in> t. g x \<in> u} \<and> {x \<in> t. g x \<in> u} \<subseteq> v \<and> v \<subseteq> w"
+ have 2: "\<exists>V. Q V \<and> y \<in> (t \<inter> g -` u) \<and> (t \<inter> g -` u) \<subseteq> V \<and> V \<subseteq> W"
apply (rule_tac x="f ` v" in exI)
apply (intro conjI Q [OF \<open>P v\<close> homv])
- using \<open>w \<subseteq> t\<close> \<open>y \<in> w\<close> \<open>f ` v \<subseteq> w\<close> uv apply (auto simp: fv)
+ using \<open>W \<subseteq> t\<close> \<open>y \<in> W\<close> \<open>f ` v \<subseteq> W\<close> uv apply (auto simp: fv)
done
- show "\<exists>u. openin (subtopology euclidean t) u \<and>
- (\<exists>v. Q v \<and> y \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"
+ show "\<exists>U. openin (subtopology euclidean t) U \<and> (\<exists>v. Q v \<and> y \<in> U \<and> U \<subseteq> v \<and> v \<subseteq> W)"
by (meson 1 2)
qed
@@ -5057,22 +5056,21 @@
and Q: "\<And>t. \<lbrakk>t \<subseteq> S; P t\<rbrakk> \<Longrightarrow> Q(f ` t)"
shows "locally Q (f ` S)"
proof (clarsimp simp add: locally_def)
- fix w y
- assume oiw: "openin (subtopology euclidean (f ` S)) w" and "y \<in> w"
- then have "w \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
- have oivf: "openin (subtopology euclidean S) {x \<in> S. f x \<in> w}"
+ fix W y
+ assume oiw: "openin (subtopology euclidean (f ` S)) W" and "y \<in> W"
+ then have "W \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
+ have oivf: "openin (subtopology euclidean S) (S \<inter> f -` W)"
by (rule continuous_on_open [THEN iffD1, rule_format, OF f oiw])
then obtain x where "x \<in> S" "f x = y"
- using \<open>w \<subseteq> f ` S\<close> \<open>y \<in> w\<close> by blast
- then obtain u v
- where "openin (subtopology euclidean S) u" "P v" "x \<in> u" "u \<subseteq> v" "v \<subseteq> {x \<in> S. f x \<in> w}"
- using P [unfolded locally_def, rule_format, of "{x. x \<in> S \<and> f x \<in> w}" x] oivf \<open>y \<in> w\<close>
+ using \<open>W \<subseteq> f ` S\<close> \<open>y \<in> W\<close> by blast
+ then obtain U V
+ where "openin (subtopology euclidean S) U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> S \<inter> f -` W"
+ using P [unfolded locally_def, rule_format, of "(S \<inter> f -` W)" x] oivf \<open>y \<in> W\<close>
by auto
- then show "\<exists>u. openin (subtopology euclidean (f ` S)) u \<and>
- (\<exists>v. Q v \<and> y \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"
- apply (rule_tac x="f ` u" in exI)
+ then show "\<exists>X. openin (subtopology euclidean (f ` S)) X \<and> (\<exists>Y. Q Y \<and> y \<in> X \<and> X \<subseteq> Y \<and> Y \<subseteq> W)"
+ apply (rule_tac x="f ` U" in exI)
apply (rule conjI, blast intro!: oo)
- apply (rule_tac x="f ` v" in exI)
+ apply (rule_tac x="f ` V" in exI)
apply (force simp: \<open>f x = y\<close> rev_image_eqI intro: Q)
done
qed
@@ -6087,7 +6085,7 @@
proposition locally_connected_quotient_image:
assumes lcS: "locally connected S"
and oo: "\<And>T. T \<subseteq> f ` S
- \<Longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T} \<longleftrightarrow>
+ \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
openin (subtopology euclidean (f ` S)) T"
shows "locally connected (f ` S)"
proof (clarsimp simp: locally_connected_open_component)
@@ -6096,53 +6094,53 @@
then have "C \<subseteq> U" "U \<subseteq> f ` S"
by (meson in_components_subset openin_imp_subset)+
then have "openin (subtopology euclidean (f ` S)) C \<longleftrightarrow>
- openin (subtopology euclidean S) {x \<in> S. f x \<in> C}"
+ openin (subtopology euclidean S) (S \<inter> f -` C)"
by (auto simp: oo)
- moreover have "openin (subtopology euclidean S) {x \<in> S. f x \<in> C}"
+ moreover have "openin (subtopology euclidean S) (S \<inter> f -` C)"
proof (subst openin_subopen, clarify)
fix x
assume "x \<in> S" "f x \<in> C"
- show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> {x \<in> S. f x \<in> C}"
+ show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> (S \<inter> f -` C)"
proof (intro conjI exI)
- show "openin (subtopology euclidean S) (connected_component_set {w \<in> S. f w \<in> U} x)"
+ show "openin (subtopology euclidean S) (connected_component_set (S \<inter> f -` U) x)"
proof (rule ccontr)
- assume **: "\<not> openin (subtopology euclidean S) (connected_component_set {a \<in> S. f a \<in> U} x)"
- then have "x \<notin> {a \<in> S. f a \<in> U}"
+ assume **: "\<not> openin (subtopology euclidean S) (connected_component_set (S \<inter> f -` U) x)"
+ then have "x \<notin> (S \<inter> f -` U)"
using \<open>U \<subseteq> f ` S\<close> opefSU lcS locally_connected_2 oo by blast
with ** show False
by (metis (no_types) connected_component_eq_empty empty_iff openin_subopen)
qed
next
- show "x \<in> connected_component_set {w \<in> S. f w \<in> U} x"
+ show "x \<in> connected_component_set (S \<inter> f -` U) x"
using \<open>C \<subseteq> U\<close> \<open>f x \<in> C\<close> \<open>x \<in> S\<close> by auto
next
have contf: "continuous_on S f"
by (simp add: continuous_on_open oo openin_imp_subset)
- then have "continuous_on (connected_component_set {w \<in> S. f w \<in> U} x) f"
+ then have "continuous_on (connected_component_set (S \<inter> f -` U) x) f"
apply (rule continuous_on_subset)
using connected_component_subset apply blast
done
- then have "connected (f ` connected_component_set {w \<in> S. f w \<in> U} x)"
+ then have "connected (f ` connected_component_set (S \<inter> f -` U) x)"
by (rule connected_continuous_image [OF _ connected_connected_component])
- moreover have "f ` connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> U"
+ moreover have "f ` connected_component_set (S \<inter> f -` U) x \<subseteq> U"
using connected_component_in by blast
- moreover have "C \<inter> f ` connected_component_set {w \<in> S. f w \<in> U} x \<noteq> {}"
+ moreover have "C \<inter> f ` connected_component_set (S \<inter> f -` U) x \<noteq> {}"
using \<open>C \<subseteq> U\<close> \<open>f x \<in> C\<close> \<open>x \<in> S\<close> by fastforce
- ultimately have fC: "f ` (connected_component_set {w \<in> S. f w \<in> U} x) \<subseteq> C"
+ ultimately have fC: "f ` (connected_component_set (S \<inter> f -` U) x) \<subseteq> C"
by (rule components_maximal [OF \<open>C \<in> components U\<close>])
- have cUC: "connected_component_set {a \<in> S. f a \<in> U} x \<subseteq> {a \<in> S. f a \<in> C}"
+ have cUC: "connected_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` C)"
using connected_component_subset fC by blast
- have "connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> connected_component_set {w \<in> S. f w \<in> C} x"
+ have "connected_component_set (S \<inter> f -` U) x \<subseteq> connected_component_set (S \<inter> f -` C) x"
proof -
- { assume "x \<in> connected_component_set {a \<in> S. f a \<in> U} x"
+ { assume "x \<in> connected_component_set (S \<inter> f -` U) x"
then have ?thesis
- by (simp add: cUC connected_component_maximal) }
+ using cUC connected_component_idemp connected_component_mono by blast }
then show ?thesis
using connected_component_eq_empty by auto
qed
- also have "... \<subseteq> {w \<in> S. f w \<in> C}"
+ also have "... \<subseteq> (S \<inter> f -` C)"
by (rule connected_component_subset)
- finally show "connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> {x \<in> S. f x \<in> C}" .
+ finally show "connected_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` C)" .
qed
qed
ultimately show "openin (subtopology euclidean (f ` S)) C"
@@ -6153,8 +6151,7 @@
proposition locally_path_connected_quotient_image:
assumes lcS: "locally path_connected S"
and oo: "\<And>T. T \<subseteq> f ` S
- \<Longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T} \<longleftrightarrow>
- openin (subtopology euclidean (f ` S)) T"
+ \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> openin (subtopology euclidean (f ` S)) T"
shows "locally path_connected (f ` S)"
proof (clarsimp simp: locally_path_connected_open_path_component)
fix U y
@@ -6162,62 +6159,62 @@
then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
by (meson path_component_subset openin_imp_subset)+
then have "openin (subtopology euclidean (f ` S)) (path_component_set U y) \<longleftrightarrow>
- openin (subtopology euclidean S) {x \<in> S. f x \<in> path_component_set U y}"
+ openin (subtopology euclidean S) (S \<inter> f -` path_component_set U y)"
proof -
have "path_component_set U y \<subseteq> f ` S"
using \<open>U \<subseteq> f ` S\<close> \<open>path_component_set U y \<subseteq> U\<close> by blast
then show ?thesis
using oo by blast
qed
- moreover have "openin (subtopology euclidean S) {x \<in> S. f x \<in> path_component_set U y}"
+ moreover have "openin (subtopology euclidean S) (S \<inter> f -` path_component_set U y)"
proof (subst openin_subopen, clarify)
fix x
assume "x \<in> S" and Uyfx: "path_component U y (f x)"
then have "f x \<in> U"
using path_component_mem by blast
- show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> {x \<in> S. f x \<in> path_component_set U y}"
+ show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> (S \<inter> f -` path_component_set U y)"
proof (intro conjI exI)
- show "openin (subtopology euclidean S) (path_component_set {w \<in> S. f w \<in> U} x)"
+ show "openin (subtopology euclidean S) (path_component_set (S \<inter> f -` U) x)"
proof (rule ccontr)
- assume **: "\<not> openin (subtopology euclidean S) (path_component_set {a \<in> S. f a \<in> U} x)"
- then have "x \<notin> {a \<in> S. f a \<in> U}"
+ assume **: "\<not> openin (subtopology euclidean S) (path_component_set (S \<inter> f -` U) x)"
+ then have "x \<notin> (S \<inter> f -` U)"
by (metis (no_types, lifting) \<open>U \<subseteq> f ` S\<close> opefSU lcS oo locally_path_connected_open_path_component)
then show False
using ** \<open>path_component_set U y \<subseteq> U\<close> \<open>x \<in> S\<close> \<open>path_component U y (f x)\<close> by blast
qed
next
- show "x \<in> path_component_set {w \<in> S. f w \<in> U} x"
- by (metis (no_types, lifting) \<open>x \<in> S\<close> IntD2 Int_Collect \<open>path_component U y (f x)\<close> path_component_mem(2) path_component_refl)
+ show "x \<in> path_component_set (S \<inter> f -` U) x"
+ by (simp add: \<open>f x \<in> U\<close> \<open>x \<in> S\<close> path_component_refl)
next
have contf: "continuous_on S f"
by (simp add: continuous_on_open oo openin_imp_subset)
- then have "continuous_on (path_component_set {w \<in> S. f w \<in> U} x) f"
+ then have "continuous_on (path_component_set (S \<inter> f -` U) x) f"
apply (rule continuous_on_subset)
using path_component_subset apply blast
done
- then have "path_connected (f ` path_component_set {w \<in> S. f w \<in> U} x)"
- by (simp add: path_connected_continuous_image path_connected_path_component)
- moreover have "f ` path_component_set {w \<in> S. f w \<in> U} x \<subseteq> U"
+ then have "path_connected (f ` path_component_set (S \<inter> f -` U) x)"
+ by (simp add: path_connected_continuous_image)
+ moreover have "f ` path_component_set (S \<inter> f -` U) x \<subseteq> U"
using path_component_mem by fastforce
- moreover have "f x \<in> f ` path_component_set {w \<in> S. f w \<in> U} x"
+ moreover have "f x \<in> f ` path_component_set (S \<inter> f -` U) x"
by (force simp: \<open>x \<in> S\<close> \<open>f x \<in> U\<close> path_component_refl_eq)
- ultimately have "f ` (path_component_set {w \<in> S. f w \<in> U} x) \<subseteq> path_component_set U (f x)"
+ ultimately have "f ` (path_component_set (S \<inter> f -` U) x) \<subseteq> path_component_set U (f x)"
by (meson path_component_maximal)
also have "... \<subseteq> path_component_set U y"
- by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym path_connected_path_component)
- finally have fC: "f ` (path_component_set {w \<in> S. f w \<in> U} x) \<subseteq> path_component_set U y" .
- have cUC: "path_component_set {a \<in> S. f a \<in> U} x \<subseteq> {a \<in> S. f a \<in> path_component_set U y}"
+ by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym)
+ finally have fC: "f ` (path_component_set (S \<inter> f -` U) x) \<subseteq> path_component_set U y" .
+ have cUC: "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)"
using path_component_subset fC by blast
- have "path_component_set {w \<in> S. f w \<in> U} x \<subseteq> path_component_set {w \<in> S. f w \<in> path_component_set U y} x"
+ have "path_component_set (S \<inter> f -` U) x \<subseteq> path_component_set (S \<inter> f -` path_component_set U y) x"
proof -
- have "\<And>a. path_component_set (path_component_set {a \<in> S. f a \<in> U} x) a \<subseteq> path_component_set {a \<in> S. f a \<in> path_component_set U y} a"
+ have "\<And>a. path_component_set (path_component_set (S \<inter> f -` U) x) a \<subseteq> path_component_set (S \<inter> f -` path_component_set U y) a"
using cUC path_component_mono by blast
then show ?thesis
using path_component_path_component by blast
qed
- also have "... \<subseteq> {w \<in> S. f w \<in> path_component_set U y}"
+ also have "... \<subseteq> (S \<inter> f -` path_component_set U y)"
by (rule path_component_subset)
- finally show "path_component_set {w \<in> S. f w \<in> U} x \<subseteq> {x \<in> S. f x \<in> path_component_set U y}" .
+ finally show "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)" .
qed
qed
ultimately show "openin (subtopology euclidean (f ` S)) (path_component_set U y)"
@@ -6234,13 +6231,10 @@
proof (clarsimp simp: continuous_openin_preimage_eq)
fix t :: "'b set"
assume "open t"
- have "{x. x \<in> S \<and> f x \<in> t} = \<Union>{{x. x \<in> c \<and> f x \<in> t} |c. c \<in> components S}"
- apply auto
- apply (metis (lifting) components_iff connected_component_refl_eq mem_Collect_eq)
- using Union_components by blast
- then show "openin (subtopology euclidean S) {x \<in> S. f x \<in> t}"
- using \<open>open t\<close> assms
- by (fastforce intro: openin_trans continuous_openin_preimage_gen)
+ have *: "S \<inter> f -` t = (\<Union>c \<in> components S. c \<inter> f -` t)"
+ by auto
+ show "openin (subtopology euclidean S) (S \<inter> f -` t)"
+ unfolding * using \<open>open t\<close> assms continuous_openin_preimage_gen openin_trans openin_Union by blast
qed
lemma continuous_on_components:
@@ -6308,11 +6302,9 @@
proof -
have "closedin (subtopology euclidean UNIV) (S \<union> \<Union>c)"
apply (rule closedin_union_complement_components [OF locally_connected_UNIV])
- using S apply (simp add: closed_closedin)
- using c apply (simp add: Compl_eq_Diff_UNIV)
+ using S c apply (simp_all add: Compl_eq_Diff_UNIV)
done
- then show ?thesis
- by (simp add: closed_closedin)
+ then show ?thesis by simp
qed
lemma closedin_Un_complement_component:
--- a/src/HOL/Analysis/Starlike.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Starlike.thy Thu Oct 19 17:16:01 2017 +0100
@@ -4973,10 +4973,16 @@
lemma setdist_eq_0_closedin:
fixes S :: "'a::euclidean_space set"
- shows "\<lbrakk>closedin (subtopology euclidean u) S; x \<in> u\<rbrakk>
+ shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U\<rbrakk>
\<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
+lemma setdist_gt_0_closedin:
+ fixes S :: "'a::euclidean_space set"
+ shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U; S \<noteq> {}; x \<notin> S\<rbrakk>
+ \<Longrightarrow> setdist {x} S > 0"
+ using less_eq_real_def setdist_eq_0_closedin by fastforce
+
subsection\<open>Basic lemmas about hyperplanes and halfspaces\<close>
lemma hyperplane_eq_Ex:
@@ -5089,25 +5095,19 @@
have contf: "continuous_on U f"
unfolding f_def by (intro continuous_intros)
show ?thesis
- proof (rule_tac S' = "{x\<in>U. f x > 0}" and T' = "{x\<in>U. f x < 0}" in that)
- show "{x \<in> U. 0 < f x} \<inter> {x \<in> U. f x < 0} = {}"
+ proof (rule_tac S' = "(U \<inter> f -` {0<..})" and T' = "(U \<inter> f -` {..<0})" in that)
+ show "(U \<inter> f -` {0<..}) \<inter> (U \<inter> f -` {..<0}) = {}"
by auto
- have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {0<..}}"
- by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
- then show "openin (subtopology euclidean U) {x \<in> U. 0 < f x}" by simp
- next
- have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {..<0}}"
+ show "openin (subtopology euclidean U) (U \<inter> f -` {0<..})"
by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
- then show "openin (subtopology euclidean U) {x \<in> U. f x < 0}" by simp
+ next
+ show "openin (subtopology euclidean U) (U \<inter> f -` {..<0})"
+ by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
next
- show "S \<subseteq> {x \<in> U. 0 < f x}"
- apply (clarsimp simp add: f_def setdist_sing_in_set)
- using assms
- by (metis False Int_insert_right closedin_imp_subset empty_not_insert insert_absorb insert_subset linorder_neqE_linordered_idom not_le setdist_eq_0_closedin setdist_pos_le)
- show "T \<subseteq> {x \<in> U. f x < 0}"
- apply (clarsimp simp add: f_def setdist_sing_in_set)
- using assms
- by (metis False closedin_subset disjoint_iff_not_equal insert_absorb insert_subset linorder_neqE_linordered_idom not_less setdist_eq_0_closedin setdist_pos_le topspace_euclidean_subtopology)
+ have "S \<subseteq> U" "T \<subseteq> U"
+ using closedin_imp_subset assms by blast+
+ then show "S \<subseteq> U \<inter> f -` {0<..}" "T \<subseteq> U \<inter> f -` {..<0}"
+ using assms False by (force simp add: f_def setdist_sing_in_set intro!: setdist_gt_0_closedin)+
qed
qed
@@ -5282,7 +5282,7 @@
proposition proper_map:
fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
assumes "closedin (subtopology euclidean S) K"
- and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact {x \<in> S. f x \<in> U}"
+ and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact (S \<inter> f -` U)"
and "f ` S \<subseteq> T"
shows "closedin (subtopology euclidean T) (f ` K)"
proof -
@@ -5298,7 +5298,7 @@
by metis
then have fX: "\<And>n. f (X n) = h n"
by metis
- have "compact (C \<inter> {a \<in> S. f a \<in> insert y (range (\<lambda>i. f(X(n + i))))})" for n
+ have "compact (C \<inter> (S \<inter> f -` insert y (range (\<lambda>i. f(X(n + i))))))" for n
apply (rule closed_Int_compact [OF \<open>closed C\<close>])
apply (rule com)
using X \<open>K \<subseteq> S\<close> \<open>f ` S \<subseteq> T\<close> \<open>y \<in> T\<close> apply blast
@@ -5350,16 +5350,16 @@
assume RHS: ?rhs
obtain g where gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
by (metis inv_into_f_f f)
- then have *: "{x \<in> S. f x \<in> U} = g ` U" if "U \<subseteq> f ` S" for U
+ then have *: "(S \<inter> f -` U) = g ` U" if "U \<subseteq> f ` S" for U
using that by fastforce
have gfim: "g ` f ` S \<subseteq> S" using gf by auto
- have **: "compact {x \<in> f ` S. g x \<in> C}" if C: "C \<subseteq> S" "compact C" for C
+ have **: "compact (f ` S \<inter> g -` C)" if C: "C \<subseteq> S" "compact C" for C
proof -
- obtain h :: "'a set \<Rightarrow> 'a" where "h C \<in> C \<and> h C \<notin> S \<or> compact (f ` C)"
+ obtain h where "h C \<in> C \<and> h C \<notin> S \<or> compact (f ` C)"
by (force simp: C RHS)
- moreover have "f ` C = {b \<in> f ` S. g b \<in> C}"
+ moreover have "f ` C = (f ` S \<inter> g -` C)"
using C gf by auto
- ultimately show "compact {b \<in> f ` S. g b \<in> C}"
+ ultimately show ?thesis
using C by auto
qed
show ?lhs
@@ -5510,14 +5510,14 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T" and "compact S"
"closedin (subtopology euclidean T) K"
- shows "compact {x. x \<in> S \<and> f x \<in> K}"
+ shows "compact (S \<inter> f -` K)"
by (rule closedin_compact [OF \<open>compact S\<close>] continuous_closedin_preimage_gen assms)+
lemma proper_map_fst:
assumes "compact T" "K \<subseteq> S" "compact K"
- shows "compact {z \<in> S \<times> T. fst z \<in> K}"
-proof -
- have "{z \<in> S \<times> T. fst z \<in> K} = K \<times> T"
+ shows "compact (S \<times> T \<inter> fst -` K)"
+proof -
+ have "(S \<times> T \<inter> fst -` K) = K \<times> T"
using assms by auto
then show ?thesis by (simp add: assms compact_Times)
qed
@@ -5535,9 +5535,9 @@
lemma proper_map_snd:
assumes "compact S" "K \<subseteq> T" "compact K"
- shows "compact {z \<in> S \<times> T. snd z \<in> K}"
-proof -
- have "{z \<in> S \<times> T. snd z \<in> K} = S \<times> K"
+ shows "compact (S \<times> T \<inter> snd -` K)"
+proof -
+ have "(S \<times> T \<inter> snd -` K) = S \<times> K"
using assms by auto
then show ?thesis by (simp add: assms compact_Times)
qed
@@ -7872,8 +7872,7 @@
and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
and "\<And>x. \<exists>V. open V \<and> x \<in> V \<and>
finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
-using paracompact_closedin [of UNIV S \<C>] assms
-by (auto simp: open_openin [symmetric] closed_closedin [symmetric])
+using paracompact_closedin [of UNIV S \<C>] assms by auto
subsection\<open>Closed-graph characterization of continuity\<close>
@@ -7883,7 +7882,7 @@
assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
shows "closedin (subtopology euclidean (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"
proof -
- have eq: "((\<lambda>x. Pair x (f x)) ` S) = {z. z \<in> S \<times> T \<and> (f \<circ> fst)z - snd z \<in> {0}}"
+ have eq: "((\<lambda>x. Pair x (f x)) ` S) =(S \<times> T \<inter> (\<lambda>z. (f \<circ> fst)z - snd z) -` {0})"
using fim by auto
show ?thesis
apply (subst eq)
@@ -7902,9 +7901,9 @@
proof (clarsimp simp add: continuous_on_closed_gen [OF fim])
fix U
assume U: "closedin (subtopology euclidean T) U"
- have eq: "{x. x \<in> S \<and> f x \<in> U} = fst ` (((\<lambda>x. Pair x (f x)) ` S) \<inter> (S \<times> U))"
+ have eq: "(S \<inter> f -` U) = fst ` (((\<lambda>x. Pair x (f x)) ` S) \<inter> (S \<times> U))"
by (force simp: image_iff)
- show "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+ show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
by (simp add: U closedin_Int closedin_Times closed_map_fst [OF \<open>compact T\<close>] that eq)
qed
with continuous_closed_graph_gen assms show ?thesis by blast
--- a/src/HOL/Analysis/Tagged_Division.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy Thu Oct 19 17:16:01 2017 +0100
@@ -66,7 +66,7 @@
shows "interior i \<subseteq> interior S"
proof -
have "box a b \<inter> cbox c d = {}"
- using inter_interval_mixed_eq_empty[of c d a b] assms
+ using Int_interval_mixed_eq_empty[of c d a b] assms
unfolding interior_cbox by auto
moreover
have "box a b \<subseteq> cbox c d \<union> S"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Oct 19 17:16:01 2017 +0100
@@ -858,10 +858,15 @@
by (simp add: closedin_def topspace_subtopology)
lemma openin_subtopology_Un:
- "openin (subtopology U T) S \<and> openin (subtopology U u) S
- \<Longrightarrow> openin (subtopology U (T \<union> u)) S"
+ "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
+ \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
by (simp add: openin_subtopology) blast
+lemma closedin_subtopology_Un:
+ "\<lbrakk>closedin (subtopology X T) S; closedin (subtopology X U) S\<rbrakk>
+ \<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
+by (simp add: closedin_subtopology) blast
+
subsubsection \<open>The standard Euclidean topology\<close>
@@ -886,6 +891,8 @@
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)
+declare closed_closedin [symmetric, simp]
+
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
using openI by auto
@@ -913,7 +920,7 @@
by (auto simp: openin_open)
lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
- by (simp add: closedin_subtopology closed_closedin Int_ac)
+ by (simp add: closedin_subtopology Int_ac)
lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> S)"
by (metis closedin_closed)
@@ -965,7 +972,7 @@
~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
openin (subtopology euclidean s) e2 \<and>
s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
- apply (simp add: connected_def openin_open, safe)
+ apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
apply (simp_all, blast+) (* SLOW *)
done
@@ -1032,7 +1039,7 @@
lemma closedin_trans[trans]:
"closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow>
closedin (subtopology euclidean U) S"
- by (auto simp: closedin_closed closed_closedin closed_Inter Int_assoc)
+ by (auto simp: closedin_closed closed_Inter Int_assoc)
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
by (auto simp: closedin_closed intro: closedin_trans)
@@ -5304,9 +5311,9 @@
qed
lemma continuous_on_open:
- "continuous_on s f \<longleftrightarrow>
- (\<forall>t. openin (subtopology euclidean (f ` s)) t \<longrightarrow>
- openin (subtopology euclidean s) {x \<in> s. f x \<in> t})"
+ "continuous_on S f \<longleftrightarrow>
+ (\<forall>T. openin (subtopology euclidean (f ` S)) T \<longrightarrow>
+ openin (subtopology euclidean S) (S \<inter> f -` T))"
unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
@@ -5315,37 +5322,42 @@
assumes "f ` S \<subseteq> T"
shows "continuous_on S f \<longleftrightarrow>
(\<forall>U. openin (subtopology euclidean T) U
- \<longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<in> U})"
+ \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
- apply (auto simp: openin_euclidean_subtopology_iff continuous_on_iff)
+ apply (clarsimp simp: openin_euclidean_subtopology_iff continuous_on_iff)
by (metis assms image_subset_iff)
next
have ope: "openin (subtopology euclidean T) (ball y e \<inter> T)" for y e
by (simp add: Int_commute openin_open_Int)
- assume ?rhs
- then show ?lhs
- apply (clarsimp simp add: continuous_on_iff)
- apply (drule_tac x = "ball (f x) e \<inter> T" in spec)
- apply (clarsimp simp add: ope openin_euclidean_subtopology_iff [of S])
- by (metis (no_types, hide_lams) assms dist_commute dist_self image_subset_iff)
+ assume R [rule_format]: ?rhs
+ show ?lhs
+ proof (clarsimp simp add: continuous_on_iff)
+ fix x and e::real
+ assume "x \<in> S" and "0 < e"
+ then have x: "x \<in> S \<inter> (f -` ball (f x) e \<inter> f -` T)"
+ using assms by auto
+ show "\<exists>d>0. \<forall>x'\<in>S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
+ using R [of "ball (f x) e \<inter> T"] x
+ by (fastforce simp add: ope openin_euclidean_subtopology_iff [of S] dist_commute)
+ qed
qed
lemma continuous_openin_preimage:
fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
shows
"\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk>
- \<Longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+ \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U)"
by (simp add: continuous_on_open_gen)
text \<open>Similarly in terms of closed sets.\<close>
lemma continuous_on_closed:
- "continuous_on s f \<longleftrightarrow>
- (\<forall>t. closedin (subtopology euclidean (f ` s)) t \<longrightarrow>
- closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})"
+ "continuous_on S f \<longleftrightarrow>
+ (\<forall>T. closedin (subtopology euclidean (f ` S)) T \<longrightarrow>
+ closedin (subtopology euclidean S) (S \<inter> f -` T))"
unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
@@ -5354,61 +5366,73 @@
assumes "f ` S \<subseteq> T"
shows "continuous_on S f \<longleftrightarrow>
(\<forall>U. closedin (subtopology euclidean T) U
- \<longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x \<in> U})"
+ \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` U))"
+ (is "?lhs = ?rhs")
proof -
- have *: "U \<subseteq> T \<Longrightarrow> {x \<in> S. f x \<in> T \<and> f x \<notin> U} = S - {x \<in> S. f x \<in> U}" for U
+ have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U
using assms by blast
show ?thesis
- apply (simp add: continuous_on_open_gen [OF assms], safe)
- apply (drule_tac [!] x="T-U" in spec)
- apply (force simp: closedin_def *)
- apply (force simp: openin_closedin_eq *)
- done
+ proof
+ assume L: ?lhs
+ show ?rhs
+ proof clarify
+ fix U
+ assume "closedin (subtopology euclidean T) U"
+ then show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
+ using L unfolding continuous_on_open_gen [OF assms]
+ by (metis * closedin_def inf_le1 topspace_euclidean_subtopology)
+ qed
+ next
+ assume R [rule_format]: ?rhs
+ show ?lhs
+ unfolding continuous_on_open_gen [OF assms]
+ by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology)
+ qed
qed
lemma continuous_closedin_preimage_gen:
fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U"
- shows "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+ shows "closedin (subtopology euclidean S) (S \<inter> f -` U)"
using assms continuous_on_closed_gen by blast
lemma continuous_on_imp_closedin:
assumes "continuous_on S f" "closedin (subtopology euclidean (f ` S)) T"
- shows "closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T}"
+ shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
using assms continuous_on_closed by blast
subsection \<open>Half-global and completely global cases.\<close>
lemma continuous_openin_preimage_gen:
- assumes "continuous_on s f" "open t"
- shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
+ assumes "continuous_on S f" "open T"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` T)"
proof -
- have *: "\<forall>x. x \<in> s \<and> f x \<in> t \<longleftrightarrow> x \<in> s \<and> f x \<in> (t \<inter> f ` s)"
+ have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
by auto
- have "openin (subtopology euclidean (f ` s)) (t \<inter> f ` s)"
- using openin_open_Int[of t "f ` s", OF assms(2)] unfolding openin_open by auto
+ have "openin (subtopology euclidean (f ` S)) (T \<inter> f ` S)"
+ using openin_open_Int[of T "f ` S", OF assms(2)] unfolding openin_open by auto
then show ?thesis
- using assms(1)[unfolded continuous_on_open, THEN spec[where x="t \<inter> f ` s"]]
+ using assms(1)[unfolded continuous_on_open, THEN spec[where x="T \<inter> f ` S"]]
using * by auto
qed
lemma continuous_closedin_preimage:
- assumes "continuous_on s f" and "closed t"
- shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
+ assumes "continuous_on S f" and "closed T"
+ shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
proof -
- have *: "\<forall>x. x \<in> s \<and> f x \<in> t \<longleftrightarrow> x \<in> s \<and> f x \<in> (t \<inter> f ` s)"
+ have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
by auto
- have "closedin (subtopology euclidean (f ` s)) (t \<inter> f ` s)"
- using closedin_closed_Int[of t "f ` s", OF assms(2)]
+ have "closedin (subtopology euclidean (f ` S)) (T \<inter> f ` S)"
+ using closedin_closed_Int[of T "f ` S", OF assms(2)]
by (simp add: Int_commute)
then show ?thesis
- using assms(1)[unfolded continuous_on_closed, THEN spec[where x="t \<inter> f ` s"]]
+ using assms(1)[unfolded continuous_on_closed, THEN spec[where x="T \<inter> f ` S"]]
using * by auto
qed
lemma continuous_openin_preimage_eq:
"continuous_on S f \<longleftrightarrow>
- (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+ (\<forall>T. open T \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T))"
apply safe
apply (simp add: continuous_openin_preimage_gen)
apply (fastforce simp add: continuous_on_open openin_open)
@@ -5416,66 +5440,55 @@
lemma continuous_closedin_preimage_eq:
"continuous_on S f \<longleftrightarrow>
- (\<forall>t. closed t \<longrightarrow> closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+ (\<forall>T. closed T \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` T))"
apply safe
apply (simp add: continuous_closedin_preimage)
apply (fastforce simp add: continuous_on_closed closedin_closed)
done
lemma continuous_open_preimage:
- assumes "continuous_on s f"
- and "open s"
- and "open t"
- shows "open {x \<in> s. f x \<in> t}"
+ assumes contf: "continuous_on S f" and "open S" "open T"
+ shows "open (S \<inter> f -` T)"
proof-
- obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
- using continuous_openin_preimage_gen[OF assms(1,3)] unfolding openin_open by auto
+ obtain U where "open U" "(S \<inter> f -` T) = S \<inter> U"
+ using continuous_openin_preimage_gen[OF contf \<open>open T\<close>]
+ unfolding openin_open by auto
then show ?thesis
- using open_Int[of s T, OF assms(2)] by auto
+ using open_Int[of S U, OF \<open>open S\<close>] by auto
qed
lemma continuous_closed_preimage:
- assumes "continuous_on s f"
- and "closed s"
- and "closed t"
- shows "closed {x \<in> s. f x \<in> t}"
+ assumes contf: "continuous_on S f" and "closed S" "closed T"
+ shows "closed (S \<inter> f -` T)"
proof-
- obtain T where "closed T" "{x \<in> s. f x \<in> t} = s \<inter> T"
- using continuous_closedin_preimage[OF assms(1,3)]
+ obtain U where "closed U" "(S \<inter> f -` T) = S \<inter> U"
+ using continuous_closedin_preimage[OF contf \<open>closed T\<close>]
unfolding closedin_closed by auto
- then show ?thesis using closed_Int[of s T, OF assms(2)] by auto
+ then show ?thesis using closed_Int[of S U, OF \<open>closed S\<close>] by auto
qed
-lemma continuous_open_preimage_univ:
- "open s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open {x. f x \<in> s}"
- using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
-
-lemma continuous_closed_preimage_univ:
- "closed s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed {x. f x \<in> s}"
- using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
-
-lemma continuous_open_vimage: "open s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` s)"
- unfolding vimage_def by (rule continuous_open_preimage_univ)
-
-lemma continuous_closed_vimage: "closed s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` s)"
- unfolding vimage_def by (rule continuous_closed_preimage_univ)
+lemma continuous_open_vimage: "open S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` S)"
+ by (metis continuous_on_eq_continuous_within open_vimage)
+
+lemma continuous_closed_vimage: "closed S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` S)"
+ by (simp add: closed_vimage continuous_on_eq_continuous_within)
lemma interior_image_subset:
assumes "inj f" "\<And>x. continuous (at x) f"
- shows "interior (f ` s) \<subseteq> f ` (interior s)"
+ shows "interior (f ` S) \<subseteq> f ` (interior S)"
proof
- fix x assume "x \<in> interior (f ` s)"
- then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` s" ..
- then have "x \<in> f ` s" by auto
- then obtain y where y: "y \<in> s" "x = f y" by auto
- have "open (vimage f T)"
- using assms \<open>open T\<close> by (metis continuous_open_vimage)
+ fix x assume "x \<in> interior (f ` S)"
+ then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` S" ..
+ then have "x \<in> f ` S" by auto
+ then obtain y where y: "y \<in> S" "x = f y" by auto
+ have "open (f -` T)"
+ using assms \<open>open T\<close> by (simp add: continuous_at_imp_continuous_on open_vimage)
moreover have "y \<in> vimage f T"
using \<open>x = f y\<close> \<open>x \<in> T\<close> by simp
- moreover have "vimage f T \<subseteq> s"
- using \<open>T \<subseteq> image f s\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto
- ultimately have "y \<in> interior s" ..
- with \<open>x = f y\<close> show "x \<in> f ` interior s" ..
+ moreover have "vimage f T \<subseteq> S"
+ using \<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto
+ ultimately have "y \<in> interior S" ..
+ with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
qed
subsection \<open>Topological properties of linear functions.\<close>
@@ -5853,7 +5866,7 @@
by auto
qed
-lemma inter_interval_mixed_eq_empty:
+lemma Int_interval_mixed_eq_empty:
fixes a :: "'a::euclidean_space"
assumes "box c d \<noteq> {}"
shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
--- a/src/HOL/Analysis/Winding_Numbers.thy Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Winding_Numbers.thy Thu Oct 19 17:16:01 2017 +0100
@@ -740,22 +740,20 @@
case True
have "path \<gamma>"
by (simp add: assms simple_path_imp_path)
- then obtain k where k: "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = k"
+ then have const: "winding_number \<gamma> constant_on inside(path_image \<gamma>)"
proof (rule winding_number_constant)
show "connected (inside(path_image \<gamma>))"
by (simp add: Jordan_inside_outside True assms)
qed (use inside_no_overlap True in auto)
obtain z where zin: "z \<in> inside (path_image \<gamma>)" and z1: "cmod (winding_number \<gamma> z) = 1"
using simple_closed_path_wn3 [of \<gamma>] True assms by blast
- with k have "winding_number \<gamma> z = k"
- by blast
have "winding_number \<gamma> z \<in> \<int>"
using zin integer_winding_number [OF \<open>path \<gamma>\<close> True] inside_def by blast
with z1 consider "winding_number \<gamma> z = 1" | "winding_number \<gamma> z = -1"
apply (auto simp: Ints_def abs_if split: if_split_asm)
by (metis of_int_1 of_int_eq_iff of_int_minus)
- then show ?thesis
- using that \<open>winding_number \<gamma> z = k\<close> k by auto
+ with that const zin show ?thesis
+ unfolding constant_on_def by metis
next
case False
then show ?thesis