equal
deleted
inserted
replaced
293 "\<And>x. x \<in> S \<Longrightarrow> f x = a" |
293 "\<And>x. x \<in> S \<Longrightarrow> f x = a" |
294 "\<And>x. x \<in> T \<Longrightarrow> f x = b" |
294 "\<And>x. x \<in> T \<Longrightarrow> f x = b" |
295 using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b]) |
295 using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b]) |
296 |
296 |
297 |
297 |
298 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> |
299 |
299 |
300 text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367. |
300 text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367. |
301 http://projecteuclid.org/euclid.pjm/1103052106\<close> |
301 http://projecteuclid.org/euclid.pjm/1103052106\<close> |
302 |
302 |
303 theorem%important Dugundji: |
303 theorem%important Dugundji: |