Quelle Urysohn.thy Sprache: Isabelle

(* Title: HOL/Analysis/Urysohn.thy
 Authors: LC Paulson, based on material from HOL Light
*)

section \<open>The Urysohn lemma, its consequences and other advanced material about metric spaces\<close>

theory Urysohn
imports Abstract_Topological_Spaces Abstract_Metric_Spaces Infinite_Sum Arcwise_Connected
begin

subsection \<open>Urysohn lemma and Tietze's theorem\<close>

proposition Urysohn_lemma:
 fixes a b :: real
 assumes "normal_space X" "closedin X S" "closedin X T" "disjnt S T" "a \ b"
 obtains f where "continuous_map X (top_of_set {a..b}) f" "f ` S \ {a}" "f ` T \ {b}"
proof -
 obtain U where "openin X U" "S \ U" "X closure_of U \ topspace X - T"
 using assms unfolding normal_space_alt disjnt_def
 by (metis Diff_mono Un_Diff_Int closedin_def subset_eq sup_bot_right)
 have "\G :: real \ 'a set. G 0 = U \ G 1 = topspace X - T \
 (\<forall>x \<in> dyadics \<inter> {0..1}. \<forall>y \<in> dyadics \<inter> {0..1}. x < y \<longrightarrow> openin X (G x) \<and> openin X (G y) \<and> X closure_of (G x) \<subseteq> G y)"
 proof (rule recursion_on_dyadic_fractions)
 show "openin X U \ openin X (topspace X - T) \ X closure_of U \ topspace X - T"
 using \<open>X closure_of U \<subseteq> topspace X - T\<close> \<open>openin X U\<close> \<open>closedin X T\<close> by blast
 show "\z. (openin X x \ openin X z \ X closure_of x \ z) \ openin X z \ openin X y \ X closure_of z \ y"
 if "openin X x \ openin X y \ X closure_of x \ y" for x y
 by (meson that closedin_closure_of normal_space_alt \<open>normal_space X\<close>)
 show "openin X x \ openin X z \ X closure_of x \ z"
 if "openin X x \ openin X y \ X closure_of x \ y" and "openin X y \ openin X z \ X closure_of y \ z" for x y z
 by (meson that closure_of_subset openin_subset subset_trans)
 qed
 then obtain G :: "real \ 'a set"
 where G0: "G 0 = U" and G1: "G 1 = topspace X - T"
 and G: "\x y. \x \ dyadics; y \ dyadics; 0 \ x; x < y; y \ 1\
 \<Longrightarrow> openin X (G x) \<and> openin X (G y) \<and> X closure_of (G x) \<subseteq> G y"
 by (smt (verit, del_insts) Int_iff atLeastAtMost_iff)
 define f where "f \ \x. Inf(insert 1 {r. r \ dyadics \ {0..1} \ x \ G r})"
 have f_ge: "f x \ 0" if "x \ topspace X" for x
 unfolding f_def by (force intro: cInf_greatest)
 moreover have f_le1: "f x \ 1" if "x \ topspace X" for x
 proof -
 have "bdd_below {r \ dyadics \ {0..1}. x \ G r}"
 by (auto simp: bdd_below_def)
 then show ?thesis
 by (auto simp: f_def cInf_lower)
 qed
 ultimately have fim: "f \ topspace X \ {0..1}"
 by (auto simp: f_def)
 have 0: "0 \ dyadics \ {0..1::real}" and 1: "1 \ dyadics \ {0..1::real}"
 by (force simp: dyadics_def)+
 then have opeG: "openin X (G r)" if "r \ dyadics \ {0..1}" for r
 using G G0 \<open>openin X U\<close> less_eq_real_def that by auto
 have "x \ G 0" if "x \ S" for x
 using G0 \<open>S \<subseteq> U\<close> that by blast
 with 0 have fimS: "f ` S \ {0}"
 unfolding f_def by (force intro!: cInf_eq_minimum)
 have False if "r \ dyadics" "0 \ r" "r < 1" "x \ G r" "x \ T" for r x
 using G [of r 1] 1
 by (smt (verit, best) DiffD2 G1 Int_iff closure_of_subset inf.orderE openin_subset that)
 then have "r\1" if "r \ dyadics" "0 \ r" "r \ 1" "x \ G r" "x \ T" for r x
 using linorder_not_le that by blast
 then have fimT: "f ` T \ {1}"
 unfolding f_def by (force intro!: cInf_eq_minimum)
 have fle1: "f z \ 1" for z
 by (force simp: f_def intro: cInf_lower)
 have fle: "f z \ x" if "x \ dyadics \ {0..1}" "z \ G x" for z x
 using that by (force simp: f_def intro: cInf_lower)
 have *: "b \ f z" if "b \ 1" "\x. \x \ dyadics \ {0..1}; z \ G x\ \ b \ x" for z b
 using that by (force simp: f_def intro: cInf_greatest)
 have **: "r \ f x" if r: "r \ dyadics \ {0..1}" "x \ G r" for r x
 proof (rule *)
 show "r \ s" if "s \ dyadics \ {0..1}" and "x \ G s" for s :: real
 using that r G [of s r] by (force simp: dest: closure_of_subset openin_subset)
 qed (use that in force)

 have "\U. openin X U \ x \ U \ (\y \ U. \f y - f x\ < \)"
 if "x \ topspace X" and "0 < \" for x \
 proof -
 have A: "\r. r \ dyadics \ {0..1} \ r < y \ \r - y\ < d" if "0 < y" "y \ 1" "0 < d" for y d::real
 proof -
 obtain n q r
 where "of_nat q / 2^n < y" "y < of_nat r / 2^n" "\q / 2^n - r / 2^n \ < d"
 by (smt (verit, del_insts) padic_rational_approximation_straddle_pos \<open>0 < d\<close> \<open>0 < y\<close>)
 then show ?thesis
 unfolding dyadics_def
 using divide_eq_0_iff that(2) by fastforce
 qed
 have B: "\r. r \ dyadics \ {0..1} \ y < r \ \r - y\ < d" if "0 \ y" "y < 1" "0 < d" for y d::real
 proof -
 obtain n q r
 where "of_nat q / 2^n \ y" "y < of_nat r / 2^n" "\q / 2^n - r / 2^n \ < d"
 using padic_rational_approximation_straddle_pos_le
 by (smt (verit, del_insts) \<open>0 < d\<close> \<open>0 \<le> y\<close>)
 then show ?thesis
 apply (clarsimp simp: dyadics_def)
 using divide_eq_0_iff \<open>y < 1\<close>
 by (smt (verit) divide_nonneg_nonneg divide_self of_nat_0_le_iff of_nat_1 power_0 zero_le_power)
 qed
 show ?thesis
 proof (cases "f x = 0")
 case True
 with B[of 0] obtain r where r: "r \ dyadics \ {0..1}" "0 < r" "\r\ < \/2"
 by (smt (verit) \<open>0 < \<epsilon>\<close> half_gt_zero)
 show ?thesis
 proof (intro exI conjI)
 show "openin X (G r)"
 using opeG r(1) by blast
 show "x \ G r"
 using True ** r by force
 show "\y \ G r. \f y - f x\ < \"
 using f_ge \<open>openin X (G r)\<close> fle openin_subset r by (fastforce simp: True)
 qed
 next
 case False
 show ?thesis
 proof (cases "f x = 1")
 case True
 with A[of 1] obtain r where r: "r \ dyadics \ {0..1}" "r < 1" "\r-1\ < \/2"
 by (smt (verit) \<open>0 < \<epsilon>\<close> half_gt_zero)
 define G' where "G' \<equiv> topspace X - X closure_of G r"
 show ?thesis
 proof (intro exI conjI)
 show "openin X G'"
 unfolding G'_def by fastforce
 obtain r' where "r' \<in> dyadics \<and> 0 \<le> r' \<and> r' \<le> 1 \<and> r < r' \<and> \<bar>r' - r\<bar> < 1 - r"
 using B r by force
 moreover
 have "1 - r \ dyadics" "0 \ r"
 using 1 r dyadics_diff by force+
 ultimately have "x \ X closure_of G r"
 using G True r fle by force
 then show "x \ G'"
 by (simp add: G'_def that)
 show "\y \ G'. \f y - f x\ < \"
 using ** f_le1 in_closure_of r by (fastforce simp: True G'_def)
 qed
 next
 case False
 have "0 < f x" "f x < 1"
 using fle1 f_ge that(1) \<open>f x \<noteq> 0\<close> \<open>f x \<noteq> 1\<close> by (metis order_le_less) +
 obtain r where r: "r \ dyadics \ {0..1}" "r < f x" "\r - f x\ < \ / 2"
 using A \<open>0 < \<epsilon>\<close> \<open>0 < f x\<close> \<open>f x < 1\<close> by (smt (verit, best) half_gt_zero)
 obtain r' where r': "r' \ dyadics \ {0..1}" "f x < r'" "\r' - f x\ < \ / 2"
 using B \<open>0 < \<epsilon>\<close> \<open>0 < f x\<close> \<open>f x < 1\<close> by (smt (verit, best) half_gt_zero)
 have "r < 1"
 using \<open>f x < 1\<close> r(2) by force
 show ?thesis
 proof (intro conjI exI)
 show "openin X (G r' - X closure_of G r)"
 using closedin_closure_of opeG r' by blast
 have "x \ X closure_of G r \ False"
 using B [of r "f x - r"] r \<open>r < 1\<close> G [of r] fle by force
 then show "x \ G r' - X closure_of G r"
 using ** r' by fastforce
 show "\y\G r' - X closure_of G r. \f y - f x\ < \"
 using r r' ** G closure_of_subset field_sum_of_halves fle openin_subset subset_eq
 by (smt (verit) DiffE opeG)
 qed
 qed
 qed
 qed
 then have contf: "continuous_map X (top_of_set {0..1}) f"
 by (auto simp: Met_TC.continuous_map_to_metric dist_real_def continuous_map_in_subtopology fim abs_minus_commute simp flip: mtopology_is_euclidean)
 define g where "g \ \x. a + (b - a) * f x"
 show thesis
 proof
 have "continuous_map X euclideanreal g"
 using contf \<open>a \<le> b\<close> unfolding g_def by (auto simp: continuous_intros continuous_map_in_subtopology)
 moreover have "g \ (topspace X) \ {a..b}"
 using mult_left_le [of "f _" "b-a"] contf \<open>a \<le> b\<close>
 by (simp add: g_def Pi_iff add.commute continuous_map_in_subtopology image_subset_iff le_diff_eq)
 ultimately show "continuous_map X (top_of_set {a..b}) g"
 using continuous_map_in_subtopology by blast
 show "g ` S \ {a}" "g ` T \ {b}"
 using fimS fimT by (auto simp: g_def)
 qed
qed

lemma Urysohn_lemma_alt:
 fixes a b :: real
 assumes "normal_space X" "closedin X S" "closedin X T" "disjnt S T"
 obtains f where "continuous_map X euclideanreal f" "f ` S \ {a}" "f ` T \ {b}"
 by (metis Urysohn_lemma assms continuous_map_in_subtopology disjnt_sym linear)

lemma normal_space_iff_Urysohn_gen_alt:
 assumes "a \ b"
 shows "normal_space X \
 (\<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T
 \<longrightarrow> (\<exists>f. continuous_map X euclideanreal f \<and> f ` S \<subseteq> {a} \<and> f ` T \<subseteq> {b}))"
(is "?lhs=?rhs")
proof
 show "?lhs \ ?rhs"
 by (metis Urysohn_lemma_alt)
next
 assume R: ?rhs
 show ?lhs
 unfolding normal_space_def
 proof clarify
 fix S T
 assume "closedin X S" and "closedin X T" and "disjnt S T"
 with R obtain f where contf: "continuous_map X euclideanreal f" and "f ` S \ {a}" "f ` T \ {b}"
 by meson
 show "\U V. openin X U \ openin X V \ S \ U \ T \ V \ disjnt U V"
 proof (intro conjI exI)
 show "openin X {x \ topspace X. f x \ ball a (\a - b\ / 2)}"
 by (force intro!: openin_continuous_map_preimage [OF contf])
 show "openin X {x \ topspace X. f x \ ball b (\a - b\ / 2)}"
 by (force intro!: openin_continuous_map_preimage [OF contf])
 show "S \ {x \ topspace X. f x \ ball a (\a - b\ / 2)}"
 using \<open>closedin X S\<close> closedin_subset \<open>f ` S \<subseteq> {a}\<close> assms by force
 show "T \ {x \ topspace X. f x \ ball b (\a - b\ / 2)}"
 using \<open>closedin X T\<close> closedin_subset \<open>f ` T \<subseteq> {b}\<close> assms by force
 have "\x. \x \ topspace X; dist a (f x) < \a-b\/2; dist b (f x) < \a-b\/2\ \ False"
 by (smt (verit, best) dist_real_def dist_triangle_half_l)
 then show "disjnt {x \ topspace X. f x \ ball a (\a-b\ / 2)} {x \ topspace X. f x \ ball b (\a-b\ / 2)}"
 using disjnt_iff by fastforce
 qed
 qed
qed

lemma normal_space_iff_Urysohn_gen:
 fixes a b::real
 shows
 "a 
 (\<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T
 \<longrightarrow> (\<exists>f. continuous_map X (top_of_set {a..b}) f \<and>
 f ` S \<subseteq> {a} \<and> f ` T \<subseteq> {b}))"
 by (metis linear not_le Urysohn_lemma normal_space_iff_Urysohn_gen_alt continuous_map_in_subtopology)

lemma normal_space_iff_Urysohn_alt:
 "normal_space X \
 (\<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T
 \<longrightarrow> (\<exists>f. continuous_map X euclideanreal f \<and>
 f ` S \<subseteq> {0} \<and> f ` T \<subseteq> {1}))"
 by (rule normal_space_iff_Urysohn_gen_alt) auto

