Quelle  Continuous_Extension.thy

(*  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 ⊆ ∪C" and opC: "∧T. T ∈ C ==> open T"
      and fin: "∧x. x ∈ S ==> ∃V. open V ∧ x ∈ V ∧ finite {U ∈ C. U ∩ V ≠ {}}"
  obtains F :: "['a set, 'a] ==> real"
    where "∧U. U ∈ C ==> continuous_on S (F U) ∧ (∀x ∈ S. 0 ≤ F U x)"
      and "∧x U. [U ∈ C; x ∈ S; x ∉ U] ==> F U x = 0"
      and "∧x. x ∈ S ==> supp_sum (λW. F W x) C = 1"
      and "∧x. x ∈ S ==> ∃V. open V ∧ x ∈ V ∧ finite {U ∈ C. ∃x∈V. F U x ≠ 0}"
proof (cases "∃W. W ∈ C ∧ S ⊆ W")
  case True
    then obtain W where "W ∈ C" "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)) C" for x
      by (simp add: supp_sum_def sum_nonneg)
    have sd_pos: "0 < setdist {x} (S - V)" if "V ∈ C" "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 ∈ C›)
      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)) C" if "x ∈ S" for x
    proof -
      obtain U where "U ∈ C" "x ∈ U" using ‹x ∈ S› ‹S ⊆ ∪C›
        by blast
      obtain V where "open V" "x ∈ V" "finite {U ∈ C. U ∩ V ≠ {}}"
        using ‹x ∈ S› fin by blast
      then have *: "finite {A ∈ C. ¬ S ⊆ A ∧ x ∉ closure (S - A)}"
        using closure_def that by (blast intro: rev_finite_subset)
      have "x ∉ closure (S - U)"
        using ‹U ∈ C› ‹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 ∈ C› ‹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)) C else 0"
    show ?thesis
    proof (rule_tac F = F in that)
      have "continuous_on S (F U)" if "U ∈ C" for U
      proof -
        have *: "continuous_on S (λx. supp_sum (λV. setdist {x} (S - V)) C)"
        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 ∈ C. 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 ∈ C ∧ V ∩ X ≠ {}. setdist {x} (S - V))
                     = supp_sum (λ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)) C)"
            apply (rule continuous_transform_within_openin
                     [where f = "λx. (sum (λV. setdist {x} (S - V)) {V ∈ C. 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 ∈ C; 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 ∈ C ==> continuous_on S (F U) ∧ (∀x∈S. 0 ≤ F U x)"
        by metis
    next
      show "∧x U. [U ∈ C; 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) C = 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 ∈ C. ∃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 🍋‹"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 B where "B = {ball x (setdist {x} S / 2) |x. x ∈ U - S}"
  have [simp]: "∧T. T ∈ B ==> open T"
    by (auto simp: B_def)
  have USS: "U - S ⊆ ∪B"
    by (auto simp: sd_pos B_def)
  obtain C where USsub: "U - S ⊆ ∪C"
       and nbrhd: "∧U. U ∈ C ==> open U ∧ (∃T. T ∈ B ∧ U ⊆ T)"
       and fin: "∧x. x ∈ U - S ==> ∃V. open V ∧ x ∈ V ∧ finite {U. U ∈ C ∧ 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 ∈ C" for T
  proof -
    obtain v where v: "T ⊆ ball v (setdist {v} S / 2)" "v ∈ U" "v ∉ S"
      using ‹T ∈ C› 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
      by force
  qed
  then obtain V A where
    VA: "∧T. T ∈ C ==> V T ∈ U ∧ V T ∉ S ∧ A T ∈ S ∧
              T ⊆ ball (V T) (setdist {V T} S / 2) ∧
              dist (V T) (A T) ≤ 2 * setdist {V T} S"
    by metis
  have sdle: "setdist {V T} S ≤ 2 * setdist {v} S" if "T ∈ C" "v ∈ T" for T v
    using setdist_Lipschitz [of "V T" S v] VA [OF ‹T ∈ C›] ‹v ∈ T› by auto
  have d6: "dist a (A T) ≤ 6 * dist a v" if "T ∈ C" "v ∈ T" "a ∈ S" for T v a
  proof -
    have "dist (V T) v < setdist {V T} S / 2"
      using that VA mem_ball by blast
    also have "… ≤ setdist {v} S"
      using sdle [OF ‹T ∈ C› ‹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 (V T) v < dist a v" .
    have VTS: "setdist {V T} S ≤ 2 * dist a v"
      using sdle that vS by force
    have "dist a (A T) ≤ dist a v + dist v (V T) + dist (V T) (A 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 (V T) (A T)"
      using VTV by (simp add: dist_commute)
    also have "… ≤ 2 * dist a v + 2 * setdist {V T} S"
      using VA [OF ‹T ∈ C›] by auto
    finally show ?thesis
      using VTS by linarith
  qed
  obtain H :: "['a set, 'a] ==> real"
    where Hcont: "∧Z. Z ∈ C ==> continuous_on (U-S) (H Z)"
      and Hge0: "∧Z x. [Z ∈ C; x ∈ U-S] ==> 0 ≤ H Z x"
      and Heq0: "∧x Z. [Z ∈ C; x ∈ U-S; x ∉ Z] ==> H Z x = 0"
      and H1: "∧x. x ∈ U-S ==> supp_sum (λW. H W x) C = 1"
      and Hfin: "∧x. x ∈ U-S ==> ∃V. open V ∧ x ∈ V ∧ finite {U ∈ C. ∃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(A T)) C"
  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 🚫› 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 (A T)) (f a) < e" if "T ∈ C" "H T y ≠ 0" for T
            proof -
              have "y ∈ T"
                using Heq0 that False ‹y ∈ U› by blast
              have "dist (A T) a < d"
                using d6 [OF ‹T ∈ C› ‹y ∈ T› ‹a ∈ S›] y
                by (simp add: dist_commute mult.commute)
              then show ?thesis
                using VA [OF ‹T ∈ C›] by (auto simp: d)
            qed
            have "supp_sum (λT. H T y *🪙R f (A T)) C ∈ 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 🚫› by fastforce
        qed
      next
        case False
        obtain N where N: "open N" "a ∈ N"
                   and finN: "finite {U ∈ C. ∃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 ∈ C" for T
          using Hcont [OF ‹T ∈ C›] False  ‹a ∈ U› ‹T ∈ C›
          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 (A T)) C)"
          proof (rule continuous_transform_within_openin)
            show "continuous (at a within U)
                    (λx. ∑T∈{U ∈ C. ∃x∈N. H U x ≠ 0}. H T x *🪙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 ==>
                         (∑T ∈ {U ∈ C. ∃x∈N. H U x ≠ 0}. H T x *🪙R f (A T))
                         = supp_sum (λT. H T x *🪙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 *🪙R f (A T)) C = 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