279 obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
279 obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
280 where "continuous_on UNIV f" |
280 where "continuous_on UNIV f" |
281 "\<And>x. f x \<in> closed_segment a b" |
281 "\<And>x. f x \<in> closed_segment a b" |
282 "\<And>x. f x = a \<longleftrightarrow> x \<in> S" |
282 "\<And>x. f x = a \<longleftrightarrow> x \<in> S" |
283 "\<And>x. f x = b \<longleftrightarrow> x \<in> T" |
283 "\<And>x. f x = b \<longleftrightarrow> x \<in> T" |
284 apply (rule Urysohn_local_strong [of UNIV S T]) |
284 using assms by (auto intro: Urysohn_local_strong [of UNIV S T]) |
285 using assms |
|
286 apply (auto simp: closed_closedin) |
|
287 done |
|
288 |
285 |
289 proposition Urysohn: |
286 proposition Urysohn: |
290 assumes US: "closed S" |
287 assumes US: "closed S" |
291 and UT: "closed T" |
288 and UT: "closed T" |
292 and "S \<inter> T = {}" |
289 and "S \<inter> T = {}" |
293 obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
290 obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
294 where "continuous_on UNIV f" |
291 where "continuous_on UNIV f" |
295 "\<And>x. f x \<in> closed_segment a b" |
292 "\<And>x. f x \<in> closed_segment a b" |
296 "\<And>x. x \<in> S \<Longrightarrow> f x = a" |
293 "\<And>x. x \<in> S \<Longrightarrow> f x = a" |
297 "\<And>x. x \<in> T \<Longrightarrow> f x = b" |
294 "\<And>x. x \<in> T \<Longrightarrow> f x = b" |
298 apply (rule Urysohn_local [of UNIV S T a b]) |
295 using assms by (auto intro: Urysohn_local [of UNIV S T a b]) |
299 using assms |
|
300 apply (auto simp: closed_closedin) |
|
301 done |
|
302 |
296 |
303 |
297 |
304 subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close> |
298 subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close> |
305 |
299 |
306 text\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367. |
300 text\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367. |