products/Sources/formale Sprachen/Isabelle/HOL/Analysis/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Continuous_Extension.thy   Sprache: Isabelle

Original von: 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
        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.16 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff