Quelle Continuous_Extension.thy Sprache: Isabelle

(* Title: HOL/Analysis/Continuous_Extension.thy
 Authors: LC Paulson, based on material from HOL Light
*)

section \<open>Continuous Extensions of Functions\<close>

theory Continuous_Extension
imports Starlike
begin

subsection\<open>Partitions of unity subordinate to locally finite open coverings\<close>

text\<open>A difference from HOL Light: all summations over infinite sets equal zero,
 so the "support" must be made explicit in the summation below!\<close>

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 \<open>V \<in> \<C>\<close>)
 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 \<open>x \<in> S\<close> 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 \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> 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 \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> 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 \
 (\<Sum>V | V \<in> \<C> \<and> V \<inter> X \<noteq> {}. setdist {x} (S - V))
 = supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>"
 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\<open>Urysohn's Lemma for Euclidean Spaces\<close>

text \<open>For Euclidean spaces the proof is easy using distances.\<close>

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 \<open>S \<noteq> {}\<close> US setdist_eq_0_closedin by auto
 have T0: "\x. x \ U \ setdist {x} T = 0 \ x \ T"
 using \<open>T \<noteq> {}\<close> 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)) *\<^sub>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 \<open>a \<noteq> b\<close> 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 \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>S \<inter> T = {}\<close> 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 \<open>T = {}\<close> \<open>a \<noteq> b\<close> 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 \<open>S \<noteq> {}\<close> assms apply simp_all
 apply (metis midpoint_eq_endpoint)
 done
 show ?thesis
 apply (rule_tac f=f in that)
 using \<open>S \<noteq> {}\<close> \<open>T = {}\<close> f \<open>a \<noteq> b\<close>
 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 \<open>S \<inter> T = {}\<close> \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>a \<noteq> b\<close>] 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 \<open>S = {}\<close> \<open>a \<noteq> b\<close> by simp
 show "(midpoint a b = b) = (x \ T)" for x
 using \<open>T = {}\<close> \<open>a \<noteq> b\<close> 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\<open>Dugundji's Extension Theorem and Tietze Variants\<close>

text \<open>See \<^cite>\<open>"dugundji"\<close>.\<close>

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: \<open>C \<noteq> {}\<close> 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 \<in> U - S}"
 have [simp]: "\T. T \ \ \ open T"
 by (auto simp: \_def)
 have USS: "U - S \ \\"
 by (auto simp: sd_pos \_def)
 obtain \<C> where USsub: "U - S \<subseteq> \<Union>\<C>"
 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 \<subseteq> ball v (setdist {v} S / 2) \<and>
 dist v a \<le> 2 * setdist {v} S" if "T \<in> \<C>" for T
 proof -
 obtain v where v: "T \ ball v (setdist {v} S / 2)" "v \ U" "v \ S"
 using \<open>T \<in> \<C>\<close> 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 \<V> \<A> where
 VA: "\T. T \ \ \ \ T \ U \ \ T \ S \ \ T \ S \
 T \<subseteq> ball (\<V> T) (setdist {\<V> T} S / 2) \<and>
 dist (\<V> T) (\<A> T) \<le> 2 * setdist {\<V> 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 \<open>T \<in> \<C>\<close> \<open>v \<in> T\<close>] by simp
 also have vS: "setdist {v} S \ dist a v"
 by (simp add: setdist_le_dist setdist_sym \<open>a \<in> S\<close>)
 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 \<open>T \<in> \<C>\<close>] 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 *\<^sub>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 \<open>0 < e\<close> 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 \<open>y \<in> U\<close> by blast
 have "dist (\ T) a < d"
 using d6 [OF \<open>T \<in> \<C>\<close> \<open>y \<in> T\<close> \<open>a \<in> S\<close>] y
 by (simp add: dist_commute mult.commute)
 then show ?thesis
 using VA [OF \<open>T \<in> \<C>\<close>] by (auto simp: d)
 qed
 have "supp_sum (\T. H T y *\<^sub>R f (\ T)) \ \ ball (f a) e"
 apply (rule convex_supp_sum [OF convex_ball])
 apply (simp_all add: False H1 Hge0 \<open>y \<in> U\<close>)
 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 \<open>0 < d\<close> 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 \<open>a \<in> U\<close> 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 \<open>T \<in> \<C>\<close>] False \<open>a \<in> U\<close> \<open>T \<in> \<C>\<close>
 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 *\<^sub>R f (\ T)) \)"
 proof (rule continuous_transform_within_openin)
 show "continuous (at a within U)
 (\<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))"
 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 \
 (\<Sum>T \<in> {U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))
 = supp_sum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>"
 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 *\<^sub>R f (\ T)) \ = g x"
 by (simp add: g_def)
 qed
 qed
 qed
 show "g ` U \ C"
 using \<open>f ` S \<subseteq> C\<close> VA
 by (fastforce simp: g_def Hge0 intro!: convex_supp_sum [OF \<open>convex C\<close>] 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\<^marker>\<open>tag unimportant\<close> 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\<^marker>\<open>tag unimportant\<close> 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\<^marker>\<open>tag unimportant\<close> 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\<^marker>\<open>tag unimportant\<close> 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\<^marker>\<open>tag unimportant\<close> 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

quality98%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.