src/HOL/Analysis/Continuous_Extension.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69518 bf88364c9e94 child 69918 eddcc7c726f3 permissions -rw-r--r--
capitalize proper names in lemma names
```     1 (*  Title:      HOL/Analysis/Continuous_Extension.thy
```
```     2     Authors:    LC Paulson, based on material from HOL Light
```
```     3 *)
```
```     4
```
```     5 section \<open>Continuous Extensions of Functions\<close>
```
```     6
```
```     7 theory Continuous_Extension
```
```     8 imports Starlike
```
```     9 begin
```
```    10
```
```    11 subsection\<open>Partitions of unity subordinate to locally finite open coverings\<close>
```
```    12
```
```    13 text\<open>A difference from HOL Light: all summations over infinite sets equal zero,
```
```    14    so the "support" must be made explicit in the summation below!\<close>
```
```    15
```
```    16 proposition subordinate_partition_of_unity:
```
```    17   fixes S :: "'a :: euclidean_space set"
```
```    18   assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
```
```    19       and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
```
```    20   obtains F :: "['a set, 'a] \<Rightarrow> real"
```
```    21     where "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x \<in> S. 0 \<le> F U x)"
```
```    22       and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
```
```    23       and "\<And>x. x \<in> S \<Longrightarrow> supp_sum (\<lambda>W. F W x) \<C> = 1"
```
```    24       and "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}"
```
```    25 proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
```
```    26   case True
```
```    27     then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
```
```    28     then show ?thesis
```
```    29       apply (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that)
```
```    30       apply (auto simp: continuous_on_const supp_sum_def support_on_def)
```
```    31       done
```
```    32 next
```
```    33   case False
```
```    34     have nonneg: "0 \<le> supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" for x
```
```    35       by (simp add: supp_sum_def sum_nonneg)
```
```    36     have sd_pos: "0 < setdist {x} (S - V)" if "V \<in> \<C>" "x \<in> S" "x \<in> V" for V x
```
```    37     proof -
```
```    38       have "closedin (subtopology euclidean S) (S - V)"
```
```    39         by (simp add: Diff_Diff_Int closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
```
```    40       with that False setdist_eq_0_closedin [of S "S-V" x] setdist_pos_le [of "{x}" "S - V"]
```
```    41         show ?thesis
```
```    42           by (simp add: order_class.order.order_iff_strict)
```
```    43     qed
```
```    44     have ss_pos: "0 < supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" if "x \<in> S" for x
```
```    45     proof -
```
```    46       obtain U where "U \<in> \<C>" "x \<in> U" using \<open>x \<in> S\<close> \<open>S \<subseteq> \<Union>\<C>\<close>
```
```    47         by blast
```
```    48       obtain V where "open V" "x \<in> V" "finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
```
```    49         using \<open>x \<in> S\<close> fin by blast
```
```    50       then have *: "finite {A \<in> \<C>. \<not> S \<subseteq> A \<and> x \<notin> closure (S - A)}"
```
```    51         using closure_def that by (blast intro: rev_finite_subset)
```
```    52       have "x \<notin> closure (S - U)"
```
```    53         by (metis \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> less_irrefl sd_pos setdist_eq_0_sing_1 that)
```
```    54       then show ?thesis
```
```    55         apply (simp add: setdist_eq_0_sing_1 supp_sum_def support_on_def)
```
```    56         apply (rule ordered_comm_monoid_add_class.sum_pos2 [OF *, of U])
```
```    57         using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> False
```
```    58         apply (auto simp: setdist_pos_le sd_pos that)
```
```    59         done
```
```    60     qed
```
```    61     define F where
```
```    62       "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>
```
```    63                  else 0"
```
```    64     show ?thesis
```
```    65     proof (rule_tac F = F in that)
```
```    66       have "continuous_on S (F U)" if "U \<in> \<C>" for U
```
```    67       proof -
```
```    68         have *: "continuous_on S (\<lambda>x. supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>)"
```
```    69         proof (clarsimp simp add: continuous_on_eq_continuous_within)
```
```    70           fix x assume "x \<in> S"
```
```    71           then obtain X where "open X" and x: "x \<in> S \<inter> X" and finX: "finite {U \<in> \<C>. U \<inter> X \<noteq> {}}"
```
```    72             using assms by blast
```
```    73           then have OSX: "openin (subtopology euclidean S) (S \<inter> X)" by blast
```
```    74           have sumeq: "\<And>x. x \<in> S \<inter> X \<Longrightarrow>
```
```    75                      (\<Sum>V | V \<in> \<C> \<and> V \<inter> X \<noteq> {}. setdist {x} (S - V))
```
```    76                      = supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>"
```
```    77             apply (simp add: supp_sum_def)
```
```    78             apply (rule sum.mono_neutral_right [OF finX])
```
```    79             apply (auto simp: setdist_eq_0_sing_1 support_on_def subset_iff)
```
```    80             apply (meson DiffI closure_subset disjoint_iff_not_equal subsetCE)
```
```    81             done
```
```    82           show "continuous (at x within S) (\<lambda>x. supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>)"
```
```    83             apply (rule continuous_transform_within_openin
```
```    84                      [where f = "\<lambda>x. (sum (\<lambda>V. setdist {x} (S - V)) {V \<in> \<C>. V \<inter> X \<noteq> {}})"
```
```    85                         and S ="S \<inter> X"])
```
```    86             apply (rule continuous_intros continuous_at_setdist continuous_at_imp_continuous_at_within OSX x)+
```
```    87             apply (simp add: sumeq)
```
```    88             done
```
```    89         qed
```
```    90         show ?thesis
```
```    91           apply (simp add: F_def)
```
```    92           apply (rule continuous_intros *)+
```
```    93           using ss_pos apply force
```
```    94           done
```
```    95       qed
```
```    96       moreover have "\<lbrakk>U \<in> \<C>; x \<in> S\<rbrakk> \<Longrightarrow> 0 \<le> F U x" for U x
```
```    97         using nonneg [of x] by (simp add: F_def divide_simps setdist_pos_le)
```
```    98       ultimately show "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x\<in>S. 0 \<le> F U x)"
```
```    99         by metis
```
```   100     next
```
```   101       show "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
```
```   102         by (simp add: setdist_eq_0_sing_1 closure_def F_def)
```
```   103     next
```
```   104       show "supp_sum (\<lambda>W. F W x) \<C> = 1" if "x \<in> S" for x
```
```   105         using that ss_pos [OF that]
```
```   106         by (simp add: F_def divide_simps supp_sum_divide_distrib [symmetric])
```
```   107     next
```
```   108       show "\<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}" if "x \<in> S" for x
```
```   109         using fin [OF that] that
```
```   110         by (fastforce simp: setdist_eq_0_sing_1 closure_def F_def elim!: rev_finite_subset)
```
```   111     qed
```
```   112 qed
```
```   113
```
```   114
```
```   115 subsection\<open>Urysohn's Lemma for Euclidean Spaces\<close>
```
```   116
```
```   117 text \<open>For Euclidean spaces the proof is easy using distances.\<close>
```
```   118
```
```   119 lemma Urysohn_both_ne:
```
```   120   assumes US: "closedin (subtopology euclidean U) S"
```
```   121       and UT: "closedin (subtopology euclidean U) T"
```
```   122       and "S \<inter> T = {}" "S \<noteq> {}" "T \<noteq> {}" "a \<noteq> b"
```
```   123   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
```
```   124     where "continuous_on U f"
```
```   125           "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
```
```   126           "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
```
```   127           "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
```
```   128 proof -
```
```   129   have S0: "\<And>x. x \<in> U \<Longrightarrow> setdist {x} S = 0 \<longleftrightarrow> x \<in> S"
```
```   130     using \<open>S \<noteq> {}\<close>  US setdist_eq_0_closedin  by auto
```
```   131   have T0: "\<And>x. x \<in> U \<Longrightarrow> setdist {x} T = 0 \<longleftrightarrow> x \<in> T"
```
```   132     using \<open>T \<noteq> {}\<close>  UT setdist_eq_0_closedin  by auto
```
```   133   have sdpos: "0 < setdist {x} S + setdist {x} T" if "x \<in> U" for x
```
```   134   proof -
```
```   135     have "\<not> (setdist {x} S = 0 \<and> setdist {x} T = 0)"
```
```   136       using assms by (metis IntI empty_iff setdist_eq_0_closedin that)
```
```   137     then show ?thesis
```
```   138       by (metis add.left_neutral add.right_neutral add_pos_pos linorder_neqE_linordered_idom not_le setdist_pos_le)
```
```   139   qed
```
```   140   define f where "f \<equiv> \<lambda>x. a + (setdist {x} S / (setdist {x} S + setdist {x} T)) *\<^sub>R (b - a)"
```
```   141   show ?thesis
```
```   142   proof (rule_tac f = f in that)
```
```   143     show "continuous_on U f"
```
```   144       using sdpos unfolding f_def
```
```   145       by (intro continuous_intros | force)+
```
```   146     show "f x \<in> closed_segment a b" if "x \<in> U" for x
```
```   147         unfolding f_def
```
```   148       apply (simp add: closed_segment_def)
```
```   149       apply (rule_tac x="(setdist {x} S / (setdist {x} S + setdist {x} T))" in exI)
```
```   150       using sdpos that apply (simp add: algebra_simps)
```
```   151       done
```
```   152     show "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
```
```   153       using S0 \<open>a \<noteq> b\<close> f_def sdpos by force
```
```   154     show "(f x = b \<longleftrightarrow> x \<in> T)" if "x \<in> U" for x
```
```   155     proof -
```
```   156       have "f x = b \<longleftrightarrow> (setdist {x} S / (setdist {x} S + setdist {x} T)) = 1"
```
```   157         unfolding f_def
```
```   158         apply (rule iffI)
```
```   159          apply (metis  \<open>a \<noteq> b\<close> add_diff_cancel_left' eq_iff_diff_eq_0 pth_1 real_vector.scale_right_imp_eq, force)
```
```   160         done
```
```   161       also have "...  \<longleftrightarrow> setdist {x} T = 0 \<and> setdist {x} S \<noteq> 0"
```
```   162         using sdpos that
```
```   163         by (simp add: divide_simps) linarith
```
```   164       also have "...  \<longleftrightarrow> x \<in> T"
```
```   165         using \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>S \<inter> T = {}\<close> that
```
```   166         by (force simp: S0 T0)
```
```   167       finally show ?thesis .
```
```   168     qed
```
```   169   qed
```
```   170 qed
```
```   171
```
```   172 proposition Urysohn_local_strong:
```
```   173   assumes US: "closedin (subtopology euclidean U) S"
```
```   174       and UT: "closedin (subtopology euclidean U) T"
```
```   175       and "S \<inter> T = {}" "a \<noteq> b"
```
```   176   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```   177     where "continuous_on U f"
```
```   178           "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
```
```   179           "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
```
```   180           "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
```
```   181 proof (cases "S = {}")
```
```   182   case True show ?thesis
```
```   183   proof (cases "T = {}")
```
```   184     case True show ?thesis
```
```   185     proof (rule_tac f = "\<lambda>x. midpoint a b" in that)
```
```   186       show "continuous_on U (\<lambda>x. midpoint a b)"
```
```   187         by (intro continuous_intros)
```
```   188       show "midpoint a b \<in> closed_segment a b"
```
```   189         using csegment_midpoint_subset by blast
```
```   190       show "(midpoint a b = a) = (x \<in> S)" for x
```
```   191         using \<open>S = {}\<close> \<open>a \<noteq> b\<close> by simp
```
```   192       show "(midpoint a b = b) = (x \<in> T)" for x
```
```   193         using \<open>T = {}\<close> \<open>a \<noteq> b\<close> by simp
```
```   194     qed
```
```   195   next
```
```   196     case False
```
```   197     show ?thesis
```
```   198     proof (cases "T = U")
```
```   199       case True with \<open>S = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
```
```   200         by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
```
```   201     next
```
```   202       case False
```
```   203       with UT closedin_subset obtain c where c: "c \<in> U" "c \<notin> T"
```
```   204         by fastforce
```
```   205       obtain f where f: "continuous_on U f"
```
```   206                 "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment (midpoint a b) b"
```
```   207                 "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
```
```   208                 "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
```
```   209         apply (rule Urysohn_both_ne [of U "{c}" T "midpoint a b" "b"])
```
```   210         using c \<open>T \<noteq> {}\<close> assms apply simp_all
```
```   211         done
```
```   212       show ?thesis
```
```   213         apply (rule_tac f=f in that)
```
```   214         using \<open>S = {}\<close> \<open>T \<noteq> {}\<close> f csegment_midpoint_subset notin_segment_midpoint [OF \<open>a \<noteq> b\<close>]
```
```   215         apply force+
```
```   216         done
```
```   217     qed
```
```   218   qed
```
```   219 next
```
```   220   case False
```
```   221   show ?thesis
```
```   222   proof (cases "T = {}")
```
```   223     case True show ?thesis
```
```   224     proof (cases "S = U")
```
```   225       case True with \<open>T = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
```
```   226         by (rule_tac f = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
```
```   227     next
```
```   228       case False
```
```   229       with US closedin_subset obtain c where c: "c \<in> U" "c \<notin> S"
```
```   230         by fastforce
```
```   231       obtain f where f: "continuous_on U f"
```
```   232                 "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a (midpoint a b)"
```
```   233                 "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
```
```   234                 "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
```
```   235         apply (rule Urysohn_both_ne [of U S "{c}" a "midpoint a b"])
```
```   236         using c \<open>S \<noteq> {}\<close> assms apply simp_all
```
```   237         apply (metis midpoint_eq_endpoint)
```
```   238         done
```
```   239       show ?thesis
```
```   240         apply (rule_tac f=f in that)
```
```   241         using \<open>S \<noteq> {}\<close> \<open>T = {}\<close> f  \<open>a \<noteq> b\<close>
```
```   242         apply simp_all
```
```   243         apply (metis (no_types) closed_segment_commute csegment_midpoint_subset midpoint_sym subset_iff)
```
```   244         apply (metis closed_segment_commute midpoint_sym notin_segment_midpoint)
```
```   245         done
```
```   246     qed
```
```   247   next
```
```   248     case False
```
```   249     show ?thesis
```
```   250       using Urysohn_both_ne [OF US UT \<open>S \<inter> T = {}\<close> \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>a \<noteq> b\<close>] that
```
```   251       by blast
```
```   252   qed
```
```   253 qed
```
```   254
```
```   255 lemma Urysohn_local:
```
```   256   assumes US: "closedin (subtopology euclidean U) S"
```
```   257       and UT: "closedin (subtopology euclidean U) T"
```
```   258       and "S \<inter> T = {}"
```
```   259   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```   260     where "continuous_on U f"
```
```   261           "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
```
```   262           "\<And>x. x \<in> S \<Longrightarrow> f x = a"
```
```   263           "\<And>x. x \<in> T \<Longrightarrow> f x = b"
```
```   264 proof (cases "a = b")
```
```   265   case True then show ?thesis
```
```   266     by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
```
```   267 next
```
```   268   case False
```
```   269   then show ?thesis
```
```   270     apply (rule Urysohn_local_strong [OF assms])
```
```   271     apply (erule that, assumption)
```
```   272     apply (meson US closedin_singleton closedin_trans)
```
```   273     apply (meson UT closedin_singleton closedin_trans)
```
```   274     done
```
```   275 qed
```
```   276
```
```   277 lemma Urysohn_strong:
```
```   278   assumes US: "closed S"
```
```   279       and UT: "closed T"
```
```   280       and "S \<inter> T = {}" "a \<noteq> b"
```
```   281   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```   282     where "continuous_on UNIV f"
```
```   283           "\<And>x. f x \<in> closed_segment a b"
```
```   284           "\<And>x. f x = a \<longleftrightarrow> x \<in> S"
```
```   285           "\<And>x. f x = b \<longleftrightarrow> x \<in> T"
```
```   286 using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
```
```   287
```
```   288 proposition Urysohn:
```
```   289   assumes US: "closed S"
```
```   290       and UT: "closed T"
```
```   291       and "S \<inter> T = {}"
```
```   292   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```   293     where "continuous_on UNIV f"
```
```   294           "\<And>x. f x \<in> closed_segment a b"
```
```   295           "\<And>x. x \<in> S \<Longrightarrow> f x = a"
```
```   296           "\<And>x. x \<in> T \<Longrightarrow> f x = b"
```
```   297   using assms by (auto intro: Urysohn_local [of UNIV S T a b])
```
```   298
```
```   299
```
```   300 subsection\<open>Dugundji's Extension Theorem and Tietze Variants\<close>
```
```   301
```
```   302 text \<open>See \cite{dugundji}.\<close>
```
```   303
```
```   304 theorem Dugundji:
```
```   305   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
```
```   306   assumes "convex C" "C \<noteq> {}"
```
```   307       and cloin: "closedin (subtopology euclidean U) S"
```
```   308       and contf: "continuous_on S f" and "f ` S \<subseteq> C"
```
```   309   obtains g where "continuous_on U g" "g ` U \<subseteq> C"
```
```   310                   "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
```
```   311 proof (cases "S = {}")
```
```   312   case True then show thesis
```
```   313     apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
```
```   314       apply (rule continuous_intros)
```
```   315      apply (meson all_not_in_conv \<open>C \<noteq> {}\<close> image_subsetI someI_ex, simp)
```
```   316     done
```
```   317 next
```
```   318   case False
```
```   319   then have sd_pos: "\<And>x. \<lbrakk>x \<in> U; x \<notin> S\<rbrakk> \<Longrightarrow> 0 < setdist {x} S"
```
```   320     using setdist_eq_0_closedin [OF cloin] le_less setdist_pos_le by fastforce
```
```   321   define \<B> where "\<B> = {ball x (setdist {x} S / 2) |x. x \<in> U - S}"
```
```   322   have [simp]: "\<And>T. T \<in> \<B> \<Longrightarrow> open T"
```
```   323     by (auto simp: \<B>_def)
```
```   324   have USS: "U - S \<subseteq> \<Union>\<B>"
```
```   325     by (auto simp: sd_pos \<B>_def)
```
```   326   obtain \<C> where USsub: "U - S \<subseteq> \<Union>\<C>"
```
```   327        and nbrhd: "\<And>U. U \<in> \<C> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<B> \<and> U \<subseteq> T)"
```
```   328        and fin: "\<And>x. x \<in> U - S
```
```   329                      \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}"
```
```   330     using paracompact [OF USS] by auto
```
```   331   have "\<exists>v a. v \<in> U \<and> v \<notin> S \<and> a \<in> S \<and>
```
```   332               T \<subseteq> ball v (setdist {v} S / 2) \<and>
```
```   333               dist v a \<le> 2 * setdist {v} S" if "T \<in> \<C>" for T
```
```   334   proof -
```
```   335     obtain v where v: "T \<subseteq> ball v (setdist {v} S / 2)" "v \<in> U" "v \<notin> S"
```
```   336       using \<open>T \<in> \<C>\<close> nbrhd by (force simp: \<B>_def)
```
```   337     then obtain a where "a \<in> S" "dist v a < 2 * setdist {v} S"
```
```   338       using setdist_ltE [of "{v}" S "2 * setdist {v} S"]
```
```   339       using False sd_pos by force
```
```   340     with v show ?thesis
```
```   341       apply (rule_tac x=v in exI)
```
```   342       apply (rule_tac x=a in exI, auto)
```
```   343       done
```
```   344   qed
```
```   345   then obtain \<V> \<A> where
```
```   346     VA: "\<And>T. T \<in> \<C> \<Longrightarrow> \<V> T \<in> U \<and> \<V> T \<notin> S \<and> \<A> T \<in> S \<and>
```
```   347               T \<subseteq> ball (\<V> T) (setdist {\<V> T} S / 2) \<and>
```
```   348               dist (\<V> T) (\<A> T) \<le> 2 * setdist {\<V> T} S"
```
```   349     by metis
```
```   350   have sdle: "setdist {\<V> T} S \<le> 2 * setdist {v} S" if "T \<in> \<C>" "v \<in> T" for T v
```
```   351     using setdist_Lipschitz [of "\<V> T" S v] VA [OF \<open>T \<in> \<C>\<close>] \<open>v \<in> T\<close> by auto
```
```   352   have d6: "dist a (\<A> T) \<le> 6 * dist a v" if "T \<in> \<C>" "v \<in> T" "a \<in> S" for T v a
```
```   353   proof -
```
```   354     have "dist (\<V> T) v < setdist {\<V> T} S / 2"
```
```   355       using that VA mem_ball by blast
```
```   356     also have "... \<le> setdist {v} S"
```
```   357       using sdle [OF \<open>T \<in> \<C>\<close> \<open>v \<in> T\<close>] by simp
```
```   358     also have vS: "setdist {v} S \<le> dist a v"
```
```   359       by (simp add: setdist_le_dist setdist_sym \<open>a \<in> S\<close>)
```
```   360     finally have VTV: "dist (\<V> T) v < dist a v" .
```
```   361     have VTS: "setdist {\<V> T} S \<le> 2 * dist a v"
```
```   362       using sdle that vS by force
```
```   363     have "dist a (\<A> T) \<le> dist a v + dist v (\<V> T) + dist (\<V> T) (\<A> T)"
```
```   364       by (metis add.commute add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
```
```   365     also have "... \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)"
```
```   366       using VTV by (simp add: dist_commute)
```
```   367     also have "... \<le> 2 * dist a v + 2 * setdist {\<V> T} S"
```
```   368       using VA [OF \<open>T \<in> \<C>\<close>] by auto
```
```   369     finally show ?thesis
```
```   370       using VTS by linarith
```
```   371   qed
```
```   372   obtain H :: "['a set, 'a] \<Rightarrow> real"
```
```   373     where Hcont: "\<And>Z. Z \<in> \<C> \<Longrightarrow> continuous_on (U-S) (H Z)"
```
```   374       and Hge0: "\<And>Z x. \<lbrakk>Z \<in> \<C>; x \<in> U-S\<rbrakk> \<Longrightarrow> 0 \<le> H Z x"
```
```   375       and Heq0: "\<And>x Z. \<lbrakk>Z \<in> \<C>; x \<in> U-S; x \<notin> Z\<rbrakk> \<Longrightarrow> H Z x = 0"
```
```   376       and H1: "\<And>x. x \<in> U-S \<Longrightarrow> supp_sum (\<lambda>W. H W x) \<C> = 1"
```
```   377       and Hfin: "\<And>x. x \<in> U-S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. H U x \<noteq> 0}"
```
```   378     apply (rule subordinate_partition_of_unity [OF USsub _ fin])
```
```   379     using nbrhd by auto
```
```   380   define g where "g \<equiv> \<lambda>x. if x \<in> S then f x else supp_sum (\<lambda>T. H T x *\<^sub>R f(\<A> T)) \<C>"
```
```   381   show ?thesis
```
```   382   proof (rule that)
```
```   383     show "continuous_on U g"
```
```   384     proof (clarsimp simp: continuous_on_eq_continuous_within)
```
```   385       fix a assume "a \<in> U"
```
```   386       show "continuous (at a within U) g"
```
```   387       proof (cases "a \<in> S")
```
```   388         case True show ?thesis
```
```   389         proof (clarsimp simp add: continuous_within_topological)
```
```   390           fix W
```
```   391           assume "open W" "g a \<in> W"
```
```   392           then obtain e where "0 < e" and e: "ball (f a) e \<subseteq> W"
```
```   393             using openE True g_def by auto
```
```   394           have "continuous (at a within S) f"
```
```   395             using True contf continuous_on_eq_continuous_within by blast
```
```   396           then obtain d where "0 < d"
```
```   397                         and d: "\<And>x. \<lbrakk>x \<in> S; dist x a < d\<rbrakk> \<Longrightarrow> dist (f x) (f a) < e"
```
```   398             using continuous_within_eps_delta \<open>0 < e\<close> by force
```
```   399           have "g y \<in> ball (f a) e" if "y \<in> U" and y: "y \<in> ball a (d / 6)" for y
```
```   400           proof (cases "y \<in> S")
```
```   401             case True
```
```   402             then have "dist (f a) (f y) < e"
```
```   403               by (metis ball_divide_subset_numeral dist_commute in_mono mem_ball y d)
```
```   404             then show ?thesis
```
```   405               by (simp add: True g_def)
```
```   406           next
```
```   407             case False
```
```   408             have *: "dist (f (\<A> T)) (f a) < e" if "T \<in> \<C>" "H T y \<noteq> 0" for T
```
```   409             proof -
```
```   410               have "y \<in> T"
```
```   411                 using Heq0 that False \<open>y \<in> U\<close> by blast
```
```   412               have "dist (\<A> T) a < d"
```
```   413                 using d6 [OF \<open>T \<in> \<C>\<close> \<open>y \<in> T\<close> \<open>a \<in> S\<close>] y
```
```   414                 by (simp add: dist_commute mult.commute)
```
```   415               then show ?thesis
```
```   416                 using VA [OF \<open>T \<in> \<C>\<close>] by (auto simp: d)
```
```   417             qed
```
```   418             have "supp_sum (\<lambda>T. H T y *\<^sub>R f (\<A> T)) \<C> \<in> ball (f a) e"
```
```   419               apply (rule convex_supp_sum [OF convex_ball])
```
```   420               apply (simp_all add: False H1 Hge0 \<open>y \<in> U\<close>)
```
```   421               by (metis dist_commute *)
```
```   422             then show ?thesis
```
```   423               by (simp add: False g_def)
```
```   424           qed
```
```   425           then show "\<exists>A. open A \<and> a \<in> A \<and> (\<forall>y\<in>U. y \<in> A \<longrightarrow> g y \<in> W)"
```
```   426             apply (rule_tac x = "ball a (d / 6)" in exI)
```
```   427             using e \<open>0 < d\<close> by fastforce
```
```   428         qed
```
```   429       next
```
```   430         case False
```
```   431         obtain N where N: "open N" "a \<in> N"
```
```   432                    and finN: "finite {U \<in> \<C>. \<exists>a\<in>N. H U a \<noteq> 0}"
```
```   433           using Hfin False \<open>a \<in> U\<close> by auto
```
```   434         have oUS: "openin (subtopology euclidean U) (U - S)"
```
```   435           using cloin by (simp add: openin_diff)
```
```   436         have HcontU: "continuous (at a within U) (H T)" if "T \<in> \<C>" for T
```
```   437           using Hcont [OF \<open>T \<in> \<C>\<close>] False  \<open>a \<in> U\<close> \<open>T \<in> \<C>\<close>
```
```   438           apply (simp add: continuous_on_eq_continuous_within continuous_within)
```
```   439           apply (rule Lim_transform_within_set)
```
```   440           using oUS
```
```   441             apply (force simp: eventually_at openin_contains_ball dist_commute dest!: bspec)+
```
```   442           done
```
```   443         show ?thesis
```
```   444         proof (rule continuous_transform_within_openin [OF _ oUS])
```
```   445           show "continuous (at a within U) (\<lambda>x. supp_sum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>)"
```
```   446           proof (rule continuous_transform_within_openin)
```
```   447             show "continuous (at a within U)
```
```   448                     (\<lambda>x. \<Sum>T\<in>{U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))"
```
```   449               by (force intro: continuous_intros HcontU)+
```
```   450           next
```
```   451             show "openin (subtopology euclidean U) ((U - S) \<inter> N)"
```
```   452               using N oUS openin_trans by blast
```
```   453           next
```
```   454             show "a \<in> (U - S) \<inter> N" using False \<open>a \<in> U\<close> N by blast
```
```   455           next
```
```   456             show "\<And>x. x \<in> (U - S) \<inter> N \<Longrightarrow>
```
```   457                          (\<Sum>T \<in> {U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))
```
```   458                          = supp_sum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>"
```
```   459               by (auto simp: supp_sum_def support_on_def
```
```   460                        intro: sum.mono_neutral_right [OF finN])
```
```   461           qed
```
```   462         next
```
```   463           show "a \<in> U - S" using False \<open>a \<in> U\<close> by blast
```
```   464         next
```
```   465           show "\<And>x. x \<in> U - S \<Longrightarrow> supp_sum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C> = g x"
```
```   466             by (simp add: g_def)
```
```   467         qed
```
```   468       qed
```
```   469     qed
```
```   470     show "g ` U \<subseteq> C"
```
```   471       using \<open>f ` S \<subseteq> C\<close> VA
```
```   472       by (fastforce simp: g_def Hge0 intro!: convex_supp_sum [OF \<open>convex C\<close>] H1)
```
```   473     show "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
```
```   474       by (simp add: g_def)
```
```   475   qed
```
```   476 qed
```
```   477
```
```   478
```
```   479 corollary Tietze:
```
```   480   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
```
```   481   assumes "continuous_on S f"
```
```   482       and "closedin (subtopology euclidean U) S"
```
```   483       and "0 \<le> B"
```
```   484       and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
```
```   485   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
```
```   486                   "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
```
```   487   using assms
```
```   488 by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
```
```   489
```
```   490 corollary%unimportant Tietze_closed_interval:
```
```   491   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```   492   assumes "continuous_on S f"
```
```   493       and "closedin (subtopology euclidean U) S"
```
```   494       and "cbox a b \<noteq> {}"
```
```   495       and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
```
```   496   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
```
```   497                   "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
```
```   498 apply (rule Dugundji [of "cbox a b" U S f])
```
```   499 using assms by auto
```
```   500
```
```   501 corollary%unimportant Tietze_closed_interval_1:
```
```   502   fixes f :: "'a::euclidean_space \<Rightarrow> real"
```
```   503   assumes "continuous_on S f"
```
```   504       and "closedin (subtopology euclidean U) S"
```
```   505       and "a \<le> b"
```
```   506       and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
```
```   507   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
```
```   508                   "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
```
```   509 apply (rule Dugundji [of "cbox a b" U S f])
```
```   510 using assms by (auto simp: image_subset_iff)
```
```   511
```
```   512 corollary%unimportant Tietze_open_interval:
```
```   513   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```   514   assumes "continuous_on S f"
```
```   515       and "closedin (subtopology euclidean U) S"
```
```   516       and "box a b \<noteq> {}"
```
```   517       and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
```
```   518   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
```
```   519                   "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
```
```   520 apply (rule Dugundji [of "box a b" U S f])
```
```   521 using assms by auto
```
```   522
```
```   523 corollary%unimportant Tietze_open_interval_1:
```
```   524   fixes f :: "'a::euclidean_space \<Rightarrow> real"
```
```   525   assumes "continuous_on S f"
```
```   526       and "closedin (subtopology euclidean U) S"
```
```   527       and "a < b"
```
```   528       and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
```
```   529   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
```
```   530                   "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
```
```   531 apply (rule Dugundji [of "box a b" U S f])
```
```   532 using assms by (auto simp: image_subset_iff)
```
```   533
```
```   534 corollary%unimportant Tietze_unbounded:
```
```   535   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
```
```   536   assumes "continuous_on S f"
```
```   537       and "closedin (subtopology euclidean U) S"
```
```   538   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
```
```   539 apply (rule Dugundji [of UNIV U S f])
```
```   540 using assms by auto
```
```   541
```
```   542 end
```