lemma normal_space_iff_Urysohn:
 "normal_space X \
 (\<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T
 \<longrightarrow> (\<exists>f::'a\<Rightarrow>real. continuous_map X (top_of_set {0..1}) f \<and>
 f ` S \<subseteq> {0} \<and> f ` T \<subseteq> {1}))"
 by (rule normal_space_iff_Urysohn_gen) auto

lemma normal_space_perfect_map_image:
 "\normal_space X; perfect_map X Y f\ \ normal_space Y"
 unfolding perfect_map_def proper_map_def
 using normal_space_continuous_closed_map_image by fastforce

lemma Hausdorff_normal_space_closed_continuous_map_image:
 "\normal_space X; closed_map X Y f; continuous_map X Y f;
 f ` topspace X = topspace Y; t1_space Y\<rbrakk>
 \<Longrightarrow> Hausdorff_space Y"
 by (metis normal_space_continuous_closed_map_image normal_t1_imp_Hausdorff_space)

lemma normal_Hausdorff_space_closed_continuous_map_image:
 "\normal_space X; Hausdorff_space X; closed_map X Y f;
 continuous_map X Y f; f ` topspace X = topspace Y\<rbrakk>
 \<Longrightarrow> normal_space Y \<and> Hausdorff_space Y"
 by (meson normal_space_continuous_closed_map_image normal_t1_eq_Hausdorff_space t1_space_closed_map_image)

lemma Lindelof_cover:
 assumes "regular_space X" and "Lindelof_space X" and "S \ {}"
 and clo: "closedin X S" "closedin X T" "disjnt S T"
 obtains h :: "nat \ 'a set" where
 "\n. openin X (h n)" "\n. disjnt T (X closure_of (h n))" and "S \ \(range h)"
proof -
 have "\U. openin X U \ x \ U \ disjnt T (X closure_of U)"
 if "x \ S" for x
 using \<open>regular_space X\<close> unfolding regular_space
 by (metis (full_types) Diff_iff \<open>disjnt S T\<close> clo closure_of_eq disjnt_iff in_closure_of that)
 then obtain h where oh: "\x. x \ S \ openin X (h x)"
 and xh: "\x. x \ S \ x \ h x"
 and dh: "\x. x \ S \ disjnt T (X closure_of h x)"
 by metis
 have "Lindelof_space(subtopology X S)"
 by (simp add: Lindelof_space_closedin_subtopology \<open>Lindelof_space X\<close> \<open>closedin X S\<close>)
 then obtain \ where \: "countable \ \<and> \ \<subseteq> h ` S \<and> S \<subseteq> \<Union>\"
 unfolding Lindelof_space_subtopology_subset [OF closedin_subset [OF \<open>closedin X S\<close>]]
 by (smt (verit, del_insts) oh xh UN_I image_iff subsetI)
 with \<open>S \<noteq> {}\<close> have "\ \<noteq> {}"
 by blast
 show ?thesis
 proof
 show "openin X (from_nat_into \ n)" for n
 by (metis \ from_nat_into image_iff \<open>\ \<noteq> {}\<close> oh subsetD)
 show "disjnt T (X closure_of (from_nat_into \) n)" for n
 using dh from_nat_into [OF \<open>\ \<noteq> {}\<close>]
 by (metis \ f_inv_into_f inv_into_into subset_eq)
 show "S \ \(range (from_nat_into \))"
 by (simp add: \ \<open>\ \<noteq> {}\<close>)
 qed
