invariance of domain
authorpaulson <lp15@cam.ac.uk>
Mon Oct 10 15:45:41 2016 +0100 (2016-10-10)
changeset 6412274fde524799e
parent 64121 f2c8f6b11dcf
child 64146 b2486964b823
invariance of domain
NEWS
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/FurtherTopology.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/NthRoot.thy
     1.1 --- a/NEWS	Sun Oct 09 16:27:01 2016 +0200
     1.2 +++ b/NEWS	Mon Oct 10 15:45:41 2016 +0100
     1.3 @@ -432,7 +432,7 @@
     1.4  "~~/src/HOL/Library/FinFun_Syntax".
     1.5  
     1.6  * HOL-Library: theory Multiset_Permutations (executably) defines the set of
     1.7 -permutations of a given set or multiset, i.e. the set of all lists that 
     1.8 +permutations of a given set or multiset, i.e. the set of all lists that
     1.9  contain every element of the carrier (multi-)set exactly once.
    1.10  
    1.11  * HOL-Library: multiset membership is now expressed using set_mset
    1.12 @@ -485,8 +485,7 @@
    1.13  and the Krein–Milman Minkowski theorem.
    1.14  
    1.15  * HOL-Analysis: Numerous results ported from the HOL Light libraries:
    1.16 -homeomorphisms, continuous function extensions and other advanced topics
    1.17 -in topology
    1.18 +homeomorphisms, continuous function extensions, invariance of domain.
    1.19  
    1.20  * HOL-Probability: the type of emeasure and nn_integral was changed from
    1.21  ereal to ennreal, INCOMPATIBILITY.
     2.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Oct 09 16:27:01 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Oct 10 15:45:41 2016 +0100
     2.3 @@ -2021,6 +2021,58 @@
     2.4      done
     2.5  qed
     2.6  
     2.7 +proposition frontier_subset_retraction:
     2.8 +  fixes S :: "'a::euclidean_space set"
     2.9 +  assumes "bounded S" and fros: "frontier S \<subseteq> T"
    2.10 +      and contf: "continuous_on (closure S) f"
    2.11 +      and fim: "f ` S \<subseteq> T"
    2.12 +      and fid: "\<And>x. x \<in> T \<Longrightarrow> f x = x"
    2.13 +    shows "S \<subseteq> T"
    2.14 +proof (rule ccontr)
    2.15 +  assume "\<not> S \<subseteq> T"
    2.16 +  then obtain a where "a \<in> S" "a \<notin> T" by blast
    2.17 +  define g where "g \<equiv> \<lambda>z. if z \<in> closure S then f z else z"
    2.18 +  have "continuous_on (closure S \<union> closure(-S)) g"
    2.19 +    unfolding g_def
    2.20 +    apply (rule continuous_on_cases)
    2.21 +    using fros fid frontier_closures
    2.22 +        apply (auto simp: contf continuous_on_id)
    2.23 +    done
    2.24 +  moreover have "closure S \<union> closure(- S) = UNIV"
    2.25 +    using closure_Un by fastforce
    2.26 +  ultimately have contg: "continuous_on UNIV g" by metis
    2.27 +  obtain B where "0 < B" and B: "closure S \<subseteq> ball a B"
    2.28 +    using \<open>bounded S\<close> bounded_subset_ballD by blast
    2.29 +  have notga: "g x \<noteq> a" for x
    2.30 +    unfolding g_def using fros fim \<open>a \<notin> T\<close>
    2.31 +    apply (auto simp: frontier_def)
    2.32 +    using fid interior_subset apply fastforce
    2.33 +    by (simp add: \<open>a \<in> S\<close> closure_def)
    2.34 +  define h where "h \<equiv> (\<lambda>y. a + (B / norm(y - a)) *\<^sub>R (y - a)) \<circ> g"
    2.35 +  have "\<not> (frontier (cball a B) retract_of (cball a B))"
    2.36 +    by (metis no_retraction_cball \<open>0 < B\<close>)
    2.37 +  then have "\<And>k. \<not> retraction (cball a B) (frontier (cball a B)) k"
    2.38 +    by (simp add: retract_of_def)
    2.39 +  moreover have "retraction (cball a B) (frontier (cball a B)) h"
    2.40 +    unfolding retraction_def
    2.41 +  proof (intro conjI ballI)
    2.42 +    show "frontier (cball a B) \<subseteq> cball a B"
    2.43 +      by (force simp:)
    2.44 +    show "continuous_on (cball a B) h"
    2.45 +      unfolding h_def
    2.46 +      apply (intro continuous_intros)
    2.47 +      using contg continuous_on_subset notga apply auto
    2.48 +      done
    2.49 +    show "h ` cball a B \<subseteq> frontier (cball a B)"
    2.50 +      using \<open>0 < B\<close> by (auto simp: h_def notga dist_norm)
    2.51 +    show "\<And>x. x \<in> frontier (cball a B) \<Longrightarrow> h x = x"
    2.52 +      apply (auto simp: h_def algebra_simps)
    2.53 +      apply (simp add: vector_add_divide_simps  notga)
    2.54 +      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)
    2.55 +  qed
    2.56 +  ultimately show False by simp
    2.57 +qed
    2.58 +
    2.59  subsection\<open>Retractions\<close>
    2.60  
    2.61  lemma retraction:
    2.62 @@ -3192,7 +3244,7 @@
    2.63    shows "S retract_of UNIV \<longleftrightarrow> AR S \<and> closed S"
    2.64  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)
    2.65  
    2.66 -lemma compact_AR [simp]:
    2.67 +lemma compact_AR:
    2.68    fixes S :: "'a::euclidean_space set"
    2.69    shows "compact S \<and> AR S \<longleftrightarrow> compact S \<and> S retract_of UNIV"
    2.70  using compact_imp_closed retract_of_UNIV by blast
    2.71 @@ -3893,7 +3945,7 @@
    2.72      apply (simp add: ENR_def)
    2.73      apply (rule_tac x = "{x. x \<in> UNIV \<and>
    2.74                               closest_point (affine hull S) x \<in> (- {a})}" in exI)
    2.75 -    apply (simp add: open_openin)
    2.76 +    apply simp
    2.77      done
    2.78  qed
    2.79  
    2.80 @@ -4189,5 +4241,89 @@
    2.81    then show ?thesis by blast
    2.82  qed
    2.83  
    2.84 +subsection\<open>The complement of a set and path-connectedness\<close>
    2.85 +
    2.86 +text\<open>Complement in dimension N > 1 of set homeomorphic to any interval in
    2.87 + any dimension is (path-)connected. This naively generalizes the argument
    2.88 + in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer fixed point theorem",
    2.89 +American Mathematical Monthly 1984.\<close>
    2.90 +
    2.91 +lemma unbounded_components_complement_absolute_retract:
    2.92 +  fixes S :: "'a::euclidean_space set"
    2.93 +  assumes C: "C \<in> components(- S)" and S: "compact S" "AR S"
    2.94 +    shows "\<not> bounded C"
    2.95 +proof -
    2.96 +  obtain y where y: "C = connected_component_set (- S) y" and "y \<notin> S"
    2.97 +    using C by (auto simp: components_def)
    2.98 +  have "open(- S)"
    2.99 +    using S by (simp add: closed_open compact_eq_bounded_closed)
   2.100 +  have "S retract_of UNIV"
   2.101 +    using S compact_AR by blast
   2.102 +  then obtain r where contr: "continuous_on UNIV r" and ontor: "range r \<subseteq> S"
   2.103 +                  and r: "\<And>x. x \<in> S \<Longrightarrow> r x = x"
   2.104 +    by (auto simp: retract_of_def retraction_def)
   2.105 +  show ?thesis
   2.106 +  proof
   2.107 +    assume "bounded C"
   2.108 +    have "connected_component_set (- S) y \<subseteq> S"
   2.109 +    proof (rule frontier_subset_retraction)
   2.110 +      show "bounded (connected_component_set (- S) y)"
   2.111 +        using \<open>bounded C\<close> y by blast
   2.112 +      show "frontier (connected_component_set (- S) y) \<subseteq> S"
   2.113 +        using C \<open>compact S\<close> compact_eq_bounded_closed frontier_of_components_closed_complement y by blast
   2.114 +      show "continuous_on (closure (connected_component_set (- S) y)) r"
   2.115 +        by (blast intro: continuous_on_subset [OF contr])
   2.116 +    qed (use ontor r in auto)
   2.117 +    with \<open>y \<notin> S\<close> show False by force
   2.118 +  qed
   2.119 +qed
   2.120 +
   2.121 +lemma connected_complement_absolute_retract:
   2.122 +  fixes S :: "'a::euclidean_space set"
   2.123 +  assumes S: "compact S" "AR S" and 2: "2 \<le> DIM('a)"
   2.124 +    shows "connected(- S)"
   2.125 +proof -
   2.126 +  have "S retract_of UNIV"
   2.127 +    using S compact_AR by blast
   2.128 +  show ?thesis
   2.129 +    apply (clarsimp simp: connected_iff_connected_component_eq)
   2.130 +    apply (rule cobounded_unique_unbounded_component [OF _ 2])
   2.131 +      apply (simp add: \<open>compact S\<close> compact_imp_bounded)
   2.132 +     apply (meson ComplI S componentsI unbounded_components_complement_absolute_retract)+
   2.133 +    done
   2.134 +qed
   2.135 +
   2.136 +lemma path_connected_complement_absolute_retract:
   2.137 +  fixes S :: "'a::euclidean_space set"
   2.138 +  assumes "compact S" "AR S" "2 \<le> DIM('a)"
   2.139 +    shows "path_connected(- S)"
   2.140 +  using connected_complement_absolute_retract [OF assms]
   2.141 +  using \<open>compact S\<close> compact_eq_bounded_closed connected_open_path_connected by blast
   2.142 +
   2.143 +theorem connected_complement_homeomorphic_convex_compact:
   2.144 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   2.145 +  assumes hom: "S homeomorphic T" and T: "convex T" "compact T" and 2: "2 \<le> DIM('a)"
   2.146 +    shows "connected(- S)"
   2.147 +proof (cases "S = {}")
   2.148 +  case True
   2.149 +  then show ?thesis
   2.150 +    by (simp add: connected_UNIV)
   2.151 +next
   2.152 +  case False
   2.153 +  show ?thesis
   2.154 +  proof (rule connected_complement_absolute_retract)
   2.155 +    show "compact S"
   2.156 +      using \<open>compact T\<close> hom homeomorphic_compactness by auto
   2.157 +    show "AR S"
   2.158 +      by (meson AR_ANR False \<open>convex T\<close> convex_imp_ANR convex_imp_contractible hom homeomorphic_ANR_iff_ANR homeomorphic_contractible_eq)
   2.159 +  qed (rule 2)
   2.160 +qed
   2.161 +
   2.162 +corollary path_connected_complement_homeomorphic_convex_compact:
   2.163 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   2.164 +  assumes hom: "S homeomorphic T" "convex T" "compact T" "2 \<le> DIM('a)"
   2.165 +    shows "path_connected(- S)"
   2.166 +  using connected_complement_homeomorphic_convex_compact [OF assms]
   2.167 +  using \<open>compact T\<close> compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast
   2.168  
   2.169  end
     3.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 09 16:27:01 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Oct 10 15:45:41 2016 +0100
     3.3 @@ -2384,7 +2384,7 @@
     3.4    shows "closed s \<and> open s \<longleftrightarrow> s = {} \<or> s = UNIV"
     3.5  apply (rule iffI)
     3.6   apply (rule connected_UNIV [unfolded connected_clopen, rule_format])
     3.7 - apply (force simp add: open_openin closed_closedin, force)
     3.8 + apply (force simp add: closed_closedin, force)
     3.9  done
    3.10  
    3.11  corollary compact_open:
    3.12 @@ -12085,15 +12085,11 @@
    3.13      show "{x \<in> U. 0 < f x} \<inter> {x \<in> U. f x < 0} = {}"
    3.14        by auto
    3.15      have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {0<..}}"
    3.16 -      apply (rule continuous_openin_preimage [where T=UNIV])
    3.17 -        apply (simp_all add: contf)
    3.18 -      using open_greaterThan open_openin by blast
    3.19 +      by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
    3.20      then show "openin (subtopology euclidean U) {x \<in> U. 0 < f x}" by simp
    3.21    next
    3.22      have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {..<0}}"
    3.23 -      apply (rule continuous_openin_preimage [where T=UNIV])
    3.24 -        apply (simp_all add: contf)
    3.25 -      using open_lessThan open_openin by blast
    3.26 +      by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
    3.27      then show "openin (subtopology euclidean U) {x \<in> U. f x < 0}" by simp
    3.28    next
    3.29      show "S \<subseteq> {x \<in> U. 0 < f x}"
    3.30 @@ -12671,7 +12667,7 @@
    3.31  apply safe
    3.32  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)
    3.33  by (metis dim_singleton dim_subset le_0_eq)
    3.34 -
    3.35 +                  
    3.36  lemma aff_dim_insert:
    3.37    fixes a :: "'a::euclidean_space"
    3.38    shows "aff_dim (insert a S) = (if a \<in> affine hull S then aff_dim S else aff_dim S + 1)"
    3.39 @@ -13594,6 +13590,24 @@
    3.40    shows "aff_dim S < DIM('a) \<longleftrightarrow> (affine hull S \<noteq> UNIV)"
    3.41  by (metis (no_types) aff_dim_affine_hull aff_dim_le_DIM aff_dim_UNIV affine_hull_UNIV less_le)
    3.42  
    3.43 +
    3.44 +lemma dim_Times:
    3.45 +  fixes S :: "'a :: euclidean_space set" and T :: "'a set"
    3.46 +  assumes "subspace S" "subspace T"
    3.47 +  shows "dim(S \<times> T) = dim S + dim T"
    3.48 +proof -
    3.49 +  have ss: "subspace ((\<lambda>x. (x, 0)) ` S)" "subspace (Pair 0 ` T)"
    3.50 +    by (rule subspace_linear_image, unfold_locales, auto simp: assms)+
    3.51 +  have "dim(S \<times> T) = dim({u + v |u v. u \<in> (\<lambda>x. (x, 0)) ` S \<and> v \<in> Pair 0 ` T})"
    3.52 +    by (simp add: Times_eq_image_sum)
    3.53 +  moreover have "dim ((\<lambda>x. (x, 0::'a)) ` S) = dim S" "dim (Pair (0::'a) ` T) = dim T"
    3.54 +    by (auto simp: additive.intro linear.intro linear_axioms.intro inj_on_def intro: dim_image_eq)
    3.55 +  moreover have "dim ((\<lambda>x. (x, 0)) ` S \<inter> Pair 0 ` T) = 0"
    3.56 +    by (subst dim_eq_0) (force simp: zero_prod_def)
    3.57 +  ultimately show ?thesis
    3.58 +    using dim_sums_Int [OF ss] by linarith
    3.59 +qed
    3.60 +
    3.61  subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
    3.62  
    3.63  lemma span_delete_0 [simp]: "span(S - {0}) = span S"
    3.64 @@ -13934,6 +13948,74 @@
    3.65      by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq orthogonal_commute orthogonal_def)
    3.66  qed
    3.67  
    3.68 +lemma aff_dim_openin:
    3.69 +  fixes S :: "'a::euclidean_space set"
    3.70 +  assumes ope: "openin (subtopology euclidean T) S" and "affine T" "S \<noteq> {}"
    3.71 +  shows "aff_dim S = aff_dim T"
    3.72 +proof -
    3.73 +  show ?thesis
    3.74 +  proof (rule order_antisym)
    3.75 +    show "aff_dim S \<le> aff_dim T"
    3.76 +      by (blast intro: aff_dim_subset [OF openin_imp_subset] ope)
    3.77 +  next
    3.78 +    obtain a where "a \<in> S"
    3.79 +      using \<open>S \<noteq> {}\<close> by blast
    3.80 +    have "S \<subseteq> T"
    3.81 +      using ope openin_imp_subset by auto
    3.82 +    then have "a \<in> T"
    3.83 +      using \<open>a \<in> S\<close> by auto
    3.84 +    then have subT': "subspace ((\<lambda>x. - a + x) ` T)"
    3.85 +      using affine_diffs_subspace \<open>affine T\<close> by auto
    3.86 +    then obtain B where Bsub: "B \<subseteq> ((\<lambda>x. - a + x) ` T)" and po: "pairwise orthogonal B"
    3.87 +                    and eq1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1" and "independent B"
    3.88 +                    and cardB: "card B = dim ((\<lambda>x. - a + x) ` T)"
    3.89 +                    and spanB: "span B = ((\<lambda>x. - a + x) ` T)"
    3.90 +      by (rule orthonormal_basis_subspace) auto
    3.91 +    obtain e where "0 < e" and e: "cball a e \<inter> T \<subseteq> S"
    3.92 +      by (meson \<open>a \<in> S\<close> openin_contains_cball ope)
    3.93 +    have "aff_dim T = aff_dim ((\<lambda>x. - a + x) ` T)"
    3.94 +      by (metis aff_dim_translation_eq)
    3.95 +    also have "... = dim ((\<lambda>x. - a + x) ` T)"
    3.96 +      using aff_dim_subspace subT' by blast
    3.97 +    also have "... = card B"
    3.98 +      by (simp add: cardB)
    3.99 +    also have "... = card ((\<lambda>x. e *\<^sub>R x) ` B)"
   3.100 +      using \<open>0 < e\<close>  by (force simp: inj_on_def card_image)
   3.101 +    also have "... \<le> dim ((\<lambda>x. - a + x) ` S)"
   3.102 +    proof (simp, rule independent_card_le_dim)
   3.103 +      have e': "cball 0 e \<inter> (\<lambda>x. x - a) ` T \<subseteq> (\<lambda>x. x - a) ` S"
   3.104 +        using e by (auto simp: dist_norm norm_minus_commute subset_eq)
   3.105 +      have "(\<lambda>x. e *\<^sub>R x) ` B \<subseteq> cball 0 e \<inter> (\<lambda>x. x - a) ` T"
   3.106 +        using Bsub \<open>0 < e\<close> eq1 subT' \<open>a \<in> T\<close> by (auto simp: subspace_def)
   3.107 +      then show "(\<lambda>x. e *\<^sub>R x) ` B \<subseteq> (\<lambda>x. x - a) ` S"
   3.108 +        using e' by blast
   3.109 +      show "independent ((\<lambda>x. e *\<^sub>R x) ` B)"
   3.110 +        using \<open>independent B\<close>
   3.111 +        apply (rule independent_injective_image, simp)
   3.112 +        by (metis \<open>0 < e\<close> injective_scaleR less_irrefl)
   3.113 +    qed
   3.114 +    also have "... = aff_dim S"
   3.115 +      using \<open>a \<in> S\<close> aff_dim_eq_dim hull_inc by force
   3.116 +    finally show "aff_dim T \<le> aff_dim S" .
   3.117 +  qed
   3.118 +qed
   3.119 +
   3.120 +lemma dim_openin:
   3.121 +  fixes S :: "'a::euclidean_space set"
   3.122 +  assumes ope: "openin (subtopology euclidean T) S" and "subspace T" "S \<noteq> {}"
   3.123 +  shows "dim S = dim T"
   3.124 +proof (rule order_antisym)
   3.125 +  show "dim S \<le> dim T"
   3.126 +    by (metis ope dim_subset openin_subset topspace_euclidean_subtopology)
   3.127 +next
   3.128 +  have "dim T = aff_dim S"
   3.129 +    using aff_dim_openin
   3.130 +    by (metis aff_dim_subspace \<open>subspace T\<close> \<open>S \<noteq> {}\<close> ope subspace_affine)
   3.131 +  also have "... \<le> dim S"
   3.132 +    by (metis aff_dim_subset aff_dim_subspace dim_span span_inc subspace_span)
   3.133 +  finally show "dim T \<le> dim S" by simp
   3.134 +qed
   3.135 +
   3.136  subsection\<open>Parallel slices, etc.\<close>
   3.137  
   3.138  text\<open> If we take a slice out of a set, we can do it perpendicularly,
   3.139 @@ -14249,7 +14331,6 @@
   3.140      done
   3.141  qed
   3.142  
   3.143 -
   3.144  corollary paracompact_closedin:
   3.145    fixes S :: "'a :: euclidean_space set"
   3.146    assumes cin: "closedin (subtopology euclidean U) S"
     4.1 --- a/src/HOL/Analysis/FurtherTopology.thy	Sun Oct 09 16:27:01 2016 +0200
     4.2 +++ b/src/HOL/Analysis/FurtherTopology.thy	Mon Oct 10 15:45:41 2016 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -section \<open>Extending Continous Maps, etc..\<close>
     4.5 +section \<open>Extending Continous Maps, Invariance of Domain, etc..\<close>
     4.6  
     4.7  text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
     4.8  
     4.9 @@ -1888,4 +1888,468 @@
    4.10      done
    4.11  qed
    4.12  
    4.13 +subsection\<open> Invariance of domain and corollaries\<close>
    4.14 +
    4.15 +lemma invariance_of_domain_ball:
    4.16 +  fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
    4.17 +  assumes contf: "continuous_on (cball a r) f" and "0 < r"
    4.18 +     and inj: "inj_on f (cball a r)"
    4.19 +   shows "open(f ` ball a r)"
    4.20 +proof (cases "DIM('a) = 1")
    4.21 +  case True
    4.22 +  obtain h::"'a\<Rightarrow>real" and k
    4.23 +        where "linear h" "linear k" "h ` UNIV = UNIV" "k ` UNIV = UNIV"
    4.24 +              "\<And>x. norm(h x) = norm x" "\<And>x. norm(k x) = norm x"
    4.25 +              "\<And>x. k(h x) = x" "\<And>x. h(k x) = x"
    4.26 +    apply (rule isomorphisms_UNIV_UNIV [where 'M='a and 'N=real])
    4.27 +      using True
    4.28 +       apply force
    4.29 +      by (metis UNIV_I UNIV_eq_I imageI)
    4.30 +    have cont: "continuous_on S h"  "continuous_on T k" for S T
    4.31 +      by (simp_all add: \<open>linear h\<close> \<open>linear k\<close> linear_continuous_on linear_linear)
    4.32 +    have "continuous_on (h ` cball a r) (h \<circ> f \<circ> k)"
    4.33 +      apply (intro continuous_on_compose cont continuous_on_subset [OF contf])
    4.34 +      apply (auto simp: \<open>\<And>x. k (h x) = x\<close>)
    4.35 +      done
    4.36 +    moreover have "is_interval (h ` cball a r)"
    4.37 +      by (simp add: is_interval_connected_1 \<open>linear h\<close> linear_continuous_on linear_linear connected_continuous_image)
    4.38 +    moreover have "inj_on (h \<circ> f \<circ> k) (h ` cball a r)"
    4.39 +      using inj by (simp add: inj_on_def) (metis \<open>\<And>x. k (h x) = x\<close>)
    4.40 +    ultimately have *: "\<And>T. \<lbrakk>open T; T \<subseteq> h ` cball a r\<rbrakk> \<Longrightarrow> open ((h \<circ> f \<circ> k) ` T)"
    4.41 +      using injective_eq_1d_open_map_UNIV by blast
    4.42 +    have "open ((h \<circ> f \<circ> k) ` (h ` ball a r))"
    4.43 +      by (rule *) (auto simp: \<open>linear h\<close> \<open>range h = UNIV\<close> open_surjective_linear_image)
    4.44 +    then have "open ((h \<circ> f) ` ball a r)"
    4.45 +      by (simp add: image_comp \<open>\<And>x. k (h x) = x\<close> cong: image_cong)
    4.46 +    then show ?thesis
    4.47 +      apply (simp add: image_comp [symmetric])
    4.48 +      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)
    4.49 +      done
    4.50 +next
    4.51 +  case False
    4.52 +  then have 2: "DIM('a) \<ge> 2"
    4.53 +    by (metis DIM_ge_Suc0 One_nat_def Suc_1 antisym not_less_eq_eq)
    4.54 +  have fimsub: "f ` ball a r \<subseteq> - f ` sphere a r"
    4.55 +    using inj  by clarsimp (metis inj_onD less_eq_real_def mem_cball order_less_irrefl)
    4.56 +  have hom: "f ` sphere a r homeomorphic sphere a r"
    4.57 +    by (meson compact_sphere contf continuous_on_subset homeomorphic_compact homeomorphic_sym inj inj_on_subset sphere_cball)
    4.58 +  then have nconn: "\<not> connected (- f ` sphere a r)"
    4.59 +    by (rule Jordan_Brouwer_separation) (auto simp: \<open>0 < r\<close>)
    4.60 +  obtain C where C: "C \<in> components (- f ` sphere a r)" and "bounded C"
    4.61 +    apply (rule cobounded_has_bounded_component [OF _ nconn])
    4.62 +      apply (simp_all add: 2)
    4.63 +    by (meson compact_imp_bounded compact_continuous_image_eq compact_sphere contf inj sphere_cball)
    4.64 +  moreover have "f ` (ball a r) = C"
    4.65 +  proof
    4.66 +    have "C \<noteq> {}"
    4.67 +      by (rule in_components_nonempty [OF C])
    4.68 +    show "C \<subseteq> f ` ball a r"
    4.69 +    proof (rule ccontr)
    4.70 +      assume nonsub: "\<not> C \<subseteq> f ` ball a r"
    4.71 +      have "- f ` cball a r \<subseteq> C"
    4.72 +      proof (rule components_maximal [OF C])
    4.73 +        have "f ` cball a r homeomorphic cball a r"
    4.74 +          using compact_cball contf homeomorphic_compact homeomorphic_sym inj by blast
    4.75 +        then show "connected (- f ` cball a r)"
    4.76 +          by (auto intro: connected_complement_homeomorphic_convex_compact 2)
    4.77 +        show "- f ` cball a r \<subseteq> - f ` sphere a r"
    4.78 +          by auto
    4.79 +        then show "C \<inter> - f ` cball a r \<noteq> {}"
    4.80 +          using \<open>C \<noteq> {}\<close> in_components_subset [OF C] nonsub
    4.81 +          using image_iff by fastforce
    4.82 +      qed
    4.83 +      then have "bounded (- f ` cball a r)"
    4.84 +        using bounded_subset \<open>bounded C\<close> by auto
    4.85 +      then have "\<not> bounded (f ` cball a r)"
    4.86 +        using cobounded_imp_unbounded by blast
    4.87 +      then show "False"
    4.88 +        using compact_continuous_image [OF contf] compact_cball compact_imp_bounded by blast
    4.89 +    qed
    4.90 +    with \<open>C \<noteq> {}\<close> have "C \<inter> f ` ball a r \<noteq> {}"
    4.91 +      by (simp add: inf.absorb_iff1)
    4.92 +    then show "f ` ball a r \<subseteq> C"
    4.93 +      by (metis components_maximal [OF C _ fimsub] connected_continuous_image ball_subset_cball connected_ball contf continuous_on_subset)
    4.94 +  qed
    4.95 +  moreover have "open (- f ` sphere a r)"
    4.96 +    using hom compact_eq_bounded_closed compact_sphere homeomorphic_compactness by blast
    4.97 +  ultimately show ?thesis
    4.98 +    using open_components by blast
    4.99 +qed
   4.100 +
   4.101 +
   4.102 +text\<open>Proved by L. E. J. Brouwer (1912)\<close>
   4.103 +theorem invariance_of_domain:
   4.104 +  fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
   4.105 +  assumes "continuous_on S f" "open S" "inj_on f S"
   4.106 +    shows "open(f ` S)"
   4.107 +  unfolding open_subopen [of "f`S"]
   4.108 +proof clarify
   4.109 +  fix a
   4.110 +  assume "a \<in> S"
   4.111 +  obtain \<delta> where "\<delta> > 0" and \<delta>: "cball a \<delta> \<subseteq> S"
   4.112 +    using \<open>open S\<close> \<open>a \<in> S\<close> open_contains_cball_eq by blast
   4.113 +  show "\<exists>T. open T \<and> f a \<in> T \<and> T \<subseteq> f ` S"
   4.114 +  proof (intro exI conjI)
   4.115 +    show "open (f ` (ball a \<delta>))"
   4.116 +      by (meson \<delta> \<open>0 < \<delta>\<close> assms continuous_on_subset inj_on_subset invariance_of_domain_ball)
   4.117 +    show "f a \<in> f ` ball a \<delta>"
   4.118 +      by (simp add: \<open>0 < \<delta>\<close>)
   4.119 +    show "f ` ball a \<delta> \<subseteq> f ` S"
   4.120 +      using \<delta> ball_subset_cball by blast
   4.121 +  qed
   4.122 +qed
   4.123 +
   4.124 +lemma inv_of_domain_ss0:
   4.125 +  fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
   4.126 +  assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
   4.127 +      and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)"
   4.128 +      and ope: "openin (subtopology euclidean S) U"
   4.129 +    shows "openin (subtopology euclidean S) (f ` U)"
   4.130 +proof -
   4.131 +  have "U \<subseteq> S"
   4.132 +    using ope openin_imp_subset by blast
   4.133 +  have "(UNIV::'b set) homeomorphic S"
   4.134 +    by (simp add: \<open>subspace S\<close> dimS dim_UNIV homeomorphic_subspaces)
   4.135 +  then obtain h k where homhk: "homeomorphism (UNIV::'b set) S h k"
   4.136 +    using homeomorphic_def by blast
   4.137 +  have homkh: "homeomorphism S (k ` S) k h"
   4.138 +    using homhk homeomorphism_image2 homeomorphism_sym by fastforce
   4.139 +  have "open ((k \<circ> f \<circ> h) ` k ` U)"
   4.140 +  proof (rule invariance_of_domain)
   4.141 +    show "continuous_on (k ` U) (k \<circ> f \<circ> h)"
   4.142 +    proof (intro continuous_intros)
   4.143 +      show "continuous_on (k ` U) h"
   4.144 +        by (meson continuous_on_subset [OF homeomorphism_cont1 [OF homhk]] top_greatest)
   4.145 +      show "continuous_on (h ` k ` U) f"
   4.146 +        apply (rule continuous_on_subset [OF contf], clarify)
   4.147 +        apply (metis homhk homeomorphism_def ope openin_imp_subset rev_subsetD)
   4.148 +        done
   4.149 +      show "continuous_on (f ` h ` k ` U) k"
   4.150 +        apply (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]])
   4.151 +        using fim homhk homeomorphism_apply2 ope openin_subset by fastforce
   4.152 +    qed
   4.153 +    have ope_iff: "\<And>T. open T \<longleftrightarrow> openin (subtopology euclidean (k ` S)) T"
   4.154 +      using homhk homeomorphism_image2 open_openin by fastforce
   4.155 +    show "open (k ` U)"
   4.156 +      by (simp add: ope_iff homeomorphism_imp_open_map [OF homkh ope])
   4.157 +    show "inj_on (k \<circ> f \<circ> h) (k ` U)"
   4.158 +      apply (clarsimp simp: inj_on_def)
   4.159 +      by (metis subsetD fim homeomorphism_apply2 [OF homhk] image_subset_iff inj_on_eq_iff injf \<open>U \<subseteq> S\<close>)
   4.160 +  qed
   4.161 +  moreover
   4.162 +  have eq: "f ` U = h ` (k \<circ> f \<circ> h \<circ> k) ` U"
   4.163 +    apply (auto simp: image_comp [symmetric])
   4.164 +    apply (metis homkh \<open>U \<subseteq> S\<close> fim homeomorphism_image2 homeomorphism_of_subsets homhk imageI subset_UNIV)
   4.165 +    by (metis \<open>U \<subseteq> S\<close> subsetD fim homeomorphism_def homhk image_eqI)
   4.166 +  ultimately show ?thesis
   4.167 +    by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
   4.168 +qed
   4.169 +
   4.170 +lemma inv_of_domain_ss1:
   4.171 +  fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
   4.172 +  assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
   4.173 +      and "subspace S"
   4.174 +      and ope: "openin (subtopology euclidean S) U"
   4.175 +    shows "openin (subtopology euclidean S) (f ` U)"
   4.176 +proof -
   4.177 +  define S' where "S' \<equiv> {y. \<forall>x \<in> S. orthogonal x y}"
   4.178 +  have "subspace S'"
   4.179 +    by (simp add: S'_def subspace_orthogonal_to_vectors)
   4.180 +  define g where "g \<equiv> \<lambda>z::'a*'a. ((f \<circ> fst)z, snd z)"
   4.181 +  have "openin (subtopology euclidean (S \<times> S')) (g ` (U \<times> S'))"
   4.182 +  proof (rule inv_of_domain_ss0)
   4.183 +    show "continuous_on (U \<times> S') g"
   4.184 +      apply (simp add: g_def)
   4.185 +      apply (intro continuous_intros continuous_on_compose2 [OF contf continuous_on_fst], auto)
   4.186 +      done
   4.187 +    show "g ` (U \<times> S') \<subseteq> S \<times> S'"
   4.188 +      using fim  by (auto simp: g_def)
   4.189 +    show "inj_on g (U \<times> S')"
   4.190 +      using injf by (auto simp: g_def inj_on_def)
   4.191 +    show "subspace (S \<times> S')"
   4.192 +      by (simp add: \<open>subspace S'\<close> \<open>subspace S\<close> subspace_Times)
   4.193 +    show "openin (subtopology euclidean (S \<times> S')) (U \<times> S')"
   4.194 +      by (simp add: openin_Times [OF ope])
   4.195 +    have "dim (S \<times> S') = dim S + dim S'"
   4.196 +      by (simp add: \<open>subspace S'\<close> \<open>subspace S\<close> dim_Times)
   4.197 +    also have "... = DIM('a)"
   4.198 +      using dim_subspace_orthogonal_to_vectors [OF \<open>subspace S\<close> subspace_UNIV]
   4.199 +      by (simp add: add.commute S'_def)
   4.200 +    finally show "dim (S \<times> S') = DIM('a)" .
   4.201 +  qed
   4.202 +  moreover have "g ` (U \<times> S') = f ` U \<times> S'"
   4.203 +    by (auto simp: g_def image_iff)
   4.204 +  moreover have "0 \<in> S'"
   4.205 +    using \<open>subspace S'\<close> subspace_affine by blast
   4.206 +  ultimately show ?thesis
   4.207 +    by (auto simp: openin_Times_eq)
   4.208 +qed
   4.209 +
   4.210 +
   4.211 +corollary invariance_of_domain_subspaces:
   4.212 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.213 +  assumes ope: "openin (subtopology euclidean U) S"
   4.214 +      and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
   4.215 +      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
   4.216 +      and injf: "inj_on f S"
   4.217 +    shows "openin (subtopology euclidean V) (f ` S)"
   4.218 +proof -
   4.219 +  obtain V' where "subspace V'" "V' \<subseteq> U" "dim V' = dim V"
   4.220 +    using choose_subspace_of_subspace [OF VU]
   4.221 +    by (metis span_eq \<open>subspace U\<close>)
   4.222 +  then have "V homeomorphic V'"
   4.223 +    by (simp add: \<open>subspace V\<close> homeomorphic_subspaces)
   4.224 +  then obtain h k where homhk: "homeomorphism V V' h k"
   4.225 +    using homeomorphic_def by blast
   4.226 +  have eq: "f ` S = k ` (h \<circ> f) ` S"
   4.227 +  proof -
   4.228 +    have "k ` h ` f ` S = f ` S"
   4.229 +      by (meson fim homeomorphism_def homeomorphism_of_subsets homhk subset_refl)
   4.230 +    then show ?thesis
   4.231 +      by (simp add: image_comp)
   4.232 +  qed
   4.233 +  show ?thesis
   4.234 +    unfolding eq
   4.235 +  proof (rule homeomorphism_imp_open_map)
   4.236 +    show homkh: "homeomorphism V' V k h"
   4.237 +      by (simp add: homeomorphism_symD homhk)
   4.238 +    have hfV': "(h \<circ> f) ` S \<subseteq> V'"
   4.239 +      using fim homeomorphism_image1 homhk by fastforce
   4.240 +    moreover have "openin (subtopology euclidean U) ((h \<circ> f) ` S)"
   4.241 +    proof (rule inv_of_domain_ss1)
   4.242 +      show "continuous_on S (h \<circ> f)"
   4.243 +        by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
   4.244 +      show "inj_on (h \<circ> f) S"
   4.245 +        apply (clarsimp simp: inj_on_def)
   4.246 +        by (metis fim homeomorphism_apply2 [OF homkh] image_subset_iff inj_onD injf)
   4.247 +      show "(h \<circ> f) ` S \<subseteq> U"
   4.248 +        using \<open>V' \<subseteq> U\<close> hfV' by auto
   4.249 +      qed (auto simp: assms)
   4.250 +    ultimately show "openin (subtopology euclidean V') ((h \<circ> f) ` S)"
   4.251 +      using openin_subset_trans \<open>V' \<subseteq> U\<close> by force
   4.252 +  qed
   4.253 +qed
   4.254 +
   4.255 +corollary invariance_of_dimension_subspaces:
   4.256 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.257 +  assumes ope: "openin (subtopology euclidean U) S"
   4.258 +      and "subspace U" "subspace V"
   4.259 +      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
   4.260 +      and injf: "inj_on f S" and "S \<noteq> {}"
   4.261 +    shows "dim U \<le> dim V"
   4.262 +proof -
   4.263 +  have "False" if "dim V < dim U"
   4.264 +  proof -
   4.265 +    obtain T where "subspace T" "T \<subseteq> U" "dim T = dim V"
   4.266 +      using choose_subspace_of_subspace [of "dim V" U]
   4.267 +      by (metis span_eq \<open>subspace U\<close> \<open>dim V < dim U\<close> linear not_le)
   4.268 +    then have "V homeomorphic T"
   4.269 +      by (simp add: \<open>subspace V\<close> homeomorphic_subspaces)
   4.270 +    then obtain h k where homhk: "homeomorphism V T h k"
   4.271 +      using homeomorphic_def  by blast
   4.272 +    have "continuous_on S (h \<circ> f)"
   4.273 +      by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
   4.274 +    moreover have "(h \<circ> f) ` S \<subseteq> U"
   4.275 +      using \<open>T \<subseteq> U\<close> fim homeomorphism_image1 homhk by fastforce
   4.276 +    moreover have "inj_on (h \<circ> f) S"
   4.277 +      apply (clarsimp simp: inj_on_def)
   4.278 +      by (metis fim homeomorphism_apply1 homhk image_subset_iff inj_onD injf)
   4.279 +    ultimately have ope_hf: "openin (subtopology euclidean U) ((h \<circ> f) ` S)"
   4.280 +      using invariance_of_domain_subspaces [OF ope \<open>subspace U\<close> \<open>subspace U\<close>] by auto
   4.281 +    have "(h \<circ> f) ` S \<subseteq> T"
   4.282 +      using fim homeomorphism_image1 homhk by fastforce
   4.283 +    then show ?thesis
   4.284 +      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)
   4.285 +  qed
   4.286 +  then show ?thesis
   4.287 +    using not_less by blast
   4.288 +qed
   4.289 +
   4.290 +corollary invariance_of_domain_affine_sets:
   4.291 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.292 +  assumes ope: "openin (subtopology euclidean U) S"
   4.293 +      and aff: "affine U" "affine V" "aff_dim V \<le> aff_dim U"
   4.294 +      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
   4.295 +      and injf: "inj_on f S"
   4.296 +    shows "openin (subtopology euclidean V) (f ` S)"
   4.297 +proof (cases "S = {}")
   4.298 +  case True
   4.299 +  then show ?thesis by auto
   4.300 +next
   4.301 +  case False
   4.302 +  obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
   4.303 +    using False fim ope openin_contains_cball by fastforce
   4.304 +  have "openin (subtopology euclidean (op + (- b) ` V)) ((op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S)"
   4.305 +  proof (rule invariance_of_domain_subspaces)
   4.306 +    show "openin (subtopology euclidean (op + (- a) ` U)) (op + (- a) ` S)"
   4.307 +      by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
   4.308 +    show "subspace (op + (- a) ` U)"
   4.309 +      by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace \<open>affine U\<close>)
   4.310 +    show "subspace (op + (- b) ` V)"
   4.311 +      by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace \<open>affine V\<close>)
   4.312 +    show "dim (op + (- b) ` V) \<le> dim (op + (- a) ` U)"
   4.313 +      by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
   4.314 +    show "continuous_on (op + (- a) ` S) (op + (- b) \<circ> f \<circ> op + a)"
   4.315 +      by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
   4.316 +    show "(op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S \<subseteq> op + (- b) ` V"
   4.317 +      using fim by auto
   4.318 +    show "inj_on (op + (- b) \<circ> f \<circ> op + a) (op + (- a) ` S)"
   4.319 +      by (auto simp: inj_on_def) (meson inj_onD injf)
   4.320 +  qed
   4.321 +  then show ?thesis
   4.322 +    by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois)
   4.323 +qed
   4.324 +
   4.325 +corollary invariance_of_dimension_affine_sets:
   4.326 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.327 +  assumes ope: "openin (subtopology euclidean U) S"
   4.328 +      and aff: "affine U" "affine V"
   4.329 +      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
   4.330 +      and injf: "inj_on f S" and "S \<noteq> {}"
   4.331 +    shows "aff_dim U \<le> aff_dim V"
   4.332 +proof -
   4.333 +  obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
   4.334 +    using \<open>S \<noteq> {}\<close> fim ope openin_contains_cball by fastforce
   4.335 +  have "dim (op + (- a) ` U) \<le> dim (op + (- b) ` V)"
   4.336 +  proof (rule invariance_of_dimension_subspaces)
   4.337 +    show "openin (subtopology euclidean (op + (- a) ` U)) (op + (- a) ` S)"
   4.338 +      by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
   4.339 +    show "subspace (op + (- a) ` U)"
   4.340 +      by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace \<open>affine U\<close>)
   4.341 +    show "subspace (op + (- b) ` V)"
   4.342 +      by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace \<open>affine V\<close>)
   4.343 +    show "continuous_on (op + (- a) ` S) (op + (- b) \<circ> f \<circ> op + a)"
   4.344 +      by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
   4.345 +    show "(op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S \<subseteq> op + (- b) ` V"
   4.346 +      using fim by auto
   4.347 +    show "inj_on (op + (- b) \<circ> f \<circ> op + a) (op + (- a) ` S)"
   4.348 +      by (auto simp: inj_on_def) (meson inj_onD injf)
   4.349 +  qed (use \<open>S \<noteq> {}\<close> in auto)
   4.350 +  then show ?thesis
   4.351 +    by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
   4.352 +qed
   4.353 +
   4.354 +corollary invariance_of_dimension:
   4.355 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.356 +  assumes contf: "continuous_on S f" and "open S"
   4.357 +      and injf: "inj_on f S" and "S \<noteq> {}"
   4.358 +    shows "DIM('a) \<le> DIM('b)"
   4.359 +  using invariance_of_dimension_subspaces [of UNIV S UNIV f] assms
   4.360 +  by auto
   4.361 +
   4.362 +
   4.363 +corollary continuous_injective_image_subspace_dim_le:
   4.364 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.365 +  assumes "subspace S" "subspace T"
   4.366 +      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
   4.367 +      and injf: "inj_on f S"
   4.368 +    shows "dim S \<le> dim T"
   4.369 +  apply (rule invariance_of_dimension_subspaces [of S S _ f])
   4.370 +  using assms by (auto simp: subspace_affine)
   4.371 +
   4.372 +lemma invariance_of_dimension_convex_domain:
   4.373 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.374 +  assumes "convex S"
   4.375 +      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> affine hull T"
   4.376 +      and injf: "inj_on f S"
   4.377 +    shows "aff_dim S \<le> aff_dim T"
   4.378 +proof (cases "S = {}")
   4.379 +  case True
   4.380 +  then show ?thesis by (simp add: aff_dim_geq)
   4.381 +next
   4.382 +  case False
   4.383 +  have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
   4.384 +  proof (rule invariance_of_dimension_affine_sets)
   4.385 +    show "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
   4.386 +      by (simp add: openin_rel_interior)
   4.387 +    show "continuous_on (rel_interior S) f"
   4.388 +      using contf continuous_on_subset rel_interior_subset by blast
   4.389 +    show "f ` rel_interior S \<subseteq> affine hull T"
   4.390 +      using fim rel_interior_subset by blast
   4.391 +    show "inj_on f (rel_interior S)"
   4.392 +      using inj_on_subset injf rel_interior_subset by blast
   4.393 +    show "rel_interior S \<noteq> {}"
   4.394 +      by (simp add: False \<open>convex S\<close> rel_interior_eq_empty)
   4.395 +  qed auto
   4.396 +  then show ?thesis
   4.397 +    by simp
   4.398 +qed
   4.399 +
   4.400 +
   4.401 +lemma homeomorphic_convex_sets_le:
   4.402 +  assumes "convex S" "S homeomorphic T"
   4.403 +  shows "aff_dim S \<le> aff_dim T"
   4.404 +proof -
   4.405 +  obtain h k where homhk: "homeomorphism S T h k"
   4.406 +    using homeomorphic_def assms  by blast
   4.407 +  show ?thesis
   4.408 +  proof (rule invariance_of_dimension_convex_domain [OF \<open>convex S\<close>])
   4.409 +    show "continuous_on S h"
   4.410 +      using homeomorphism_def homhk by blast
   4.411 +    show "h ` S \<subseteq> affine hull T"
   4.412 +      by (metis homeomorphism_def homhk hull_subset)
   4.413 +    show "inj_on h S"
   4.414 +      by (meson homeomorphism_apply1 homhk inj_on_inverseI)
   4.415 +  qed
   4.416 +qed
   4.417 +
   4.418 +lemma homeomorphic_convex_sets:
   4.419 +  assumes "convex S" "convex T" "S homeomorphic T"
   4.420 +  shows "aff_dim S = aff_dim T"
   4.421 +  by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym)
   4.422 +
   4.423 +lemma homeomorphic_convex_compact_sets_eq:
   4.424 +  assumes "convex S" "compact S" "convex T" "compact T"
   4.425 +  shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
   4.426 +  by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets)
   4.427 +
   4.428 +lemma invariance_of_domain_gen:
   4.429 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.430 +  assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
   4.431 +    shows "open(f ` S)"
   4.432 +  using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto
   4.433 +
   4.434 +lemma injective_into_1d_imp_open_map_UNIV:
   4.435 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
   4.436 +  assumes "open T" "continuous_on S f" "inj_on f S" "T \<subseteq> S"
   4.437 +    shows "open (f ` T)"
   4.438 +  apply (rule invariance_of_domain_gen [OF \<open>open T\<close>])
   4.439 +  using assms apply (auto simp: elim: continuous_on_subset subset_inj_on)
   4.440 +  done
   4.441 +
   4.442 +lemma continuous_on_inverse_open:
   4.443 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.444 +  assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" and gf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
   4.445 +    shows "continuous_on (f ` S) g"
   4.446 +proof (clarsimp simp add: continuous_openin_preimage_eq)
   4.447 +  fix T :: "'a set"
   4.448 +  assume "open T"
   4.449 +  have eq: "{x. x \<in> f ` S \<and> g x \<in> T} = f ` (S \<inter> T)"
   4.450 +    by (auto simp: gf)
   4.451 +  show "openin (subtopology euclidean (f ` S)) {x \<in> f ` S. g x \<in> T}"
   4.452 +    apply (subst eq)
   4.453 +    apply (rule open_openin_trans)
   4.454 +      apply (rule invariance_of_domain_gen)
   4.455 +    using assms
   4.456 +         apply auto
   4.457 +    using inj_on_inverseI apply auto[1]
   4.458 +    by (metis \<open>open T\<close> continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq)
   4.459 +qed
   4.460 +
   4.461 +lemma invariance_of_domain_homeomorphism:
   4.462 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.463 +  assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
   4.464 +  obtains g where "homeomorphism S (f ` S) f g"
   4.465 +proof
   4.466 +  show "homeomorphism S (f ` S) f (inv_into S f)"
   4.467 +    by (simp add: assms continuous_on_inverse_open homeomorphism_def)
   4.468 +qed
   4.469 +
   4.470 +corollary invariance_of_domain_homeomorphic:
   4.471 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.472 +  assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
   4.473 +  shows "S homeomorphic (f ` S)"
   4.474 +  using invariance_of_domain_homeomorphism [OF assms]
   4.475 +  by (meson homeomorphic_def)
   4.476 +
   4.477  end
     5.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Oct 09 16:27:01 2016 +0200
     5.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Oct 10 15:45:41 2016 +0100
     5.3 @@ -2178,7 +2178,7 @@
     5.4  
     5.5  text \<open>More lemmas about dimension.\<close>
     5.6  
     5.7 -lemma dim_UNIV: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
     5.8 +lemma dim_UNIV [simp]: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
     5.9    using independent_Basis
    5.10    by (intro dim_unique[of Basis]) auto
    5.11  
     6.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun Oct 09 16:27:01 2016 +0200
     6.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Mon Oct 10 15:45:41 2016 +0100
     6.3 @@ -1261,8 +1261,90 @@
     6.4    using midpoints_in_convex_hull segment_convex_hull by blast
     6.5  
     6.6  lemma midpoint_in_open_segment [simp]: "midpoint a b \<in> open_segment a b \<longleftrightarrow> a \<noteq> b"
     6.7 -  by (simp add: midpoint_eq_endpoint(1) midpoint_eq_endpoint(2) open_segment_def)
     6.8 -
     6.9 +  by (simp add: open_segment_def)
    6.10 +
    6.11 +lemma continuous_IVT_local_extremum:
    6.12 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
    6.13 +  assumes contf: "continuous_on (closed_segment a b) f"
    6.14 +      and "a \<noteq> b" "f a = f b"
    6.15 +  obtains z where "z \<in> open_segment a b"
    6.16 +                  "(\<forall>w \<in> closed_segment a b. (f w) \<le> (f z)) \<or>
    6.17 +                   (\<forall>w \<in> closed_segment a b. (f z) \<le> (f w))"
    6.18 +proof -
    6.19 +  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"
    6.20 +    using continuous_attains_sup [of "closed_segment a b" f] contf by auto
    6.21 +  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"
    6.22 +    using continuous_attains_inf [of "closed_segment a b" f] contf by auto
    6.23 +  show ?thesis
    6.24 +  proof (cases "c \<in> open_segment a b \<or> d \<in> open_segment a b")
    6.25 +    case True
    6.26 +    then show ?thesis
    6.27 +      using c d that by blast
    6.28 +  next
    6.29 +    case False
    6.30 +    then have "(c = a \<or> c = b) \<and> (d = a \<or> d = b)"
    6.31 +      by (simp add: \<open>c \<in> closed_segment a b\<close> \<open>d \<in> closed_segment a b\<close> open_segment_def)
    6.32 +    with \<open>a \<noteq> b\<close> \<open>f a = f b\<close> c d show ?thesis
    6.33 +      by (rule_tac z = "midpoint a b" in that) (fastforce+)
    6.34 +  qed
    6.35 +qed
    6.36 +
    6.37 +text\<open>An injective map into R is also an open map w.r.T. the universe, and conversely. \<close>
    6.38 +proposition injective_eq_1d_open_map_UNIV:
    6.39 +  fixes f :: "real \<Rightarrow> real"
    6.40 +  assumes contf: "continuous_on S f" and S: "is_interval S"
    6.41 +    shows "inj_on f S \<longleftrightarrow> (\<forall>T. open T \<and> T \<subseteq> S \<longrightarrow> open(f ` T))"
    6.42 +          (is "?lhs = ?rhs")
    6.43 +proof safe
    6.44 +  fix T
    6.45 +  assume injf: ?lhs and "open T" and "T \<subseteq> S"
    6.46 +  have "\<exists>U. open U \<and> f x \<in> U \<and> U \<subseteq> f ` T" if "x \<in> T" for x
    6.47 +  proof -
    6.48 +    obtain \<delta> where "\<delta> > 0" and \<delta>: "cball x \<delta> \<subseteq> T"
    6.49 +      using \<open>open T\<close> \<open>x \<in> T\<close> open_contains_cball_eq by blast
    6.50 +    show ?thesis
    6.51 +    proof (intro exI conjI)
    6.52 +      have "closed_segment (x-\<delta>) (x+\<delta>) = {x-\<delta>..x+\<delta>}"
    6.53 +        using \<open>0 < \<delta>\<close> by (auto simp: closed_segment_eq_real_ivl)
    6.54 +      also have "... \<subseteq> S"
    6.55 +        using \<delta> \<open>T \<subseteq> S\<close> by (auto simp: dist_norm subset_eq)
    6.56 +      finally have "f ` (open_segment (x-\<delta>) (x+\<delta>)) = open_segment (f (x-\<delta>)) (f (x+\<delta>))"
    6.57 +        using continuous_injective_image_open_segment_1
    6.58 +        by (metis continuous_on_subset [OF contf] inj_on_subset [OF injf])
    6.59 +      then show "open (f ` {x-\<delta><..<x+\<delta>})"
    6.60 +        using \<open>0 < \<delta>\<close> by (simp add: open_segment_eq_real_ivl)
    6.61 +      show "f x \<in> f ` {x - \<delta><..<x + \<delta>}"
    6.62 +        by (auto simp: \<open>\<delta> > 0\<close>)
    6.63 +      show "f ` {x - \<delta><..<x + \<delta>} \<subseteq> f ` T"
    6.64 +        using \<delta> by (auto simp: dist_norm subset_iff)
    6.65 +    qed
    6.66 +  qed
    6.67 +  with open_subopen show "open (f ` T)"
    6.68 +    by blast
    6.69 +next
    6.70 +  assume R: ?rhs
    6.71 +  have False if xy: "x \<in> S" "y \<in> S" and "f x = f y" "x \<noteq> y" for x y
    6.72 +  proof -
    6.73 +    have "open (f ` open_segment x y)"
    6.74 +      using R
    6.75 +      by (metis S convex_contains_open_segment is_interval_convex open_greaterThanLessThan open_segment_eq_real_ivl xy)
    6.76 +    moreover
    6.77 +    have "continuous_on (closed_segment x y) f"
    6.78 +      by (meson S closed_segment_subset contf continuous_on_subset is_interval_convex that)
    6.79 +    then obtain \<xi> where "\<xi> \<in> open_segment x y"
    6.80 +                    and \<xi>: "(\<forall>w \<in> closed_segment x y. (f w) \<le> (f \<xi>)) \<or>
    6.81 +                            (\<forall>w \<in> closed_segment x y. (f \<xi>) \<le> (f w))"
    6.82 +      using continuous_IVT_local_extremum [of x y f] \<open>f x = f y\<close> \<open>x \<noteq> y\<close> by blast
    6.83 +    ultimately obtain e where "e>0" and e: "\<And>u. dist u (f \<xi>) < e \<Longrightarrow> u \<in> f ` open_segment x y"
    6.84 +      using open_dist by (metis image_eqI)
    6.85 +    have fin: "f \<xi> + (e/2) \<in> f ` open_segment x y" "f \<xi> - (e/2) \<in> f ` open_segment x y"
    6.86 +      using e [of "f \<xi> + (e/2)"] e [of "f \<xi> - (e/2)"] \<open>e > 0\<close> by (auto simp: dist_norm)
    6.87 +    show ?thesis
    6.88 +      using \<xi> \<open>0 < e\<close> fin open_closed_segment by fastforce
    6.89 +  qed
    6.90 +  then show ?lhs
    6.91 +    by (force simp: inj_on_def)
    6.92 +qed
    6.93  
    6.94  subsection \<open>Bounding a point away from a path\<close>
    6.95  
    6.96 @@ -2319,9 +2401,10 @@
    6.97    by (metis cobounded_unique_unbounded_component)
    6.98  
    6.99  lemma cobounded_has_bounded_component:
   6.100 -    fixes s :: "'a :: euclidean_space set"
   6.101 -    shows "\<lbrakk>bounded (- s); ~connected s; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> components s \<and> bounded c"
   6.102 -  by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq)
   6.103 +  fixes S :: "'a :: euclidean_space set"
   6.104 +  assumes "bounded (- S)" "\<not> connected S" "2 \<le> DIM('a)"
   6.105 +  obtains C where "C \<in> components S" "bounded C"
   6.106 +  by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq assms)
   6.107  
   6.108  
   6.109  section\<open>The "inside" and "outside" of a set\<close>
   6.110 @@ -7510,7 +7593,7 @@
   6.111      have hUS: "h ` U \<subseteq> h ` S"
   6.112        by (meson homeomorphism_imp_open_map homeomorphism_of_subsets homhj hull_subset opeS opeU open_UNIV openin_open_eq)
   6.113      have op: "openin (subtopology euclidean (affine hull S)) U \<Longrightarrow> open (h ` U)" for U
   6.114 -      using homeomorphism_imp_open_map [OF homhj]  by (simp add: open_openin)
   6.115 +      using homeomorphism_imp_open_map [OF homhj]  by simp
   6.116      have "open (h ` U)" "open (h ` S)"
   6.117        by (auto intro: opeS opeU openin_trans op)
   6.118      then obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g"
     7.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 09 16:27:01 2016 +0200
     7.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Oct 10 15:45:41 2016 +0100
     7.3 @@ -18,6 +18,11 @@
     7.4  
     7.5  (* FIXME: move elsewhere *)
     7.6  
     7.7 +lemma Times_eq_image_sum:
     7.8 +  fixes S :: "'a :: comm_monoid_add set" and T :: "'b :: comm_monoid_add set"
     7.9 +  shows "S \<times> T = {u + v |u v. u \<in> (\<lambda>x. (x, 0)) ` S \<and> v \<in> Pair 0 ` T}"
    7.10 +  by force
    7.11 +
    7.12  lemma halfspace_Int_eq:
    7.13       "{x. a \<bullet> x \<le> b} \<inter> {x. b \<le> a \<bullet> x} = {x. a \<bullet> x = b}"
    7.14       "{x. b \<le> a \<bullet> x} \<inter> {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
    7.15 @@ -730,20 +735,19 @@
    7.16    apply (auto simp add: istopology_def)
    7.17    done
    7.18  
    7.19 +declare open_openin [symmetric, simp]
    7.20 +
    7.21  lemma topspace_euclidean [simp]: "topspace euclidean = UNIV"
    7.22 -  apply (simp add: topspace_def)
    7.23 -  apply (rule set_eqI)
    7.24 -  apply (auto simp add: open_openin[symmetric])
    7.25 -  done
    7.26 +  by (force simp add: topspace_def)
    7.27  
    7.28  lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S"
    7.29 -  by (simp add: topspace_euclidean topspace_subtopology)
    7.30 +  by (simp add: topspace_subtopology)
    7.31  
    7.32  lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
    7.33 -  by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV)
    7.34 +  by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)
    7.35  
    7.36  lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
    7.37 -  by (simp add: open_openin openin_subopen[symmetric])
    7.38 +  using openI by auto
    7.39  
    7.40  lemma openin_subtopology_self [simp]: "openin (subtopology euclidean S) S"
    7.41    by (metis openin_topspace topspace_euclidean_subtopology)
    7.42 @@ -751,7 +755,7 @@
    7.43  text \<open>Basic "localization" results are handy for connectedness.\<close>
    7.44  
    7.45  lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
    7.46 -  by (auto simp add: openin_subtopology open_openin[symmetric])
    7.47 +  by (auto simp add: openin_subtopology)
    7.48  
    7.49  lemma openin_Int_open:
    7.50     "\<lbrakk>openin (subtopology euclidean U) S; open T\<rbrakk>
    7.51 @@ -1968,7 +1972,7 @@
    7.52  lemma closure_UNIV [simp]: "closure UNIV = UNIV"
    7.53    using closed_UNIV by (rule closure_closed)
    7.54  
    7.55 -lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
    7.56 +lemma closure_Un [simp]: "closure (S \<union> T) = closure S \<union> closure T"
    7.57    unfolding closure_interior by simp
    7.58  
    7.59  lemma closure_eq_empty [iff]: "closure S = {} \<longleftrightarrow> S = {}"
    7.60 @@ -2084,6 +2088,71 @@
    7.61       \<Longrightarrow> openin (subtopology euclidean T) S"
    7.62    by (auto simp: openin_open)
    7.63  
    7.64 +lemma openin_Times:
    7.65 +   "\<lbrakk>openin (subtopology euclidean S) S'; openin (subtopology euclidean T) T'\<rbrakk>
    7.66 +    \<Longrightarrow> openin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
    7.67 +  unfolding openin_open using open_Times by blast
    7.68 +
    7.69 +lemma Times_in_interior_subtopology:
    7.70 +  fixes U :: "('a::metric_space * 'b::metric_space) set"
    7.71 +  assumes "(x, y) \<in> U" "openin (subtopology euclidean (S \<times> T)) U"
    7.72 +  obtains V W where "openin (subtopology euclidean S) V" "x \<in> V"
    7.73 +                    "openin (subtopology euclidean T) W" "y \<in> W" "(V \<times> W) \<subseteq> U"
    7.74 +proof -
    7.75 +  from assms obtain e where "e > 0" and "U \<subseteq> S \<times> T"
    7.76 +                and e: "\<And>x' y'. \<lbrakk>x'\<in>S; y'\<in>T; dist (x', y') (x, y) < e\<rbrakk> \<Longrightarrow> (x', y') \<in> U"
    7.77 +    by (force simp: openin_euclidean_subtopology_iff)
    7.78 +  with assms have "x \<in> S" "y \<in> T"
    7.79 +    by auto
    7.80 +  show ?thesis
    7.81 +  proof
    7.82 +    show "openin (subtopology euclidean S) (ball x (e/2) \<inter> S)"
    7.83 +      by (simp add: Int_commute openin_open_Int)
    7.84 +    show "x \<in> ball x (e / 2) \<inter> S"
    7.85 +      by (simp add: \<open>0 < e\<close> \<open>x \<in> S\<close>)
    7.86 +    show "openin (subtopology euclidean T) (ball y (e/2) \<inter> T)"
    7.87 +      by (simp add: Int_commute openin_open_Int)
    7.88 +    show "y \<in> ball y (e / 2) \<inter> T"
    7.89 +      by (simp add: \<open>0 < e\<close> \<open>y \<in> T\<close>)
    7.90 +    show "(ball x (e / 2) \<inter> S) \<times> (ball y (e / 2) \<inter> T) \<subseteq> U"
    7.91 +      by clarify (simp add: e dist_Pair_Pair \<open>0 < e\<close> dist_commute sqrt_sum_squares_half_less)
    7.92 +  qed
    7.93 +qed
    7.94 +
    7.95 +lemma openin_Times_eq:
    7.96 +  fixes S :: "'a::metric_space set" and T :: "'b::metric_space set"
    7.97 +  shows
    7.98 +   "openin (subtopology euclidean (S \<times> T)) (S' \<times> T') \<longleftrightarrow>
    7.99 +    (S' = {} \<or> T' = {} \<or>
   7.100 +     openin (subtopology euclidean S) S' \<and> openin (subtopology euclidean T) T')"
   7.101 +    (is "?lhs = ?rhs")
   7.102 +proof (cases "S' = {} \<or> T' = {}")
   7.103 +  case True
   7.104 +  then show ?thesis by auto
   7.105 +next
   7.106 +  case False
   7.107 +  then obtain x y where "x \<in> S'" "y \<in> T'"
   7.108 +    by blast
   7.109 +  show ?thesis
   7.110 +  proof
   7.111 +    assume L: ?lhs
   7.112 +    have "openin (subtopology euclidean S) S'"
   7.113 +      apply (subst openin_subopen, clarify)
   7.114 +      apply (rule Times_in_interior_subtopology [OF _ L])
   7.115 +      using \<open>y \<in> T'\<close> by auto
   7.116 +    moreover have "openin (subtopology euclidean T) T'"
   7.117 +      apply (subst openin_subopen, clarify)
   7.118 +      apply (rule Times_in_interior_subtopology [OF _ L])
   7.119 +      using \<open>x \<in> S'\<close> by auto
   7.120 +    ultimately show ?rhs
   7.121 +      by simp
   7.122 +  next
   7.123 +    assume ?rhs
   7.124 +    with False show ?lhs
   7.125 +      by (simp add: openin_Times)
   7.126 +  qed
   7.127 +qed
   7.128 +
   7.129  lemma closedin_Times:
   7.130     "\<lbrakk>closedin (subtopology euclidean S) S'; closedin (subtopology euclidean T) T'\<rbrakk>
   7.131      \<Longrightarrow> closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
   7.132 @@ -8502,7 +8571,7 @@
   7.133  proof -
   7.134    from gt_ex obtain b where "a < b" by auto
   7.135    hence "{a<..} = {a<..<b} \<union> {b..}" by auto
   7.136 -  also have "closure \<dots> = {a..}" using \<open>a < b\<close> unfolding closure_union
   7.137 +  also have "closure \<dots> = {a..}" using \<open>a < b\<close> unfolding closure_Un
   7.138      by auto
   7.139    finally show ?thesis .
   7.140  qed
   7.141 @@ -8513,7 +8582,7 @@
   7.142  proof -
   7.143    from lt_ex obtain a where "a < b" by auto
   7.144    hence "{..<b} = {a<..<b} \<union> {..a}" by auto
   7.145 -  also have "closure \<dots> = {..b}" using \<open>a < b\<close> unfolding closure_union
   7.146 +  also have "closure \<dots> = {..b}" using \<open>a < b\<close> unfolding closure_Un
   7.147      by auto
   7.148    finally show ?thesis .
   7.149  qed
   7.150 @@ -8524,7 +8593,7 @@
   7.151    shows "closure {a ..< b} = {a .. b}"
   7.152  proof -
   7.153    from assms have "{a ..< b} = {a} \<union> {a <..< b}" by auto
   7.154 -  also have "closure \<dots> = {a .. b}" unfolding closure_union
   7.155 +  also have "closure \<dots> = {a .. b}" unfolding closure_Un
   7.156      by (auto simp add: assms less_imp_le)
   7.157    finally show ?thesis .
   7.158  qed
   7.159 @@ -8535,7 +8604,7 @@
   7.160    shows "closure {a <.. b} = {a .. b}"
   7.161  proof -
   7.162    from assms have "{a <.. b} = {b} \<union> {a <..< b}" by auto
   7.163 -  also have "closure \<dots> = {a .. b}" unfolding closure_union
   7.164 +  also have "closure \<dots> = {a .. b}" unfolding closure_Un
   7.165      by (auto simp add: assms less_imp_le)
   7.166    finally show ?thesis .
   7.167  qed
     8.1 --- a/src/HOL/NthRoot.thy	Sun Oct 09 16:27:01 2016 +0200
     8.2 +++ b/src/HOL/NthRoot.thy	Mon Oct 10 15:45:41 2016 +0100
     8.3 @@ -692,15 +692,12 @@
     8.4    by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four
     8.5        real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85))
     8.6  
     8.7 -
     8.8 -text \<open>Needed for the infinitely close relation over the nonstandard complex numbers.\<close>
     8.9 -lemma lemma_sqrt_hcomplex_capprox:
    8.10 -  "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"
    8.11 +lemma sqrt_sum_squares_half_less:
    8.12 +  "x < u/2 \<Longrightarrow> y < u/2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u"
    8.13    apply (rule real_sqrt_sum_squares_less)
    8.14     apply (auto simp add: abs_if field_simps)
    8.15     apply (rule le_less_trans [where y = "x*2"])
    8.16 -  using less_eq_real_def sqrt2_less_2
    8.17 -    apply force
    8.18 +  using less_eq_real_def sqrt2_less_2 apply force
    8.19     apply assumption
    8.20    apply (rule le_less_trans [where y = "y*2"])
    8.21    using less_eq_real_def sqrt2_less_2 mult_le_cancel_left