(* Title: HOL/Analysis/Continuous_Extension.thy Authors: LC Paulson, based on material from HOL Light *) section ‹Continuous Extensions of Functions› theory Continuous_Extension imports Starlike begin subsection‹Partitions of unity subordinate to locally finite open coverings› text‹A difference from HOL Light: all summations over infinite sets equal zero, so the "support" must be made explicit in the summation below!› proposition subordinate_partition_of_unity: fixes S :: "'a::metric_space set" assumes "S ⊆ ⋃𝒞" and opC: "⋀T. T ∈ 𝒞 ⟹ open T" and fin: "⋀x. x ∈ S ⟹ ∃V. open V ∧ x ∈ V ∧ finite {U ∈ 𝒞. U ∩ V ≠ {}}" obtains F :: "['a set, 'a] ⇒ real" where "⋀U. U ∈ 𝒞 ⟹ continuous_on S (F U) ∧ (∀x ∈ S. 0 ≤ F U x)" and "⋀x U. ⟦U ∈ 𝒞; x ∈ S; x ∉ U⟧ ⟹ F U x = 0" and "⋀x. x ∈ S ⟹ supp_sum (λW. F W x) 𝒞 = 1" and "⋀x. x ∈ S ⟹ ∃V. open V ∧ x ∈ V ∧ finite {U ∈ 𝒞. ∃x∈V. F U x ≠ 0}" proof (cases "∃W. W ∈ 𝒞 ∧ S ⊆ W") case True then obtain W where "W ∈ 𝒞" "S ⊆ W" by metis then show ?thesis by (rule_tac F = "λV x. if V = W then 1 else 0" in that) (auto simp: supp_sum_def support_on_def) next case False have nonneg: "0 ≤ supp_sum (λV. setdist {x} (S - V)) 𝒞" for x by (simp add: supp_sum_def sum_nonneg) have sd_pos: "0 < setdist {x} (S - V)" if "V ∈ 𝒞" "x ∈ S" "x ∈ V" for V x proof - have "closedin (top_of_set S) (S - V)" by (simp add: Diff_Diff_Int closedin_def opC openin_open_Int ‹V ∈ 𝒞›) with that False setdist_pos_le [of "{x}" "S - V"] show ?thesis using setdist_gt_0_closedin by fastforce qed have ss_pos: "0 < supp_sum (λV. setdist {x} (S - V)) 𝒞" if "x ∈ S" for x proof - obtain U where "U ∈ 𝒞" "x ∈ U" using ‹x ∈ S› ‹S ⊆ ⋃𝒞› by blast obtain V where "open V" "x ∈ V" "finite {U ∈ 𝒞. U ∩ V ≠ {}}" using ‹x ∈ S› fin by blast then have *: "finite {A ∈ 𝒞. ¬ S ⊆ A ∧ x ∉ closure (S - A)}" using closure_def that by (blast intro: rev_finite_subset) have "x ∉ closure (S - U)" using ‹U ∈ 𝒞› ‹x ∈ U› opC open_Int_closure_eq_empty by fastforce then show ?thesis apply (simp add: setdist_eq_0_sing_1 supp_sum_def support_on_def) apply (rule ordered_comm_monoid_add_class.sum_pos2 [OF *, of U]) using ‹U ∈ 𝒞› ‹x ∈ U› False apply (auto simp: sd_pos that) done qed define F where "F ≡ λW x. if x ∈ S then setdist {x} (S - W) / supp_sum (λV. setdist {x} (S - V)) 𝒞 else 0" show ?thesis proof (rule_tac F = F in that) have "continuous_on S (F U)" if "U ∈ 𝒞" for U proof - have *: "continuous_on S (λx. supp_sum (λV. setdist {x} (S - V)) 𝒞)" proof (clarsimp simp add: continuous_on_eq_continuous_within) fix x assume "x ∈ S" then obtain X where "open X" and x: "x ∈ S ∩ X" and finX: "finite {U ∈ 𝒞. U ∩ X ≠ {}}" using assms by blast then have OSX: "openin (top_of_set S) (S ∩ X)" by blast have sumeq: "⋀x. x ∈ S ∩ X ⟹ (∑V | V ∈ 𝒞 ∧ V ∩ X ≠ {}. setdist {x} (S - V)) = supp_sum (λV. setdist {x} (S - V)) 𝒞" apply (simp add: supp_sum_def) apply (rule sum.mono_neutral_right [OF finX]) apply (auto simp: setdist_eq_0_sing_1 support_on_def subset_iff) apply (meson DiffI closure_subset disjoint_iff_not_equal subsetCE) done show "continuous (at x within S) (λx. supp_sum (λV. setdist {x} (S - V)) 𝒞)" apply (rule continuous_transform_within_openin [where f = "λx. (sum (λV. setdist {x} (S - V)) {V ∈ 𝒞. V ∩ X ≠ {}})" and S ="S ∩ X"]) apply (rule continuous_intros continuous_at_setdist continuous_at_imp_continuous_at_within OSX x)+ apply (simp add: sumeq) done qed show ?thesis apply (simp add: F_def) apply (rule continuous_intros *)+ using ss_pos apply force done qed moreover have "⟦U ∈ 𝒞; x ∈ S⟧ ⟹ 0 ≤ F U x" for U x using nonneg [of x] by (simp add: F_def field_split_simps) ultimately show "⋀U. U ∈ 𝒞 ⟹ continuous_on S (F U) ∧ (∀x∈S. 0 ≤ F U x)" by metis next show "⋀x U. ⟦U ∈ 𝒞; x ∈ S; x ∉ U⟧ ⟹ F U x = 0" by (simp add: setdist_eq_0_sing_1 closure_def F_def) next show "supp_sum (λW. F W x) 𝒞 = 1" if "x ∈ S" for x using that ss_pos [OF that] by (simp add: F_def field_split_simps supp_sum_divide_distrib [symmetric]) next show "∃V. open V ∧ x ∈ V ∧ finite {U ∈ 𝒞. ∃x∈V. F U x ≠ 0}" if "x ∈ S" for x using fin [OF that] that by (fastforce simp: setdist_eq_0_sing_1 closure_def F_def elim!: rev_finite_subset) qed qed subsection‹Urysohn's Lemma for Euclidean Spaces› text ‹For Euclidean spaces the proof is easy using distances.› lemma Urysohn_both_ne: assumes US: "closedin (top_of_set U) S" and UT: "closedin (top_of_set U) T" and "S ∩ T = {}" "S ≠ {}" "T ≠ {}" "a ≠ b" obtains f :: "'a::euclidean_space ⇒ 'b::real_normed_vector" where "continuous_on U f" "⋀x. x ∈ U ⟹ f x ∈ closed_segment a b" "⋀x. x ∈ U ⟹ (f x = a ⟷ x ∈ S)" "⋀x. x ∈ U ⟹ (f x = b ⟷ x ∈ T)" proof - have S0: "⋀x. x ∈ U ⟹ setdist {x} S = 0 ⟷ x ∈ S" using ‹S ≠ {}› US setdist_eq_0_closedin by auto have T0: "⋀x. x ∈ U ⟹ setdist {x} T = 0 ⟷ x ∈ T" using ‹T ≠ {}› UT setdist_eq_0_closedin by auto have sdpos: "0 < setdist {x} S + setdist {x} T" if "x ∈ U" for x proof - have "¬ (setdist {x} S = 0 ∧ setdist {x} T = 0)" using assms by (metis IntI empty_iff setdist_eq_0_closedin that) then show ?thesis by (metis add.left_neutral add.right_neutral add_pos_pos linorder_neqE_linordered_idom not_le setdist_pos_le) qed define f where "f ≡ λx. a + (setdist {x} S / (setdist {x} S + setdist {x} T)) *⇩_{R}(b - a)" show ?thesis proof (rule_tac f = f in that) show "continuous_on U f" using sdpos unfolding f_def by (intro continuous_intros | force)+ show "f x ∈ closed_segment a b" if "x ∈ U" for x unfolding f_def apply (simp add: closed_segment_def) apply (rule_tac x="(setdist {x} S / (setdist {x} S + setdist {x} T))" in exI) using sdpos that apply (simp add: algebra_simps) done show "⋀x. x ∈ U ⟹ (f x = a ⟷ x ∈ S)" using S0 ‹a ≠ b› f_def sdpos by force show "(f x = b ⟷ x ∈ T)" if "x ∈ U" for x proof - have "f x = b ⟷ (setdist {x} S / (setdist {x} S + setdist {x} T)) = 1" unfolding f_def by (metis add_diff_cancel_left' ‹a ≠ b› diff_add_cancel eq_iff_diff_eq_0 scaleR_cancel_right scaleR_one) also have "... ⟷ setdist {x} T = 0 ∧ setdist {x} S ≠ 0" using sdpos that by (simp add: field_split_simps) linarith also have "... ⟷ x ∈ T" using ‹S ≠ {}› ‹T ≠ {}› ‹S ∩ T = {}› that by (force simp: S0 T0) finally show ?thesis . qed qed qed lemma Urysohn_local_strong_aux: assumes US: "closedin (top_of_set U) S" and UT: "closedin (top_of_set U) T" and "S ∩ T = {}" "a ≠ b" "S ≠ {}" obtains f :: "'a::euclidean_space ⇒ 'b::euclidean_space" where "continuous_on U f" "⋀x. x ∈ U ⟹ f x ∈ closed_segment a b" "⋀x. x ∈ U ⟹ (f x = a ⟷ x ∈ S)" "⋀x. x ∈ U ⟹ (f x = b ⟷ x ∈ T)" proof (cases "T = {}") case True show ?thesis proof (cases "S = U") case True with ‹T = {}› ‹a ≠ b› show ?thesis by (rule_tac f = "λx. a" in that) (auto) next case False with US closedin_subset obtain c where c: "c ∈ U" "c ∉ S" by fastforce obtain f where f: "continuous_on U f" "⋀x. x ∈ U ⟹ f x ∈ closed_segment a (midpoint a b)" "⋀x. x ∈ U ⟹ (f x = midpoint a b ⟷ x = c)" "⋀x. x ∈ U ⟹ (f x = a ⟷ x ∈ S)" apply (rule Urysohn_both_ne [of U S "{c}" a "midpoint a b"]) using c ‹S ≠ {}› assms apply simp_all apply (metis midpoint_eq_endpoint) done show ?thesis apply (rule_tac f=f in that) using ‹S ≠ {}› ‹T = {}› f ‹a ≠ b› apply simp_all apply (metis (no_types) closed_segment_commute csegment_midpoint_subset midpoint_sym subset_iff) apply (metis closed_segment_commute midpoint_sym notin_segment_midpoint) done qed next case False show ?thesis using Urysohn_both_ne [OF US UT ‹S ∩ T = {}› ‹S ≠ {}› ‹T ≠ {}› ‹a ≠ b›] that by blast qed proposition Urysohn_local_strong: assumes US: "closedin (top_of_set U) S" and UT: "closedin (top_of_set U) T" and "S ∩ T = {}" "a ≠ b" obtains f :: "'a::euclidean_space ⇒ 'b::euclidean_space" where "continuous_on U f" "⋀x. x ∈ U ⟹ f x ∈ closed_segment a b" "⋀x. x ∈ U ⟹ (f x = a ⟷ x ∈ S)" "⋀x. x ∈ U ⟹ (f x = b ⟷ x ∈ T)" proof (cases "S = {}") case True show ?thesis proof (cases "T = {}") case True show ?thesis proof (rule_tac f = "λx. midpoint a b" in that) show "continuous_on U (λx. midpoint a b)" by (intro continuous_intros) show "midpoint a b ∈ closed_segment a b" using csegment_midpoint_subset by blast show "(midpoint a b = a) = (x ∈ S)" for x using ‹S = {}› ‹a ≠ b› by simp show "(midpoint a b = b) = (x ∈ T)" for x using ‹T = {}› ‹a ≠ b› by simp qed next case False with Urysohn_local_strong_aux [OF UT US] assms show ?thesis by (smt (verit) True closed_segment_commute inf_bot_right that) qed next case False with Urysohn_local_strong_aux [OF assms] show ?thesis using that by blast qed lemma Urysohn_local: assumes US: "closedin (top_of_set U) S" and UT: "closedin (top_of_set U) T" and "S ∩ T = {}" obtains f :: "'a::euclidean_space ⇒ 'b::euclidean_space" where "continuous_on U f" "⋀x. x ∈ U ⟹ f x ∈ closed_segment a b" "⋀x. x ∈ S ⟹ f x = a" "⋀x. x ∈ T ⟹ f x = b" proof (cases "a = b") case True then show ?thesis by (rule_tac f = "λx. b" in that) (auto) next case False with Urysohn_local_strong [OF assms] show ?thesis by (smt (verit) US UT closedin_imp_subset subset_eq that) qed lemma Urysohn_strong: assumes US: "closed S" and UT: "closed T" and "S ∩ T = {}" "a ≠ b" obtains f :: "'a::euclidean_space ⇒ 'b::euclidean_space" where "continuous_on UNIV f" "⋀x. f x ∈ closed_segment a b" "⋀x. f x = a ⟷ x ∈ S" "⋀x. f x = b ⟷ x ∈ T" using assms by (auto intro: Urysohn_local_strong [of UNIV S T]) proposition Urysohn: assumes US: "closed S" and UT: "closed T" and "S ∩ T = {}" obtains f :: "'a::euclidean_space ⇒ 'b::euclidean_space" where "continuous_on UNIV f" "⋀x. f x ∈ closed_segment a b" "⋀x. x ∈ S ⟹ f x = a" "⋀x. x ∈ T ⟹ f x = b" using assms by (auto intro: Urysohn_local [of UNIV S T a b]) subsection‹Dugundji's Extension Theorem and Tietze Variants› text ‹See \<^cite>‹"dugundji"›.› theorem Dugundji: fixes f :: "'a::{metric_space,second_countable_topology} ⇒ 'b::real_inner" assumes "convex C" "C ≠ {}" and cloin: "closedin (top_of_set U) S" and contf: "continuous_on S f" and "f ` S ⊆ C" obtains g where "continuous_on U g" "g ` U ⊆ C" "⋀x. x ∈ S ⟹ g x = f x" proof (cases "S = {}") case True show thesis proof show "continuous_on U (λx. SOME y. y ∈ C)" by (rule continuous_intros) show "(λx. SOME y. y ∈ C) ` U ⊆ C" by (simp add: ‹C ≠ {}› image_subsetI some_in_eq) qed (use True in auto) next case False then have sd_pos: "⋀x. ⟦x ∈ U; x ∉ S⟧ ⟹ 0 < setdist {x} S" using setdist_eq_0_closedin [OF cloin] le_less setdist_pos_le by fastforce define ℬ where "ℬ = {ball x (setdist {x} S / 2) |x. x ∈ U - S}" have [simp]: "⋀T. T ∈ ℬ ⟹ open T" by (auto simp: ℬ_def) have USS: "U - S ⊆ ⋃ℬ" by (auto simp: sd_pos ℬ_def) obtain 𝒞 where USsub: "U - S ⊆ ⋃𝒞" and nbrhd: "⋀U. U ∈ 𝒞 ⟹ open U ∧ (∃T. T ∈ ℬ ∧ U ⊆ T)" and fin: "⋀x. x ∈ U - S ⟹ ∃V. open V ∧ x ∈ V ∧ finite {U. U ∈ 𝒞 ∧ U ∩ V ≠ {}}" by (rule paracompact [OF USS]) auto have "∃v a. v ∈ U ∧ v ∉ S ∧ a ∈ S ∧ T ⊆ ball v (setdist {v} S / 2) ∧ dist v a ≤ 2 * setdist {v} S" if "T ∈ 𝒞" for T proof - obtain v where v: "T ⊆ ball v (setdist {v} S / 2)" "v ∈ U" "v ∉ S" using ‹T ∈ 𝒞› nbrhd by (force simp: ℬ_def) then obtain a where "a ∈ S" "dist v a < 2 * setdist {v} S" using setdist_ltE [of "{v}" S "2 * setdist {v} S"] using False sd_pos by force with v show ?thesis by force qed then obtain 𝒱 𝒜 where VA: "⋀T. T ∈ 𝒞 ⟹ 𝒱 T ∈ U ∧ 𝒱 T ∉ S ∧ 𝒜 T ∈ S ∧ T ⊆ ball (𝒱 T) (setdist {𝒱 T} S / 2) ∧ dist (𝒱 T) (𝒜 T) ≤ 2 * setdist {𝒱 T} S" by metis have sdle: "setdist {𝒱 T} S ≤ 2 * setdist {v} S" if "T ∈ 𝒞" "v ∈ T" for T v using setdist_Lipschitz [of "𝒱 T" S v] VA [OF ‹T ∈ 𝒞›] ‹v ∈ T› by auto have d6: "dist a (𝒜 T) ≤ 6 * dist a v" if "T ∈ 𝒞" "v ∈ T" "a ∈ S" for T v a proof - have "dist (𝒱 T) v < setdist {𝒱 T} S / 2" using that VA mem_ball by blast also have "… ≤ setdist {v} S" using sdle [OF ‹T ∈ 𝒞› ‹v ∈ T›] by simp also have vS: "setdist {v} S ≤ dist a v" by (simp add: setdist_le_dist setdist_sym ‹a ∈ S›) finally have VTV: "dist (𝒱 T) v < dist a v" . have VTS: "setdist {𝒱 T} S ≤ 2 * dist a v" using sdle that vS by force have "dist a (𝒜 T) ≤ dist a v + dist v (𝒱 T) + dist (𝒱 T) (𝒜 T)" by (metis add.commute add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le) also have "… ≤ dist a v + dist a v + dist (𝒱 T) (𝒜 T)" using VTV by (simp add: dist_commute) also have "… ≤ 2 * dist a v + 2 * setdist {𝒱 T} S" using VA [OF ‹T ∈ 𝒞›] by auto finally show ?thesis using VTS by linarith qed obtain H :: "['a set, 'a] ⇒ real" where Hcont: "⋀Z. Z ∈ 𝒞 ⟹ continuous_on (U-S) (H Z)" and Hge0: "⋀Z x. ⟦Z ∈ 𝒞; x ∈ U-S⟧ ⟹ 0 ≤ H Z x" and Heq0: "⋀x Z. ⟦Z ∈ 𝒞; x ∈ U-S; x ∉ Z⟧ ⟹ H Z x = 0" and H1: "⋀x. x ∈ U-S ⟹ supp_sum (λW. H W x) 𝒞 = 1" and Hfin: "⋀x. x ∈ U-S ⟹ ∃V. open V ∧ x ∈ V ∧ finite {U ∈ 𝒞. ∃x∈V. H U x ≠ 0}" apply (rule subordinate_partition_of_unity [OF USsub _ fin]) using nbrhd by auto define g where "g ≡ λx. if x ∈ S then f x else supp_sum (λT. H T x *⇩_{R}f(𝒜 T)) 𝒞" show ?thesis proof (rule that) show "continuous_on U g" proof (clarsimp simp: continuous_on_eq_continuous_within) fix a assume "a ∈ U" show "continuous (at a within U) g" proof (cases "a ∈ S") case True show ?thesis proof (clarsimp simp add: continuous_within_topological) fix W assume "open W" "g a ∈ W" then obtain e where "0 < e" and e: "ball (f a) e ⊆ W" using openE True g_def by auto have "continuous (at a within S) f" using True contf continuous_on_eq_continuous_within by blast then obtain d where "0 < d" and d: "⋀x. ⟦x ∈ S; dist x a < d⟧ ⟹ dist (f x) (f a) < e" using continuous_within_eps_delta ‹0 < e› by force have "g y ∈ ball (f a) e" if "y ∈ U" and y: "y ∈ ball a (d / 6)" for y proof (cases "y ∈ S") case True then have "dist (f a) (f y) < e" by (metis ball_divide_subset_numeral dist_commute in_mono mem_ball y d) then show ?thesis by (simp add: True g_def) next case False have *: "dist (f (𝒜 T)) (f a) < e" if "T ∈ 𝒞" "H T y ≠ 0" for T proof - have "y ∈ T" using Heq0 that False ‹y ∈ U› by blast have "dist (𝒜 T) a < d" using d6 [OF ‹T ∈ 𝒞› ‹y ∈ T› ‹a ∈ S›] y by (simp add: dist_commute mult.commute) then show ?thesis using VA [OF ‹T ∈ 𝒞›] by (auto simp: d) qed have "supp_sum (λT. H T y *⇩_{R}f (𝒜 T)) 𝒞 ∈ ball (f a) e" apply (rule convex_supp_sum [OF convex_ball]) apply (simp_all add: False H1 Hge0 ‹y ∈ U›) by (metis dist_commute *) then show ?thesis by (simp add: False g_def) qed then show "∃A. open A ∧ a ∈ A ∧ (∀y∈U. y ∈ A ⟶ g y ∈ W)" apply (rule_tac x = "ball a (d / 6)" in exI) using e ‹0 < d› by fastforce qed next case False obtain N where N: "open N" "a ∈ N" and finN: "finite {U ∈ 𝒞. ∃a∈N. H U a ≠ 0}" using Hfin False ‹a ∈ U› by auto have oUS: "openin (top_of_set U) (U - S)" using cloin by (simp add: openin_diff) have HcontU: "continuous (at a within U) (H T)" if "T ∈ 𝒞" for T using Hcont [OF ‹T ∈ 𝒞›] False ‹a ∈ U› ‹T ∈ 𝒞› apply (simp add: continuous_on_eq_continuous_within continuous_within) apply (rule Lim_transform_within_set) using oUS apply (force simp: eventually_at openin_contains_ball dist_commute dest!: bspec)+ done show ?thesis proof (rule continuous_transform_within_openin [OF _ oUS]) show "continuous (at a within U) (λx. supp_sum (λT. H T x *⇩_{R}f (𝒜 T)) 𝒞)" proof (rule continuous_transform_within_openin) show "continuous (at a within U) (λx. ∑T∈{U ∈ 𝒞. ∃x∈N. H U x ≠ 0}. H T x *⇩_{R}f (𝒜 T))" by (force intro: continuous_intros HcontU)+ next show "openin (top_of_set U) ((U - S) ∩ N)" using N oUS openin_trans by blast next show "a ∈ (U - S) ∩ N" using False ‹a ∈ U› N by blast next show "⋀x. x ∈ (U - S) ∩ N ⟹ (∑T ∈ {U ∈ 𝒞. ∃x∈N. H U x ≠ 0}. H T x *⇩_{R}f (𝒜 T)) = supp_sum (λT. H T x *⇩_{R}f (𝒜 T)) 𝒞" by (auto simp: supp_sum_def support_on_def intro: sum.mono_neutral_right [OF finN]) qed next show "a ∈ U - S" using False ‹a ∈ U› by blast next show "⋀x. x ∈ U - S ⟹ supp_sum (λT. H T x *⇩_{R}f (𝒜 T)) 𝒞 = g x" by (simp add: g_def) qed qed qed show "g ` U ⊆ C" using ‹f ` S ⊆ C› VA by (fastforce simp: g_def Hge0 intro!: convex_supp_sum [OF ‹convex C›] H1) show "⋀x. x ∈ S ⟹ g x = f x" by (simp add: g_def) qed qed corollary Tietze: fixes f :: "'a::{metric_space,second_countable_topology} ⇒ 'b::real_inner" assumes "continuous_on S f" and "closedin (top_of_set U) S" and "0 ≤ B" and "⋀x. x ∈ S ⟹ norm(f x) ≤ B" obtains g where "continuous_on U g" "⋀x. x ∈ S ⟹ g x = f x" "⋀x. x ∈ U ⟹ norm(g x) ≤ B" using assms by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f]) corollary✐‹tag unimportant› Tietze_closed_interval: fixes f :: "'a::{metric_space,second_countable_topology} ⇒ 'b::euclidean_space" assumes "continuous_on S f" and "closedin (top_of_set U) S" and "cbox a b ≠ {}" and "⋀x. x ∈ S ⟹ f x ∈ cbox a b" obtains g where "continuous_on U g" "⋀x. x ∈ S ⟹ g x = f x" "⋀x. x ∈ U ⟹ g x ∈ cbox a b" apply (rule Dugundji [of "cbox a b" U S f]) using assms by auto corollary✐‹tag unimportant› Tietze_closed_interval_1: fixes f :: "'a::{metric_space,second_countable_topology} ⇒ real" assumes "continuous_on S f" and "closedin (top_of_set U) S" and "a ≤ b" and "⋀x. x ∈ S ⟹ f x ∈ cbox a b" obtains g where "continuous_on U g" "⋀x. x ∈ S ⟹ g x = f x" "⋀x. x ∈ U ⟹ g x ∈ cbox a b" apply (rule Dugundji [of "cbox a b" U S f]) using assms by (auto simp: image_subset_iff) corollary✐‹tag unimportant› Tietze_open_interval: fixes f :: "'a::{metric_space,second_countable_topology} ⇒ 'b::euclidean_space" assumes "continuous_on S f" and "closedin (top_of_set U) S" and "box a b ≠ {}" and "⋀x. x ∈ S ⟹ f x ∈ box a b" obtains g where "continuous_on U g" "⋀x. x ∈ S ⟹ g x = f x" "⋀x. x ∈ U ⟹ g x ∈ box a b" apply (rule Dugundji [of "box a b" U S f]) using assms by auto corollary✐‹tag unimportant› Tietze_open_interval_1: fixes f :: "'a::{metric_space,second_countable_topology} ⇒ real" assumes "continuous_on S f" and "closedin (top_of_set U) S" and "a < b" and no: "⋀x. x ∈ S ⟹ f x ∈ box a b" obtains g where "continuous_on U g" "⋀x. x ∈ S ⟹ g x = f x" "⋀x. x ∈ U ⟹ g x ∈ box a b" apply (rule Dugundji [of "box a b" U S f]) using assms by (auto simp: image_subset_iff) corollary✐‹tag unimportant› Tietze_unbounded: fixes f :: "'a::{metric_space,second_countable_topology} ⇒ 'b::real_inner" assumes "continuous_on S f" and "closedin (top_of_set U) S" obtains g where "continuous_on U g" "⋀x. x ∈ S ⟹ g x = f x" apply (rule Dugundji [of UNIV U S f]) using assms by auto end