qed

lemma regular_Lindelof_imp_normal_space:
 assumes "regular_space X" and "Lindelof_space X"
 shows "normal_space X"
 unfolding normal_space_def
proof clarify
 fix S T
 assume clo: "closedin X S" "closedin X T" and "disjnt S T"
 show "\U V. openin X U \ openin X V \ S \ U \ T \ V \ disjnt U V"
 proof (cases "S={} \ T={}")
 case True
 with clo show ?thesis
 by (meson closedin_def disjnt_empty1 disjnt_empty2 openin_empty openin_topspace subset_empty)
 next
 case False
 obtain h :: "nat \ 'a set" where
 opeh: "\n. openin X (h n)" and dish: "\n. disjnt T (X closure_of (h n))"
 and Sh: "S \ \(range h)"
 by (metis Lindelof_cover False \<open>disjnt S T\<close> assms clo)
 obtain k :: "nat \ 'a set" where
 opek: "\n. openin X (k n)" and disk: "\n. disjnt S (X closure_of (k n))"
 and Tk: "T \ \(range k)"
 by (metis Lindelof_cover False \<open>disjnt S T\<close> assms clo disjnt_sym)
 define U where "U \ \i. h i - (\j
 define V where "V \ \i. k i - (\j\i. X closure_of h j)"
 show ?thesis
 proof (intro exI conjI)
 show "openin X U" "openin X V"
 unfolding U_def V_def
 by (force intro!: opek opeh closedin_Union closedin_closure_of)+
 show "S \ U" "T \ V"
 using Sh Tk dish disk by (fastforce simp: U_def V_def disjnt_iff)+
 have "\x i j. \x \ k i; x \ h j; \j\i. x \ X closure_of h j\
 \<Longrightarrow> \<exists>i<j. x \<in> X closure_of k i"
 by (metis in_closure_of linorder_not_less opek openin_subset subsetD)
 then show "disjnt U V"
 by (force simp: U_def V_def disjnt_iff)
 qed
 qed
qed

theorem Tietze_extension_closed_real_interval:
 assumes "normal_space X" and "closedin X S"
 and contf: "continuous_map (subtopology X S) euclideanreal f"
 and fim: "f ` S \ {a..b}" and "a \ b"
 obtains g
 where "continuous_map X euclideanreal g"
 "\x. x \ S \ g x = f x" "g ` topspace X \ {a..b}"
