(* Title: HOL/Analysis/Arcwise_Connected.thy
Authors: LC Paulson, based on material from HOL Light
*)
section \<open>Urysohn lemma and its Consequences\<close>
theory Urysohn
imports Abstract_Topological_Spaces Abstract_Metric_Spaces Infinite_Sum Arcwise_Connected
begin
subsection \<open>Urysohn lemma and Tietze's theorem\<close>
lemma Urysohn_lemma:
fixes a b :: real
assumes "normal_space X" "closedin X S" "closedin X T" "disjnt S T" "a \<le> b"
obtains f where "continuous_map X (top_of_set {a..b}) f" "f ` S \<subseteq> {a}" "f ` T \<subseteq> {b}"
proof -
obtain U where "openin X U" "S \<subseteq> U" "X closure_of U \<subseteq> 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 "\<exists>G :: real \<Rightarrow> 'a set. G 0 = U \<and> G 1 = topspace X - T \<and>
(\<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 \<and> openin X (topspace X - T) \<and> X closure_of U \<subseteq> 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 "\<exists>z. (openin X x \<and> openin X z \<and> X closure_of x \<subseteq> z) \<and> openin X z \<and> openin X y \<and> X closure_of z \<subseteq> y"
if "openin X x \<and> openin X y \<and> X closure_of x \<subseteq> y" for x y
by (meson that closedin_closure_of normal_space_alt \<open>normal_space X\<close>)
show "openin X x \<and> openin X z \<and> X closure_of x \<subseteq> z"
if "openin X x \<and> openin X y \<and> X closure_of x \<subseteq> y" and "openin X y \<and> openin X z \<and> X closure_of y \<subseteq> z" for x y z
by (meson that closure_of_subset openin_subset subset_trans)
qed
then obtain G :: "real \<Rightarrow> 'a set"
where G0: "G 0 = U" and G1: "G 1 = topspace X - T"
and G: "\<And>x y. \<lbrakk>x \<in> dyadics; y \<in> dyadics; 0 \<le> x; x < y; y \<le> 1\<rbrakk>
\<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 \<equiv> \<lambda>x. Inf(insert 1 {r. r \<in> dyadics \<inter> {0..1} \<and> x \<in> G r})"
have f_ge: "f x \<ge> 0" if "x \<in> topspace X" for x
unfolding f_def by (force intro: cInf_greatest)
moreover have f_le1: "f x \<le> 1" if "x \<in> topspace X" for x
proof -
have "bdd_below {r \<in> dyadics \<inter> {0..1}. x \<in> 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 \<subseteq> {0..1}"
by (auto simp: f_def)
have 0: "0 \<in> dyadics \<inter> {0..1::real}" and 1: "1 \<in> dyadics \<inter> {0..1::real}"
by (force simp: dyadics_def)+
then have opeG: "openin X (G r)" if "r \<in> dyadics \<inter> {0..1}" for r
using G G0 \<open>openin X U\<close> less_eq_real_def that by auto
have "x \<in> G 0" if "x \<in> S" for x
using G0 \<open>S \<subseteq> U\<close> that by blast
with 0 have fimS: "f ` S \<subseteq> {0}"
unfolding f_def by (force intro!: cInf_eq_minimum)
have False if "r \<in> dyadics" "0 \<le> r" "r < 1" "x \<in> G r" "x \<in> 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\<ge>1" if "r \<in> dyadics" "0 \<le> r" "r \<le> 1" "x \<in> G r" "x \<in> T" for r x
using linorder_not_le that by blast
then have fimT: "f ` T \<subseteq> {1}"
unfolding f_def by (force intro!: cInf_eq_minimum)
have fle1: "f z \<le> 1" for z
by (force simp: f_def intro: cInf_lower)
have fle: "f z \<le> x" if "x \<in> dyadics \<inter> {0..1}" "z \<in> G x" for z x
using that by (force simp: f_def intro: cInf_lower)
have *: "b \<le> f z" if "b \<le> 1" "\<And>x. \<lbrakk>x \<in> dyadics \<inter> {0..1}; z \<in> G x\<rbrakk> \<Longrightarrow> b \<le> x" for z b
using that by (force simp: f_def intro: cInf_greatest)
have **: "r \<le> f x" if r: "r \<in> dyadics \<inter> {0..1}" "x \<notin> G r" for r x
proof (rule *)
show "r \<le> s" if "s \<in> dyadics \<inter> {0..1}" and "x \<in> G s" for s :: real
using that r G [of s r] by (force simp add: dest: closure_of_subset openin_subset)
qed (use that in force)
have "\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y \<in> U. \<bar>f y - f x\<bar> < \<epsilon>)"
if "x \<in> topspace X" and "0 < \<epsilon>" for x \<epsilon>
proof -
have A: "\<exists>r. r \<in> dyadics \<inter> {0..1} \<and> r < y \<and> \<bar>r - y\<bar> < d" if "0 < y" "y \<le> 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" "\<bar>q / 2^n - r / 2^n \<bar> < 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: "\<exists>r. r \<in> dyadics \<inter> {0..1} \<and> y < r \<and> \<bar>r - y\<bar> < d" if "0 \<le> y" "y < 1" "0 < d" for y d::real
proof -
obtain n q r
where "of_nat q / 2^n \<le> y" "y < of_nat r / 2^n" "\<bar>q / 2^n - r / 2^n \<bar> < 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 \<in> dyadics \<inter> {0..1}" "0 < r" "\<bar>r\<bar> < \<epsilon>/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 \<in> G r"
using True ** r by force
show "\<forall>y \<in> G r. \<bar>f y - f x\<bar> < \<epsilon>"
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 \<in> dyadics \<inter> {0..1}" "r < 1" "\<bar>r-1\<bar> < \<epsilon>/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 \<in> dyadics" "0 \<le> r"
using 1 r dyadics_diff by force+
ultimately have "x \<notin> X closure_of G r"
using G True r fle by force
then show "x \<in> G'"
by (simp add: G'_def that)
show "\<forall>y \<in> G'. \<bar>f y - f x\<bar> < \<epsilon>"
using ** f_le1 in_closure_of r by (fastforce simp add: 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 \<in> dyadics \<inter> {0..1}" "r < f x" "\<bar>r - f x\<bar> < \<epsilon> / 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' \<in> dyadics \<inter> {0..1}" "f x < r'" "\<bar>r' - f x\<bar> < \<epsilon> / 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 \<in> X closure_of G r \<Longrightarrow> False"
using B [of r "f x - r"] r \<open>r < 1\<close> G [of r] fle by force
then show "x \<in> G r' - X closure_of G r"
using ** r' by fastforce
show "\<forall>y\<in>G r' - X closure_of G r. \<bar>f y - f x\<bar> < \<epsilon>"
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 (force simp add: Met_TC.continuous_map_to_metric dist_real_def continuous_map_in_subtopology fim simp flip: mtopology_is_euclidean)
define g where "g \<equiv> \<lambda>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) \<subseteq> {a..b}"
using mult_left_le [of "f _" "b-a"] contf \<open>a \<le> b\<close>
by (simp add: g_def add.commute continuous_map_in_subtopology image_subset_iff le_diff_eq)
ultimately show "continuous_map X (top_of_set {a..b}) g"
by (meson continuous_map_in_subtopology)
show "g ` S \<subseteq> {a}" "g ` T \<subseteq> {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 \<subseteq> {a}" "f ` T \<subseteq> {b}"
by (metis Urysohn_lemma assms continuous_map_in_subtopology disjnt_sym linear)
lemma normal_space_iff_Urysohn_gen_alt:
assumes "a \<noteq> b"
shows "normal_space X \<longleftrightarrow>
(\<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 \<Longrightarrow> ?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 \<subseteq> {a}" "f ` T \<subseteq> {b}"
by meson
show "\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
proof (intro conjI exI)
show "openin X {x \<in> topspace X. f x \<in> ball a (\<bar>a - b\<bar> / 2)}"
by (force intro!: openin_continuous_map_preimage [OF contf])
show "openin X {x \<in> topspace X. f x \<in> ball b (\<bar>a - b\<bar> / 2)}"
by (force intro!: openin_continuous_map_preimage [OF contf])
show "S \<subseteq> {x \<in> topspace X. f x \<in> ball a (\<bar>a - b\<bar> / 2)}"
using \<open>closedin X S\<close> closedin_subset \<open>f ` S \<subseteq> {a}\<close> assms by force
show "T \<subseteq> {x \<in> topspace X. f x \<in> ball b (\<bar>a - b\<bar> / 2)}"
using \<open>closedin X T\<close> closedin_subset \<open>f ` T \<subseteq> {b}\<close> assms by force
have "\<And>x. \<lbrakk>x \<in> topspace X; dist a (f x) < \<bar>a-b\<bar>/2; dist b (f x) < \<bar>a-b\<bar>/2\<rbrakk> \<Longrightarrow> False"
by (smt (verit, best) dist_real_def dist_triangle_half_l)
then show "disjnt {x \<in> topspace X. f x \<in> ball a (\<bar>a-b\<bar> / 2)} {x \<in> topspace X. f x \<in> ball b (\<bar>a-b\<bar> / 2)}"
using disjnt_iff by fastforce
qed
qed
qed
lemma normal_space_iff_Urysohn_gen:
fixes a b::real
shows
"a < b \<Longrightarrow>
normal_space X \<longleftrightarrow>
(\<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 \<longleftrightarrow>
(\<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 \<longleftrightarrow>
(\<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:
"\<lbrakk>normal_space X; perfect_map X Y f\<rbrakk> \<Longrightarrow> 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:
"\<lbrakk>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:
"\<lbrakk>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 \<noteq> {}"
and clo: "closedin X S" "closedin X T" "disjnt S T"
obtains h :: "nat \<Rightarrow> 'a set" where
"\<And>n. openin X (h n)" "\<And>n. disjnt T (X closure_of (h n))" and "S \<subseteq> \<Union>(range h)"
proof -
have "\<exists>U. openin X U \<and> x \<in> U \<and> disjnt T (X closure_of U)"
if "x \<in> 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: "\<And>x. x \<in> S \<Longrightarrow> openin X (h x)"
and xh: "\<And>x. x \<in> S \<Longrightarrow> x \<in> h x"
and dh: "\<And>x. x \<in> S \<Longrightarrow> 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 \<U> where \<U>: "countable \<U> \<and> \<U> \<subseteq> h ` S \<and> S \<subseteq> \<Union>\<U>"
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 "\<U> \<noteq> {}"
by blast
show ?thesis
proof
show "openin X (from_nat_into \<U> n)" for n
by (metis \<U> from_nat_into image_iff \<open>\<U> \<noteq> {}\<close> oh subsetD)
show "disjnt T (X closure_of (from_nat_into \<U>) n)" for n
using dh from_nat_into [OF \<open>\<U> \<noteq> {}\<close>]
by (metis \<U> f_inv_into_f inv_into_into subset_eq)
show "S \<subseteq> \<Union>(range (from_nat_into \<U>))"
by (simp add: \<U> \<open>\<U> \<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 "\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
proof (cases "S={} \<or> 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 \<Rightarrow> 'a set" where
opeh: "\<And>n. openin X (h n)" and dish: "\<And>n. disjnt T (X closure_of (h n))"
and Sh: "S \<subseteq> \<Union>(range h)"
by (metis Lindelof_cover False \<open>disjnt S T\<close> assms clo)
obtain k :: "nat \<Rightarrow> 'a set" where
opek: "\<And>n. openin X (k n)" and disk: "\<And>n. disjnt S (X closure_of (k n))"
and Tk: "T \<subseteq> \<Union>(range k)"
by (metis Lindelof_cover False \<open>disjnt S T\<close> assms clo disjnt_sym)
define U where "U \<equiv> \<Union>i. h i - (\<Union>j<i. X closure_of k j)"
define V where "V \<equiv> \<Union>i. k i - (\<Union>j\<le>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 \<subseteq> U" "T \<subseteq> V"
using Sh Tk dish disk by (fastforce simp: U_def V_def disjnt_iff)+
have "\<And>x i j. \<lbrakk>x \<in> k i; x \<in> h j; \<forall>j\<le>i. x \<notin> X closure_of h j\<rbrakk>
\<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 add: U_def V_def disjnt_iff)
qed
qed
qed
lemma 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 \<subseteq> {a..b}" and "a \<le> b"
obtains g
where "continuous_map X euclideanreal g"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x" "g ` topspace X \<subseteq> {a..b}"
proof -
define c where "c \<equiv> max \<bar>a\<bar> \<bar>b\<bar> + 1"
have "0 < c" and c: "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<le> c"
using fim by (auto simp: c_def image_subset_iff)
define good where
"good \<equiv> \<lambda>g n. continuous_map X euclideanreal g \<and> (\<forall>x \<in> S. \<bar>f x - g x\<bar> \<le> c * (2/3)^n)"
have step: "\<exists>g. good g (Suc n) \<and>
(\<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 \<subseteq> topspace X"
using \<open>closedin X S\<close> closedin_subset by auto
define d where "d \<equiv> c/3 * (2/3) ^ n"
define SA where "SA \<equiv> {x \<in> S. f x - h x \<in> {..-d}}"
define SB where "SB \<equiv> {x \<in> S. f x - h x \<in> {d..}}"
have contfh: "continuous_map (subtopology X S) euclideanreal (\<lambda>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
by (smt (verit, del_insts) closed_closedin continuous_map_closedin Collect_cong S_eq closed_real_atMost)
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 \<le> 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 \<subseteq> {- d}" and gb: "g ` SB \<subseteq> {d}"
using Urysohn_lemma \<open>normal_space X\<close> by metis
then have g_le_d: "\<And>x. x \<in> topspace X \<Longrightarrow> \<bar>g x\<bar> \<le> d"
by (simp add: abs_le_iff continuous_map_def minus_le_iff)
have g_eq_d: "\<And>x. \<lbrakk>x \<in> S; f x - h x \<le> -d\<rbrakk> \<Longrightarrow> g x = -d"
using ga by (auto simp: SA_def)
have g_eq_negd: "\<And>x. \<lbrakk>x \<in> S; f x - h x \<ge> d\<rbrakk> \<Longrightarrow> 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 (\<lambda>x. h x + g x)"
using contg continuous_map_add continuous_map_in_subtopology that
unfolding good_def by blast
show "\<bar>f x - (h x + g x)\<bar> \<le> c * (2 / 3) ^ Suc n" if "x \<in> S" for x
proof -
have x: "x \<in> topspace X"
using \<open>S \<subseteq> topspace X\<close> that by auto
have "\<bar>f x - h x\<bar> \<le> 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 "\<bar>f x - (h x + g x)\<bar> \<le> d + d"
unfolding d_def by linarith
then show ?thesis
by (simp add: d_def)
qed
show "\<bar>h x + g x - h x\<bar> \<le> c * (2 / 3) ^ n / 3" if "x \<in> topspace X" for x
using that d_def g_le_d by auto
qed
qed
then obtain nxtg where nxtg: "\<And>h n. good h n \<Longrightarrow>
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 \<equiv> rec_nat (\<lambda>x. 0) (\<lambda>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 *: "\<And>n x. x \<in> topspace X \<Longrightarrow> \<bar>g(Suc n) x - g n x\<bar> \<le> c * (2/3) ^ n / 3"
using nxtg g_Suc good by force
obtain h where conth: "continuous_map X euclideanreal h"
and h: "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>topspace X. dist (g n x) (h x) < \<epsilon>"
proof (rule Met_TC.continuous_map_uniformly_Cauchy_limit)
show "\<forall>\<^sub>F n in sequentially. continuous_map X (Met_TC.mtopology) (g n)"
using good good_def by fastforce
show "\<exists>N. \<forall>m n x. N \<le> m \<longrightarrow> N \<le> n \<longrightarrow> x \<in> topspace X \<longrightarrow> dist (g m x) (g n x) < \<epsilon>"
if "\<epsilon> > 0" for \<epsilon>
proof -
have "\<forall>\<^sub>F n in sequentially. \<bar>(2/3) ^ n\<bar> < \<epsilon>/c"
proof (rule Archimedean_eventually_pow_inverse)
show "0 < \<epsilon> / c"
by (simp add: \<open>0 < c\<close> that)
qed auto
then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> \<bar>(2/3) ^ n\<bar> < \<epsilon>/c"
by (meson eventually_sequentially order_le_less_trans)
have "\<bar>g m x - g n x\<bar> < \<epsilon>"
if "N \<le> m" "N \<le> n" and x: "x \<in> topspace X" "m \<le> n" for m n x
proof (cases "m < n")
case True
have 23: "(\<Sum>k = m..<n. (2/3)^k) = 3 * ((2/3) ^ m - (2/3::real) ^ n)"
using \<open>m \<le> n\<close>
by (induction n) (auto simp: le_Suc_eq)
have "\<bar>g m x - g n x\<bar> \<le> \<bar>\<Sum>k = m..<n. g (Suc k) x - g k x\<bar>"
by (subst sum_Suc_diff' [OF \<open>m \<le> n\<close>]) linarith
also have "\<dots> \<le> (\<Sum>k = m..<n. \<bar>g (Suc k) x - g k x\<bar>)"
by (rule sum_abs)
also have "\<dots> \<le> (\<Sum>k = m..<n. c * (2/3)^k / 3)"
by (meson "*" sum_mono x(1))
also have "\<dots> = (c/3) * (\<Sum>k = m..<n. (2/3)^k)"
by (simp add: sum_distrib_left)
also have "\<dots> = (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 "\<dots> < \<epsilon>"
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 \<phi>"
unfolding \<phi>_def using conth by (intro continuous_intros) auto
show "\<phi> x = f x" if "x \<in> S" for x
proof -
have x: "x \<in> 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 (\<lambda>n. g n x) (h x) sequentially"
using h x by (force simp: tendsto_iff eventually_sequentially)
show "limitin Met_TC.mtopology (\<lambda>n. g n x) (f x) sequentially"
proof (clarsimp simp: tendsto_iff)
fix \<epsilon>::real
assume "\<epsilon> > 0"
then have "\<forall>\<^sub>F n in sequentially. \<bar>(2/3) ^ n\<bar> < \<epsilon>/c"
by (intro Archimedean_eventually_pow_inverse) (auto simp: \<open>c > 0\<close>)
then show "\<forall>\<^sub>F n in sequentially. dist (g n x) (f x) < \<epsilon>"
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 "\<phi> ` topspace X \<subseteq> {a..b}"
using fim \<open>a \<le> b\<close> by (auto simp: \<phi>_def)
qed
qed
lemma Tietze_extension_realinterval:
assumes XS: "normal_space X" "closedin X S" and T: "is_interval T" "T \<noteq> {}"
and contf: "continuous_map (subtopology X S) euclideanreal f"
and "f ` S \<subseteq> T"
obtains g where "continuous_map X euclideanreal g" "g ` topspace X \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof -
define \<Phi> where
"\<Phi> \<equiv> \<lambda>T::real set. \<forall>f. continuous_map (subtopology X S) euclidean f \<longrightarrow> f`S \<subseteq> 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 "\<Phi> T"
if *: "\<And>T. \<lbrakk>bounded T; is_interval T; T \<noteq> {}\<rbrakk> \<Longrightarrow> \<Phi> T"
and "is_interval T" "T \<noteq> {}" for T
unfolding \<Phi>_def
proof (intro strip)
fix f
assume contf: "continuous_map (subtopology X S) euclideanreal f"
and "f ` S \<subseteq> T"
have \<Phi>T: "\<Phi> ((\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T)"
proof (rule *)
show "bounded ((\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T)"
using shrink_range [of T] by (force intro: boundedI [where B=1])
show "is_interval ((\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T)"
using connected_shrink that(2) is_interval_connected_1 by blast
show "(\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T \<noteq> {}"
using \<open>T \<noteq> {}\<close> by auto
qed
moreover have "continuous_map (subtopology X S) euclidean ((\<lambda>x. x / (1 + \<bar>x\<bar>)) \<circ> f)"
by (metis contf continuous_map_compose continuous_map_into_fulltopology continuous_map_real_shrink)
moreover have "((\<lambda>x. x / (1 + \<bar>x\<bar>)) \<circ> f) ` S \<subseteq> (\<lambda>x. x / (1 + \<bar>x\<bar>)) ` 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 \<subseteq> (\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T"
and geq: "\<And>x. x \<in> S \<Longrightarrow> g x = ((\<lambda>x. x / (1 + \<bar>x\<bar>)) \<circ> f) x"
using \<Phi>T unfolding \<Phi>_def by force
show "\<exists>g. continuous_map X euclideanreal g \<and> g ` topspace X \<subseteq> T \<and> (\<forall>x\<in>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 ((\<lambda>x. x / (1 - \<bar>x\<bar>)) \<circ> g)"
by (rule continuous_map_compose) (auto simp: continuous_on_real_grow)
show "((\<lambda>x. x / (1 - \<bar>x\<bar>)) \<circ> g) ` topspace X \<subseteq> T"
using gim real_grow_shrink by fastforce
show "\<forall>x\<in>S. ((\<lambda>x. x / (1 - \<bar>x\<bar>)) \<circ> g) x = f x"
using geq real_grow_shrink by force
qed
qed
moreover have "\<Phi> T"
if "bounded T" "is_interval T" "T \<noteq> {}" for T
unfolding \<Phi>_def
proof (intro strip)
fix f
assume contf: "continuous_map (subtopology X S) euclideanreal f"
and "f ` S \<subseteq> 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 \<subseteq> {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: "\<And>x. x \<in> S \<Longrightarrow> g x = f x" and gim: "g ` topspace X \<subseteq> {a..b}"
using Tietze_extension_closed_real_interval [OF XS contf _ \<open>a \<le> b\<close>] by metis
define W where "W \<equiv> {x \<in> topspace X. g x \<in> closure T - T}"
have "{a..b} - {a, b} \<subseteq> 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 \<Rightarrow> real"
where conth: "continuous_map X (top_of_set {0..1}) h"
and him: "h ` W \<subseteq> {0}" "h ` S \<subseteq> {1}"
by (metis XS normal_space_iff_Urysohn)
then have him01: "h ` topspace X \<subseteq> {0..1}"
by (meson continuous_map_in_subtopology)
obtain z where "z \<in> T"
using \<open>T \<noteq> {}\<close> by blast
define g' where "g' \<equiv> \<lambda>x. z + h x * (g x - z)"
show "\<exists>g. continuous_map X euclidean g \<and> g ` topspace X \<subseteq> T \<and> (\<forall>x\<in>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 \<subseteq> T"
unfolding g'_def
proof clarify
fix x
assume "x \<in> topspace X"
show "z + h x * (g x - z) \<in> T"
proof (cases "g x \<in> T")
case True
define w where "w \<equiv> z + h x * (g x - z)"
have "\<bar>h x\<bar> * \<bar>g x - z\<bar> \<le> \<bar>g x - z\<bar>" "\<bar>1 - h x\<bar> * \<bar>g x - z\<bar> \<le> \<bar>g x - z\<bar>"
using him01 \<open>x \<in> topspace X\<close> by (force simp: intro: mult_left_le_one_le)+
then consider "z \<le> w \<and> w \<le> g x" | "g x \<le> w \<and> w \<le> 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 \<in> 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 "\<forall>x\<in>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 \<longleftrightarrow>
(\<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 \<longleftrightarrow> ?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 \<union> T)"
by (simp add: closedin_Un)
moreover
have "continuous_map (subtopology X (S \<union> T)) euclideanreal (\<lambda>x. if x \<in> S then 0 else 1)"
unfolding continuous_map_closedin
proof (intro conjI strip)
fix C :: "real set"
define D where "D \<equiv> {x \<in> topspace X. if x \<in> S then 0 \<in> C else x \<in> T \<and> 1 \<in> C}"
have "D \<in> {{}, S, T, S \<union> 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 \<union> T)) {x \<in> topspace (subtopology X (S \<union> T)). (if x \<in> S then 0::real else 1) \<in> 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 \<Rightarrow> real" where
contg: "continuous_map X euclidean g" and gf: "\<forall>x \<in> S \<union> T. g x = (if x \<in> S then 0 else 1)"
using R by blast
then show "\<exists>f. continuous_map X euclideanreal f \<and> f ` S \<subseteq> {0} \<and> f ` T \<subseteq> {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 \<subseteq> M" and S: "\<forall>K. compactin mtopology K \<longrightarrow> closedin (subtopology mtopology K) (K \<inter> S)"
have "l \<in> S"
if \<sigma>: "range \<sigma> \<subseteq> S" and l: "limitin mtopology \<sigma> l sequentially" for \<sigma> l
proof -
define K where "K \<equiv> insert l (range \<sigma>)"
interpret Submetric M d K
proof
show "K \<subseteq> 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 \<inter> S)"
by (simp add: S mtopology_submetric)
have "\<sigma> n \<in> K \<inter> S" for n
by (simp add: K_def range_subsetD \<sigma>)
moreover have "limitin sub.mtopology \<sigma> l sequentially"
using l
unfolding sub.limit_metric_sequentially limit_metric_sequentially
by (force simp: K_def)
ultimately have "l \<in> K \<inter> 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 "\<And>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 \<subseteq> 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 \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
using assms [of S T] by (meson separatedin_subtopology)
then show "\<exists>U V. openin (subtopology X W) U \<and> openin (subtopology X W) V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> 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: "\<And>U. openin X U \<Longrightarrow> normal_space (subtopology X U)"
shows "\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
proof -
define ST where "ST \<equiv> X closure_of S \<inter> X closure_of T"
have subX: "S \<subseteq> topspace X" "T \<subseteq> topspace X"
by (meson \<open>separatedin X S T\<close> separation_closedin_Un_gen)+
have sub: "S \<subseteq> topspace X - ST" "T \<subseteq> 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 \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> normal_space(subtopology X U))"
by (metis hereditarily_B hereditarily_C hereditarily)
lemma hereditarily_normal_separation:
"hereditarily normal_space X \<longleftrightarrow>
(\<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 \<Longrightarrow> hereditarily normal_space X"
by (simp add: hereditarily metrizable_imp_normal_space metrizable_space_subtopology)
lemma metrizable_space_separation:
"\<lbrakk>metrizable_space X; separatedin X S T\<rbrakk>
\<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 \<longleftrightarrow>
(\<forall>\<U>. finite \<U> \<and> (\<forall>S \<in> \<U>. S \<subseteq> topspace X) \<and> pairwise (separatedin X) \<U>
\<longrightarrow> (\<exists>\<F>. (\<forall>S \<in> \<U>. openin X (\<F> S) \<and> S \<subseteq> \<F> S) \<and>
pairwise (\<lambda>S T. disjnt (\<F> S) (\<F> T)) \<U>))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume L: ?lhs
show ?rhs
proof clarify
fix \<U>
assume "finite \<U>" and \<U>: "\<forall>S\<in>\<U>. S \<subseteq> topspace X"
and pw\<U>: "pairwise (separatedin X) \<U>"
have "\<exists>V W. openin X V \<and> openin X W \<and> S \<subseteq> V \<and>
(\<forall>T. T \<in> \<U> \<and> T \<noteq> S \<longrightarrow> T \<subseteq> W) \<and> disjnt V W"
if "S \<in> \<U>" for S
proof -
have "separatedin X S (\<Union>(\<U> - {S}))"
by (metis \<U> \<open>finite \<U>\<close> pw\<U> 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 *: "\<And>S. S \<in> \<U> \<Longrightarrow> S \<subseteq> \<F> S \<and> (\<forall>T. T \<in> \<U> \<and> T \<noteq> S \<longrightarrow> T \<subseteq> \<G> S)"
and ope: "\<And>S. S \<in> \<U> \<Longrightarrow> openin X (\<F> S) \<and> openin X (\<G> S)"
and dis: "\<And>S. S \<in> \<U> \<Longrightarrow> disjnt (\<F> S) (\<G> S)"
by metis
define \<H> where "\<H> \<equiv> \<lambda>S. \<F> S \<inter> (\<Inter>T \<in> \<U> - {S}. \<G> T)"
show "\<exists>\<F>. (\<forall>S\<in>\<U>. openin X (\<F> S) \<and> S \<subseteq> \<F> S) \<and> pairwise (\<lambda>S T. disjnt (\<F> S) (\<F> T)) \<U>"
proof (intro exI conjI strip)
show "openin X (\<H> S)" if "S \<in> \<U>" for S
unfolding \<H>_def
by (smt (verit) ope that DiffD1 \<open>finite \<U>\<close> finite_Diff finite_imageI imageE openin_Int_Inter)
show "S \<subseteq> \<H> S" if "S \<in> \<U>" for S
unfolding \<H>_def using "*" that by auto
show "pairwise (\<lambda>S T. disjnt (\<H> S) (\<H> T)) \<U>"
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 "\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> 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 "\<forall>S\<in>{S, T}. S \<subseteq> 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:
"\<lbrakk>hereditarily normal_space X; perfect_map X Y f\<rbrakk> \<Longrightarrow> 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 \<and> 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 \<equiv>
\<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: "(\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> 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 \<in> topspace Y" and "x \<notin> S"
then have "closedin X (g`S)"
using hmg homeomorphic_map_closedness_eq by blast
moreover have "g x \<notin> 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}) (\<phi> \<circ> g)"
by (meson continuous_map_compose hmg homeomorphic_imp_continuous_map)
then show "\<exists>\<psi>. continuous_map Y (top_of_set {0..1::real}) \<psi> \<and> \<psi> x = 0 \<and> \<psi> ` S \<subseteq> {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 \<longleftrightarrow> completely_regular_space Y"
by (meson assms homeomorphic_completely_regular_space_aux homeomorphic_space_sym)
lemma completely_regular_space_alt:
"completely_regular_space X \<longleftrightarrow>
(\<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 "\<exists>f. continuous_map X (top_of_set {0..1::real}) f \<and> f x = 0 \<and> f ` S \<subseteq> {1}"
if "closedin X S" "x \<in> topspace X - S" and f: "continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {1}"
for S x f
proof (intro exI conjI)
show "continuous_map X (top_of_set {0..1}) (\<lambda>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 \<longleftrightarrow>
(\<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 \<noteq> b"
shows "completely_regular_space X \<longleftrightarrow>
(\<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 "\<exists>f. continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {1}"
if "closedin X S" "x \<in> topspace X - S"
and f: "continuous_map X euclidean f \<and> f x = a \<and> f ` S \<subseteq> {b}"
for S x f
proof (intro exI conjI)
show "continuous_map X euclideanreal ((\<lambda>x. inverse(b - a) * (x - a)) \<circ> f)"
using that by (intro continuous_intros) auto
qed (use that assms in auto)
moreover
have "\<exists>f. continuous_map X euclidean f \<and> f x = a \<and> f ` S \<subseteq> {b}"
if "closedin X S" "x \<in> topspace X - S"
and f: "continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {1}"
for S x f
proof (intro exI conjI)
show "continuous_map X euclideanreal ((\<lambda>x. a + (b - a) * x) \<circ> 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 \<noteq> b"
shows "completely_regular_space X \<longleftrightarrow>
(\<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 \<longleftrightarrow>
(\<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 "\<exists>f. continuous_map X (top_of_set {a..b}) f \<and> f x = a \<and> f ` S \<subseteq> {b}"
if "closedin X S" "x \<in> topspace X - S"
and f: "continuous_map X euclidean f \<and> f x = a \<and> f ` S \<subseteq> {b}"
for S x f
proof (intro exI conjI)
show "continuous_map X (top_of_set {a..b}) (\<lambda>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 \<notin> S"
assume "x \<in> 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 "\<exists>f. continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {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 \<notin> S" "x \<in> topspace X"
then obtain U C where "openin X U" "closedin X C" "x \<in> U" "U \<subseteq> C" "C \<subseteq> 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 \<and> f ` C \<subseteq> {0} \<and> f ` S \<subseteq> {1}"
using assms unfolding normal_space_iff_Urysohn_alt
by (metis Diff_iff \<open>closedin X S\<close> disjnt_iff subsetD)
then show "\<exists>f. continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {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:
"\<lbrakk>normal_space X; t1_space X \<or> Hausdorff_space X \<or> regular_space X\<rbrakk> \<Longrightarrow> 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:
"\<lbrakk>normal_space X; Hausdorff_space X \<or> regular_space X\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 \<in> topspace (subtopology X S)" and "x \<notin> A"
then obtain T where "closedin X T" "A = S \<inter> T" "x \<in> topspace X" "x \<in> S"
by (force simp: closedin_subtopology_alt image_iff)
then show "\<exists>f. continuous_map (subtopology X S) (top_of_set {0::real..1}) f \<and> f x = 0 \<and> f ` A \<subseteq> {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:
" \<lbrakk>retraction_map X Y r; completely_regular_space X\<rbrakk> \<Longrightarrow> 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 *: "\<exists>U V. openin X U \<and> openin X V \<and> a \<in> U \<and> C \<subseteq> V \<and> disjnt U V"
if contf: "continuous_map X euclideanreal f" and a: "a \<in> topspace X - C" and "closedin X C"
and fim: "f ` topspace X \<subseteq> {0..1}" and f0: "f a = 0" and f1: "f ` C \<subseteq> {1}"
for C a f
proof (intro exI conjI)
show "openin X {x \<in> topspace X. f x \<in> {..<1 / 2}}" "openin X {x \<in> topspace X. f x \<in> {1 / 2<..}}"
using openin_continuous_map_preimage [OF contf]
by (meson open_lessThan open_greaterThan open_openin)+
show "a \<in> {x \<in> topspace X. f x \<in> {..<1 / 2}}"
using a f0 by auto
show "C \<subseteq> {x \<in> topspace X. f x \<in> {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 (meson "*")
qed
lemma locally_compact_regular_imp_completely_regular_space:
assumes "locally_compact_space X" "Hausdorff_space X \<or> regular_space X"
shows "completely_regular_space X"
unfolding completely_regular_space_def
proof clarify
fix S x
assume "closedin X S" and "x \<in> topspace X" and "x \<notin> S"
have "regular_space X"
using assms locally_compact_Hausdorff_imp_regular_space by blast
then have nbase: "neighbourhood_base_of (\<lambda>C. compactin X C \<and> 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 \<in> U" "U \<subseteq> M" "M \<subseteq> 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 \<subseteq> topspace X"
by blast
obtain V K where "openin X V" "closedin X K" "x \<in> V" "V \<subseteq> K" "K \<subseteq> 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\<Rightarrow>real" where contf: "continuous_map (subtopology X M) (top_of_set {0..1}) f"
and f0: "f ` K \<subseteq> {0}" and f1: "f ` (M - U) \<subseteq> {1}"
using Urysohn_lemma [of "subtopology X M" K "M-U" 0 1] by auto
then obtain g::"'a\<Rightarrow>real" where contg: "continuous_map (subtopology X M) euclidean g" and gim: "g ` M \<subseteq> {0..1}"
and g0: "\<And>x. x \<in> K \<Longrightarrow> g x = 0" and g1: "\<And>x. \<lbrakk>x \<in> M; x \<notin> U\<rbrakk> \<Longrightarrow> g x = 1"
using \<open>M \<subseteq> topspace X\<close> by (force simp add: continuous_map_in_subtopology image_subset_iff)
show "\<exists>f::'a\<Rightarrow>real. continuous_map X (top_of_set {0..1}) f \<and> f x = 0 \<and> f ` S \<subseteq> {1}"
proof (intro exI conjI)
show "continuous_map X (top_of_set {0..1}) (\<lambda>x. if x \<in> 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 \<in> topspace X. (if x \<in> M then g x else 1) \<in> C} = {x \<in> M. g x \<in> C} \<union> (if 1 \<in> 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 \<in> topspace X. (if x \<in> M then g x else 1) \<in> 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 \<in> M. g x \<in> C}"
using closedin_continuous_map_preimage_gen [OF contg] \<open>M \<subseteq> topspace X\<close> by auto
then show "closedin X {x \<in> M. g x \<in> 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 \<in> 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 "(\<lambda>x. if x \<in> M then g x else 1) ` S \<subseteq> {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) \<longleftrightarrow>
topspace (prod_topology X Y) = {} \<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 "topspace(prod_topology X Y) = {}")
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) \<in> W"
then obtain U V where "openin X U" "openin Y V" "x \<in> U" "y \<in> V" "U\<times>V \<subseteq> W"
by (force simp: openin_prod_topology_alt)
then have "x \<in> topspace X" "y \<in> topspace Y"
using openin_subset by fastforce+
obtain f where contf: "continuous_map X euclideanreal f" and "f x = 0"
and f1: "\<And>x. x \<in> topspace X \<Longrightarrow> x \<notin> U \<Longrightarrow> 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: "\<And>y. y \<in> topspace Y \<Longrightarrow> y \<notin> V \<Longrightarrow> 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 \<equiv> \<lambda>(x,y). 1 - (1 - f x) * (1 - g y)"
show "\<exists>h. continuous_map (prod_topology X Y) euclideanreal h \<and> h (x,y) = 0 \<and> h ` (topspace (prod_topology X Y) - W) \<subseteq> {1}"
proof (intro exI conjI)
have "continuous_map (prod_topology X Y) euclideanreal (f \<circ> fst)"
using contf continuous_map_of_fst by blast
moreover
have "continuous_map (prod_topology X Y) euclideanreal (g \<circ> 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) \<subseteq> {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
lemma completely_regular_space_product_topology:
"completely_regular_space (product_topology X I) \<longleftrightarrow>
(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {} \<or> (\<forall>i \<in> I. completely_regular_space (X i))"
(is "?lhs \<longleftrightarrow> ?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 "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {}")
case False
show ?thesis
unfolding completely_regular_space_alt'
proof clarify
fix W x
assume W: "openin (product_topology X I) W" and "x \<in> W"
then obtain U where finU: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
and ope: "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (U i)"
and x: "x \<in> Pi\<^sub>E I U" and "Pi\<^sub>E I U \<subseteq> W"
by (auto simp: openin_product_topology_alt)
have "\<forall>i \<in> I. openin (X i) (U i) \<and> x i \<in> 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 "\<And>i. \<exists>f. i \<in> I \<longrightarrow> 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)"
by auto
then obtain f where f: "\<And>i. i \<in> I \<Longrightarrow> continuous_map (X i) euclideanreal (f i) \<and>
f i (x i) = 0 \<and> (\<forall>x \<in> topspace (X i). x \<notin> U i \<longrightarrow> f i x = 1)"
by metis
define h where "h \<equiv> \<lambda>z. 1 - prod (\<lambda>i. 1 - f i (z i)) {i\<in>I. U i \<noteq> topspace(X i)}"
show "\<exists>h. continuous_map (product_topology X I) euclideanreal h \<and> h x = 0 \<and>
h ` (topspace (product_topology X I) - W) \<subseteq> {1}"
proof (intro conjI exI)
have "continuous_map (product_topology X I) euclidean (f i \<circ> (\<lambda>x. x i))" if "i\<in>I" for i
using f that
by (blast intro: continuous_intros continuous_map_product_projection)
then show "continuous_map (product_topology X I) euclideanreal h"
unfolding h_def o_def by (intro continuous_intros) (auto simp: finU)
show "h x = 0"
by (simp add: h_def f)
show "h ` (topspace (product_topology X I) - W) \<subseteq> {1}"
proof -
have "\<exists>i. i \<in> I \<and> U i \<noteq> topspace (X i) \<and> f i (x' i) = 1"
if "x' \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" "x' \<notin> W" for x'
using that \<open>Pi\<^sub>E I U \<subseteq> W\<close> by (smt (verit, best) PiE_iff f in_mono)
then show ?thesis
by (auto simp: f h_def finU)
qed
qed
qed
qed (force simp: completely_regular_space_def)
qed
lemma (in Metric_space) t1_space_mtopology:
"t1_space mtopology"
using Hausdorff_space_mtopology t1_or_Hausdorff_space by blast
subsection\<open>More generally, the k-ification functor\<close>
definition kification_open
where "kification_open \<equiv>
\<lambda>X S. S \<subseteq> topspace X \<and> (\<forall>K. compactin X K \<longrightarrow> openin (subtopology X K) (K \<inter> S))"
definition kification
where "kification X \<equiv> topology (kification_open X)"
lemma istopology_kification_open: "istopology (kification_open X)"
unfolding istopology_def
proof (intro conjI strip)
show "kification_open X (S \<inter> T)"
if "kification_open X S" and "kification_open X T" for S T
using that unfolding kification_open_def
by (smt (verit, best) inf.idem inf_commute inf_left_commute le_infI2 openin_Int)
show "kification_open X (\<Union> \<K>)" if "\<forall>K\<in>\<K>. kification_open X K" for \<K>
using that unfolding kification_open_def Int_Union by blast
qed
lemma openin_kification:
"openin (kification X) U \<longleftrightarrow>
U \<subseteq> topspace X \<and>
(\<forall>K. compactin X K \<longrightarrow> openin (subtopology X K) (K \<inter> U))"
by (metis topology_inverse' kification_def istopology_kification_open kification_open_def)
lemma openin_kification_finer:
"openin X S \<Longrightarrow> openin (kification X) S"
by (simp add: openin_kification openin_subset openin_subtopology_Int2)
lemma topspace_kification [simp]:
"topspace(kification X) = topspace X"
by (meson openin_kification openin_kification_finer openin_topspace subset_antisym)
lemma closedin_kification:
"closedin (kification X) U \<longleftrightarrow>
U \<subseteq> topspace X \<and>
(\<forall>K. compactin X K \<longrightarrow> closedin (subtopology X K) (K \<inter> U))"
proof (cases "U \<subseteq> topspace X")
case True
then show ?thesis
by (simp add: closedin_def Diff_Int_distrib inf_commute le_infI2 openin_kification)
qed (simp add: closedin_def)
lemma closedin_kification_finer: "closedin X S \<Longrightarrow> closedin (kification X) S"
by (simp add: closedin_def openin_kification_finer)
lemma kification_eq_self: "kification X = X \<longleftrightarrow> k_space X"
unfolding fun_eq_iff openin_kification k_space_alt openin_inject [symmetric]
by (metis openin_closedin_eq)
lemma compactin_kification [simp]:
"compactin (kification X) K \<longleftrightarrow> compactin X K" (is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs then show ?rhs
by (simp add: compactin_contractive openin_kification_finer)
next
assume R: ?rhs
show ?lhs
unfolding compactin_def
proof (intro conjI strip)
show "K \<subseteq> topspace (kification X)"
by (simp add: R compactin_subset_topspace)
fix \<U>
assume \<U>: "Ball \<U> (openin (kification X)) \<and> K \<subseteq> \<Union> \<U>"
then have *: "\<And>U. U \<in> \<U> \<Longrightarrow> U \<subseteq> topspace X \<and> openin (subtopology X K) (K \<inter> U)"
by (simp add: R openin_kification)
have "K \<subseteq> topspace X" "compact_space (subtopology X K)"
using R compactin_subspace by force+
then have "\<exists>V. finite V \<and> V \<subseteq> (\<lambda>U. K \<inter> U) ` \<U> \<and> \<Union> V = topspace (subtopology X K)"
unfolding compact_space
by (smt (verit, del_insts) Int_Union \<U> * image_iff inf.order_iff inf_commute topspace_subtopology)
then show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union> \<F>"
by (metis Int_Union \<open>K \<subseteq> topspace X\<close> finite_subset_image inf.orderI topspace_subtopology_subset)
qed
qed
lemma compact_space_kification [simp]:
"compact_space(kification X) \<longleftrightarrow> compact_space X"
by (simp add: compact_space_def)
lemma kification_kification [simp]:
"kification(kification X) = kification X"
unfolding openin_inject [symmetric]
proof
fix U
show "openin (kification (kification X)) U = openin (kification X) U"
proof
show "openin (kification (kification X)) U \<Longrightarrow> openin (kification X) U"
by (metis compactin_kification inf_commute openin_kification openin_subtopology topspace_kification)
qed (simp add: openin_kification_finer)
qed
lemma k_space_kification [iff]: "k_space(kification X)"
using kification_eq_self by fastforce
lemma continuous_map_into_kification:
assumes "k_space X"
shows "continuous_map X (kification Y) f \<longleftrightarrow> continuous_map X Y f" (is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs then show ?rhs
by (simp add: continuous_map_def openin_kification_finer)
next
assume R: ?rhs
have "openin X {x \<in> topspace X. f x \<in> V}" if V: "openin (kification Y) V" for V
proof -
have "openin (subtopology X K) (K \<inter> {x \<in> topspace X. f x \<in> V})"
if "compactin X K" for K
proof -
have "compactin Y (f ` K)"
using R image_compactin that by blast
then have "openin (subtopology Y (f ` K)) (f ` K \<inter> V)"
by (meson V openin_kification)
then obtain U where U: "openin Y U" "f`K \<inter> V = U \<inter> f`K"
by (meson openin_subtopology)
show ?thesis
unfolding openin_subtopology
proof (intro conjI exI)
show "openin X {x \<in> topspace X. f x \<in> U}"
using R U openin_continuous_map_preimage_gen by (simp add: continuous_map_def)
qed (use U in auto)
qed
then show ?thesis
by (metis (full_types) Collect_subset assms k_space_open)
qed
with R show ?lhs
by (simp add: continuous_map_def)
qed
lemma continuous_map_from_kification:
"continuous_map X Y f \<Longrightarrow> continuous_map (kification X) Y f"
by (simp add: continuous_map_openin_preimage_eq openin_kification_finer)
lemma continuous_map_kification:
"continuous_map X Y f \<Longrightarrow> continuous_map (kification X) (kification Y) f"
by (simp add: continuous_map_from_kification continuous_map_into_kification)
lemma subtopology_kification_compact:
assumes "compactin X K"
shows "subtopology (kification X) K = subtopology X K"
unfolding openin_inject [symmetric]
proof
fix U
show "openin (subtopology (kification X) K) U = openin (subtopology X K) U"
by (metis assms inf_commute openin_kification openin_subset openin_subtopology)
qed
lemma subtopology_kification_finer:
assumes "openin (subtopology (kification X) S) U"
shows "openin (kification (subtopology X S)) U"
using assms
by (fastforce simp: openin_subtopology_alt image_iff openin_kification subtopology_subtopology compactin_subtopology)
lemma proper_map_from_kification:
assumes "k_space Y"
shows "proper_map (kification X) Y f \<longleftrightarrow> proper_map X Y f" (is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs then show ?rhs
by (simp add: closed_map_def closedin_kification_finer proper_map_alt)
next
assume R: ?rhs
have "compactin Y K \<Longrightarrow> compactin X {x \<in> topspace X. f x \<in> K}" for K
using R proper_map_alt by auto
with R show ?lhs
by (simp add: assms proper_map_into_k_space_eq subtopology_kification_compact)
qed
lemma perfect_map_from_kification:
"\<lbrakk>k_space Y; perfect_map X Y f\<rbrakk> \<Longrightarrow> perfect_map(kification X) Y f"
by (simp add: continuous_map_from_kification perfect_map_def proper_map_from_kification)
lemma k_space_perfect_map_image_eq:
assumes "Hausdorff_space X" "perfect_map X Y f"
shows "k_space X \<longleftrightarrow> k_space Y"
proof
show "k_space X \<Longrightarrow> k_space Y"
using k_space_perfect_map_image assms by blast
assume "k_space Y"
have "homeomorphic_map (kification X) X id"
unfolding homeomorphic_eq_injective_perfect_map
proof (intro conjI perfect_map_from_composition_right [where f = id])
show "perfect_map (kification X) Y (f \<circ> id)"
by (simp add: \<open>k_space Y\<close> assms(2) perfect_map_from_kification)
show "continuous_map (kification X) X id"
by (simp add: continuous_map_from_kification)
qed (use assms perfect_map_def in auto)
then show "k_space X"
using homeomorphic_k_space homeomorphic_space by blast
qed
subsection\<open>One-point compactifications and the Alexandroff extension construction\<close>
lemma one_point_compactification_dense:
"\<lbrakk>compact_space X; \<not> compactin X (topspace X - {a})\<rbrakk> \<Longrightarrow> X closure_of (topspace X - {a}) = topspace X"
unfolding closure_of_complement
by (metis Diff_empty closedin_compact_space interior_of_eq_empty openin_closedin_eq subset_singletonD)
lemma one_point_compactification_interior:
"\<lbrakk>compact_space X; \<not> compactin X (topspace X - {a})\<rbrakk> \<Longrightarrow> X interior_of {a} = {}"
by (simp add: interior_of_eq_empty_complement one_point_compactification_dense)
lemma kc_space_one_point_compactification_gen:
assumes "compact_space X"
shows "kc_space X \<longleftrightarrow>
openin X (topspace X - {a}) \<and> (\<forall>K. compactin X K \<and> a\<notin>K \<longrightarrow> closedin X K) \<and>
k_space (subtopology X (topspace X - {a})) \<and> kc_space (subtopology X (topspace X - {a}))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume L: ?lhs show ?rhs
proof (intro conjI strip)
show "openin X (topspace X - {a})"
using L kc_imp_t1_space t1_space_openin_delete_alt by auto
then show "k_space (subtopology X (topspace X - {a}))"
by (simp add: L assms k_space_open_subtopology_aux)
show "closedin X k" if "compactin X k \<and> a \<notin> k" for k :: "'a set"
using L kc_space_def that by blast
show "kc_space (subtopology X (topspace X - {a}))"
by (simp add: L kc_space_subtopology)
qed
next
assume R: ?rhs
show ?lhs
unfolding kc_space_def
proof (intro strip)
fix S
assume "compactin X S"
then have "S \<subseteq>topspace X"
by (simp add: compactin_subset_topspace)
show "closedin X S"
proof (cases "a \<in> S")
case True
then have "topspace X - S = topspace X - {a} - (S - {a})"
by auto
moreover have "openin X (topspace X - {a} - (S - {a}))"
proof (rule openin_trans_full)
show "openin (subtopology X (topspace X - {a})) (topspace X - {a} - (S - {a}))"
proof
show "openin (subtopology X (topspace X - {a})) (topspace X - {a})"
using R openin_open_subtopology by blast
have "closedin (subtopology X ((topspace X - {a}) \<inter> K)) (K \<inter> (S - {a}))"
if "compactin X K" "K \<subseteq> topspace X - {a}" for K
proof (intro closedin_subset_topspace)
show "closedin X (K \<inter> (S - {a}))"
using that
by (metis IntD1 Int_insert_right_if0 R True \<open>compactin X S\<close> closed_Int_compactin insert_Diff subset_Diff_insert)
qed (use that in auto)
moreover have "k_space (subtopology X (topspace X - {a}))"
using R by blast
moreover have "S-{a} \<subseteq> topspace X \<and> S-{a} \<subseteq> topspace X - {a}"
using \<open>S \<subseteq> topspace X\<close> by auto
ultimately show "closedin (subtopology X (topspace X - {a})) (S - {a})"
using \<open>S \<subseteq> topspace X\<close> True
by (simp add: k_space_def compactin_subtopology subtopology_subtopology)
qed
show "openin X (topspace X - {a})"
by (simp add: R)
qed
ultimately show ?thesis
by (simp add: \<open>S \<subseteq> topspace X\<close> closedin_def)
next
case False
then show ?thesis
by (simp add: R \<open>compactin X S\<close>)
qed
qed
qed
inductive Alexandroff_open for X where
base: "openin X U \<Longrightarrow> Alexandroff_open X (Some ` U)"
| ext: "\<lbrakk>compactin X C; closedin X C\<rbrakk> \<Longrightarrow> Alexandroff_open X (insert None (Some ` (topspace X - C)))"
hide_fact (open) base ext
lemma Alexandroff_open_iff: "Alexandroff_open X S \<longleftrightarrow>
(\<exists>U. (S = Some ` U \<and> openin X U) \<or> (S = insert None (Some ` (topspace X - U)) \<and> compactin X U \<and> closedin X U))"
by (meson Alexandroff_open.cases Alexandroff_open.ext Alexandroff_open.base)
lemma Alexandroff_open_Un_aux:
assumes U: "openin X U" and "Alexandroff_open X T"
shows "Alexandroff_open X (Some ` U \<union> T)"
using \<open>Alexandroff_open X T\<close>
proof (induction rule: Alexandroff_open.induct)
case (base V)
then show ?case
by (metis Alexandroff_open.base U image_Un openin_Un)
next
case (ext C)
have "U \<subseteq> topspace X"
by (simp add: U openin_subset)
then have eq: "Some ` U \<union> insert None (Some ` (topspace X - C)) = insert None (Some ` (topspace X - (C \<inter> (topspace X - U))))"
by force
have "closedin X (C \<inter> (topspace X - U))"
using U ext.hyps(2) by blast
moreover
have "compactin X (C \<inter> (topspace X - U))"
using U compact_Int_closedin ext.hyps(1) by blast
ultimately show ?case
unfolding eq using Alexandroff_open.ext by blast
qed
lemma Alexandroff_open_Un:
assumes "Alexandroff_open X S" and "Alexandroff_open X T"
shows "Alexandroff_open X (S \<union> T)"
using assms
proof (induction rule: Alexandroff_open.induct)
case (base U)
then show ?case
by (simp add: Alexandroff_open_Un_aux)
next
case (ext C)
then show ?case
by (smt (verit, best) Alexandroff_open_Un_aux Alexandroff_open_iff Un_commute Un_insert_left closedin_def insert_absorb2)
qed
lemma Alexandroff_open_Int_aux:
assumes U: "openin X U" and "Alexandroff_open X T"
shows "Alexandroff_open X (Some ` U \<inter> T)"
using \<open>Alexandroff_open X T\<close>
proof (induction rule: Alexandroff_open.induct)
case (base V)
then show ?case
by (metis Alexandroff_open.base U image_Int inj_Some openin_Int)
next
case (ext C)
have eq: "Some ` U \<inter> insert None (Some ` (topspace X - C)) = Some ` (topspace X - (C \<union> (topspace X - U)))"
by force
have "openin X (topspace X - (C \<union> (topspace X - U)))"
using U ext.hyps(2) by blast
then show ?case
unfolding eq using Alexandroff_open.base by blast
qed
lemma istopology_Alexandroff_open: "istopology (Alexandroff_open X)"
unfolding istopology_def
proof (intro conjI strip)
fix S T
assume "Alexandroff_open X S" and "Alexandroff_open X T"
then show "Alexandroff_open X (S \<inter> T)"
proof (induction rule: Alexandroff_open.induct)
case (base U)
then show ?case
using Alexandroff_open_Int_aux by blast
next
case EC: (ext C)
show ?case
using \<open>Alexandroff_open X T\<close>
proof (induction rule: Alexandroff_open.induct)
case (base V)
then show ?case
by (metis Alexandroff_open.ext Alexandroff_open_Int_aux EC.hyps inf_commute)
next
case (ext D)
have eq: "insert None (Some ` (topspace X - C)) \<inter> insert None (Some ` (topspace X - D))
= insert None (Some ` (topspace X - (C \<union> D)))"
by auto
show ?case
unfolding eq
by (simp add: Alexandroff_open.ext EC.hyps closedin_Un compactin_Un ext.hyps)
qed
qed
next
fix \<K>
assume \<section>: "\<forall>K\<in>\<K>. Alexandroff_open X K"
show "Alexandroff_open X (\<Union>\<K>)"
proof (cases "None \<in> \<Union>\<K>")
case True
have "\<forall>K\<in>\<K>. \<exists>U. (openin X U \<and> K = Some ` U) \<or> (K = insert None (Some ` (topspace X - U)) \<and> compactin X U \<and> closedin X U)"
by (metis \<section> Alexandroff_open_iff)
then obtain U where U:
"\<And>K. K \<in> \<K> \<Longrightarrow> openin X (U K) \<and> K = Some ` (U K)
\<or> (K = insert None (Some ` (topspace X - U K)) \<and> compactin X (U K) \<and> closedin X (U K))"
by metis
define \<K>N where "\<K>N \<equiv> {K \<in> \<K>. None \<in> K}"
define A where "A \<equiv> \<Union>K\<in>\<K>-\<K>N. U K"
define B where "B \<equiv> \<Inter>K\<in>\<K>N. U K"
have U1: "\<And>K. K \<in> \<K>-\<K>N \<Longrightarrow> openin X (U K) \<and> K = Some ` (U K)"
using U \<K>N_def by auto
have U2: "\<And>K. K \<in> \<K>N \<Longrightarrow> K = insert None (Some ` (topspace X - U K)) \<and> compactin X (U K) \<and> closedin X (U K)"
using U \<K>N_def by auto
have eqA: "\<Union>(\<K>-\<K>N) = Some ` A"
proof
show "\<Union> (\<K> - \<K>N) \<subseteq> Some ` A"
by (metis A_def Sup_le_iff U1 UN_upper subset_image_iff)
show "Some ` A \<subseteq> \<Union> (\<K> - \<K>N)"
using A_def U1 by blast
qed
have eqB: "\<Union>\<K>N = insert None (Some ` (topspace X - B))"
using U2 True
by (auto simp: B_def image_iff \<K>N_def)
have "\<Union>\<K> = \<Union>\<K>N \<union> \<Union>(\<K>-\<K>N)"
by (auto simp: \<K>N_def)
then have eq: "\<Union>\<K> = (Some ` A) \<union> (insert None (Some ` (topspace X - B)))"
by (simp add: eqA eqB Un_commute)
show ?thesis
unfolding eq
proof (intro Alexandroff_open_Un Alexandroff_open.intros)
show "openin X A"
using A_def U1 by blast
show "closedin X B"
unfolding B_def using U2 True \<K>N_def by auto
show "compactin X B"
by (metis B_def U2 eqB Inf_lower Union_iff \<open>closedin X B\<close> closed_compactin imageI insertI1)
qed
next
case False
then have "\<forall>K\<in>\<K>. \<exists>U. openin X U \<and> K = Some ` U"
by (metis Alexandroff_open.simps UnionI \<section> insertCI)
then obtain U where U: "\<forall>K\<in>\<K>. openin X (U K) \<and> K = Some ` (U K)"
by metis
then have eq: "\<Union>\<K> = Some ` (\<Union> K\<in>\<K>. U K)"
using image_iff by fastforce
show ?thesis
unfolding eq by (simp add: U Alexandroff_open.base openin_clauses(3))
qed
qed
definition Alexandroff_compactification where
"Alexandroff_compactification X \<equiv> topology (Alexandroff_open X)"
lemma openin_Alexandroff_compactification:
"openin(Alexandroff_compactification X) V \<longleftrightarrow>
(\<exists>U. openin X U \<and> V = Some ` U) \<or>
(\<exists>C. compactin X C \<and> closedin X C \<and> V = insert None (Some ` (topspace X - C)))"
by (auto simp: Alexandroff_compactification_def istopology_Alexandroff_open Alexandroff_open.simps)
lemma topspace_Alexandroff_compactification [simp]:
"topspace(Alexandroff_compactification X) = insert None (Some ` topspace X)"
(is "?lhs = ?rhs")
proof
show "?lhs \<subseteq> ?rhs"
by (force simp add: topspace_def openin_Alexandroff_compactification)
have "None \<in> topspace (Alexandroff_compactification X)"
by (meson closedin_empty compactin_empty insert_subset openin_Alexandroff_compactification openin_subset)
moreover have "Some x \<in> topspace (Alexandroff_compactification X)"
if "x \<in> topspace X" for x
by (meson that imageI openin_Alexandroff_compactification openin_subset openin_topspace subsetD)
ultimately show "?rhs \<subseteq> ?lhs"
by (auto simp: image_subset_iff)
qed
lemma closedin_Alexandroff_compactification:
"closedin (Alexandroff_compactification X) C \<longleftrightarrow>
(\<exists>K. compactin X K \<and> closedin X K \<and> C = Some ` K) \<or>
(\<exists>U. openin X U \<and> C = topspace(Alexandroff_compactification X) - Some ` U)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
show "?lhs \<Longrightarrow> ?rhs"
apply (clarsimp simp: closedin_def openin_Alexandroff_compactification)
by (smt (verit) Diff_Diff_Int None_notin_image_Some image_set_diff inf.absorb_iff2 inj_Some insert_Diff_if subset_insert)
show "?rhs \<Longrightarrow> ?lhs"
using openin_subset
by (fastforce simp: closedin_def openin_Alexandroff_compactification)
qed
lemma openin_Alexandroff_compactification_image_Some [simp]:
"openin(Alexandroff_compactification X) (Some ` U) \<longleftrightarrow> openin X U"
by (auto simp: openin_Alexandroff_compactification inj_image_eq_iff)
lemma closedin_Alexandroff_compactification_image_Some [simp]:
"closedin (Alexandroff_compactification X) (Some ` K) \<longleftrightarrow> compactin X K \<and> closedin X K"
by (auto simp: closedin_Alexandroff_compactification inj_image_eq_iff)
lemma open_map_Some: "open_map X (Alexandroff_compactification X) Some"
using open_map_def openin_Alexandroff_compactification by blast
lemma continuous_map_Some: "continuous_map X (Alexandroff_compactification X) Some"
unfolding continuous_map_def
proof (intro conjI strip)
fix U
assume "openin (Alexandroff_compactification X) U"
then consider V where "openin X V" "U = Some ` V"
| C where "compactin X C" "closedin X C" "U = insert None (Some ` (topspace X - C))"
by (auto simp: openin_Alexandroff_compactification)
then show "openin X {x \<in> topspace X. Some x \<in> U}"
proof cases
case 1
then show ?thesis
using openin_subopen openin_subset by fastforce
next
case 2
then show ?thesis
by (simp add: closedin_def image_iff set_diff_eq)
qed
qed auto
lemma embedding_map_Some: "embedding_map X (Alexandroff_compactification X) Some"
by (simp add: continuous_map_Some injective_open_imp_embedding_map open_map_Some)
lemma compact_space_Alexandroff_compactification [simp]:
"compact_space(Alexandroff_compactification X)"
proof (clarsimp simp: compact_space_alt image_subset_iff)
fix \<U> U
assume ope [rule_format]: "\<forall>U\<in>\<U>. openin (Alexandroff_compactification X) U"
and cover: "\<forall>x\<in>topspace X. \<exists>X\<in>\<U>. Some x \<in> X"
and "U \<in> \<U>" "None \<in> U"
then have Usub: "U \<subseteq> insert None (Some ` topspace X)"
by (metis openin_subset topspace_Alexandroff_compactification)
with ope [OF \<open>U \<in> \<U>\<close>] \<open>None \<in> U\<close>
obtain C where C: "compactin X C \<and> closedin X C \<and>
insert None (Some ` topspace X) - U = Some ` C"
by (auto simp: openin_closedin closedin_Alexandroff_compactification)
then have D: "compactin (Alexandroff_compactification X) (insert None (Some ` topspace X) - U)"
by (metis continuous_map_Some image_compactin)
consider V where "openin X V" "U = Some ` V"
| C where "compactin X C" "closedin X C" "U = insert None (Some ` (topspace X - C))"
using ope [OF \<open>U \<in> \<U>\<close>] by (auto simp: openin_Alexandroff_compactification)
then show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> (\<exists>X\<in>\<F>. None \<in> X) \<and> (\<forall>x\<in>topspace X. \<exists>X\<in>\<F>. Some x \<in> X)"
proof cases
case 1
then show ?thesis
using \<open>None \<in> U\<close> by blast
next
case 2
obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<U>" "insert None (Some ` topspace X) - U \<subseteq> \<Union>\<F>"
by (smt (verit, del_insts) C D Union_iff compactinD compactin_subset_topspace cover image_subset_iff ope subsetD)
with \<open>U \<in> \<U>\<close> show ?thesis
by (rule_tac x="insert U \<F>" in exI) auto
qed
qed
lemma topspace_Alexandroff_compactification_delete:
"topspace(Alexandroff_compactification X) - {None} = Some ` topspace X"
by simp
lemma Alexandroff_compactification_dense:
assumes "\<not> compact_space X"
shows "(Alexandroff_compactification X) closure_of (Some ` topspace X) =
topspace(Alexandroff_compactification X)"
unfolding topspace_Alexandroff_compactification_delete [symmetric]
proof (intro one_point_compactification_dense)
show "\<not> compactin (Alexandroff_compactification X) (topspace (Alexandroff_compactification X) - {None})"
using assms compact_space_proper_map_preimage compact_space_subtopology embedding_map_Some embedding_map_def homeomorphic_imp_proper_map by fastforce
qed auto
lemma t0_space_one_point_compactification:
assumes "compact_space X \<and> openin X (topspace X - {a})"
shows "t0_space X \<longleftrightarrow> t0_space (subtopology X (topspace X - {a}))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
show "?lhs \<Longrightarrow> ?rhs"
using t0_space_subtopology by blast
show "?rhs \<Longrightarrow> ?lhs"
using assms
unfolding t0_space_def by (bestsimp simp flip: Int_Diff dest: openin_trans_full)
qed
lemma t0_space_Alexandroff_compactification [simp]:
"t0_space (Alexandroff_compactification X) \<longleftrightarrow> t0_space X"
using t0_space_one_point_compactification [of "Alexandroff_compactification X" None]
using embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_t0_space by fastforce
lemma t1_space_one_point_compactification:
assumes Xa: "openin X (topspace X - {a})"
and \<section>: "\<And>K. \<lbrakk>compactin (subtopology X (topspace X - {a})) K; closedin (subtopology X (topspace X - {a})) K\<rbrakk> \<Longrightarrow> closedin X K"
shows "t1_space X \<longleftrightarrow> t1_space (subtopology X (topspace X - {a}))" (is "?lhs \<longleftrightarrow> ?rhs")
proof
show "?lhs \<Longrightarrow> ?rhs"
using t1_space_subtopology by blast
assume R: ?rhs
show ?lhs
unfolding t1_space_closedin_singleton
proof (intro strip)
fix x
assume "x \<in> topspace X"
show "closedin X {x}"
proof (cases "x=a")
case True
then show ?thesis
using \<open>x \<in> topspace X\<close> Xa closedin_def by blast
next
case False
show ?thesis
by (simp add: "\<section>" False R \<open>x \<in> topspace X\<close> closedin_t1_singleton)
qed
qed
qed
lemma closedin_Alexandroff_I:
assumes "compactin (Alexandroff_compactification X) K" "K \<subseteq> Some ` topspace X"
"closedin (Alexandroff_compactification X) T" "K = T \<inter> Some ` topspace X"
shows "closedin (Alexandroff_compactification X) K"
proof -
obtain S where S: "S \<subseteq> topspace X" "K = Some ` S"
by (meson \<open>K \<subseteq> Some ` topspace X\<close> subset_imageE)
with assms have "compactin X S"
by (metis compactin_subtopology embedding_map_Some embedding_map_def homeomorphic_map_compactness)
moreover have "closedin X S"
using assms S
by (metis closedin_subtopology embedding_map_Some embedding_map_def homeomorphic_map_closedness)
ultimately show ?thesis
by (simp add: S)
qed
lemma t1_space_Alexandroff_compactification [simp]:
"t1_space(Alexandroff_compactification X) \<longleftrightarrow> t1_space X"
proof -
have "openin (Alexandroff_compactification X) (topspace (Alexandroff_compactification X) - {None})"
by auto
then show ?thesis
using t1_space_one_point_compactification [of "Alexandroff_compactification X" None]
using embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_t1_space
by (fastforce simp add: compactin_subtopology closedin_Alexandroff_I closedin_subtopology)
qed
lemma kc_space_one_point_compactification:
assumes "compact_space X"
and ope: "openin X (topspace X - {a})"
and \<section>: "\<And>K. \<lbrakk>compactin (subtopology X (topspace X - {a})) K; closedin (subtopology X (topspace X - {a})) K\<rbrakk>
\<Longrightarrow> closedin X K"
shows "kc_space X \<longleftrightarrow>
k_space (subtopology X (topspace X - {a})) \<and> kc_space (subtopology X (topspace X - {a}))"
proof -
have "closedin X K"
if "kc_space (subtopology X (topspace X - {a}))" and "compactin X K" "a \<notin> K" for K
using that unfolding kc_space_def
by (metis "\<section>" Diff_empty compactin_subspace compactin_subtopology subset_Diff_insert)
then show ?thesis
by (metis \<open>compact_space X\<close> kc_space_one_point_compactification_gen ope)
qed
lemma kc_space_Alexandroff_compactification:
"kc_space(Alexandroff_compactification X) \<longleftrightarrow> (k_space X \<and> kc_space X)" (is "kc_space ?Y = _")
proof -
have "kc_space (Alexandroff_compactification X) \<longleftrightarrow>
(k_space (subtopology ?Y (topspace ?Y - {None})) \<and> kc_space (subtopology ?Y (topspace ?Y - {None})))"
by (rule kc_space_one_point_compactification) (auto simp: compactin_subtopology closedin_subtopology closedin_Alexandroff_I)
also have "... \<longleftrightarrow> k_space X \<and> kc_space X"
using embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_k_space homeomorphic_kc_space by simp blast
finally show ?thesis .
qed
lemma regular_space_one_point_compactification:
assumes "compact_space X" and ope: "openin X (topspace X - {a})"
and \<section>: "\<And>K. \<lbrakk>compactin (subtopology X (topspace X - {a})) K; closedin (subtopology X (topspace X - {a})) K\<rbrakk> \<Longrightarrow> closedin X K"
shows "regular_space X \<longleftrightarrow>
regular_space (subtopology X (topspace X - {a})) \<and> locally_compact_space (subtopology X (topspace X - {a}))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
show "?lhs \<Longrightarrow> ?rhs"
using assms(1) compact_imp_locally_compact_space locally_compact_space_open_subset ope regular_space_subtopology by blast
assume R: ?rhs
let ?Xa = "subtopology X (topspace X - {a})"
show ?lhs
unfolding neighbourhood_base_of_closedin [symmetric] neighbourhood_base_of imp_conjL
proof (intro strip)
fix W x
assume "openin X W" and "x \<in> W"
show "\<exists>U V. openin X U \<and> closedin X V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
proof (cases "x=a")
case True
have "compactin ?Xa (topspace X - W)"
using \<open>openin X W\<close> assms(1) closedin_compact_space
by (metis Diff_mono True \<open>x \<in> W\<close> compactin_subtopology empty_subsetI insert_subset openin_closedin_eq order_refl)
then obtain V K where V: "openin ?Xa V" and K: "compactin ?Xa K" "closedin ?Xa K" and "topspace X - W \<subseteq> V" "V \<subseteq> K"
by (metis locally_compact_space_compact_closed_compact R)
show ?thesis
proof (intro exI conjI)
show "openin X (topspace X - K)"
using "\<section>" K by blast
show "closedin X (topspace X - V)"
using V ope openin_trans_full by blast
show "x \<in> topspace X - K"
proof (rule)
show "x \<in> topspace X"
using \<open>openin X W\<close> \<open>x \<in> W\<close> openin_subset by blast
show "x \<notin> K"
using K True closedin_imp_subset by blast
qed
show "topspace X - K \<subseteq> topspace X - V"
by (simp add: Diff_mono \<open>V \<subseteq> K\<close>)
show "topspace X - V \<subseteq> W"
using \<open>topspace X - W \<subseteq> V\<close> by auto
qed
next
case False
have "openin ?Xa ((topspace X - {a}) \<inter> W)"
using \<open>openin X W\<close> openin_subtopology_Int2 by blast
moreover have "x \<in> (topspace X - {a}) \<inter> W"
using \<open>openin X W\<close> \<open>x \<in> W\<close> openin_subset False by blast
ultimately obtain U V where "openin ?Xa U" "compactin ?Xa V" "closedin ?Xa V"
"x \<in> U" "U \<subseteq> V" "V \<subseteq> (topspace X - {a}) \<inter> W"
using R locally_compact_regular_space_neighbourhood_base neighbourhood_base_of
by (metis (no_types, lifting))
then show ?thesis
by (meson "\<section>" le_infE ope openin_trans_full)
qed
qed
qed
lemma regular_space_Alexandroff_compactification:
"regular_space(Alexandroff_compactification X) \<longleftrightarrow> regular_space X \<and> locally_compact_space X"
(is "regular_space ?Y = ?rhs")
proof -
have "regular_space ?Y \<longleftrightarrow>
regular_space (subtopology ?Y (topspace ?Y - {None})) \<and> locally_compact_space (subtopology ?Y (topspace ?Y - {None}))"
by (rule regular_space_one_point_compactification) (auto simp: compactin_subtopology closedin_subtopology closedin_Alexandroff_I)
also have "... \<longleftrightarrow> regular_space X \<and> locally_compact_space X"
by (metis embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_locally_compact_space
homeomorphic_regular_space topspace_Alexandroff_compactification_delete)
finally show ?thesis .
qed
lemma Hausdorff_space_one_point_compactification:
assumes "compact_space X" and "openin X (topspace X - {a})"
and "\<And>K. \<lbrakk>compactin (subtopology X (topspace X - {a})) K; closedin (subtopology X (topspace X - {a})) K\<rbrakk> \<Longrightarrow> closedin X K"
shows "Hausdorff_space X \<longleftrightarrow>
Hausdorff_space (subtopology X (topspace X - {a})) \<and> locally_compact_space (subtopology X (topspace X - {a}))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
show ?rhs if ?lhs
proof -
have "locally_compact_space (subtopology X (topspace X - {a}))"
using assms that compact_imp_locally_compact_space locally_compact_space_open_subset
by blast
with that show ?rhs
by (simp add: Hausdorff_space_subtopology)
qed
next
show "?rhs \<Longrightarrow> ?lhs"
by (metis assms locally_compact_Hausdorff_or_regular regular_space_one_point_compactification
regular_t1_eq_Hausdorff_space t1_space_one_point_compactification)
qed
lemma Hausdorff_space_Alexandroff_compactification:
"Hausdorff_space(Alexandroff_compactification X) \<longleftrightarrow> Hausdorff_space X \<and> locally_compact_space X"
by (meson compact_Hausdorff_imp_regular_space compact_space_Alexandroff_compactification
locally_compact_Hausdorff_or_regular regular_space_Alexandroff_compactification
regular_t1_eq_Hausdorff_space t1_space_Alexandroff_compactification)
lemma completely_regular_space_Alexandroff_compactification:
"completely_regular_space(Alexandroff_compactification X) \<longleftrightarrow>
completely_regular_space X \<and> locally_compact_space X"
by (metis regular_space_Alexandroff_compactification completely_regular_eq_regular_space
compact_imp_locally_compact_space compact_space_Alexandroff_compactification)
lemma Hausdorff_space_one_point_compactification_asymmetric_prod:
assumes "compact_space X"
shows "Hausdorff_space X \<longleftrightarrow>
kc_space (prod_topology X (subtopology X (topspace X - {a}))) \<and>
k_space (prod_topology X (subtopology X (topspace X - {a})))" (is "?lhs \<longleftrightarrow> ?rhs")
proof (cases "a \<in> topspace X")
case True
show ?thesis
proof
show ?rhs if ?lhs
proof
show "kc_space (prod_topology X (subtopology X (topspace X - {a})))"
using Hausdorff_imp_kc_space kc_space_prod_topology_right kc_space_subtopology that by blast
show "k_space (prod_topology X (subtopology X (topspace X - {a})))"
by (meson Hausdorff_imp_kc_space assms compact_imp_locally_compact_space k_space_prod_topology_left
kc_space_one_point_compactification_gen that)
qed
next
assume R: ?rhs
define D where "D \<equiv> (\<lambda>x. (x,x)) ` (topspace X - {a})"
show ?lhs
proof (cases "topspace X = {a}")
case True
then show ?thesis
by (simp add: Hausdorff_space_def)
next
case False
then have "kc_space X"
using kc_space_retraction_map_image [of "prod_topology X (subtopology X (topspace X - {a}))" X fst]
by (metis Diff_subset R True insert_Diff retraction_map_fst topspace_subtopology_subset)
have "closedin (subtopology (prod_topology X (subtopology X (topspace X - {a}))) K) (K \<inter> D)"
if "compactin (prod_topology X (subtopology X (topspace X - {a}))) K" for K
proof (intro closedin_subtopology_Int_subset[where V=K] closedin_subset_topspace)
show "fst ` K \<times> snd ` K \<inter> D \<subseteq> fst ` K \<times> snd ` K" "K \<subseteq> fst ` K \<times> snd ` K"
by force+
have eq: "(fst ` K \<times> snd ` K \<inter> D) = ((\<lambda>x. (x,x)) ` (fst ` K \<inter> snd ` K))"
using compactin_subset_topspace that by (force simp: D_def image_iff)
have "compactin (prod_topology X (subtopology X (topspace X - {a}))) (fst ` K \<times> snd ` K \<inter> D)"
unfolding eq
proof (rule image_compactin [of "subtopology X (topspace X - {a})"])
have "compactin X (fst ` K)" "compactin X (snd ` K)"
by (meson compactin_subtopology continuous_map_fst continuous_map_snd image_compactin that)+
moreover have "fst ` K \<inter> snd ` K \<subseteq> topspace X - {a}"
using compactin_subset_topspace that by force
ultimately
show "compactin (subtopology X (topspace X - {a})) (fst ` K \<inter> snd ` K)"
unfolding compactin_subtopology
by (meson \<open>kc_space X\<close> closed_Int_compactin kc_space_def)
show "continuous_map (subtopology X (topspace X - {a})) (prod_topology X (subtopology X (topspace X - {a}))) (\<lambda>x. (x,x))"
by (simp add: continuous_map_paired)
qed
then show "closedin (prod_topology X (subtopology X (topspace X - {a}))) (fst ` K \<times> snd ` K \<inter> D)"
using R compactin_imp_closedin_gen by blast
qed
moreover have "D \<subseteq> topspace X \<times> (topspace X \<inter> (topspace X - {a}))"
by (auto simp: D_def)
ultimately have *: "closedin (prod_topology X (subtopology X (topspace X - {a}))) D"
using R by (auto simp: k_space)
have "x=y"
if "x \<in> topspace X" "y \<in> topspace X"
and \<section>: "\<And>T. \<lbrakk>(x,y) \<in> T; openin (prod_topology X X) T\<rbrakk> \<Longrightarrow> \<exists>z \<in> topspace X. (z,z) \<in> T" for x y
proof (cases "x=a \<and> y=a")
case False
then consider "x\<noteq>a" | "y\<noteq>a"
by blast
then show ?thesis
proof cases
case 1
have "\<exists>z \<in> topspace X - {a}. (z,z) \<in> T"
if "(y,x) \<in> T" "openin (prod_topology X (subtopology X (topspace X - {a}))) T" for T
proof -
have "(x,y) \<in> {z \<in> topspace (prod_topology X X). (snd z,fst z) \<in> T \<inter> topspace X \<times> (topspace X - {a})}"
by (simp add: "1" \<open>x \<in> topspace X\<close> \<open>y \<in> topspace X\<close> that)
moreover have "openin (prod_topology X X) {z \<in> topspace (prod_topology X X). (snd z,fst z) \<in> T \<inter> topspace X \<times> (topspace X - {a})}"
proof (rule openin_continuous_map_preimage)
show "continuous_map (prod_topology X X) (prod_topology X X) (\<lambda>x. (snd x, fst x))"
by (simp add: continuous_map_fst continuous_map_pairedI continuous_map_snd)
have "openin (prod_topology X X) (topspace X \<times> (topspace X - {a}))"
using \<open>kc_space X\<close> assms kc_space_one_point_compactification_gen openin_prod_Times_iff by fastforce
moreover have "openin (prod_topology X X) T"
using kc_space_one_point_compactification_gen [OF \<open>compact_space X\<close>] \<open>kc_space X\<close> that
by (metis openin_prod_Times_iff openin_topspace openin_trans_full prod_topology_subtopology(2))
ultimately show "openin (prod_topology X X) (T \<inter> topspace X \<times> (topspace X - {a}))"
by blast
qed
ultimately show ?thesis
by (smt (verit) \<section> Int_iff fst_conv mem_Collect_eq mem_Sigma_iff snd_conv)
qed
then have "(y,x) \<in> prod_topology X (subtopology X (topspace X - {a})) closure_of D"
by (simp add: "1" D_def in_closure_of that)
then show ?thesis
using that "*" D_def closure_of_closedin by fastforce
next
case 2
have "\<exists>z \<in> topspace X - {a}. (z,z) \<in> T"
if "(x,y) \<in> T" "openin (prod_topology X (subtopology X (topspace X - {a}))) T" for T
proof -
have "openin (prod_topology X X) (topspace X \<times> (topspace X - {a}))"
using \<open>kc_space X\<close> assms kc_space_one_point_compactification_gen openin_prod_Times_iff by fastforce
moreover have XXT: "openin (prod_topology X X) T"
using kc_space_one_point_compactification_gen [OF \<open>compact_space X\<close>] \<open>kc_space X\<close> that
by (metis openin_prod_Times_iff openin_topspace openin_trans_full prod_topology_subtopology(2))
ultimately have "openin (prod_topology X X) (T \<inter> topspace X \<times> (topspace X - {a}))"
by blast
then show ?thesis
by (smt (verit) "\<section>" Diff_subset XXT mem_Sigma_iff openin_subset subsetD that topspace_prod_topology topspace_subtopology_subset)
qed
then have "(x,y) \<in> prod_topology X (subtopology X (topspace X - {a})) closure_of D"
by (simp add: "2" D_def in_closure_of that)
then show ?thesis
using that "*" D_def closure_of_closedin by fastforce
qed
qed auto
then show ?thesis
unfolding Hausdorff_space_closedin_diagonal closure_of_subset_eq [symmetric]
by (force simp add: closure_of_def)
qed
qed
next
case False
then show ?thesis
by (simp add: assms compact_imp_k_space compact_space_prod_topology kc_space_compact_prod_topology)
qed
lemma Hausdorff_space_Alexandroff_compactification_asymmetric_prod:
"Hausdorff_space(Alexandroff_compactification X) \<longleftrightarrow>
kc_space(prod_topology (Alexandroff_compactification X) X) \<and>
k_space(prod_topology (Alexandroff_compactification X) X)"
(is "Hausdorff_space ?Y = ?rhs")
proof -
have *: "subtopology (Alexandroff_compactification X)
(topspace (Alexandroff_compactification X) -
{None}) homeomorphic_space X"
using embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_space_sym by fastforce
have "Hausdorff_space (Alexandroff_compactification X) \<longleftrightarrow>
(kc_space (prod_topology ?Y (subtopology ?Y (topspace ?Y - {None}))) \<and>
k_space (prod_topology ?Y (subtopology ?Y (topspace ?Y - {None}))))"
by (rule Hausdorff_space_one_point_compactification_asymmetric_prod) (auto simp: compactin_subtopology closedin_subtopology closedin_Alexandroff_I)
also have "... \<longleftrightarrow> ?rhs"
using homeomorphic_k_space homeomorphic_kc_space homeomorphic_space_prod_topology
homeomorphic_space_refl * by blast
finally show ?thesis .
qed
lemma kc_space_as_compactification_unique:
assumes "kc_space X" "compact_space X"
shows "openin X U \<longleftrightarrow>
(if a \<in> U then U \<subseteq> topspace X \<and> compactin X (topspace X - U)
else openin (subtopology X (topspace X - {a})) U)"
proof (cases "a \<in> U")
case True
then show ?thesis
by (meson assms closedin_compact_space compactin_imp_closedin_gen openin_closedin_eq)
next
case False
then show ?thesis
by (metis Diff_empty kc_space_one_point_compactification_gen openin_open_subtopology openin_subset subset_Diff_insert assms)
qed
lemma kc_space_as_compactification_unique_explicit:
assumes "kc_space X" "compact_space X"
shows "openin X U \<longleftrightarrow>
(if a \<in> U then U \<subseteq> topspace X \<and>
compactin (subtopology X (topspace X - {a})) (topspace X - U) \<and>
closedin (subtopology X (topspace X - {a})) (topspace X - U)
else openin (subtopology X (topspace X - {a})) U)"
apply (simp add: kc_space_subtopology compactin_imp_closedin_gen assms compactin_subtopology cong: conj_cong)
by (metis Diff_mono assms bot.extremum insert_subset kc_space_as_compactification_unique subset_refl)
lemma Alexandroff_compactification_unique:
assumes "kc_space X" "compact_space X" and a: "a \<in> topspace X"
shows "Alexandroff_compactification (subtopology X (topspace X - {a})) homeomorphic_space X"
(is "?Y homeomorphic_space X")
proof -
have [simp]: "topspace X \<inter> (topspace X - {a}) = topspace X - {a}"
by auto
have [simp]: "insert None (Some ` A) = insert None (Some ` B) \<longleftrightarrow> A = B"
"insert None (Some ` A) \<noteq> Some ` B" for A B
by auto
have "quotient_map X ?Y (\<lambda>x. if x = a then None else Some x)"
unfolding quotient_map_def
proof (intro conjI strip)
show "(\<lambda>x. if x = a then None else Some x) ` topspace X = topspace ?Y"
using \<open>a \<in> topspace X\<close> by force
show "openin X {x \<in> topspace X. (if x = a then None else Some x) \<in> U} = openin ?Y U" (is "?L = ?R")
if "U \<subseteq> topspace ?Y" for U
proof (cases "None \<in> U")
case True
then obtain T where T[simp]: "U = insert None (Some ` T)"
by (metis Int_insert_right UNIV_I UNIV_option_conv inf.orderE inf_le2 subsetI subset_imageE)
have Tsub: "T \<subseteq> topspace X - {a}"
using in_these_eq that by auto
then have "{x \<in> topspace X. (if x = a then None else Some x) \<in> U} = insert a T"
by (auto simp: a image_iff cong: conj_cong)
then have "?L \<longleftrightarrow> openin X (insert a T)"
by metis
also have "\<dots> \<longleftrightarrow> ?R"
using Tsub assms
apply (simp add: openin_Alexandroff_compactification kc_space_as_compactification_unique_explicit [where a=a])
by (smt (verit, best) Diff_insert2 Diff_subset closedin_imp_subset double_diff)
finally show ?thesis .
next
case False
then obtain T where [simp]: "U = Some ` T"
by (metis Int_insert_right UNIV_I UNIV_option_conv inf.orderE inf_le2 subsetI subset_imageE)
have **: "\<And>V. openin X V \<Longrightarrow> openin X (V - {a})"
by (simp add: assms compactin_imp_closedin_gen openin_diff)
have Tsub: "T \<subseteq> topspace X - {a}"
using in_these_eq that by auto
then have "{x \<in> topspace X. (if x = a then None else Some x) \<in> U} = T"
by (auto simp: image_iff cong: conj_cong)
then show ?thesis
by (simp add: "**" Tsub openin_open_subtopology)
qed
qed
moreover have "inj_on (\<lambda>x. if x = a then None else Some x) (topspace X)"
by (auto simp: inj_on_def)
ultimately show ?thesis
using homeomorphic_space_sym homeomorphic_space homeomorphic_map_def by blast
qed
end