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