proof -
 define c where "c \ max \a\ \b\ + 1"
 have "0 < c" and c: "\x. x \ S \ \f x\ \ c"
 using fim by (auto simp: c_def image_subset_iff)
 define good where
 "good \ \g n. continuous_map X euclideanreal g \ (\x \ S. \f x - g x\ \ c * (2/3)^n)"
 have step: "\g. good g (Suc n) \
 (\<forall>x \<in> topspace X. \<bar>g x - h x\<bar> \<le> c * (2/3)^n / 3)"
 if h: "good h n" for n h
 proof -
 have pos: "0 < c * (2/3) ^ n"
 by (simp add: \<open>0 < c\<close>)
 have S_eq: "S = topspace(subtopology X S)" and "S \ topspace X"
 using \<open>closedin X S\<close> closedin_subset by auto
 define d where "d \ c/3 * (2/3) ^ n"
 define SA where "SA \ {x \ S. f x - h x \ {..-d}}"
 define SB where "SB \ {x \ S. f x - h x \ {d..}}"
 have contfh: "continuous_map (subtopology X S) euclideanreal (\x. f x - h x)"
 using that
 by (simp add: contf good_def continuous_map_diff continuous_map_from_subtopology)
 then have "closedin (subtopology X S) SA"
 unfolding SA_def continuous_map_closedin
 by (metis (full_types) S_eq closed_atMost closed_closedin)
 then have "closedin X SA"
 using \<open>closedin X S\<close> closedin_trans_full by blast
 moreover have "closedin (subtopology X S) SB"
 unfolding SB_def
 using closedin_continuous_map_preimage_gen [OF contfh]
 by (metis (full_types) S_eq closed_atLeast closed_closedin closedin_topspace)
 then have "closedin X SB"
 using \<open>closedin X S\<close> closedin_trans_full by blast
 moreover have "disjnt SA SB"
 using pos by (auto simp: d_def disjnt_def SA_def SB_def)
 moreover have "-d \ d"
 using pos by (auto simp: d_def)
 ultimately
 obtain g where contg: "continuous_map X (top_of_set {- d..d}) g"
 and ga: "g ` SA \ {- d}" and gb: "g ` SB \ {d}"
 using Urysohn_lemma \<open>normal_space X\<close> by metis
 then have g_le_d: "\x. x \ topspace X \ \g x\ \ d"
 by (fastforce simp: abs_le_iff continuous_map_def minus_le_iff)
 have g_eq_d: "\x. \x \ S; f x - h x \ -d\ \ g x = -d"
 using ga by (auto simp: SA_def)
 have g_eq_negd: "\x. \x \ S; f x - h x \ d\ \ g x = d"
 using gb by (auto simp: SB_def)
 show ?thesis
 unfolding good_def
 proof (intro conjI strip exI)
 show "continuous_map X euclideanreal (\x. h x + g x)"
 using contg continuous_map_add continuous_map_in_subtopology that
 unfolding good_def by blast
 show "\f x - (h x + g x)\ \ c * (2 / 3) ^ Suc n" if "x \ S" for x
 proof -
 have x: "x \ topspace X"
 using \<open>S \<subseteq> topspace X\<close> that by auto
 have "\f x - h x\ \ c * (2/3) ^ n"
 using good_def h that by blast
 with g_eq_d [OF that] g_eq_negd [OF that] g_le_d [OF x]
 have "\f x - (h x + g x)\ \ d + d"
 unfolding d_def by linarith
 then show ?thesis
 by (simp add: d_def)
 qed
 show "\h x + g x - h x\ \ c * (2 / 3) ^ n / 3" if "x \ topspace X" for x
 using that d_def g_le_d by auto
 qed
 qed
 then obtain nxtg where nxtg: "\h n. good h n \
 good (nxtg h n) (Suc n) \<and> (\<forall>x \<in> topspace X. \<bar>nxtg h n x - h x\<bar> \<le> c * (2/3)^n / 3)"
 by metis
 define g where "g \ rec_nat (\x. 0) (\n r. nxtg r n)"
 have [simp]: "g 0 x = 0" for x
 by (auto simp: g_def)
 have g_Suc: "g(Suc n) = nxtg (g n) n" for n
 by (auto simp: g_def)
 have good: "good (g n) n" for n
 proof (induction n)
 case 0
 with c show ?case
 by (auto simp: good_def)
 qed (simp add: g_Suc nxtg)
 have *: "\n x. x \ topspace X \ \g(Suc n) x - g n x\ \ c * (2/3) ^ n / 3"
 using nxtg g_Suc good by force
 obtain h where conth: "continuous_map X euclideanreal h"
 and h: "\\. 0 < \ \ \\<^sub>F n in sequentially. \x\topspace X. dist (g n x) (h x) < \"
 proof (rule Met_TC.continuous_map_uniformly_Cauchy_limit)
 show "\\<^sub>F n in sequentially. continuous_map X (Met_TC.mtopology) (g n)"
 using good good_def by fastforce
 show "\N. \m n x. N \ m \ N \ n \ x \ topspace X \ dist (g m x) (g n x) < \"
 if "\ > 0" for \
 proof -
 have "\\<^sub>F n in sequentially. \(2/3) ^ n\ < \/c"
 proof (rule Archimedean_eventually_pow_inverse)
 show "0 < \ / c"
 by (simp add: \<open>0 < c\<close> that)
 qed auto
 then obtain N where N: "\n. n \ N \ \(2/3) ^ n\ < \/c"
 by (meson eventually_sequentially order_le_less_trans)
 have "\g m x - g n x\ < \"
 if "N \ m" "N \ n" and x: "x \ topspace X" "m \ n" for m n x
 proof (cases "m < n")
 case True
 have 23: "(\k = m..
 using \<open>m \<le> n\<close>
 by (induction n) (auto simp: le_Suc_eq)
 have "\g m x - g n x\ \ \\k = m.."
 by (subst sum_Suc_diff' [OF \m \ n\]) linarith
 also have "\ \ (\k = m..g (Suc k) x - g k x\)"
 by (rule sum_abs)
 also have "\ \ (\k = m..
 by (meson "*" sum_mono x(1))
 also have "\ = (c/3) * (\k = m..
 by (simp add: sum_distrib_left)
 also have "\ = (c/3) * 3 * ((2/3) ^ m - (2/3) ^ n)"
 by (simp add: sum_distrib_left 23)
 also have "... < (c/3) * 3 * ((2/3) ^ m)"
 using \<open>0 < c\<close> by auto
 also have "\ < \"
 using N [OF \<open>N \<le> m\<close>] \<open>0 < c\<close> by (simp add: field_simps)
 finally show ?thesis .
 qed (use \<open>0 < \<epsilon>\<close> \<open>m \<le> n\<close> in auto)
 then show ?thesis
 by (metis dist_commute_lessI dist_real_def nle_le)
 qed
 qed auto
 define \<phi> where "\<phi> \<equiv> \<lambda>x. max a (min (h x) b)"
 show thesis
 proof
 show "continuous_map X euclidean \"
 unfolding \<phi>_def using conth by (intro continuous_intros) auto
 show "\ x = f x" if "x \ S" for x
 proof -
 have x: "x \ topspace X"
 using \<open>closedin X S\<close> closedin_subset that by blast
 have "h x = f x"
 proof (rule Met_TC.limitin_metric_unique)
 show "limitin Met_TC.mtopology (\n. g n x) (h x) sequentially"
 using h x by (force simp: tendsto_iff eventually_sequentially)
 show "limitin Met_TC.mtopology (\n. g n x) (f x) sequentially"
 proof (clarsimp simp: tendsto_iff)
 fix \<epsilon>::real
 assume "\ > 0"
 then have "\\<^sub>F n in sequentially. \(2/3) ^ n\ < \/c"
 by (intro Archimedean_eventually_pow_inverse) (auto simp: \<open>c > 0\<close>)
 then show "\\<^sub>F n in sequentially. dist (g n x) (f x) < \"
 apply eventually_elim
 by (smt (verit) good x good_def \<open>c > 0\<close> dist_real_def mult.commute pos_less_divide_eq that)
 qed
 qed auto
 then show ?thesis
 using that fim by (auto simp: \<phi>_def)
 qed
 then show "\ ` topspace X \ {a..b}"
 using fim \<open>a \<le> b\<close> by (auto simp: \<phi>_def)
 qed
qed

theorem Tietze_extension_realinterval:
 assumes XS: "normal_space X" "closedin X S" and T: "is_interval T" "T \ {}"
 and contf: "continuous_map (subtopology X S) euclideanreal f"
 and "f ` S \ T"
 obtains g where "continuous_map X euclideanreal g" "g ` topspace X \ T" "\x. x \ S \ g x = f x"
proof -
 define \<Phi> where
 "\ \ \T::real set. \f. continuous_map (subtopology X S) euclidean f \ f`S \ T
 \<longrightarrow> (\<exists>g. continuous_map X euclidean g \<and> g ` topspace X \<subseteq> T \<and> (\<forall>x \<in> S. g x = f x))"
 have "\ T"
 if *: "\T. \bounded T; is_interval T; T \ {}\ \ \ T"
 and "is_interval T" "T \ {}" for T
 unfolding \<Phi>_def
 proof (intro strip)
 fix f
 assume contf: "continuous_map (subtopology X S) euclideanreal f"
 and "f ` S \ T"
 have \<Phi>T: "\<Phi> ((\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T)"
 proof (rule *)
 show "bounded ((\x. x / (1 + \x\)) ` T)"
 using shrink_range [of T] by (force intro: boundedI [where B=1])
 show "is_interval ((\x. x / (1 + \x\)) ` T)"
 using connected_shrink that(2) is_interval_connected_1 by blast
 show "(\x. x / (1 + \x\)) ` T \ {}"
 using \<open>T \<noteq> {}\<close> by auto
 qed
 moreover have "continuous_map (subtopology X S) euclidean ((\x. x / (1 + \x\)) \ f)"
 by (metis contf continuous_map_compose continuous_map_into_fulltopology continuous_map_real_shrink)
 moreover have "((\x. x / (1 + \x\)) \ f) ` S \ (\x. x / (1 + \x\)) ` T"
 using \<open>f ` S \<subseteq> T\<close> by auto
 ultimately obtain g
 where contg: "continuous_map X euclidean g"
 and gim: "g ` topspace X \ (\x. x / (1 + \x\)) ` T"
 and geq: "\x. x \ S \ g x = ((\x. x / (1 + \x\)) \ f) x"
 using \<Phi>T unfolding \<Phi>_def by force
 show "\g. continuous_map X euclideanreal g \ g ` topspace X \ T \ (\x\S. g x = f x)"
 proof (intro conjI exI)
 have "continuous_map X (top_of_set {-1<..<1}) g"
 using contg continuous_map_in_subtopology gim shrink_range by blast
 then show "continuous_map X euclideanreal ((\x. x / (1 - \x\)) \ g)"
 by (rule continuous_map_compose) (auto simp: continuous_on_real_grow)
 show "((\x. x / (1 - \x\)) \ g) ` topspace X \ T"
 using gim real_grow_shrink by fastforce
 show "\x\S. ((\x. x / (1 - \x\)) \ g) x = f x"
 using geq real_grow_shrink by force
 qed
 qed
 moreover have "\ T"
 if "bounded T" "is_interval T" "T \ {}" for T
 unfolding \<Phi>_def
 proof (intro strip)
 fix f
 assume contf: "continuous_map (subtopology X S) euclideanreal f"
 and "f ` S \ T"
 obtain a b where ab: "closure T = {a..b}"
 by (meson \<open>bounded T\<close> \<open>is_interval T\<close> compact_closure connected_compact_interval_1
 connected_imp_connected_closure is_interval_connected)
 with \<open>T \<noteq> {}\<close> have "a \<le> b" by auto
 have "f ` S \ {a..b}"
 using \<open>f ` S \<subseteq> T\<close> ab closure_subset by auto
 then obtain g where contg: "continuous_map X euclideanreal g"
 and gf: "\x. x \ S \ g x = f x" and gim: "g ` topspace X \ {a..b}"
 using Tietze_extension_closed_real_interval [OF XS contf _ \<open>a \<le> b\<close>] by metis
 define W where "W \ {x \ topspace X. g x \ closure T - T}"
 have "{a..b} - {a, b} \ T"
 using that
 by (metis ab atLeastAtMost_diff_ends convex_interior_closure interior_atLeastAtMost_real
 interior_subset is_interval_convex)
 with finite_imp_compact have "compact (closure T - T)"
 by (metis Diff_eq_empty_iff Diff_insert2 ab finite.emptyI finite_Diff_insert)
 then have "closedin X W"
 unfolding W_def using closedin_continuous_map_preimage [OF contg] compact_imp_closed by force
 moreover have "disjnt W S"
 unfolding W_def disjnt_iff using \<open>f ` S \<subseteq> T\<close> gf by blast
 ultimately obtain h :: "'a \ real"
 where conth: "continuous_map X (top_of_set {0..1}) h"
 and him: "h ` W \ {0}" "h ` S \ {1}"
 by (metis XS normal_space_iff_Urysohn)
 then have him01: "h \ topspace X \ {0..1}"
 by (metis continuous_map_in_subtopology)
 obtain z where "z \ T"
 using \<open>T \<noteq> {}\<close> by blast
 define g' where "g' \<equiv> \<lambda>x. z + h x * (g x - z)"
 show "\g. continuous_map X euclidean g \ g ` topspace X \ T \ (\x\S. g x = f x)"
 proof (intro exI conjI)
 show "continuous_map X euclideanreal g'"
 unfolding g'_def using contg conth continuous_map_in_subtopology
 by (intro continuous_intros) auto
 show "g' ` topspace X \ T"
 unfolding g'_def
 proof clarify
 fix x
 assume "x \ topspace X"
 show "z + h x * (g x - z) \ T"
 proof (cases "g x \ T")
 case True
 define w where "w \ z + h x * (g x - z)"
 have "\h x\ * \g x - z\ \ \g x - z\" "\1 - h x\ * \g x - z\ \ \g x - z\"
 using him01 \<open>x \<in> topspace X\<close> by (force simp: intro: mult_left_le_one_le)+
 then consider "z \ w \ w \ g x" | "g x \ w \ w \ z"
 unfolding w_def by (smt (verit) left_diff_distrib mult_cancel_right2 mult_minus_right zero_less_mult_iff)
 then show ?thesis
 using \<open>is_interval T\<close> unfolding w_def is_interval_1 by (metis True \<open>z \<in> T\<close>)
 next
 case False
 then have "g x \ closure T"
 using \<open>x \<in> topspace X\<close> ab gim by blast
 then have "h x = 0"
 using him False \<open>x \<in> topspace X\<close> by (auto simp: W_def image_subset_iff)
 then show ?thesis
 by (simp add: \<open>z \<in> T\<close>)
 qed
 qed
 show "\x\S. g' x = f x"
 using gf him by (auto simp: W_def g'_def)
 qed
 qed
 ultimately show thesis
 using assms that unfolding \<Phi>_def by best
qed

lemma normal_space_iff_Tietze:
 "normal_space X \
 (\<forall>f S. closedin X S \<and>
 continuous_map (subtopology X S) euclidean f
 \<longrightarrow> (\<exists>g:: 'a \<Rightarrow> real. continuous_map X euclidean g \<and> (\<forall>x \<in> S. g x = f x)))"
 (is "?lhs \ ?rhs")
proof
 assume ?lhs
 then show ?rhs
 by (metis Tietze_extension_realinterval empty_not_UNIV is_interval_univ subset_UNIV)
next
 assume R: ?rhs
 show ?lhs
 unfolding normal_space_iff_Urysohn_alt
 proof clarify
 fix S T
 assume "closedin X S"
 and "closedin X T"
 and "disjnt S T"
 then have cloST: "closedin X (S \ T)"
 by (simp add: closedin_Un)
 moreover
 have "continuous_map (subtopology X (S \ T)) euclideanreal (\x. if x \ S then 0 else 1)"
 unfolding continuous_map_closedin
 proof (intro conjI strip)
 fix C :: "real set"
 define D where "D \ {x \ topspace X. if x \ S then 0 \ C else x \ T \ 1 \ C}"
 have "D \ {{}, S, T, S \ T}"
 unfolding D_def
 using closedin_subset [OF \<open>closedin X S\<close>] closedin_subset [OF \<open>closedin X T\<close>] \<open>disjnt S T\<close>
 by (auto simp: disjnt_iff)
 then have "closedin X D"
 using \<open>closedin X S\<close> \<open>closedin X T\<close> closedin_empty by blast
 with closedin_subset_topspace
 show "closedin (subtopology X (S \ T)) {x \ topspace (subtopology X (S \ T)). (if x \ S then 0::real else 1) \ C}"
 apply (simp add: D_def)
 by (smt (verit, best) Collect_cong Collect_mono_iff Un_def closedin_subset_topspace)
 qed auto
 ultimately obtain g :: "'a \ real" where
 contg: "continuous_map X euclidean g" and gf: "\x \ S \ T. g x = (if x \ S then 0 else 1)"
 using R by blast
 then show "\f. continuous_map X euclideanreal f \ f ` S \ {0} \ f ` T \ {1}"
 by (smt (verit) Un_iff \<open>disjnt S T\<close> disjnt_iff image_subset_iff insert_iff)
 qed
qed

subsection \<open>Random metric space stuff\<close>

lemma metrizable_imp_k_space:
 assumes "metrizable_space X"
 shows "k_space X"
proof -
 obtain M d where "Metric_space M d" and Xeq: "X = Metric_space.mtopology M d"
 using assms unfolding metrizable_space_def by metis
 then interpret Metric_space M d
 by blast
 show ?thesis
 unfolding k_space Xeq
 proof clarsimp
 fix S
 assume "S \ M" and S: "\K. compactin mtopology K \ closedin (subtopology mtopology K) (K \ S)"
 have "l \ S"
 if \<sigma>: "range \<sigma> \<subseteq> S" and l: "limitin mtopology \<sigma> l sequentially" for \<sigma> l
 proof -
 define K where "K \ insert l (range \)"
 interpret Submetric M d K
 proof
 show "K \ M"
 unfolding K_def using l limitin_mspace \<open>S \<subseteq> M\<close> \<sigma> by blast
 qed
 have "compactin mtopology K"
 unfolding K_def using \<open>S \<subseteq> M\<close> \<sigma>
 by (force intro: compactin_sequence_with_limit [OF l])
 then have *: "closedin sub.mtopology (K \ S)"
 by (simp add: S mtopology_submetric)
 have "\ n \ K \ S" for n
 by (simp add: K_def range_subsetD \<sigma>)
 moreover have "limitin sub.mtopology \ l sequentially"
 using l
 unfolding sub.limit_metric_sequentially limit_metric_sequentially
 by (force simp: K_def)
 ultimately have "l \ K \ S"
 by (meson * \<sigma> image_subsetI sub.metric_closedin_iff_sequentially_closed)
 then show ?thesis
 by simp
 qed
 then show "closedin mtopology S"
 unfolding metric_closedin_iff_sequentially_closed
 using \<open>S \<subseteq> M\<close> by blast
 qed
qed

lemma (in Metric_space) k_space_mtopology: "k_space mtopology"
 by (simp add: metrizable_imp_k_space metrizable_space_mtopology)

lemma k_space_euclideanreal: "k_space (euclidean :: 'a::metric_space topology)"
 using metrizable_imp_k_space metrizable_space_euclidean by auto

subsection\<open>Hereditarily normal spaces\<close>

lemma hereditarily_B:
 assumes "\S T. separatedin X S T
 \<Longrightarrow> \<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
 shows "hereditarily normal_space X"
 unfolding hereditarily_def
proof (intro strip)
 fix W
 assume "W \ topspace X"
 show "normal_space (subtopology X W)"
 unfolding normal_space_def
 proof clarify
 fix S T
 assume clo: "closedin (subtopology X W) S" "closedin (subtopology X W) T"
 and "disjnt S T"
 then have "separatedin (subtopology X W) S T"
 by (simp add: separatedin_closed_sets)
 then obtain U V where "openin X U \ openin X V \ S \ U \ T \ V \ disjnt U V"
 using assms [of S T] by (meson separatedin_subtopology)
 then show "\U V. openin (subtopology X W) U \ openin (subtopology X W) V \ S \ U \ T \ V \ disjnt U V"
 apply (simp add: openin_subtopology_alt)
 by (meson clo closedin_imp_subset disjnt_subset1 disjnt_subset2 inf_le2)
 qed
qed

lemma hereditarily_C:
 assumes "separatedin X S T" and norm: "\U. openin X U \ normal_space (subtopology X U)"
 shows "\U V. openin X U \ openin X V \ S \ U \ T \ V \ disjnt U V"
proof -
 define ST where "ST \ X closure_of S \ X closure_of T"
 have subX: "S \ topspace X" "T \ topspace X"
 by (meson \<open>separatedin X S T\<close> separation_closedin_Un_gen)+
 have sub: "S \ topspace X - ST" "T \ topspace X - ST"
 unfolding ST_def
 by (metis Diff_mono Diff_triv \<open>separatedin X S T\<close> Int_lower1 Int_lower2 separatedin_def)+
 have "normal_space (subtopology X (topspace X - ST))"
 by (simp add: ST_def norm closedin_Int openin_diff)
 moreover have " disjnt (subtopology X (topspace X - ST) closure_of S)
 (subtopology X (topspace X - ST) closure_of T)"
 using Int_absorb1 ST_def sub by (fastforce simp: disjnt_iff closure_of_subtopology)
 ultimately show ?thesis
 using sub subX
 apply (simp add: normal_space_closures)
 by (metis ST_def closedin_Int closedin_closure_of closedin_def openin_trans_full)
qed

lemma hereditarily_normal_space:
 "hereditarily normal_space X \ (\U. openin X U \ normal_space(subtopology X U))"
 by (metis hereditarily_B hereditarily_C hereditarily)

lemma hereditarily_normal_separation:
 "hereditarily normal_space X \
 (\<forall>S T. separatedin X S T
 \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V))"
 by (metis hereditarily_B hereditarily_C hereditarily)

lemma metrizable_imp_hereditarily_normal_space:
 "metrizable_space X \ hereditarily normal_space X"
 by (simp add: hereditarily metrizable_imp_normal_space metrizable_space_subtopology)

lemma metrizable_space_separation:
 "\metrizable_space X; separatedin X S T\
 \<Longrightarrow> \<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
 by (metis hereditarily hereditarily_C metrizable_imp_hereditarily_normal_space)

lemma hereditarily_normal_separation_pairwise:
 "hereditarily normal_space X \
 (\<forall>\. finite \ \<and> (\<forall>S \<in> \. S \<subseteq> topspace X) \<and> pairwise (separatedin X) \
 \<longrightarrow> (\<exists>\<F>. (\<forall>S \<in> \. openin X (\<F> S) \<and> S \<subseteq> \<F> S) \<and>
 pairwise (\<lambda>S T. disjnt (\<F> S) (\<F> T)) \))"
 (is "?lhs \ ?rhs")
