src/HOL/Analysis/Continuous_Extension.thy

           "\<And>x. x \<in> S \<Longrightarrow> f x = a"
           "\<And>x. x \<in> T \<Longrightarrow> f x = b"
   using assms by (auto intro: Urysohn_local [of UNIV S T a b])
 
 
-subsection\<open>The Dugundji Extension Theorem and Tietze Variants\<close>
-
-text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
-https://projecteuclid.org/euclid.pjm/1103052106\<close>
+subsection\<open>Dugundji's Extension Theorem and Tietze Variants\<close>
+
+text \<open>See \cite{dugundji}.\<close>
 
 theorem Dugundji:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
   assumes "convex C" "C \<noteq> {}"
       and cloin: "closedin (subtopology euclidean U) S"

   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
                   "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
   using assms
 by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
 
-corollary Tietze_closed_interval:
+corollary%unimportant Tietze_closed_interval:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f"
       and "closedin (subtopology euclidean U) S"
       and "cbox a b \<noteq> {}"
       and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
                   "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
 apply (rule Dugundji [of "cbox a b" U S f])
 using assms by auto
 
-corollary Tietze_closed_interval_1:
+corollary%unimportant Tietze_closed_interval_1:
   fixes f :: "'a::euclidean_space \<Rightarrow> real"
   assumes "continuous_on S f"
       and "closedin (subtopology euclidean U) S"
       and "a \<le> b"
       and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
                   "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
 apply (rule Dugundji [of "cbox a b" U S f])
 using assms by (auto simp: image_subset_iff)
 
-corollary Tietze_open_interval:
+corollary%unimportant Tietze_open_interval:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f"
       and "closedin (subtopology euclidean U) S"
       and "box a b \<noteq> {}"
       and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
                   "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
 apply (rule Dugundji [of "box a b" U S f])
 using assms by auto
 
-corollary Tietze_open_interval_1:
+corollary%unimportant Tietze_open_interval_1:
   fixes f :: "'a::euclidean_space \<Rightarrow> real"
   assumes "continuous_on S f"
       and "closedin (subtopology euclidean U) S"
       and "a < b"
       and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
                   "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
 apply (rule Dugundji [of "box a b" U S f])
 using assms by (auto simp: image_subset_iff)
 
-corollary Tietze_unbounded:
+corollary%unimportant Tietze_unbounded:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
   assumes "continuous_on S f"
       and "closedin (subtopology euclidean U) S"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
 apply (rule Dugundji [of UNIV U S f])