(* 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
apply (rule iffI)
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)
done
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
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
show ?thesis
proof (cases "T = U")
case True with \<open>S = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
by (rule_tac f = "\x. b" in that) (auto)
next
case False
with UT closedin_subset obtain c where c: "c \ U" "c \ T"
by fastforce
obtain f where f: "continuous_on U f"
"\x. x \ U \ f x \ closed_segment (midpoint a b) b"
"\x. x \ U \ (f x = midpoint a b \ x = c)"
"\x. x \ U \ (f x = b \ x \ T)"
apply (rule Urysohn_both_ne [of U "{c}" T "midpoint a b" "b"])
using c \<open>T \<noteq> {}\<close> assms apply simp_all
done
show ?thesis
apply (rule_tac f=f in that)
using \<open>S = {}\<close> \<open>T \<noteq> {}\<close> f csegment_midpoint_subset notin_segment_midpoint [OF \<open>a \<noteq> b\<close>]
apply force+
done
qed
qed
next
case False
show ?thesis
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
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
then show ?thesis
apply (rule Urysohn_local_strong [OF assms])
apply (erule that, assumption)
apply (meson US closedin_singleton closedin_trans)
apply (meson UT closedin_singleton closedin_trans)
done
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{dugundji}.\<close>
lemma convex_supp_sum:
assumes "convex S" and 1: "supp_sum u I = 1"
and "\i. i \ I \ 0 \ u i \ (u i = 0 \ f i \ S)"
shows "supp_sum (\i. u i *\<^sub>R f i) I \ S"
proof -
have fin: "finite {i \ I. u i \ 0}"
using 1 sum.infinite by (force simp: supp_sum_def support_on_def)
then have "supp_sum (\i. u i *\<^sub>R f i) I = sum (\i. u i *\<^sub>R f i) {i \ I. u i \ 0}"
by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def)
also have "... \ S"
using 1 assms by (force simp: supp_sum_def support_on_def intro: convex_sum [OF fin \<open>convex S\<close>])
finally show ?thesis .
qed
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 then show thesis
apply (rule_tac g="\x. SOME y. y \ C" in that)
apply (rule continuous_intros)
apply (meson all_not_in_conv \<open>C \<noteq> {}\<close> image_subsetI someI_ex, simp)
done
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 \<B> where "\<B> = {ball x (setdist {x} S / 2) |x. x \<in> U - S}"
have [simp]: "\T. T \ \ \ open T"
by (auto simp: \<B>_def)
have USS: "U - S \ \\"
by (auto simp: sd_pos \<B>_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: \<B>_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
apply (rule_tac x=v in exI)
apply (rule_tac x=a in exI, auto)
done
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
¤ Dauer der Verarbeitung: 0.6 Sekunden
(vorverarbeitet)
¤
|
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.
|