proof
 assume L: ?lhs
 show ?rhs
 proof clarify
 fix \
 assume "finite \" and \: "\S\\. S \ topspace X"
 and pw\: "pairwise (separatedin X) \"
 have "\V W. openin X V \ openin X W \ S \ V \
 (\<forall>T. T \<in> \ \<and> T \<noteq> S \<longrightarrow> T \<subseteq> W) \<and> disjnt V W"
 if "S \ \" for S
 proof -
 have "separatedin X S (\(\ - {S}))"
 by (metis \ \<open>finite \\<close> pw\ finite_Diff pairwise_alt separatedin_Union(1) that)
 with L show ?thesis
 unfolding hereditarily_normal_separation
 by (smt (verit) Diff_iff UnionI empty_iff insert_iff subset_iff)
 qed
 then obtain \<F> \<G>
 where *: "\S. S \ \ \ S \ \ S \ (\T. T \ \ \ T \ S \ T \ \ S)"
 and ope: "\S. S \ \ \ openin X (\ S) \ openin X (\ S)"
 and dis: "\S. S \ \ \ disjnt (\ S) (\ S)"
 by metis
 define \<H> where "\<H> \<equiv> \<lambda>S. \<F> S \<inter> (\<Inter>T \<in> \ - {S}. \<G> T)"
 show "\\. (\S\\. openin X (\ S) \ S \ \ S) \ pairwise (\S T. disjnt (\ S) (\ T)) \"
 proof (intro exI conjI strip)
 show "openin X (\ S)" if "S \ \" for S
 unfolding \<H>_def
 by (smt (verit) ope that DiffD1 \<open>finite \\<close> finite_Diff finite_imageI imageE openin_Int_Inter)
 show "S \ \ S" if "S \ \" for S
 unfolding \<H>_def using "*" that by auto
 show "pairwise (\S T. disjnt (\ S) (\ T)) \"
 using dis by (fastforce simp: disjnt_iff pairwise_alt \<H>_def)
 qed
 qed
