--- a/NEWS Sun Oct 09 16:27:01 2016 +0200
+++ b/NEWS Mon Oct 10 15:45:41 2016 +0100
@@ -432,7 +432,7 @@
"~~/src/HOL/Library/FinFun_Syntax".
* HOL-Library: theory Multiset_Permutations (executably) defines the set of
-permutations of a given set or multiset, i.e. the set of all lists that
+permutations of a given set or multiset, i.e. the set of all lists that
contain every element of the carrier (multi-)set exactly once.
* HOL-Library: multiset membership is now expressed using set_mset
@@ -485,8 +485,7 @@
and the Krein–Milman Minkowski theorem.
* HOL-Analysis: Numerous results ported from the HOL Light libraries:
-homeomorphisms, continuous function extensions and other advanced topics
-in topology
+homeomorphisms, continuous function extensions, invariance of domain.
* HOL-Probability: the type of emeasure and nn_integral was changed from
ereal to ennreal, INCOMPATIBILITY.
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Oct 10 15:45:41 2016 +0100
@@ -2021,6 +2021,58 @@
done
qed
+proposition frontier_subset_retraction:
+ fixes S :: "'a::euclidean_space set"
+ assumes "bounded S" and fros: "frontier S \<subseteq> T"
+ and contf: "continuous_on (closure S) f"
+ and fim: "f ` S \<subseteq> T"
+ and fid: "\<And>x. x \<in> T \<Longrightarrow> f x = x"
+ shows "S \<subseteq> T"
+proof (rule ccontr)
+ assume "\<not> S \<subseteq> T"
+ then obtain a where "a \<in> S" "a \<notin> T" by blast
+ define g where "g \<equiv> \<lambda>z. if z \<in> closure S then f z else z"
+ have "continuous_on (closure S \<union> closure(-S)) g"
+ unfolding g_def
+ apply (rule continuous_on_cases)
+ using fros fid frontier_closures
+ apply (auto simp: contf continuous_on_id)
+ done
+ moreover have "closure S \<union> closure(- S) = UNIV"
+ using closure_Un by fastforce
+ ultimately have contg: "continuous_on UNIV g" by metis
+ obtain B where "0 < B" and B: "closure S \<subseteq> ball a B"
+ using \<open>bounded S\<close> bounded_subset_ballD by blast
+ have notga: "g x \<noteq> a" for x
+ unfolding g_def using fros fim \<open>a \<notin> T\<close>
+ apply (auto simp: frontier_def)
+ using fid interior_subset apply fastforce
+ by (simp add: \<open>a \<in> S\<close> closure_def)
+ define h where "h \<equiv> (\<lambda>y. a + (B / norm(y - a)) *\<^sub>R (y - a)) \<circ> g"
+ have "\<not> (frontier (cball a B) retract_of (cball a B))"
+ by (metis no_retraction_cball \<open>0 < B\<close>)
+ then have "\<And>k. \<not> retraction (cball a B) (frontier (cball a B)) k"
+ by (simp add: retract_of_def)
+ moreover have "retraction (cball a B) (frontier (cball a B)) h"
+ unfolding retraction_def
+ proof (intro conjI ballI)
+ show "frontier (cball a B) \<subseteq> cball a B"
+ by (force simp:)
+ show "continuous_on (cball a B) h"
+ unfolding h_def
+ apply (intro continuous_intros)
+ using contg continuous_on_subset notga apply auto
+ done
+ show "h ` cball a B \<subseteq> frontier (cball a B)"
+ using \<open>0 < B\<close> by (auto simp: h_def notga dist_norm)
+ show "\<And>x. x \<in> frontier (cball a B) \<Longrightarrow> h x = x"
+ apply (auto simp: h_def algebra_simps)
+ apply (simp add: vector_add_divide_simps notga)
+ by (metis (no_types, hide_lams) B add.commute dist_commute dist_norm g_def mem_ball not_less_iff_gr_or_eq subset_eq)
+ qed
+ ultimately show False by simp
+qed
+
subsection\<open>Retractions\<close>
lemma retraction:
@@ -3192,7 +3244,7 @@
shows "S retract_of UNIV \<longleftrightarrow> AR S \<and> closed S"
by (metis AR_ANR AR_imp_retract ENR_def ENR_imp_ANR closed_UNIV closed_closedin contractible_UNIV empty_not_UNIV open_UNIV retract_of_closed retract_of_contractible retract_of_empty(1) subtopology_UNIV)
-lemma compact_AR [simp]:
+lemma compact_AR:
fixes S :: "'a::euclidean_space set"
shows "compact S \<and> AR S \<longleftrightarrow> compact S \<and> S retract_of UNIV"
using compact_imp_closed retract_of_UNIV by blast
@@ -3893,7 +3945,7 @@
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 add: open_openin)
+ apply simp
done
qed
@@ -4189,5 +4241,89 @@
then show ?thesis by blast
qed
+subsection\<open>The complement of a set and path-connectedness\<close>
+
+text\<open>Complement in dimension N > 1 of set homeomorphic to any interval in
+ any dimension is (path-)connected. This naively generalizes the argument
+ in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer fixed point theorem",
+American Mathematical Monthly 1984.\<close>
+
+lemma unbounded_components_complement_absolute_retract:
+ fixes S :: "'a::euclidean_space set"
+ assumes C: "C \<in> components(- S)" and S: "compact S" "AR S"
+ shows "\<not> bounded C"
+proof -
+ obtain y where y: "C = connected_component_set (- S) y" and "y \<notin> S"
+ using C by (auto simp: components_def)
+ have "open(- S)"
+ using S by (simp add: closed_open compact_eq_bounded_closed)
+ have "S retract_of UNIV"
+ using S compact_AR by blast
+ then obtain r where contr: "continuous_on UNIV r" and ontor: "range r \<subseteq> S"
+ and r: "\<And>x. x \<in> S \<Longrightarrow> r x = x"
+ by (auto simp: retract_of_def retraction_def)
+ show ?thesis
+ proof
+ assume "bounded C"
+ have "connected_component_set (- S) y \<subseteq> S"
+ proof (rule frontier_subset_retraction)
+ show "bounded (connected_component_set (- S) y)"
+ using \<open>bounded C\<close> y by blast
+ show "frontier (connected_component_set (- S) y) \<subseteq> S"
+ using C \<open>compact S\<close> compact_eq_bounded_closed frontier_of_components_closed_complement y by blast
+ show "continuous_on (closure (connected_component_set (- S) y)) r"
+ by (blast intro: continuous_on_subset [OF contr])
+ qed (use ontor r in auto)
+ with \<open>y \<notin> S\<close> show False by force
+ qed
+qed
+
+lemma connected_complement_absolute_retract:
+ fixes S :: "'a::euclidean_space set"
+ assumes S: "compact S" "AR S" and 2: "2 \<le> DIM('a)"
+ shows "connected(- S)"
+proof -
+ have "S retract_of UNIV"
+ using S compact_AR by blast
+ show ?thesis
+ apply (clarsimp simp: connected_iff_connected_component_eq)
+ apply (rule cobounded_unique_unbounded_component [OF _ 2])
+ apply (simp add: \<open>compact S\<close> compact_imp_bounded)
+ apply (meson ComplI S componentsI unbounded_components_complement_absolute_retract)+
+ done
+qed
+
+lemma path_connected_complement_absolute_retract:
+ fixes S :: "'a::euclidean_space set"
+ assumes "compact S" "AR S" "2 \<le> DIM('a)"
+ shows "path_connected(- S)"
+ using connected_complement_absolute_retract [OF assms]
+ using \<open>compact S\<close> compact_eq_bounded_closed connected_open_path_connected by blast
+
+theorem connected_complement_homeomorphic_convex_compact:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes hom: "S homeomorphic T" and T: "convex T" "compact T" and 2: "2 \<le> DIM('a)"
+ shows "connected(- S)"
+proof (cases "S = {}")
+ case True
+ then show ?thesis
+ by (simp add: connected_UNIV)
+next
+ case False
+ show ?thesis
+ proof (rule connected_complement_absolute_retract)
+ show "compact S"
+ using \<open>compact T\<close> hom homeomorphic_compactness by auto
+ show "AR S"
+ by (meson AR_ANR False \<open>convex T\<close> convex_imp_ANR convex_imp_contractible hom homeomorphic_ANR_iff_ANR homeomorphic_contractible_eq)
+ qed (rule 2)
+qed
+
+corollary path_connected_complement_homeomorphic_convex_compact:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes hom: "S homeomorphic T" "convex T" "compact T" "2 \<le> DIM('a)"
+ shows "path_connected(- S)"
+ 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/Convex_Euclidean_Space.thy Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Oct 10 15:45:41 2016 +0100
@@ -2384,7 +2384,7 @@
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: open_openin closed_closedin, force)
+ apply (force simp add: closed_closedin, force)
done
corollary compact_open:
@@ -12085,15 +12085,11 @@
show "{x \<in> U. 0 < f x} \<inter> {x \<in> U. f x < 0} = {}"
by auto
have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {0<..}}"
- apply (rule continuous_openin_preimage [where T=UNIV])
- apply (simp_all add: contf)
- using open_greaterThan open_openin by blast
+ 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}}"
- apply (rule continuous_openin_preimage [where T=UNIV])
- apply (simp_all add: contf)
- using open_lessThan open_openin by blast
+ 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 "S \<subseteq> {x \<in> U. 0 < f x}"
@@ -12671,7 +12667,7 @@
apply safe
apply (metis DIM_positive DIM_real card_ge_dim_independent contra_subsetD dim_empty dim_insert dim_singleton empty_subsetI independent_empty less_not_refl zero_le)
by (metis dim_singleton dim_subset le_0_eq)
-
+
lemma aff_dim_insert:
fixes a :: "'a::euclidean_space"
shows "aff_dim (insert a S) = (if a \<in> affine hull S then aff_dim S else aff_dim S + 1)"
@@ -13594,6 +13590,24 @@
shows "aff_dim S < DIM('a) \<longleftrightarrow> (affine hull S \<noteq> UNIV)"
by (metis (no_types) aff_dim_affine_hull aff_dim_le_DIM aff_dim_UNIV affine_hull_UNIV less_le)
+
+lemma dim_Times:
+ fixes S :: "'a :: euclidean_space set" and T :: "'a set"
+ assumes "subspace S" "subspace T"
+ shows "dim(S \<times> T) = dim S + dim T"
+proof -
+ have ss: "subspace ((\<lambda>x. (x, 0)) ` S)" "subspace (Pair 0 ` T)"
+ by (rule subspace_linear_image, unfold_locales, auto simp: assms)+
+ have "dim(S \<times> T) = dim({u + v |u v. u \<in> (\<lambda>x. (x, 0)) ` S \<and> v \<in> Pair 0 ` T})"
+ by (simp add: Times_eq_image_sum)
+ moreover have "dim ((\<lambda>x. (x, 0::'a)) ` S) = dim S" "dim (Pair (0::'a) ` T) = dim T"
+ by (auto simp: additive.intro linear.intro linear_axioms.intro inj_on_def intro: dim_image_eq)
+ moreover have "dim ((\<lambda>x. (x, 0)) ` S \<inter> Pair 0 ` T) = 0"
+ by (subst dim_eq_0) (force simp: zero_prod_def)
+ ultimately show ?thesis
+ using dim_sums_Int [OF ss] by linarith
+qed
+
subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
lemma span_delete_0 [simp]: "span(S - {0}) = span S"
@@ -13934,6 +13948,74 @@
by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq orthogonal_commute orthogonal_def)
qed
+lemma aff_dim_openin:
+ fixes S :: "'a::euclidean_space set"
+ assumes ope: "openin (subtopology euclidean T) S" and "affine T" "S \<noteq> {}"
+ shows "aff_dim S = aff_dim T"
+proof -
+ show ?thesis
+ proof (rule order_antisym)
+ show "aff_dim S \<le> aff_dim T"
+ by (blast intro: aff_dim_subset [OF openin_imp_subset] ope)
+ next
+ obtain a where "a \<in> S"
+ using \<open>S \<noteq> {}\<close> by blast
+ have "S \<subseteq> T"
+ using ope openin_imp_subset by auto
+ then have "a \<in> T"
+ using \<open>a \<in> S\<close> by auto
+ then have subT': "subspace ((\<lambda>x. - a + x) ` T)"
+ using affine_diffs_subspace \<open>affine T\<close> by auto
+ then obtain B where Bsub: "B \<subseteq> ((\<lambda>x. - a + x) ` T)" and po: "pairwise orthogonal B"
+ and eq1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1" and "independent B"
+ and cardB: "card B = dim ((\<lambda>x. - a + x) ` T)"
+ and spanB: "span B = ((\<lambda>x. - a + x) ` T)"
+ by (rule orthonormal_basis_subspace) auto
+ obtain e where "0 < e" and e: "cball a e \<inter> T \<subseteq> S"
+ by (meson \<open>a \<in> S\<close> openin_contains_cball ope)
+ have "aff_dim T = aff_dim ((\<lambda>x. - a + x) ` T)"
+ by (metis aff_dim_translation_eq)
+ also have "... = dim ((\<lambda>x. - a + x) ` T)"
+ using aff_dim_subspace subT' by blast
+ also have "... = card B"
+ by (simp add: cardB)
+ also have "... = card ((\<lambda>x. e *\<^sub>R x) ` B)"
+ using \<open>0 < e\<close> by (force simp: inj_on_def card_image)
+ also have "... \<le> dim ((\<lambda>x. - a + x) ` S)"
+ proof (simp, rule independent_card_le_dim)
+ have e': "cball 0 e \<inter> (\<lambda>x. x - a) ` T \<subseteq> (\<lambda>x. x - a) ` S"
+ using e by (auto simp: dist_norm norm_minus_commute subset_eq)
+ have "(\<lambda>x. e *\<^sub>R x) ` B \<subseteq> cball 0 e \<inter> (\<lambda>x. x - a) ` T"
+ using Bsub \<open>0 < e\<close> eq1 subT' \<open>a \<in> T\<close> by (auto simp: subspace_def)
+ then show "(\<lambda>x. e *\<^sub>R x) ` B \<subseteq> (\<lambda>x. x - a) ` S"
+ using e' by blast
+ show "independent ((\<lambda>x. e *\<^sub>R x) ` B)"
+ using \<open>independent B\<close>
+ apply (rule independent_injective_image, simp)
+ by (metis \<open>0 < e\<close> injective_scaleR less_irrefl)
+ qed
+ also have "... = aff_dim S"
+ using \<open>a \<in> S\<close> aff_dim_eq_dim hull_inc by force
+ finally show "aff_dim T \<le> aff_dim S" .
+ qed
+qed
+
+lemma dim_openin:
+ fixes S :: "'a::euclidean_space set"
+ assumes ope: "openin (subtopology euclidean T) S" and "subspace T" "S \<noteq> {}"
+ shows "dim S = dim T"
+proof (rule order_antisym)
+ show "dim S \<le> dim T"
+ by (metis ope dim_subset openin_subset topspace_euclidean_subtopology)
+next
+ have "dim T = aff_dim S"
+ using aff_dim_openin
+ by (metis aff_dim_subspace \<open>subspace T\<close> \<open>S \<noteq> {}\<close> ope subspace_affine)
+ also have "... \<le> dim S"
+ by (metis aff_dim_subset aff_dim_subspace dim_span span_inc subspace_span)
+ finally show "dim T \<le> dim S" by simp
+qed
+
subsection\<open>Parallel slices, etc.\<close>
text\<open> If we take a slice out of a set, we can do it perpendicularly,
@@ -14249,7 +14331,6 @@
done
qed
-
corollary paracompact_closedin:
fixes S :: "'a :: euclidean_space set"
assumes cin: "closedin (subtopology euclidean U) S"
--- a/src/HOL/Analysis/FurtherTopology.thy Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/FurtherTopology.thy Mon Oct 10 15:45:41 2016 +0100
@@ -1,4 +1,4 @@
-section \<open>Extending Continous Maps, etc..\<close>
+section \<open>Extending Continous Maps, Invariance of Domain, etc..\<close>
text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
@@ -1888,4 +1888,468 @@
done
qed
+subsection\<open> Invariance of domain and corollaries\<close>
+
+lemma invariance_of_domain_ball:
+ fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
+ assumes contf: "continuous_on (cball a r) f" and "0 < r"
+ and inj: "inj_on f (cball a r)"
+ shows "open(f ` ball a r)"
+proof (cases "DIM('a) = 1")
+ case True
+ obtain h::"'a\<Rightarrow>real" and k
+ where "linear h" "linear k" "h ` UNIV = UNIV" "k ` UNIV = UNIV"
+ "\<And>x. norm(h x) = norm x" "\<And>x. norm(k x) = norm x"
+ "\<And>x. k(h x) = x" "\<And>x. h(k x) = x"
+ apply (rule isomorphisms_UNIV_UNIV [where 'M='a and 'N=real])
+ using True
+ apply force
+ by (metis UNIV_I UNIV_eq_I imageI)
+ have cont: "continuous_on S h" "continuous_on T k" for S T
+ by (simp_all add: \<open>linear h\<close> \<open>linear k\<close> linear_continuous_on linear_linear)
+ have "continuous_on (h ` cball a r) (h \<circ> f \<circ> k)"
+ apply (intro continuous_on_compose cont continuous_on_subset [OF contf])
+ apply (auto simp: \<open>\<And>x. k (h x) = x\<close>)
+ done
+ moreover have "is_interval (h ` cball a r)"
+ by (simp add: is_interval_connected_1 \<open>linear h\<close> linear_continuous_on linear_linear connected_continuous_image)
+ moreover have "inj_on (h \<circ> f \<circ> k) (h ` cball a r)"
+ using inj by (simp add: inj_on_def) (metis \<open>\<And>x. k (h x) = x\<close>)
+ ultimately have *: "\<And>T. \<lbrakk>open T; T \<subseteq> h ` cball a r\<rbrakk> \<Longrightarrow> open ((h \<circ> f \<circ> k) ` T)"
+ using injective_eq_1d_open_map_UNIV by blast
+ have "open ((h \<circ> f \<circ> k) ` (h ` ball a r))"
+ by (rule *) (auto simp: \<open>linear h\<close> \<open>range h = UNIV\<close> open_surjective_linear_image)
+ then have "open ((h \<circ> f) ` ball a r)"
+ by (simp add: image_comp \<open>\<And>x. k (h x) = x\<close> cong: image_cong)
+ then show ?thesis
+ apply (simp add: image_comp [symmetric])
+ apply (metis open_bijective_linear_image_eq \<open>linear h\<close> \<open>\<And>x. k (h x) = x\<close> \<open>range h = UNIV\<close> bijI inj_on_def)
+ done
+next
+ case False
+ then have 2: "DIM('a) \<ge> 2"
+ by (metis DIM_ge_Suc0 One_nat_def Suc_1 antisym not_less_eq_eq)
+ have fimsub: "f ` ball a r \<subseteq> - f ` sphere a r"
+ using inj by clarsimp (metis inj_onD less_eq_real_def mem_cball order_less_irrefl)
+ have hom: "f ` sphere a r homeomorphic sphere a r"
+ by (meson compact_sphere contf continuous_on_subset homeomorphic_compact homeomorphic_sym inj inj_on_subset sphere_cball)
+ then have nconn: "\<not> connected (- f ` sphere a r)"
+ by (rule Jordan_Brouwer_separation) (auto simp: \<open>0 < r\<close>)
+ obtain C where C: "C \<in> components (- f ` sphere a r)" and "bounded C"
+ apply (rule cobounded_has_bounded_component [OF _ nconn])
+ apply (simp_all add: 2)
+ by (meson compact_imp_bounded compact_continuous_image_eq compact_sphere contf inj sphere_cball)
+ moreover have "f ` (ball a r) = C"
+ proof
+ have "C \<noteq> {}"
+ by (rule in_components_nonempty [OF C])
+ show "C \<subseteq> f ` ball a r"
+ proof (rule ccontr)
+ assume nonsub: "\<not> C \<subseteq> f ` ball a r"
+ have "- f ` cball a r \<subseteq> C"
+ proof (rule components_maximal [OF C])
+ have "f ` cball a r homeomorphic cball a r"
+ using compact_cball contf homeomorphic_compact homeomorphic_sym inj by blast
+ then show "connected (- f ` cball a r)"
+ by (auto intro: connected_complement_homeomorphic_convex_compact 2)
+ show "- f ` cball a r \<subseteq> - f ` sphere a r"
+ by auto
+ then show "C \<inter> - f ` cball a r \<noteq> {}"
+ using \<open>C \<noteq> {}\<close> in_components_subset [OF C] nonsub
+ using image_iff by fastforce
+ qed
+ then have "bounded (- f ` cball a r)"
+ using bounded_subset \<open>bounded C\<close> by auto
+ then have "\<not> bounded (f ` cball a r)"
+ using cobounded_imp_unbounded by blast
+ then show "False"
+ using compact_continuous_image [OF contf] compact_cball compact_imp_bounded by blast
+ qed
+ with \<open>C \<noteq> {}\<close> have "C \<inter> f ` ball a r \<noteq> {}"
+ by (simp add: inf.absorb_iff1)
+ then show "f ` ball a r \<subseteq> C"
+ by (metis components_maximal [OF C _ fimsub] connected_continuous_image ball_subset_cball connected_ball contf continuous_on_subset)
+ qed
+ moreover have "open (- f ` sphere a r)"
+ using hom compact_eq_bounded_closed compact_sphere homeomorphic_compactness by blast
+ ultimately show ?thesis
+ using open_components by blast
+qed
+
+
+text\<open>Proved by L. E. J. Brouwer (1912)\<close>
+theorem invariance_of_domain:
+ fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
+ assumes "continuous_on S f" "open S" "inj_on f S"
+ shows "open(f ` S)"
+ unfolding open_subopen [of "f`S"]
+proof clarify
+ fix a
+ assume "a \<in> S"
+ obtain \<delta> where "\<delta> > 0" and \<delta>: "cball a \<delta> \<subseteq> S"
+ using \<open>open S\<close> \<open>a \<in> S\<close> open_contains_cball_eq by blast
+ show "\<exists>T. open T \<and> f a \<in> T \<and> T \<subseteq> f ` S"
+ proof (intro exI conjI)
+ show "open (f ` (ball a \<delta>))"
+ by (meson \<delta> \<open>0 < \<delta>\<close> assms continuous_on_subset inj_on_subset invariance_of_domain_ball)
+ show "f a \<in> f ` ball a \<delta>"
+ by (simp add: \<open>0 < \<delta>\<close>)
+ show "f ` ball a \<delta> \<subseteq> f ` S"
+ using \<delta> ball_subset_cball by blast
+ qed
+qed
+
+lemma inv_of_domain_ss0:
+ fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
+ assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
+ and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)"
+ and ope: "openin (subtopology euclidean S) U"
+ shows "openin (subtopology euclidean S) (f ` U)"
+proof -
+ have "U \<subseteq> S"
+ using ope openin_imp_subset by blast
+ have "(UNIV::'b set) homeomorphic S"
+ by (simp add: \<open>subspace S\<close> dimS dim_UNIV homeomorphic_subspaces)
+ then obtain h k where homhk: "homeomorphism (UNIV::'b set) S h k"
+ using homeomorphic_def by blast
+ have homkh: "homeomorphism S (k ` S) k h"
+ using homhk homeomorphism_image2 homeomorphism_sym by fastforce
+ have "open ((k \<circ> f \<circ> h) ` k ` U)"
+ proof (rule invariance_of_domain)
+ show "continuous_on (k ` U) (k \<circ> f \<circ> h)"
+ proof (intro continuous_intros)
+ show "continuous_on (k ` U) h"
+ by (meson continuous_on_subset [OF homeomorphism_cont1 [OF homhk]] top_greatest)
+ show "continuous_on (h ` k ` U) f"
+ apply (rule continuous_on_subset [OF contf], clarify)
+ apply (metis homhk homeomorphism_def ope openin_imp_subset rev_subsetD)
+ done
+ show "continuous_on (f ` h ` k ` U) k"
+ apply (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]])
+ using fim homhk homeomorphism_apply2 ope openin_subset by fastforce
+ qed
+ have ope_iff: "\<And>T. open T \<longleftrightarrow> openin (subtopology euclidean (k ` S)) T"
+ using homhk homeomorphism_image2 open_openin by fastforce
+ show "open (k ` U)"
+ by (simp add: ope_iff homeomorphism_imp_open_map [OF homkh ope])
+ show "inj_on (k \<circ> f \<circ> h) (k ` U)"
+ apply (clarsimp simp: inj_on_def)
+ by (metis subsetD fim homeomorphism_apply2 [OF homhk] image_subset_iff inj_on_eq_iff injf \<open>U \<subseteq> S\<close>)
+ qed
+ moreover
+ have eq: "f ` U = h ` (k \<circ> f \<circ> h \<circ> k) ` U"
+ apply (auto simp: image_comp [symmetric])
+ apply (metis homkh \<open>U \<subseteq> S\<close> fim homeomorphism_image2 homeomorphism_of_subsets homhk imageI subset_UNIV)
+ by (metis \<open>U \<subseteq> S\<close> subsetD fim homeomorphism_def homhk image_eqI)
+ ultimately show ?thesis
+ by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
+qed
+
+lemma inv_of_domain_ss1:
+ fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
+ assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
+ and "subspace S"
+ and ope: "openin (subtopology euclidean S) U"
+ shows "openin (subtopology euclidean S) (f ` U)"
+proof -
+ define S' where "S' \<equiv> {y. \<forall>x \<in> S. orthogonal x y}"
+ have "subspace S'"
+ by (simp add: S'_def subspace_orthogonal_to_vectors)
+ define g where "g \<equiv> \<lambda>z::'a*'a. ((f \<circ> fst)z, snd z)"
+ have "openin (subtopology euclidean (S \<times> S')) (g ` (U \<times> S'))"
+ proof (rule inv_of_domain_ss0)
+ show "continuous_on (U \<times> S') g"
+ apply (simp add: g_def)
+ apply (intro continuous_intros continuous_on_compose2 [OF contf continuous_on_fst], auto)
+ done
+ show "g ` (U \<times> S') \<subseteq> S \<times> S'"
+ using fim by (auto simp: g_def)
+ show "inj_on g (U \<times> S')"
+ using injf by (auto simp: g_def inj_on_def)
+ show "subspace (S \<times> S')"
+ by (simp add: \<open>subspace S'\<close> \<open>subspace S\<close> subspace_Times)
+ show "openin (subtopology euclidean (S \<times> S')) (U \<times> S')"
+ by (simp add: openin_Times [OF ope])
+ have "dim (S \<times> S') = dim S + dim S'"
+ by (simp add: \<open>subspace S'\<close> \<open>subspace S\<close> dim_Times)
+ also have "... = DIM('a)"
+ using dim_subspace_orthogonal_to_vectors [OF \<open>subspace S\<close> subspace_UNIV]
+ by (simp add: add.commute S'_def)
+ finally show "dim (S \<times> S') = DIM('a)" .
+ qed
+ moreover have "g ` (U \<times> S') = f ` U \<times> S'"
+ by (auto simp: g_def image_iff)
+ moreover have "0 \<in> S'"
+ using \<open>subspace S'\<close> subspace_affine by blast
+ ultimately show ?thesis
+ by (auto simp: openin_Times_eq)
+qed
+
+
+corollary invariance_of_domain_subspaces:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes ope: "openin (subtopology euclidean U) S"
+ and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and injf: "inj_on f S"
+ shows "openin (subtopology euclidean V) (f ` S)"
+proof -
+ obtain V' where "subspace V'" "V' \<subseteq> U" "dim V' = dim V"
+ using choose_subspace_of_subspace [OF VU]
+ by (metis span_eq \<open>subspace U\<close>)
+ then have "V homeomorphic V'"
+ by (simp add: \<open>subspace V\<close> homeomorphic_subspaces)
+ then obtain h k where homhk: "homeomorphism V V' h k"
+ using homeomorphic_def by blast
+ have eq: "f ` S = k ` (h \<circ> f) ` S"
+ proof -
+ have "k ` h ` f ` S = f ` S"
+ by (meson fim homeomorphism_def homeomorphism_of_subsets homhk subset_refl)
+ then show ?thesis
+ by (simp add: image_comp)
+ qed
+ show ?thesis
+ unfolding eq
+ proof (rule homeomorphism_imp_open_map)
+ show homkh: "homeomorphism V' V k h"
+ by (simp add: homeomorphism_symD homhk)
+ have hfV': "(h \<circ> f) ` S \<subseteq> V'"
+ using fim homeomorphism_image1 homhk by fastforce
+ moreover have "openin (subtopology euclidean U) ((h \<circ> f) ` S)"
+ proof (rule inv_of_domain_ss1)
+ show "continuous_on S (h \<circ> f)"
+ by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
+ show "inj_on (h \<circ> f) S"
+ apply (clarsimp simp: inj_on_def)
+ by (metis fim homeomorphism_apply2 [OF homkh] image_subset_iff inj_onD injf)
+ show "(h \<circ> f) ` S \<subseteq> U"
+ using \<open>V' \<subseteq> U\<close> hfV' by auto
+ qed (auto simp: assms)
+ ultimately show "openin (subtopology euclidean V') ((h \<circ> f) ` S)"
+ using openin_subset_trans \<open>V' \<subseteq> U\<close> by force
+ qed
+qed
+
+corollary invariance_of_dimension_subspaces:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes ope: "openin (subtopology euclidean U) S"
+ and "subspace U" "subspace V"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and injf: "inj_on f S" and "S \<noteq> {}"
+ shows "dim U \<le> dim V"
+proof -
+ have "False" if "dim V < dim U"
+ proof -
+ obtain T where "subspace T" "T \<subseteq> U" "dim T = dim V"
+ using choose_subspace_of_subspace [of "dim V" U]
+ by (metis span_eq \<open>subspace U\<close> \<open>dim V < dim U\<close> linear not_le)
+ then have "V homeomorphic T"
+ by (simp add: \<open>subspace V\<close> homeomorphic_subspaces)
+ then obtain h k where homhk: "homeomorphism V T h k"
+ using homeomorphic_def by blast
+ have "continuous_on S (h \<circ> f)"
+ by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
+ moreover have "(h \<circ> f) ` S \<subseteq> U"
+ using \<open>T \<subseteq> U\<close> fim homeomorphism_image1 homhk by fastforce
+ moreover have "inj_on (h \<circ> f) S"
+ apply (clarsimp simp: inj_on_def)
+ by (metis fim homeomorphism_apply1 homhk image_subset_iff inj_onD injf)
+ ultimately have ope_hf: "openin (subtopology euclidean U) ((h \<circ> f) ` S)"
+ using invariance_of_domain_subspaces [OF ope \<open>subspace U\<close> \<open>subspace U\<close>] by auto
+ have "(h \<circ> f) ` S \<subseteq> T"
+ using fim homeomorphism_image1 homhk by fastforce
+ then show ?thesis
+ by (metis dim_openin \<open>dim T = dim V\<close> ope_hf \<open>subspace U\<close> \<open>S \<noteq> {}\<close> dim_subset image_is_empty not_le that)
+ qed
+ then show ?thesis
+ using not_less by blast
+qed
+
+corollary invariance_of_domain_affine_sets:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes ope: "openin (subtopology euclidean U) S"
+ and aff: "affine U" "affine V" "aff_dim V \<le> aff_dim U"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and injf: "inj_on f S"
+ shows "openin (subtopology euclidean V) (f ` S)"
+proof (cases "S = {}")
+ case True
+ then show ?thesis by auto
+next
+ case False
+ obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
+ using False fim ope openin_contains_cball by fastforce
+ have "openin (subtopology euclidean (op + (- b) ` V)) ((op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S)"
+ proof (rule invariance_of_domain_subspaces)
+ show "openin (subtopology euclidean (op + (- a) ` U)) (op + (- a) ` S)"
+ by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
+ show "subspace (op + (- a) ` U)"
+ by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace \<open>affine U\<close>)
+ show "subspace (op + (- b) ` V)"
+ by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace \<open>affine V\<close>)
+ show "dim (op + (- b) ` V) \<le> dim (op + (- a) ` U)"
+ by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
+ show "continuous_on (op + (- a) ` S) (op + (- b) \<circ> f \<circ> op + a)"
+ by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
+ show "(op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S \<subseteq> op + (- b) ` V"
+ using fim by auto
+ show "inj_on (op + (- b) \<circ> f \<circ> op + a) (op + (- a) ` S)"
+ by (auto simp: inj_on_def) (meson inj_onD injf)
+ qed
+ then show ?thesis
+ by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois)
+qed
+
+corollary invariance_of_dimension_affine_sets:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes ope: "openin (subtopology euclidean U) S"
+ and aff: "affine U" "affine V"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and injf: "inj_on f S" and "S \<noteq> {}"
+ shows "aff_dim U \<le> aff_dim V"
+proof -
+ obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
+ using \<open>S \<noteq> {}\<close> fim ope openin_contains_cball by fastforce
+ have "dim (op + (- a) ` U) \<le> dim (op + (- b) ` V)"
+ proof (rule invariance_of_dimension_subspaces)
+ show "openin (subtopology euclidean (op + (- a) ` U)) (op + (- a) ` S)"
+ by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
+ show "subspace (op + (- a) ` U)"
+ by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace \<open>affine U\<close>)
+ show "subspace (op + (- b) ` V)"
+ by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace \<open>affine V\<close>)
+ show "continuous_on (op + (- a) ` S) (op + (- b) \<circ> f \<circ> op + a)"
+ by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
+ show "(op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S \<subseteq> op + (- b) ` V"
+ using fim by auto
+ show "inj_on (op + (- b) \<circ> f \<circ> op + a) (op + (- a) ` S)"
+ by (auto simp: inj_on_def) (meson inj_onD injf)
+ qed (use \<open>S \<noteq> {}\<close> in auto)
+ then show ?thesis
+ by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
+qed
+
+corollary invariance_of_dimension:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes contf: "continuous_on S f" and "open S"
+ and injf: "inj_on f S" and "S \<noteq> {}"
+ shows "DIM('a) \<le> DIM('b)"
+ using invariance_of_dimension_subspaces [of UNIV S UNIV f] assms
+ by auto
+
+
+corollary continuous_injective_image_subspace_dim_le:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "subspace S" "subspace T"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
+ and injf: "inj_on f S"
+ shows "dim S \<le> dim T"
+ apply (rule invariance_of_dimension_subspaces [of S S _ f])
+ using assms by (auto simp: subspace_affine)
+
+lemma invariance_of_dimension_convex_domain:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "convex S"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> affine hull T"
+ and injf: "inj_on f S"
+ shows "aff_dim S \<le> aff_dim T"
+proof (cases "S = {}")
+ case True
+ then show ?thesis by (simp add: aff_dim_geq)
+next
+ case False
+ have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
+ proof (rule invariance_of_dimension_affine_sets)
+ show "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
+ by (simp add: openin_rel_interior)
+ show "continuous_on (rel_interior S) f"
+ using contf continuous_on_subset rel_interior_subset by blast
+ show "f ` rel_interior S \<subseteq> affine hull T"
+ using fim rel_interior_subset by blast
+ show "inj_on f (rel_interior S)"
+ using inj_on_subset injf rel_interior_subset by blast
+ show "rel_interior S \<noteq> {}"
+ by (simp add: False \<open>convex S\<close> rel_interior_eq_empty)
+ qed auto
+ then show ?thesis
+ by simp
+qed
+
+
+lemma homeomorphic_convex_sets_le:
+ assumes "convex S" "S homeomorphic T"
+ shows "aff_dim S \<le> aff_dim T"
+proof -
+ obtain h k where homhk: "homeomorphism S T h k"
+ using homeomorphic_def assms by blast
+ show ?thesis
+ proof (rule invariance_of_dimension_convex_domain [OF \<open>convex S\<close>])
+ show "continuous_on S h"
+ using homeomorphism_def homhk by blast
+ show "h ` S \<subseteq> affine hull T"
+ by (metis homeomorphism_def homhk hull_subset)
+ show "inj_on h S"
+ by (meson homeomorphism_apply1 homhk inj_on_inverseI)
+ qed
+qed
+
+lemma homeomorphic_convex_sets:
+ assumes "convex S" "convex T" "S homeomorphic T"
+ shows "aff_dim S = aff_dim T"
+ by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym)
+
+lemma homeomorphic_convex_compact_sets_eq:
+ assumes "convex S" "compact S" "convex T" "compact T"
+ shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
+ by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets)
+
+lemma invariance_of_domain_gen:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
+ shows "open(f ` S)"
+ using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto
+
+lemma injective_into_1d_imp_open_map_UNIV:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes "open T" "continuous_on S f" "inj_on f S" "T \<subseteq> S"
+ shows "open (f ` T)"
+ apply (rule invariance_of_domain_gen [OF \<open>open T\<close>])
+ using assms apply (auto simp: elim: continuous_on_subset subset_inj_on)
+ done
+
+lemma continuous_on_inverse_open:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" and gf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+ shows "continuous_on (f ` S) g"
+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)"
+ by (auto simp: gf)
+ show "openin (subtopology euclidean (f ` S)) {x \<in> f ` S. g x \<in> T}"
+ apply (subst eq)
+ apply (rule open_openin_trans)
+ apply (rule invariance_of_domain_gen)
+ using assms
+ apply auto
+ using inj_on_inverseI apply auto[1]
+ by (metis \<open>open T\<close> continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq)
+qed
+
+lemma invariance_of_domain_homeomorphism:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
+ obtains g where "homeomorphism S (f ` S) f g"
+proof
+ show "homeomorphism S (f ` S) f (inv_into S f)"
+ by (simp add: assms continuous_on_inverse_open homeomorphism_def)
+qed
+
+corollary invariance_of_domain_homeomorphic:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
+ shows "S homeomorphic (f ` S)"
+ using invariance_of_domain_homeomorphism [OF assms]
+ by (meson homeomorphic_def)
+
end
--- a/src/HOL/Analysis/Linear_Algebra.thy Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Mon Oct 10 15:45:41 2016 +0100
@@ -2178,7 +2178,7 @@
text \<open>More lemmas about dimension.\<close>
-lemma dim_UNIV: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
+lemma dim_UNIV [simp]: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
using independent_Basis
by (intro dim_unique[of Basis]) auto
--- a/src/HOL/Analysis/Path_Connected.thy Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Mon Oct 10 15:45:41 2016 +0100
@@ -1261,8 +1261,90 @@
using midpoints_in_convex_hull segment_convex_hull by blast
lemma midpoint_in_open_segment [simp]: "midpoint a b \<in> open_segment a b \<longleftrightarrow> a \<noteq> b"
- by (simp add: midpoint_eq_endpoint(1) midpoint_eq_endpoint(2) open_segment_def)
-
+ by (simp add: open_segment_def)
+
+lemma continuous_IVT_local_extremum:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes contf: "continuous_on (closed_segment a b) f"
+ and "a \<noteq> b" "f a = f b"
+ obtains z where "z \<in> open_segment a b"
+ "(\<forall>w \<in> closed_segment a b. (f w) \<le> (f z)) \<or>
+ (\<forall>w \<in> closed_segment a b. (f z) \<le> (f w))"
+proof -
+ obtain c where "c \<in> closed_segment a b" and c: "\<And>y. y \<in> closed_segment a b \<Longrightarrow> f y \<le> f c"
+ using continuous_attains_sup [of "closed_segment a b" f] contf by auto
+ obtain d where "d \<in> closed_segment a b" and d: "\<And>y. y \<in> closed_segment a b \<Longrightarrow> f d \<le> f y"
+ using continuous_attains_inf [of "closed_segment a b" f] contf by auto
+ show ?thesis
+ proof (cases "c \<in> open_segment a b \<or> d \<in> open_segment a b")
+ case True
+ then show ?thesis
+ using c d that by blast
+ next
+ case False
+ then have "(c = a \<or> c = b) \<and> (d = a \<or> d = b)"
+ by (simp add: \<open>c \<in> closed_segment a b\<close> \<open>d \<in> closed_segment a b\<close> open_segment_def)
+ with \<open>a \<noteq> b\<close> \<open>f a = f b\<close> c d show ?thesis
+ by (rule_tac z = "midpoint a b" in that) (fastforce+)
+ qed
+qed
+
+text\<open>An injective map into R is also an open map w.r.T. the universe, and conversely. \<close>
+proposition injective_eq_1d_open_map_UNIV:
+ fixes f :: "real \<Rightarrow> real"
+ assumes contf: "continuous_on S f" and S: "is_interval S"
+ shows "inj_on f S \<longleftrightarrow> (\<forall>T. open T \<and> T \<subseteq> S \<longrightarrow> open(f ` T))"
+ (is "?lhs = ?rhs")
+proof safe
+ fix T
+ assume injf: ?lhs and "open T" and "T \<subseteq> S"
+ have "\<exists>U. open U \<and> f x \<in> U \<and> U \<subseteq> f ` T" if "x \<in> T" for x
+ proof -
+ obtain \<delta> where "\<delta> > 0" and \<delta>: "cball x \<delta> \<subseteq> T"
+ using \<open>open T\<close> \<open>x \<in> T\<close> open_contains_cball_eq by blast
+ show ?thesis
+ proof (intro exI conjI)
+ have "closed_segment (x-\<delta>) (x+\<delta>) = {x-\<delta>..x+\<delta>}"
+ using \<open>0 < \<delta>\<close> by (auto simp: closed_segment_eq_real_ivl)
+ also have "... \<subseteq> S"
+ using \<delta> \<open>T \<subseteq> S\<close> by (auto simp: dist_norm subset_eq)
+ finally have "f ` (open_segment (x-\<delta>) (x+\<delta>)) = open_segment (f (x-\<delta>)) (f (x+\<delta>))"
+ using continuous_injective_image_open_segment_1
+ by (metis continuous_on_subset [OF contf] inj_on_subset [OF injf])
+ then show "open (f ` {x-\<delta><..<x+\<delta>})"
+ using \<open>0 < \<delta>\<close> by (simp add: open_segment_eq_real_ivl)
+ show "f x \<in> f ` {x - \<delta><..<x + \<delta>}"
+ by (auto simp: \<open>\<delta> > 0\<close>)
+ show "f ` {x - \<delta><..<x + \<delta>} \<subseteq> f ` T"
+ using \<delta> by (auto simp: dist_norm subset_iff)
+ qed
+ qed
+ with open_subopen show "open (f ` T)"
+ by blast
+next
+ assume R: ?rhs
+ have False if xy: "x \<in> S" "y \<in> S" and "f x = f y" "x \<noteq> y" for x y
+ proof -
+ have "open (f ` open_segment x y)"
+ using R
+ by (metis S convex_contains_open_segment is_interval_convex open_greaterThanLessThan open_segment_eq_real_ivl xy)
+ moreover
+ have "continuous_on (closed_segment x y) f"
+ by (meson S closed_segment_subset contf continuous_on_subset is_interval_convex that)
+ then obtain \<xi> where "\<xi> \<in> open_segment x y"
+ and \<xi>: "(\<forall>w \<in> closed_segment x y. (f w) \<le> (f \<xi>)) \<or>
+ (\<forall>w \<in> closed_segment x y. (f \<xi>) \<le> (f w))"
+ using continuous_IVT_local_extremum [of x y f] \<open>f x = f y\<close> \<open>x \<noteq> y\<close> by blast
+ ultimately obtain e where "e>0" and e: "\<And>u. dist u (f \<xi>) < e \<Longrightarrow> u \<in> f ` open_segment x y"
+ using open_dist by (metis image_eqI)
+ have fin: "f \<xi> + (e/2) \<in> f ` open_segment x y" "f \<xi> - (e/2) \<in> f ` open_segment x y"
+ using e [of "f \<xi> + (e/2)"] e [of "f \<xi> - (e/2)"] \<open>e > 0\<close> by (auto simp: dist_norm)
+ show ?thesis
+ using \<xi> \<open>0 < e\<close> fin open_closed_segment by fastforce
+ qed
+ then show ?lhs
+ by (force simp: inj_on_def)
+qed
subsection \<open>Bounding a point away from a path\<close>
@@ -2319,9 +2401,10 @@
by (metis cobounded_unique_unbounded_component)
lemma cobounded_has_bounded_component:
- fixes s :: "'a :: euclidean_space set"
- shows "\<lbrakk>bounded (- s); ~connected s; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> components s \<and> bounded c"
- by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq)
+ fixes S :: "'a :: euclidean_space set"
+ assumes "bounded (- S)" "\<not> connected S" "2 \<le> DIM('a)"
+ obtains C where "C \<in> components S" "bounded C"
+ by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq assms)
section\<open>The "inside" and "outside" of a set\<close>
@@ -7510,7 +7593,7 @@
have hUS: "h ` U \<subseteq> h ` S"
by (meson homeomorphism_imp_open_map homeomorphism_of_subsets homhj hull_subset opeS opeU open_UNIV openin_open_eq)
have op: "openin (subtopology euclidean (affine hull S)) U \<Longrightarrow> open (h ` U)" for U
- using homeomorphism_imp_open_map [OF homhj] by (simp add: open_openin)
+ using homeomorphism_imp_open_map [OF homhj] by simp
have "open (h ` U)" "open (h ` S)"
by (auto intro: opeS opeU openin_trans op)
then obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Oct 10 15:45:41 2016 +0100
@@ -18,6 +18,11 @@
(* FIXME: move elsewhere *)
+lemma Times_eq_image_sum:
+ fixes S :: "'a :: comm_monoid_add set" and T :: "'b :: comm_monoid_add set"
+ shows "S \<times> T = {u + v |u v. u \<in> (\<lambda>x. (x, 0)) ` S \<and> v \<in> Pair 0 ` T}"
+ by force
+
lemma halfspace_Int_eq:
"{x. a \<bullet> x \<le> b} \<inter> {x. b \<le> a \<bullet> x} = {x. a \<bullet> x = b}"
"{x. b \<le> a \<bullet> x} \<inter> {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
@@ -730,20 +735,19 @@
apply (auto simp add: istopology_def)
done
+declare open_openin [symmetric, simp]
+
lemma topspace_euclidean [simp]: "topspace euclidean = UNIV"
- apply (simp add: topspace_def)
- apply (rule set_eqI)
- apply (auto simp add: open_openin[symmetric])
- done
+ by (force simp add: topspace_def)
lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S"
- by (simp add: topspace_euclidean topspace_subtopology)
+ by (simp add: topspace_subtopology)
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
- by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV)
+ by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
- by (simp add: open_openin openin_subopen[symmetric])
+ using openI by auto
lemma openin_subtopology_self [simp]: "openin (subtopology euclidean S) S"
by (metis openin_topspace topspace_euclidean_subtopology)
@@ -751,7 +755,7 @@
text \<open>Basic "localization" results are handy for connectedness.\<close>
lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
- by (auto simp add: openin_subtopology open_openin[symmetric])
+ by (auto simp add: openin_subtopology)
lemma openin_Int_open:
"\<lbrakk>openin (subtopology euclidean U) S; open T\<rbrakk>
@@ -1968,7 +1972,7 @@
lemma closure_UNIV [simp]: "closure UNIV = UNIV"
using closed_UNIV by (rule closure_closed)
-lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
+lemma closure_Un [simp]: "closure (S \<union> T) = closure S \<union> closure T"
unfolding closure_interior by simp
lemma closure_eq_empty [iff]: "closure S = {} \<longleftrightarrow> S = {}"
@@ -2084,6 +2088,71 @@
\<Longrightarrow> openin (subtopology euclidean T) S"
by (auto simp: openin_open)
+lemma openin_Times:
+ "\<lbrakk>openin (subtopology euclidean S) S'; openin (subtopology euclidean T) T'\<rbrakk>
+ \<Longrightarrow> openin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
+ unfolding openin_open using open_Times by blast
+
+lemma Times_in_interior_subtopology:
+ fixes U :: "('a::metric_space * 'b::metric_space) set"
+ assumes "(x, y) \<in> U" "openin (subtopology euclidean (S \<times> T)) U"
+ obtains V W where "openin (subtopology euclidean S) V" "x \<in> V"
+ "openin (subtopology euclidean T) W" "y \<in> W" "(V \<times> W) \<subseteq> U"
+proof -
+ from assms obtain e where "e > 0" and "U \<subseteq> S \<times> T"
+ and e: "\<And>x' y'. \<lbrakk>x'\<in>S; y'\<in>T; dist (x', y') (x, y) < e\<rbrakk> \<Longrightarrow> (x', y') \<in> U"
+ by (force simp: openin_euclidean_subtopology_iff)
+ with assms have "x \<in> S" "y \<in> T"
+ by auto
+ show ?thesis
+ proof
+ show "openin (subtopology euclidean S) (ball x (e/2) \<inter> S)"
+ by (simp add: Int_commute openin_open_Int)
+ show "x \<in> ball x (e / 2) \<inter> S"
+ by (simp add: \<open>0 < e\<close> \<open>x \<in> S\<close>)
+ show "openin (subtopology euclidean T) (ball y (e/2) \<inter> T)"
+ by (simp add: Int_commute openin_open_Int)
+ show "y \<in> ball y (e / 2) \<inter> T"
+ by (simp add: \<open>0 < e\<close> \<open>y \<in> T\<close>)
+ show "(ball x (e / 2) \<inter> S) \<times> (ball y (e / 2) \<inter> T) \<subseteq> U"
+ by clarify (simp add: e dist_Pair_Pair \<open>0 < e\<close> dist_commute sqrt_sum_squares_half_less)
+ qed
+qed
+
+lemma openin_Times_eq:
+ fixes S :: "'a::metric_space set" and T :: "'b::metric_space set"
+ shows
+ "openin (subtopology euclidean (S \<times> T)) (S' \<times> T') \<longleftrightarrow>
+ (S' = {} \<or> T' = {} \<or>
+ openin (subtopology euclidean S) S' \<and> openin (subtopology euclidean T) T')"
+ (is "?lhs = ?rhs")
+proof (cases "S' = {} \<or> T' = {}")
+ case True
+ then show ?thesis by auto
+next
+ case False
+ then obtain x y where "x \<in> S'" "y \<in> T'"
+ by blast
+ show ?thesis
+ proof
+ assume L: ?lhs
+ have "openin (subtopology euclidean S) S'"
+ apply (subst openin_subopen, clarify)
+ apply (rule Times_in_interior_subtopology [OF _ L])
+ using \<open>y \<in> T'\<close> by auto
+ moreover have "openin (subtopology euclidean T) T'"
+ apply (subst openin_subopen, clarify)
+ apply (rule Times_in_interior_subtopology [OF _ L])
+ using \<open>x \<in> S'\<close> by auto
+ ultimately show ?rhs
+ by simp
+ next
+ assume ?rhs
+ with False show ?lhs
+ by (simp add: openin_Times)
+ qed
+qed
+
lemma closedin_Times:
"\<lbrakk>closedin (subtopology euclidean S) S'; closedin (subtopology euclidean T) T'\<rbrakk>
\<Longrightarrow> closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
@@ -8502,7 +8571,7 @@
proof -
from gt_ex obtain b where "a < b" by auto
hence "{a<..} = {a<..<b} \<union> {b..}" by auto
- also have "closure \<dots> = {a..}" using \<open>a < b\<close> unfolding closure_union
+ also have "closure \<dots> = {a..}" using \<open>a < b\<close> unfolding closure_Un
by auto
finally show ?thesis .
qed
@@ -8513,7 +8582,7 @@
proof -
from lt_ex obtain a where "a < b" by auto
hence "{..<b} = {a<..<b} \<union> {..a}" by auto
- also have "closure \<dots> = {..b}" using \<open>a < b\<close> unfolding closure_union
+ also have "closure \<dots> = {..b}" using \<open>a < b\<close> unfolding closure_Un
by auto
finally show ?thesis .
qed
@@ -8524,7 +8593,7 @@
shows "closure {a ..< b} = {a .. b}"
proof -
from assms have "{a ..< b} = {a} \<union> {a <..< b}" by auto
- also have "closure \<dots> = {a .. b}" unfolding closure_union
+ also have "closure \<dots> = {a .. b}" unfolding closure_Un
by (auto simp add: assms less_imp_le)
finally show ?thesis .
qed
@@ -8535,7 +8604,7 @@
shows "closure {a <.. b} = {a .. b}"
proof -
from assms have "{a <.. b} = {b} \<union> {a <..< b}" by auto
- also have "closure \<dots> = {a .. b}" unfolding closure_union
+ also have "closure \<dots> = {a .. b}" unfolding closure_Un
by (auto simp add: assms less_imp_le)
finally show ?thesis .
qed
--- a/src/HOL/NthRoot.thy Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/NthRoot.thy Mon Oct 10 15:45:41 2016 +0100
@@ -692,15 +692,12 @@
by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four
real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85))
-
-text \<open>Needed for the infinitely close relation over the nonstandard complex numbers.\<close>
-lemma lemma_sqrt_hcomplex_capprox:
- "0 < u \<Longrightarrow> x < u/2 \<Longrightarrow> y < u/2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u"
+lemma sqrt_sum_squares_half_less:
+ "x < u/2 \<Longrightarrow> y < u/2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u"
apply (rule real_sqrt_sum_squares_less)
apply (auto simp add: abs_if field_simps)
apply (rule le_less_trans [where y = "x*2"])
- using less_eq_real_def sqrt2_less_2
- apply force
+ using less_eq_real_def sqrt2_less_2 apply force
apply assumption
apply (rule le_less_trans [where y = "y*2"])
using less_eq_real_def sqrt2_less_2 mult_le_cancel_left