next
 assume R: ?rhs
 show ?lhs
 unfolding hereditarily_normal_separation
 proof (intro strip)
 fix S T
 assume "separatedin X S T"
 show "\U V. openin X U \ openin X V \ S \ U \ T \ V \ disjnt U V"
 proof (cases "T=S")
 case True
 then show ?thesis
 using \<open>separatedin X S T\<close> by force
 next
 case False
 have "pairwise (separatedin X) {S, T}"
 by (simp add: \<open>separatedin X S T\<close> pairwise_insert separatedin_sym)
 moreover have "\S\{S, T}. S \ topspace X"
 by (metis \<open>separatedin X S T\<close> insertE separatedin_def singletonD)
 ultimately show ?thesis
 using R by (smt (verit) False finite.emptyI finite.insertI insertCI pairwiseD)
 qed
 qed
qed

lemma hereditarily_normal_space_perfect_map_image:
 "\hereditarily normal_space X; perfect_map X Y f\ \ hereditarily normal_space Y"
 unfolding perfect_map_def proper_map_def
 by (meson hereditarily_normal_space_continuous_closed_map_image)

lemma regular_second_countable_imp_hereditarily_normal_space:
 assumes "regular_space X \ second_countable X"
 shows "hereditarily normal_space X"
 unfolding hereditarily
 proof (intro regular_Lindelof_imp_normal_space strip)
 show "regular_space (subtopology X S)" for S
 by (simp add: assms regular_space_subtopology)
 show "Lindelof_space (subtopology X S)" for S
 using assms by (simp add: second_countable_imp_Lindelof_space second_countable_subtopology)
qed

subsection\<open>Completely regular spaces\<close>

definition completely_regular_space where
"completely_regular_space X \
 \<forall>S x. closedin X S \<and> x \<in> topspace X - S
 \<longrightarrow> (\<exists>f::'a\<Rightarrow>real. continuous_map X (top_of_set {0..1}) f \<and>
 f x = 0 \<and> (f ` S \<subseteq> {1}))"

lemma homeomorphic_completely_regular_space_aux:
 assumes X: "completely_regular_space X" and hom: "X homeomorphic_space Y"
 shows "completely_regular_space Y"
proof -
 obtain f g where hmf: "homeomorphic_map X Y f" and hmg: "homeomorphic_map Y X g"
 and fg: "(\x \ topspace X. g(f x) = x) \ (\y \ topspace Y. f(g y) = y)"
 using assms X homeomorphic_maps_map homeomorphic_space_def by fastforce
 show ?thesis
 unfolding completely_regular_space_def
 proof clarify
 fix S x
 assume A: "closedin Y S" and x: "x \ topspace Y" and "x \ S"
 then have "closedin X (g`S)"
 using hmg homeomorphic_map_closedness_eq by blast
 moreover have "g x \ g`S"
 by (meson A x \<open>x \<notin> S\<close> closedin_subset hmg homeomorphic_imp_injective_map inj_on_image_mem_iff)
 ultimately obtain \<phi> where \<phi>: "continuous_map X (top_of_set {0..1::real}) \<phi> \<and> \<phi> (g x) = 0 \<and> \<phi> ` g`S \<subseteq> {1}"
 by (metis DiffI X completely_regular_space_def hmg homeomorphic_imp_surjective_map image_eqI x)
 then have "continuous_map Y (top_of_set {0..1::real}) (\ \ g)"
 by (meson continuous_map_compose hmg homeomorphic_imp_continuous_map)
 then show "\\. continuous_map Y (top_of_set {0..1::real}) \ \ \ x = 0 \ \ ` S \ {1}"
 by (metis \<phi> comp_apply image_comp)
 qed
qed

lemma homeomorphic_completely_regular_space:
 assumes "X homeomorphic_space Y"
 shows "completely_regular_space X \ completely_regular_space Y"
 by (meson assms homeomorphic_completely_regular_space_aux homeomorphic_space_sym)

lemma completely_regular_space_alt:
 "completely_regular_space X \
 (\<forall>S x. closedin X S \<longrightarrow> x \<in> topspace X - S
 \<longrightarrow> (\<exists>f. continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {1}))"
proof -
 have "\f. continuous_map X (top_of_set {0..1::real}) f \ f x = 0 \ f ` S \ {1}"
 if "closedin X S" "x \ topspace X - S" and f: "continuous_map X euclideanreal f \ f x = 0 \ f ` S \ {1}"
 for S x f
 proof (intro exI conjI)
 show "continuous_map X (top_of_set {0..1}) (\x. max 0 (min (f x) 1))"
 using that
 by (auto simp: continuous_map_in_subtopology intro!: continuous_map_real_max continuous_map_real_min)
 qed (use that in auto)
 with continuous_map_in_subtopology show ?thesis
 unfolding completely_regular_space_def by metis
qed

text \<open>As above, but with @{term openin}\<close>
lemma completely_regular_space_alt':
 "completely_regular_space X \
 (\<forall>S x. openin X S \<longrightarrow> x \<in> S
 \<longrightarrow> (\<exists>f. continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` (topspace X - S) \<subseteq> {1}))"
 apply (simp add: completely_regular_space_alt all_closedin)
 by (meson openin_subset subsetD)

lemma completely_regular_space_gen_alt:
 fixes a b::real
 assumes "a \ b"
 shows "completely_regular_space X \
 (\<forall>S x. closedin X S \<longrightarrow> x \<in> topspace X - S
 \<longrightarrow> (\<exists>f. continuous_map X euclidean f \<and> f x = a \<and> (f ` S \<subseteq> {b})))"
proof -
 have "\f. continuous_map X euclideanreal f \ f x = 0 \ f ` S \ {1}"
 if "closedin X S" "x \ topspace X - S"
 and f: "continuous_map X euclidean f \ f x = a \ f ` S \ {b}"
 for S x f
 proof (intro exI conjI)
 show "continuous_map X euclideanreal ((\x. inverse(b - a) * (x - a)) \ f)"
 using that by (intro continuous_intros) auto
 qed (use that assms in auto)
 moreover
 have "\f. continuous_map X euclidean f \ f x = a \ f ` S \ {b}"
 if "closedin X S" "x \ topspace X - S"
 and f: "continuous_map X euclideanreal f \ f x = 0 \ f ` S \ {1}"
 for S x f
 proof (intro exI conjI)
 show "continuous_map X euclideanreal ((\x. a + (b - a) * x) \ f)"
 using that by (intro continuous_intros) auto
 qed (use that in auto)
 ultimately show ?thesis
 unfolding completely_regular_space_alt by meson
qed

text \<open>As above, but with @{term openin}\<close>
lemma completely_regular_space_gen_alt':
 fixes a b::real
 assumes "a \ b"
 shows "completely_regular_space X \
 (\<forall>S x. openin X S \<longrightarrow> x \<in> S
 \<longrightarrow> (\<exists>f. continuous_map X euclidean f \<and> f x = a \<and> (f ` (topspace X - S) \<subseteq> {b})))"
 apply (simp add: completely_regular_space_gen_alt[OF assms] all_closedin)
 by (meson openin_subset subsetD)

lemma completely_regular_space_gen:
 fixes a b::real
 assumes "a < b"
 shows "completely_regular_space X \
 (\<forall>S x. closedin X S \<and> x \<in> topspace X - S
 \<longrightarrow> (\<exists>f. continuous_map X (top_of_set {a..b}) f \<and> f x = a \<and> f ` S \<subseteq> {b}))"
proof -
 have "\f. continuous_map X (top_of_set {a..b}) f \ f x = a \ f ` S \ {b}"
 if "closedin X S" "x \ topspace X - S"
 and f: "continuous_map X euclidean f \ f x = a \ f ` S \ {b}"
 for S x f
 proof (intro exI conjI)
 show "continuous_map X (top_of_set {a..b}) (\x. max a (min (f x) b))"
 using that assms
 by (auto simp: continuous_map_in_subtopology intro!: continuous_map_real_max continuous_map_real_min)
 qed (use that assms in auto)
 with continuous_map_in_subtopology assms show ?thesis
 using completely_regular_space_gen_alt [of a b]
 by (smt (verit) atLeastAtMost_singleton atLeastatMost_empty singletonI)
qed

lemma normal_imp_completely_regular_space_A:
 assumes "normal_space X" "t1_space X"
 shows "completely_regular_space X"
 unfolding completely_regular_space_alt
proof clarify
 fix x S
 assume A: "closedin X S" "x \ S"
 assume "x \ topspace X"
 then have "closedin X {x}"
 by (simp add: \<open>t1_space X\<close> closedin_t1_singleton)
 with A \<open>normal_space X\<close> have "\<exists>f. continuous_map X euclideanreal f \<and> f ` {x} \<subseteq> {0} \<and> f ` S \<subseteq> {1}"
 using assms unfolding normal_space_iff_Urysohn_alt disjnt_iff by blast
 then show "\f. continuous_map X euclideanreal f \ f x = 0 \ f ` S \ {1}"
 by auto
qed

lemma normal_imp_completely_regular_space_B:
 assumes "normal_space X" "regular_space X"
 shows "completely_regular_space X"
 unfolding completely_regular_space_alt
proof clarify
 fix x S
 assume "closedin X S" "x \ S" "x \ topspace X"
 then obtain U C where "openin X U" "closedin X C" "x \ U" "U \ C" "C \ topspace X - S"
 using assms
 unfolding neighbourhood_base_of_closedin [symmetric] neighbourhood_base_of closedin_def by (metis Diff_iff)
 then obtain f where "continuous_map X euclideanreal f \ f ` C \ {0} \ f ` S \ {1}"
 using assms unfolding normal_space_iff_Urysohn_alt
 by (metis Diff_iff \<open>closedin X S\<close> disjnt_iff subsetD)
 then show "\f. continuous_map X euclideanreal f \ f x = 0 \ f ` S \ {1}"
 by (meson \<open>U \<subseteq> C\<close> \<open>x \<in> U\<close> image_subset_iff singletonD subsetD)
qed

lemma normal_imp_completely_regular_space_gen:
 "\normal_space X; t1_space X \ Hausdorff_space X \ regular_space X\ \ completely_regular_space X"
 using normal_imp_completely_regular_space_A normal_imp_completely_regular_space_B t1_or_Hausdorff_space by blast

lemma normal_imp_completely_regular_space:
 "\normal_space X; Hausdorff_space X \ regular_space X\ \ completely_regular_space X"
 by (simp add: normal_imp_completely_regular_space_gen)

lemma (in Metric_space) completely_regular_space_mtopology:
 "completely_regular_space mtopology"
 by (simp add: normal_imp_completely_regular_space normal_space_mtopology regular_space_mtopology)

lemma metrizable_imp_completely_regular_space:
 "metrizable_space X \ completely_regular_space X"
 by (simp add: metrizable_imp_normal_space metrizable_imp_regular_space normal_imp_completely_regular_space)

lemma completely_regular_space_discrete_topology:
 "completely_regular_space(discrete_topology U)"
 by (simp add: normal_imp_completely_regular_space normal_space_discrete_topology)

lemma completely_regular_space_subtopology:
 assumes "completely_regular_space X"
 shows "completely_regular_space (subtopology X S)"
 unfolding completely_regular_space_def
proof clarify
 fix A x
 assume "closedin (subtopology X S) A" and x: "x \ topspace (subtopology X S)" and "x \ A"
 then obtain T where "closedin X T" "A = S \ T" "x \ topspace X" "x \ S"
 by (force simp: closedin_subtopology_alt image_iff)
 then show "\f. continuous_map (subtopology X S) (top_of_set {0::real..1}) f \ f x = 0 \ f ` A \ {1}"
 using assms \<open>x \<notin> A\<close>
 apply (simp add: completely_regular_space_def continuous_map_from_subtopology)
 using continuous_map_from_subtopology by fastforce
qed

lemma completely_regular_space_retraction_map_image:
 " \retraction_map X Y r; completely_regular_space X\ \ completely_regular_space Y"
 using completely_regular_space_subtopology hereditary_imp_retractive_property homeomorphic_completely_regular_space by blast

lemma completely_regular_imp_regular_space:
 assumes "completely_regular_space X"
 shows "regular_space X"
proof -
 have *: "\U V. openin X U \ openin X V \ a \ U \ C \ V \ disjnt U V"
 if contf: "continuous_map X euclideanreal f" and a: "a \ topspace X - C" and "closedin X C"
 and fim: "f \ topspace X \ {0..1}" and f0: "f a = 0" and f1: "f ` C \ {1}"
 for C a f
 proof (intro exI conjI)
 show "openin X {x \ topspace X. f x \ {..<1 / 2}}" "openin X {x \ topspace X. f x \ {1 / 2<..}}"
 using openin_continuous_map_preimage [OF contf]
 by (meson open_lessThan open_greaterThan open_openin)+
 show "a \ {x \ topspace X. f x \ {..<1 / 2}}"
 using a f0 by auto
 show "C \ {x \ topspace X. f x \ {1 / 2<..}}"
 using \<open>closedin X C\<close> f1 closedin_subset by auto
 qed (auto simp: disjnt_iff)
 show ?thesis
 using assms *
 unfolding completely_regular_space_def regular_space_def continuous_map_in_subtopology
 by metis
qed

proposition locally_compact_regular_imp_completely_regular_space:
 assumes "locally_compact_space X" "Hausdorff_space X \ regular_space X"
 shows "completely_regular_space X"
 unfolding completely_regular_space_def
proof clarify
 fix S x
 assume "closedin X S" and "x \ topspace X" and "x \ S"
 have "regular_space X"
 using assms locally_compact_Hausdorff_imp_regular_space by blast
 then have nbase: "neighbourhood_base_of (\C. compactin X C \ closedin X C) X"
 using assms(1) locally_compact_regular_space_neighbourhood_base by blast
 then obtain U M where "openin X U" "compactin X M" "closedin X M" "x \ U" "U \ M" "M \ topspace X - S"
 unfolding neighbourhood_base_of by (metis (no_types, lifting) Diff_iff \<open>closedin X S\<close> \<open>x \<in> topspace X\<close> \<open>x \<notin> S\<close> closedin_def)
 then have "M \ topspace X"
 by blast
 obtain V K where "openin X V" "closedin X K" "x \ V" "V \ K" "K \ U"
 by (metis (no_types, lifting) \<open>openin X U\<close> \<open>x \<in> U\<close> neighbourhood_base_of nbase)
 have "compact_space (subtopology X M)"
 by (simp add: \<open>compactin X M\<close> compact_space_subtopology)
 then have "normal_space (subtopology X M)"
 by (simp add: \<open>regular_space X\<close> compact_Hausdorff_or_regular_imp_normal_space regular_space_subtopology)
 moreover have "closedin (subtopology X M) K"
 using \<open>K \<subseteq> U\<close> \<open>U \<subseteq> M\<close> \<open>closedin X K\<close> closedin_subset_topspace by fastforce
 moreover have "closedin (subtopology X M) (M - U)"
 by (simp add: \<open>closedin X M\<close> \<open>openin X U\<close> closedin_diff closedin_subset_topspace)
 moreover have "disjnt K (M - U)"
 by (meson DiffD2 \<open>K \<subseteq> U\<close> disjnt_iff subsetD)
 ultimately obtain f::"'a\real" where contf: "continuous_map (subtopology X M) (top_of_set {0..1}) f"
 and f0: "f ` K \ {0}" and f1: "f ` (M - U) \ {1}"
 using Urysohn_lemma [of "subtopology X M" K "M-U" 0 1] by auto
 then obtain g::"'a\real" where contg: "continuous_map (subtopology X M) euclidean g" and gim: "g ` M \ {0..1}"
 and g0: "\x. x \ K \ g x = 0" and g1: "\x. \x \ M; x \ U\ \ g x = 1"
 using \<open>M \<subseteq> topspace X\<close> by (force simp: continuous_map_in_subtopology image_subset_iff)
 show "\f::'a\real. continuous_map X (top_of_set {0..1}) f \ f x = 0 \ f ` S \ {1}"
 proof (intro exI conjI)
 show "continuous_map X (top_of_set {0..1}) (\x. if x \ M then g x else 1)"
 unfolding continuous_map_closedin
 proof (intro strip conjI)
 fix C
 assume C: "closedin (top_of_set {0::real..1}) C"
 have eq: "{x \ topspace X. (if x \ M then g x else 1) \ C} = {x \ M. g x \ C} \ (if 1 \ C then topspace X - U else {})"
 using \<open>U \<subseteq> M\<close> \<open>M \<subseteq> topspace X\<close> g1 by auto
 show "closedin X {x \ topspace X. (if x \ M then g x else 1) \ C}"
 unfolding eq
 proof (intro closedin_Un)
 have "closedin euclidean C"
 using C closed_closedin closedin_closed_trans by blast
 then have "closedin (subtopology X M) {x \ M. g x \ C}"
 using closedin_continuous_map_preimage_gen [OF contg] \<open>M \<subseteq> topspace X\<close> by auto
 then show "closedin X {x \ M. g x \ C}"
 using \<open>closedin X M\<close> closedin_trans_full by blast
 qed (use \<open>openin X U\<close> in force)
 qed (use gim in force)
 show "(if x \ M then g x else 1) = 0"
 using \<open>U \<subseteq> M\<close> \<open>V \<subseteq> K\<close> g0 \<open>x \<in> U\<close> \<open>x \<in> V\<close> by auto
 show "(\x. if x \ M then g x else 1) ` S \ {1}"
 using \<open>M \<subseteq> topspace X - S\<close> by auto
 qed
qed

lemma completely_regular_eq_regular_space:
 "locally_compact_space X
 \<Longrightarrow> (completely_regular_space X \<longleftrightarrow> regular_space X)"
 using completely_regular_imp_regular_space locally_compact_regular_imp_completely_regular_space
 by blast

lemma completely_regular_space_prod_topology:
 "completely_regular_space (prod_topology X Y) \
 (prod_topology X Y) = trivial_topology \<or>
 completely_regular_space X \<and> completely_regular_space Y" (is "?lhs=?rhs")
proof
 assume ?lhs then show ?rhs
 by (rule topological_property_of_prod_component)
 (auto simp: completely_regular_space_subtopology homeomorphic_completely_regular_space)
next
 assume R: ?rhs
 show ?lhs
 proof (cases "(prod_topology X Y) = trivial_topology")
 case False
 then have X: "completely_regular_space X" and Y: "completely_regular_space Y"
 using R by blast+
 show ?thesis
 unfolding completely_regular_space_alt'
 proof clarify
 fix W x y
 assume "openin (prod_topology X Y) W" and "(x, y) \ W"
 then obtain U V where "openin X U" "openin Y V" "x \ U" "y \ V" "U\V \ W"
 by (force simp: openin_prod_topology_alt)
 then have "x \ topspace X" "y \ topspace Y"
 using openin_subset by fastforce+
 obtain f where contf: "continuous_map X euclideanreal f" and "f x = 0"
 and f1: "\x. x \ topspace X \ x \ U \ f x = 1"
 using X \<open>openin X U\<close> \<open>x \<in> U\<close> unfolding completely_regular_space_alt'
 by (smt (verit, best) Diff_iff image_subset_iff singletonD)
 obtain g where contg: "continuous_map Y euclideanreal g" and "g y = 0"
 and g1: "\y. y \ topspace Y \ y \ V \ g y = 1"
 using Y \<open>openin Y V\<close> \<open>y \<in> V\<close> unfolding completely_regular_space_alt'
 by (smt (verit, best) Diff_iff image_subset_iff singletonD)
 define h where "h \ \(x,y). 1 - (1 - f x) * (1 - g y)"
 show "\h. continuous_map (prod_topology X Y) euclideanreal h \ h (x,y) = 0 \ h ` (topspace (prod_topology X Y) - W) \ {1}"
 proof (intro exI conjI)
 have "continuous_map (prod_topology X Y) euclideanreal (f \ fst)"
 using contf continuous_map_of_fst by blast
 moreover
 have "continuous_map (prod_topology X Y) euclideanreal (g \ snd)"
 using contg continuous_map_of_snd by blast
 ultimately
 show "continuous_map (prod_topology X Y) euclideanreal h"
 unfolding o_def h_def case_prod_unfold
 by (intro continuous_intros) auto
 show "h (x, y) = 0"
 by (simp add: h_def \<open>f x = 0\<close> \<open>g y = 0\<close>)
 show "h ` (topspace (prod_topology X Y) - W) \ {1}"
 using \<open>U \<times> V \<subseteq> W\<close> f1 g1 by (force simp: h_def)
 qed
 qed
 qed (force simp: completely_regular_space_def)
qed

proposition completely_regular_space_product_topology:
 "completely_regular_space (product_topology X I) \
 (\<exists>i\<in>I. X i = trivial_topology) \<or> (\<forall>i \<in> I. completely_regular_space (X i))"
 (is "?lhs \ ?rhs")
proof
 assume ?lhs then show ?rhs
 by (rule topological_property_of_product_component)
 (auto simp: completely_regular_space_subtopology homeomorphic_completely_regular_space)
next
 assume R: ?rhs
 show ?lhs
 proof (cases "\i\I. X i = trivial_topology")
 case False
 show ?thesis
 unfolding completely_regular_space_alt'
 proof clarify
 fix W x
 assume W: "openin (product_topology X I) W" and "x \ W"
 then obtain U where finU: "finite {i \ I. U i \ topspace (X i)}"
 and ope: "\i. i\I \ openin (X i) (U i)"
 and x: "x \ Pi\<^sub>E I U" and "Pi\<^sub>E I U \ W"
 by (auto simp: openin_product_topology_alt)
 have "\i \ I. openin (X i) (U i) \ x i \ U i
 \<longrightarrow> (\<exists>f. continuous_map (X i) euclideanreal f \<and>
 f (x i) = 0 \<and> (\<forall>x \<in> topspace(X i). x \<notin> U i \<longrightarrow> f x = 1))"
 using R unfolding completely_regular_space_alt'
 by (smt (verit) DiffI False image_subset_iff singletonD)
 with ope x have "\i. \f. i \ I \ continuous_map (X i) euclideanreal f \
 f (x i) = 0 \<and> (\<forall>x \<in> topspace (X i). x \<notin> U i \<longrightarrow> f x = 1)"
 by auto
 then obtain f where f: "\i. i \ I \ continuous_map (X i) euclideanreal (f i) \
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.