--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy Wed Jul 05 15:01:46 2023 +0200
@@ -1438,7 +1438,7 @@
have "topspace Y = topspace X"
by (auto simp: Y_def)
have "openin X T \<longrightarrow> openin Y T" for T
- by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase openin_subset relative_to_subset)
+ by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase openin_subset relative_to_subset_inc)
have "compact_space Y"
proof (rule Alexander_subbase_alt)
show "\<exists>\<F>'. finite \<F>' \<and> \<F>' \<subseteq> \<C> \<and> topspace X \<subseteq> \<Union> \<F>'"
@@ -1465,7 +1465,7 @@
have "Y = X"
using R \<open>\<And>S. openin X S \<longrightarrow> openin Y S\<close> \<open>compact_space Y\<close> \<open>topspace Y = topspace X\<close> by blast
moreover have "openin Y (topspace X - S)"
- by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase relative_to_subset)
+ by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase relative_to_subset_inc)
ultimately show "closedin X S"
unfolding closedin_def using S compactin_subset_topspace by blast
qed
@@ -2580,7 +2580,6 @@
qed
-
subsection\<open>Locally compact spaces\<close>
definition locally_compact_space
@@ -3897,6 +3896,9 @@
by (metis Diff_disjoint Diff_iff Un_Diff_cancel closedin_def disjnt_def inf_commute sup.orderE sup_commute)
qed
+lemma quasi_components_lepoll_topspace: "quasi_components_of X \<lesssim> topspace X"
+ by (simp add: image_lepoll quasi_components_of_def)
+
lemma quasi_component_of_separated:
"quasi_component_of X x y \<longleftrightarrow>
x \<in> topspace X \<and> y \<in> topspace X \<and>
--- a/src/HOL/Analysis/Abstract_Topology.thy Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Wed Jul 05 15:01:46 2023 +0200
@@ -4490,7 +4490,7 @@
next
case (Basis s)
then show ?case
- by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
+ by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset_inc)
qed auto
next
fix A
--- a/src/HOL/Analysis/Abstract_Topology_2.thy Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Wed Jul 05 15:01:46 2023 +0200
@@ -8,9 +8,9 @@
theory Abstract_Topology_2
imports
- Elementary_Topology
- Abstract_Topology
+ Elementary_Topology Abstract_Topology
"HOL-Library.Indicator_Function"
+ "HOL-Library.Equipollence"
begin
text \<open>Combination of Elementary and Abstract Topology\<close>
@@ -1695,4 +1695,30 @@
by (metis continuous_on_subset continuous_shrink subset_UNIV)
qed
+lemma card_eq_real_subset:
+ fixes a b::real
+ assumes "a < b" and S: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> x \<in> S"
+ shows "S \<approx> (UNIV::real set)"
+proof (rule lepoll_antisym)
+ show "S \<lesssim> (UNIV::real set)"
+ by (simp add: subset_imp_lepoll)
+ define f where "f \<equiv> \<lambda>x. (a+b) / 2 + (b-a) / 2 * (x / (1 + \<bar>x\<bar>))"
+ show "(UNIV::real set) \<lesssim> S"
+ unfolding lepoll_def
+ proof (intro exI conjI)
+ show "inj f"
+ unfolding inj_on_def f_def
+ by (smt (verit, ccfv_SIG) real_shrink_eq \<open>a<b\<close> divide_eq_0_iff mult_cancel_left times_divide_eq_right)
+ have pos: "(b-a) / 2 > 0"
+ using \<open>a<b\<close> by auto
+ have *: "a < (a + b) / 2 + (b - a) / 2 * x \<longleftrightarrow> (b - a) > (b - a) * -x"
+ "(a + b) / 2 + (b - a) / 2 * x < b \<longleftrightarrow> (b - a) * x < (b - a)" for x
+ by (auto simp: field_simps)
+ show "range f \<subseteq> S"
+ using shrink_range [of UNIV] \<open>a < b\<close>
+ unfolding subset_iff f_def greaterThanLessThan_iff image_iff
+ by (smt (verit, best) S * mult_less_cancel_left2 mult_minus_right)
+ qed
+qed
+
end
\ No newline at end of file
--- a/src/HOL/Analysis/FSigma.thy Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/FSigma.thy Wed Jul 05 15:01:46 2023 +0200
@@ -27,7 +27,7 @@
by (simp add: countable_intersection_of_inc)
then show ?thesis
unfolding gdelta_in_def
- by (metis countable_intersection_of_inter relative_to_def relative_to_imp_subset relative_to_subset)
+ by (metis countable_intersection_of_inter relative_to_def relative_to_imp_subset relative_to_subset_inc)
qed
lemma fsigma_in_subset: "fsigma_in X S \<Longrightarrow> S \<subseteq> topspace X"
--- a/src/HOL/Analysis/Locally.thy Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/Locally.thy Wed Jul 05 15:01:46 2023 +0200
@@ -968,5 +968,191 @@
qed
qed
+subsection \<open>Dimension of a topological space\<close>
+
+text\<open>Basic definition of the small inductive dimension relation. Works in any topological space.\<close>
+
+inductive dimension_le :: "['a topology, int] \<Rightarrow> bool" (infix "dim'_le" 50)
+ where "\<lbrakk>-1 \<le> n;
+ \<And>V a. \<lbrakk>openin X V; a \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and> (subtopology X (X frontier_of U)) dim_le (n-1)\<rbrakk>
+ \<Longrightarrow> X dim_le (n::int)"
+
+lemma dimension_le_neighbourhood_base:
+ "X dim_le n \<longleftrightarrow>
+ -1 \<le> n \<and> neighbourhood_base_of (\<lambda>U. openin X U \<and> (subtopology X (X frontier_of U)) dim_le (n-1)) X"
+ by (smt (verit, best) dimension_le.simps open_neighbourhood_base_of)
+
+lemma dimension_le_bound: "X dim_le n \<Longrightarrow>-1 \<le> n"
+ using dimension_le.simps by blast
+
+lemma dimension_le_mono [rule_format]:
+ assumes "X dim_le m"
+ shows "m \<le> n \<longrightarrow> X dim_le n"
+ using assms
+proof (induction arbitrary: n rule: dimension_le.induct)
+ case (1 m X)
+ show ?case
+ proof (intro strip dimension_le.intros)
+ show "-1 \<le> n" if "m \<le> n" for n :: int using that using "1.hyps" by fastforce
+ show "\<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and> subtopology X (X frontier_of U) dim_le n-1"
+ if "m \<le> n" and "openin X V" and "a \<in> V" for n V a
+ using that by (meson "1.IH" diff_right_mono)
+ qed
+qed
+
+lemma dimension_le_eq_empty:
+ "X dim_le -1 \<longleftrightarrow> topspace X = {}"
+proof
+ assume "X dim_le (-1)"
+ then show "topspace X = {}"
+ by (smt (verit, ccfv_threshold) Diff_empty Diff_eq_empty_iff dimension_le.cases openin_topspace subset_eq)
+next
+ assume "topspace X = {}"
+ then show "X dim_le (-1)"
+ using dimension_le.simps openin_subset by fastforce
+qed
+
+lemma dimension_le_0_neighbourhood_base_of_clopen:
+ "X dim_le 0 \<longleftrightarrow> neighbourhood_base_of (\<lambda>U. closedin X U \<and> openin X U) X"
+proof -
+ have "(subtopology X (X frontier_of U) dim_le -1) =
+ closedin X U" if "openin X U" for U
+ by (metis dimension_le_eq_empty frontier_of_eq_empty frontier_of_subset_topspace openin_subset that topspace_subtopology_subset)
+ then show ?thesis
+ by (smt (verit, del_insts) dimension_le.simps open_neighbourhood_base_of)
+qed
+
+lemma dimension_le_subtopology:
+ "X dim_le n \<Longrightarrow> subtopology X S dim_le n"
+proof (induction arbitrary: S rule: dimension_le.induct)
+ case (1 n X)
+ show ?case
+ proof (intro dimension_le.intros)
+ show "- 1 \<le> n"
+ by (simp add: "1.hyps")
+ fix U' a
+ assume U': "openin (subtopology X S) U'" and "a \<in> U'"
+ then obtain U where U: "openin X U" "U' = U \<inter> S"
+ by (meson openin_subtopology)
+ then obtain V where "a \<in> V" "V \<subseteq> U" "openin X V"
+ and subV: "subtopology X (X frontier_of V) dim_le n-1"
+ and dimV: "\<And>T. subtopology X (X frontier_of V \<inter> T) dim_le n-1"
+ by (metis "1.IH" Int_iff \<open>a \<in> U'\<close> subtopology_subtopology)
+ show "\<exists>W. a \<in> W \<and> W \<subseteq> U' \<and> openin (subtopology X S) W \<and> subtopology (subtopology X S) (subtopology X S frontier_of W) dim_le n-1"
+ proof (intro exI conjI)
+ show "a \<in> S \<inter> V" "S \<inter> V \<subseteq> U'"
+ using \<open>U' = U \<inter> S\<close> \<open>a \<in> U'\<close> \<open>a \<in> V\<close> \<open>V \<subseteq> U\<close> by blast+
+ show "openin (subtopology X S) (S \<inter> V)"
+ by (simp add: \<open>openin X V\<close> openin_subtopology_Int2)
+ have "S \<inter> subtopology X S frontier_of V \<subseteq> X frontier_of V"
+ by (simp add: frontier_of_subtopology_subset)
+ then show "subtopology (subtopology X S) (subtopology X S frontier_of (S \<inter> V)) dim_le n-1"
+ by (metis dimV frontier_of_restrict inf.absorb_iff2 inf_left_idem subtopology_subtopology topspace_subtopology)
+ qed
+ qed
+qed
+
+lemma dimension_le_subtopologies:
+ "\<lbrakk>subtopology X T dim_le n; S \<subseteq> T\<rbrakk> \<Longrightarrow> (subtopology X S) dim_le n"
+ by (metis dimension_le_subtopology inf.absorb_iff2 subtopology_subtopology)
+
+lemma dimension_le_eq_subtopology:
+ "(subtopology X S) dim_le n \<longleftrightarrow>
+ -1 \<le> n \<and>
+ (\<forall>V a. openin X V \<and> a \<in> V \<and> a \<in> S
+ \<longrightarrow> (\<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and>
+ subtopology X (subtopology X S frontier_of (S \<inter> U)) dim_le (n-1)))"
+proof -
+ have *: "(\<exists>T. a \<in> T \<and> T \<inter> S \<subseteq> V \<inter> S \<and> openin X T \<and> subtopology X (S \<inter> (subtopology X S frontier_of (T \<inter> S))) dim_le n-1)
+ \<longleftrightarrow> (\<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and> subtopology X (subtopology X S frontier_of (S \<inter> U)) dim_le n-1)"
+ if "a \<in> V" "a \<in> S" "openin X V" for a V
+ proof -
+ have "\<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and> subtopology X (subtopology X S frontier_of (S \<inter> U)) dim_le n-1"
+ if "a \<in> T" and sub: "T \<inter> S \<subseteq> V \<inter> S" and "openin X T"
+ and dim: "subtopology X (S \<inter> subtopology X S frontier_of (T \<inter> S)) dim_le n-1"
+ for T
+ proof (intro exI conjI)
+ show "openin X (T \<inter> V)"
+ using \<open>openin X V\<close> \<open>openin X T\<close> by blast
+ show "subtopology X (subtopology X S frontier_of (S \<inter> (T \<inter> V))) dim_le n-1"
+ by (metis dim frontier_of_subset_subtopology inf.boundedE inf_absorb2 inf_assoc inf_commute sub)
+ qed (use \<open>a \<in> V\<close> \<open>a \<in> T\<close> in auto)
+ moreover have "\<exists>T. a \<in> T \<and> T \<inter> S \<subseteq> V \<inter> S \<and> openin X T \<and> subtopology X (S \<inter> subtopology X S frontier_of (T \<inter> S)) dim_le n-1"
+ if "a \<in> U" and "U \<subseteq> V" and "openin X U"
+ and dim: "subtopology X (subtopology X S frontier_of (S \<inter> U)) dim_le n-1"
+ for U
+ by (metis that frontier_of_subset_subtopology inf_absorb2 inf_commute inf_le1 le_inf_iff)
+ ultimately show ?thesis
+ by safe
+ qed
+ show ?thesis
+ apply (simp add: dimension_le.simps [of _ n] subtopology_subtopology openin_subtopology flip: *)
+ by (safe; metis Int_iff inf_le2 le_inf_iff)
+qed
+
+
+lemma homeomorphic_space_dimension_le_aux:
+ assumes "X homeomorphic_space Y" "X dim_le of_nat n - 1"
+ shows "Y dim_le of_nat n - 1"
+ using assms
+proof (induction n arbitrary: X Y)
+ case 0
+ then show ?case
+ by (simp add: dimension_le_eq_empty homeomorphic_empty_space)
+next
+ case (Suc n)
+ then have X_dim_n: "X dim_le n"
+ by simp
+ show ?case
+ proof (clarsimp simp add: dimension_le.simps [of Y n])
+ fix V b
+ assume "openin Y V" and "b \<in> V"
+ obtain f g where fg: "homeomorphic_maps X Y f g"
+ using \<open>X homeomorphic_space Y\<close> homeomorphic_space_def by blast
+ then have "openin X (g ` V)"
+ using \<open>openin Y V\<close> homeomorphic_map_openness_eq homeomorphic_maps_map by blast
+ then obtain U where "g b \<in> U" "openin X U" and gim: "U \<subseteq> g ` V" and sub: "subtopology X (X frontier_of U) dim_le int n - int 1"
+ using X_dim_n unfolding dimension_le.simps [of X n] by (metis \<open>b \<in> V\<close> imageI of_nat_eq_1_iff)
+ show "\<exists>U. b \<in> U \<and> U \<subseteq> V \<and> openin Y U \<and> subtopology Y (Y frontier_of U) dim_le int n - 1"
+ proof (intro conjI exI)
+ show "b \<in> f ` U"
+ by (metis (no_types, lifting) \<open>b \<in> V\<close> \<open>g b \<in> U\<close> \<open>openin Y V\<close> fg homeomorphic_maps_map image_iff openin_subset subsetD)
+ show "f ` U \<subseteq> V"
+ by (smt (verit, ccfv_threshold) \<open>openin Y V\<close> fg gim homeomorphic_maps_map image_iff openin_subset subset_iff)
+ show "openin Y (f ` U)"
+ using \<open>openin X U\<close> fg homeomorphic_map_openness_eq homeomorphic_maps_map by blast
+ show "subtopology Y (Y frontier_of f ` U) dim_le int n-1"
+ proof (rule Suc.IH)
+ have "homeomorphic_maps (subtopology X (X frontier_of U)) (subtopology Y (Y frontier_of f ` U)) f g"
+ using \<open>openin X U\<close> fg
+ by (metis frontier_of_subset_topspace homeomorphic_map_frontier_of homeomorphic_maps_map homeomorphic_maps_subtopologies openin_subset topspace_subtopology topspace_subtopology_subset)
+ then show "subtopology X (X frontier_of U) homeomorphic_space subtopology Y (Y frontier_of f ` U)"
+ using homeomorphic_space_def by blast
+ show "subtopology X (X frontier_of U) dim_le int n-1"
+ using sub by fastforce
+ qed
+ qed
+ qed
+qed
+
+lemma homeomorphic_space_dimension_le:
+ assumes "X homeomorphic_space Y"
+ shows "X dim_le n \<longleftrightarrow> Y dim_le n"
+proof (cases "n \<ge> -1")
+ case True
+ then show ?thesis
+ using homeomorphic_space_dimension_le_aux [of _ _ "nat(n+1)"] by (smt (verit) assms homeomorphic_space_sym nat_eq_iff)
+next
+ case False
+ then show ?thesis
+ by (metis dimension_le_bound)
+qed
+
+lemma dimension_le_retraction_map_image:
+ "\<lbrakk>retraction_map X Y r; X dim_le n\<rbrakk> \<Longrightarrow> Y dim_le n"
+ by (meson dimension_le_subtopology homeomorphic_space_dimension_le retraction_map_def retraction_maps_section_image2)
+
+lemma dimension_le_discrete_topology [simp]: "(discrete_topology U) dim_le 0"
+ using dimension_le.simps dimension_le_eq_empty by fastforce
end
--- a/src/HOL/Analysis/Urysohn.thy Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/Urysohn.thy Wed Jul 05 15:01:46 2023 +0200
@@ -1263,6 +1263,27 @@
qed
+lemma zero_dimensional_imp_completely_regular_space:
+ assumes "X dim_le 0"
+ shows "completely_regular_space X"
+proof (clarsimp simp: completely_regular_space_def)
+ fix C a
+ assume "closedin X C" and "a \<in> topspace X" and "a \<notin> C"
+ then obtain U where "closedin X U" "openin X U" "a \<in> U" and U: "U \<subseteq> topspace X - C"
+ using assms by (force simp add: closedin_def dimension_le_0_neighbourhood_base_of_clopen open_neighbourhood_base_of)
+ show "\<exists>f. continuous_map X (top_of_set {0::real..1}) f \<and> f a = 0 \<and> f ` C \<subseteq> {1}"
+ proof (intro exI conjI)
+ have "continuous_map X euclideanreal (\<lambda>x. if x \<in> U then 0 else 1)"
+ using \<open>closedin X U\<close> \<open>openin X U\<close> apply (clarsimp simp: continuous_map_def closedin_def)
+ by (smt (verit) Diff_iff mem_Collect_eq openin_subopen subset_eq)
+ then show "continuous_map X (top_of_set {0::real..1}) (\<lambda>x. if x \<in> U then 0 else 1)"
+ by (auto simp: continuous_map_in_subtopology)
+ qed (use U \<open>a \<in> U\<close> in auto)
+qed
+
+lemma zero_dimensional_imp_regular_space: "X dim_le 0 \<Longrightarrow> regular_space X"
+ by (simp add: completely_regular_imp_regular_space zero_dimensional_imp_completely_regular_space)
+
lemma (in Metric_space) t1_space_mtopology:
"t1_space mtopology"
using Hausdorff_space_mtopology t1_or_Hausdorff_space by blast
@@ -4301,4 +4322,864 @@
qed
qed
+subsection\<open>Size bounds on connected or path-connected spaces\<close>
+
+lemma connected_space_imp_card_ge_alt:
+ assumes "connected_space X" "completely_regular_space X" "closedin X S" "S \<noteq> {}" "S \<noteq> topspace X"
+ shows "(UNIV::real set) \<lesssim> topspace X"
+proof -
+ have "S \<subseteq> topspace X"
+ using \<open>closedin X S\<close> closedin_subset by blast
+ then obtain a where "a \<in> topspace X" "a \<notin> S"
+ using \<open>S \<noteq> topspace X\<close> by blast
+ have "(UNIV::real set) \<lesssim> {0..1::real}"
+ using card_eq_real_subset
+ by (meson atLeastAtMost_iff eqpoll_imp_lepoll eqpoll_sym less_eq_real_def zero_less_one)
+ also have "\<dots> \<lesssim> topspace X"
+ proof -
+ obtain f where contf: "continuous_map X euclidean f"
+ and fim: "f \<in> (topspace X) \<rightarrow> {0..1::real}"
+ and f0: "f a = 0" and f1: "f ` S \<subseteq> {1}"
+ using \<open>completely_regular_space X\<close>
+ unfolding completely_regular_space_def
+ by (metis Diff_iff \<open>a \<in> topspace X\<close> \<open>a \<notin> S\<close> \<open>closedin X S\<close> continuous_map_in_subtopology image_subset_iff_funcset)
+ have "\<exists>y\<in>topspace X. x = f y" if "0 \<le> x" and "x \<le> 1" for x
+ proof -
+ have "connectedin euclidean (f ` topspace X)"
+ using \<open>connected_space X\<close> connectedin_continuous_map_image connectedin_topspace contf by blast
+ moreover have "\<exists>y. 0 = f y \<and> y \<in> topspace X"
+ using \<open>a \<in> topspace X\<close> f0 by auto
+ moreover have "\<exists>y. 1 = f y \<and> y \<in> topspace X"
+ using \<open>S \<subseteq> topspace X\<close> \<open>S \<noteq> {}\<close> f1 by fastforce
+ ultimately show ?thesis
+ using that by (fastforce simp: is_interval_1 simp flip: is_interval_connected_1)
+ qed
+ then show ?thesis
+ unfolding lepoll_iff using atLeastAtMost_iff by blast
+ qed
+ finally show ?thesis .
+qed
+
+
+lemma connected_space_imp_card_ge_gen:
+ assumes "connected_space X" "normal_space X" "closedin X S" "closedin X T" "S \<noteq> {}" "T \<noteq> {}" "disjnt S T"
+ shows "(UNIV::real set) \<lesssim> topspace X"
+proof -
+ have "(UNIV::real set) \<lesssim> {0..1::real}"
+ by (metis atLeastAtMost_iff card_eq_real_subset eqpoll_imp_lepoll eqpoll_sym less_le_not_le zero_less_one)
+ also have "\<dots>\<lesssim> topspace X"
+ proof -
+ obtain f where contf: "continuous_map X euclidean f"
+ and fim: "f \<in> (topspace X) \<rightarrow> {0..1::real}"
+ and f0: "f ` S \<subseteq> {0}" and f1: "f ` T \<subseteq> {1}"
+ using assms by (metis continuous_map_in_subtopology normal_space_iff_Urysohn image_subset_iff_funcset)
+ have "\<exists>y\<in>topspace X. x = f y" if "0 \<le> x" and "x \<le> 1" for x
+ proof -
+ have "connectedin euclidean (f ` topspace X)"
+ using \<open>connected_space X\<close> connectedin_continuous_map_image connectedin_topspace contf by blast
+ moreover have "\<exists>y. 0 = f y \<and> y \<in> topspace X"
+ using \<open>closedin X S\<close> \<open>S \<noteq> {}\<close> closedin_subset f0 by fastforce
+ moreover have "\<exists>y. 1 = f y \<and> y \<in> topspace X"
+ using \<open>closedin X T\<close> \<open>T \<noteq> {}\<close> closedin_subset f1 by fastforce
+ ultimately show ?thesis
+ using that by (fastforce simp: is_interval_1 simp flip: is_interval_connected_1)
+ qed
+ then show ?thesis
+ unfolding lepoll_iff using atLeastAtMost_iff by blast
+ qed
+ finally show ?thesis .
+qed
+
+lemma connected_space_imp_card_ge:
+ assumes "connected_space X" "normal_space X" "t1_space X" and nosing: "\<not> (\<exists>a. topspace X \<subseteq> {a})"
+ shows "(UNIV::real set) \<lesssim> topspace X"
+proof -
+ obtain a b where "a \<in> topspace X" "b \<in> topspace X" "a \<noteq> b"
+ by (metis nosing singletonI subset_iff)
+ then have "{a} \<noteq> topspace X"
+ by force
+ with connected_space_imp_card_ge_alt assms show ?thesis
+ by (metis \<open>a \<in> topspace X\<close> closedin_t1_singleton insert_not_empty normal_imp_completely_regular_space_A)
+qed
+
+lemma connected_space_imp_infinite_gen:
+ "\<lbrakk>connected_space X; t1_space X; \<nexists>a. topspace X \<subseteq> {a}\<rbrakk> \<Longrightarrow> infinite(topspace X)"
+ by (metis connected_space_discrete_topology finite_t1_space_imp_discrete_topology)
+
+lemma connected_space_imp_infinite:
+ "\<lbrakk>connected_space X; Hausdorff_space X; \<nexists>a. topspace X \<subseteq> {a}\<rbrakk> \<Longrightarrow> infinite(topspace X)"
+ by (simp add: Hausdorff_imp_t1_space connected_space_imp_infinite_gen)
+
+lemma connected_space_imp_infinite_alt:
+ assumes "connected_space X" "regular_space X" "closedin X S" "S \<noteq> {}" "S \<noteq> topspace X"
+ shows "infinite(topspace X)"
+proof -
+ have "S \<subseteq> topspace X"
+ using \<open>closedin X S\<close> closedin_subset by blast
+ then obtain a where a: "a \<in> topspace X" "a \<notin> S"
+ using \<open>S \<noteq> topspace X\<close> by blast
+ have "\<exists>\<Phi>. \<forall>n. (disjnt (\<Phi> n) S \<and> a \<in> \<Phi> n \<and> openin X (\<Phi> n)) \<and> \<Phi>(Suc n) \<subset> \<Phi> n"
+ proof (rule dependent_nat_choice)
+ show "\<exists>T. disjnt T S \<and> a \<in> T \<and> openin X T"
+ by (metis Diff_iff a \<open>closedin X S\<close> closedin_def disjnt_iff)
+ fix V n
+ assume \<section>: "disjnt V S \<and> a \<in> V \<and> openin X V"
+ then obtain U C where U: "openin X U" "closedin X C" "a \<in> U" "U \<subseteq> C" "C \<subseteq> V"
+ using \<open>regular_space X\<close> by (metis neighbourhood_base_of neighbourhood_base_of_closedin)
+ with assms have "U \<subset> V"
+ by (metis "\<section>" \<open>S \<subseteq> topspace X\<close> connected_space_clopen_in disjnt_def empty_iff inf.absorb_iff2 inf.orderE psubsetI subset_trans)
+ with U show "\<exists>U. (disjnt U S \<and> a \<in> U \<and> openin X U) \<and> U \<subset> V"
+ using "\<section>" disjnt_subset1 by blast
+ qed
+ then obtain \<Phi> where \<Phi>: "\<And>n. disjnt (\<Phi> n) S \<and> a \<in> \<Phi> n \<and> openin X (\<Phi> n)"
+ and \<Phi>sub: "\<And>n. \<Phi> (Suc n) \<subset> \<Phi> n" by metis
+ then have "decseq \<Phi>"
+ by (simp add: decseq_SucI psubset_eq)
+ have "\<forall>n. \<exists>x. x \<in> \<Phi> n \<and> x \<notin> \<Phi>(Suc n)"
+ by (meson \<Phi>sub psubsetE subsetI)
+ then obtain f where fin: "\<And>n. f n \<in> \<Phi> n" and fout: "\<And>n. f n \<notin> \<Phi>(Suc n)"
+ by metis
+ have "range f \<subseteq> topspace X"
+ by (meson \<Phi> fin image_subset_iff openin_subset subset_iff)
+ moreover have "inj f"
+ by (metis Suc_le_eq \<open>decseq \<Phi>\<close> decseq_def fin fout linorder_injI subsetD)
+ ultimately show ?thesis
+ using infinite_iff_countable_subset by blast
+qed
+
+lemma path_connected_space_imp_card_ge:
+ assumes "path_connected_space X" "Hausdorff_space X" and nosing: "\<not> (\<exists>x. topspace X \<subseteq> {x})"
+ shows "(UNIV::real set) \<lesssim> topspace X"
+proof -
+ obtain a b where "a \<in> topspace X" "b \<in> topspace X" "a \<noteq> b"
+ by (metis nosing singletonI subset_iff)
+ then obtain \<gamma> where \<gamma>: "pathin X \<gamma>" "\<gamma> 0 = a" "\<gamma> 1 = b"
+ by (meson \<open>a \<in> topspace X\<close> \<open>b \<in> topspace X\<close> \<open>path_connected_space X\<close> path_connected_space_def)
+ let ?Y = "subtopology X (\<gamma> ` (topspace (subtopology euclidean {0..1})))"
+ have "(UNIV::real set) \<lesssim> topspace ?Y"
+ proof (intro compact_Hausdorff_or_regular_imp_normal_space connected_space_imp_card_ge)
+ show "connected_space ?Y"
+ using \<open>pathin X \<gamma>\<close> connectedin_def connectedin_path_image by auto
+ show "Hausdorff_space ?Y \<or> regular_space ?Y"
+ using Hausdorff_space_subtopology \<open>Hausdorff_space X\<close> by blast
+ show "t1_space ?Y"
+ using Hausdorff_imp_t1_space \<open>Hausdorff_space X\<close> t1_space_subtopology by blast
+ show "compact_space ?Y"
+ by (simp add: \<open>pathin X \<gamma>\<close> compact_space_subtopology compactin_path_image)
+ have "a \<in> topspace ?Y" "b \<in> topspace ?Y"
+ using \<gamma> pathin_subtopology by fastforce+
+ with \<open>a \<noteq> b\<close> show "\<nexists>x. topspace ?Y \<subseteq> {x}"
+ by blast
+ qed
+ also have "\<dots> \<lesssim> \<gamma> ` {0..1}"
+ by (simp add: subset_imp_lepoll)
+ also have "\<dots> \<lesssim> topspace X"
+ by (meson \<gamma> path_image_subset_topspace subset_imp_lepoll image_subset_iff_funcset)
+ finally show ?thesis .
+qed
+
+lemma connected_space_imp_uncountable:
+ assumes "connected_space X" "regular_space X" "Hausdorff_space X" "\<not> (\<exists>a. topspace X \<subseteq> {a})"
+ shows "\<not> countable(topspace X)"
+proof
+ assume coX: "countable (topspace X)"
+ with \<open>regular_space X\<close> have "normal_space X"
+ using countable_imp_Lindelof_space regular_Lindelof_imp_normal_space by blast
+ then have "(UNIV::real set) \<lesssim> topspace X"
+ by (simp add: Hausdorff_imp_t1_space assms connected_space_imp_card_ge)
+ with coX show False
+ using countable_lepoll uncountable_UNIV_real by blast
+qed
+
+lemma path_connected_space_imp_uncountable:
+ assumes "path_connected_space X" "t1_space X" and nosing: "\<not> (\<exists>a. topspace X \<subseteq> {a})"
+ shows "\<not> countable(topspace X)"
+proof
+ assume coX: "countable (topspace X)"
+ obtain a b where "a \<in> topspace X" "b \<in> topspace X" "a \<noteq> b"
+ by (metis nosing singletonI subset_iff)
+ then obtain \<gamma> where "pathin X \<gamma>" "\<gamma> 0 = a" "\<gamma> 1 = b"
+ by (meson \<open>a \<in> topspace X\<close> \<open>b \<in> topspace X\<close> \<open>path_connected_space X\<close> path_connected_space_def)
+ then have "\<gamma> ` {0..1} \<lesssim> topspace X"
+ by (meson path_image_subset_topspace subset_imp_lepoll image_subset_iff_funcset)
+ define \<A> where "\<A> \<equiv> ((\<lambda>a. {x \<in> {0..1}. \<gamma> x \<in> {a}}) ` topspace X) - {{}}"
+ have \<A>01: "\<A> = {{0..1}}"
+ proof (rule real_Sierpinski_lemma)
+ show "countable \<A>"
+ using \<A>_def coX by blast
+ show "disjoint \<A>"
+ by (auto simp: \<A>_def disjnt_iff pairwise_def)
+ show "\<Union>\<A> = {0..1}"
+ using \<open>pathin X \<gamma>\<close> path_image_subset_topspace by (fastforce simp: \<A>_def Bex_def)
+ fix C
+ assume "C \<in> \<A>"
+ then obtain a where "a \<in> topspace X" and C: "C = {x \<in> {0..1}. \<gamma> x \<in> {a}}" "C \<noteq> {}"
+ by (auto simp: \<A>_def)
+ then have "closedin X {a}"
+ by (meson \<open>t1_space X\<close> closedin_t1_singleton)
+ then have "closedin (top_of_set {0..1}) C"
+ using C \<open>pathin X \<gamma>\<close> closedin_continuous_map_preimage pathin_def by fastforce
+ then show "closed C \<and> C \<noteq> {}"
+ using C closedin_closed_trans by blast
+ qed auto
+ then have "{0..1} \<in> \<A>"
+ by blast
+ then have "\<exists>a \<in> topspace X. {0..1} \<subseteq> {x. \<gamma> x = a}"
+ using \<A>_def image_iff by auto
+ then show False
+ using \<open>\<gamma> 0 = a\<close> \<open>\<gamma> 1 = b\<close> \<open>a \<noteq> b\<close> atLeastAtMost_iff zero_less_one_class.zero_le_one by blast
+qed
+
+
+subsection\<open>Lavrentiev extension etc\<close>
+
+lemma (in Metric_space) convergent_eq_zero_oscillation_gen:
+ assumes "mcomplete" and fim: "f \<in> (topspace X \<inter> S) \<rightarrow> M"
+ shows "(\<exists>l. limitin mtopology f l (atin_within X a S)) \<longleftrightarrow>
+ M \<noteq> {} \<and>
+ (a \<in> topspace X
+ \<longrightarrow> (\<forall>\<epsilon>>0. \<exists>U. openin X U \<and> a \<in> U \<and>
+ (\<forall>x \<in> (S \<inter> U) - {a}. \<forall>y \<in> (S \<inter> U) - {a}. d (f x) (f y) < \<epsilon>)))"
+proof (cases "M = {}")
+ case True
+ with limitin_mspace show ?thesis
+ by blast
+next
+ case False
+ show ?thesis
+ proof (cases "a \<in> topspace X")
+ case True
+ let ?R = "\<forall>\<epsilon>>0. \<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>)"
+ show ?thesis
+ proof (cases "a \<in> X derived_set_of S")
+ case True
+ have ?R
+ if "limitin mtopology f l (atin_within X a S)" for l
+ proof (intro strip)
+ fix \<epsilon>::real
+ assume "\<epsilon>>0"
+ with that \<open>a \<in> topspace X\<close>
+ obtain U where U: "openin X U" "a \<in> U" "l \<in> M"
+ and Uless: "\<forall>x\<in>U - {a}. x \<in> S \<longrightarrow> f x \<in> M \<and> d (f x) l < \<epsilon>/2"
+ unfolding limitin_metric eventually_within_imp eventually_atin
+ using half_gt_zero by blast
+ show "\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>)"
+ proof (intro exI strip conjI)
+ fix x y
+ assume x: "x \<in> S \<inter> U - {a}" and y: "y \<in> S \<inter> U - {a}"
+ then have "d (f x) l < \<epsilon>/2" "d (f y) l < \<epsilon>/2" "f x \<in> M" "f y \<in> M"
+ using Uless by auto
+ then show "d (f x) (f y) < \<epsilon>"
+ using triangle' \<open>l \<in> M\<close> by fastforce
+ qed (auto simp add: U)
+ qed
+ moreover have "\<exists>l. limitin mtopology f l (atin_within X a S)"
+ if R [rule_format]: ?R
+ proof -
+ define F where "F \<equiv> \<lambda>U. mtopology closure_of f ` (S \<inter> U - {a})"
+ define \<C> where "\<C> \<equiv> F ` {U. openin X U \<and> a \<in> U}"
+ have \<C>_clo: "\<forall>C \<in> \<C>. closedin mtopology C"
+ by (force simp add: \<C>_def F_def)
+ moreover have sub_mcball: "\<exists>C a. C \<in> \<C> \<and> C \<subseteq> mcball a \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+ proof -
+ obtain U where U: "openin X U" "a \<in> U"
+ and Uless: "\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>"
+ using R [OF \<open>\<epsilon>>0\<close>] by blast
+ then obtain b where b: "b \<noteq> a" "b \<in> S" "b \<in> U"
+ using True by (auto simp add: in_derived_set_of)
+ have "U \<subseteq> topspace X"
+ by (simp add: U(1) openin_subset)
+ have "f b \<in> M"
+ using b \<open>openin X U\<close> by (metis image_subset_iff_funcset Int_iff fim image_eqI openin_subset subsetD)
+ moreover
+ have "mtopology closure_of f ` ((S \<inter> U) - {a}) \<subseteq> mcball (f b) \<epsilon>"
+ proof (rule closure_of_minimal)
+ have "f y \<in> M" if "y \<in> S" and "y \<in> U" for y
+ using \<open>U \<subseteq> topspace X\<close> fim that by (auto simp: Pi_iff)
+ moreover
+ have "d (f b) (f y) \<le> \<epsilon>" if "y \<in> S" "y \<in> U" "y \<noteq> a" for y
+ using that Uless b by force
+ ultimately show "f ` (S \<inter> U - {a}) \<subseteq> mcball (f b) \<epsilon>"
+ by (force simp: \<open>f b \<in> M\<close>)
+ qed auto
+ ultimately show ?thesis
+ using U by (auto simp add: \<C>_def F_def)
+ qed
+ moreover have "\<Inter>\<F> \<noteq> {}" if "finite \<F>" "\<F> \<subseteq> \<C>" for \<F>
+ proof -
+ obtain \<G> where sub: "\<G> \<subseteq> {U. openin X U \<and> a \<in> U}" and eq: "\<F> = F ` \<G>" and "finite \<G>"
+ by (metis (no_types, lifting) \<C>_def \<open>\<F> \<subseteq> \<C>\<close> \<open>finite \<F>\<close> finite_subset_image)
+ then have "U \<subseteq> topspace X" if "U \<in> \<G>" for U
+ using openin_subset that by auto
+ then have "T \<subseteq> mtopology closure_of T"
+ if "T \<in> (\<lambda>U. f ` (S \<inter> U - {a})) ` \<G>" for T
+ using that fim by (fastforce simp add: intro!: closure_of_subset)
+ moreover
+ have ain: "a \<in> \<Inter> (insert (topspace X) \<G>)" "openin X (\<Inter> (insert (topspace X) \<G>))"
+ using True in_derived_set_of sub \<open>finite \<G>\<close> by (fastforce intro!: openin_Inter)+
+ then obtain y where "y \<noteq> a" "y \<in> S" and y: "y \<in> \<Inter> (insert (topspace X) \<G>)"
+ by (meson \<open>a \<in> X derived_set_of S\<close> sub in_derived_set_of)
+ then have "f y \<in> \<Inter>\<F>"
+ using eq that ain fim by (auto simp add: F_def image_subset_iff in_closure_of)
+ then show ?thesis by blast
+ qed
+ ultimately have "\<Inter>\<C> \<noteq> {}"
+ using \<open>mcomplete\<close> mcomplete_fip by metis
+ then obtain b where "b \<in> \<Inter>\<C>"
+ by auto
+ then have "b \<in> M"
+ using sub_mcball \<C>_clo mbounded_alt_pos mbounded_empty metric_closedin_iff_sequentially_closed by force
+ have "limitin mtopology f b (atin_within X a S)"
+ proof (clarsimp simp: limitin_metric \<open>b \<in> M\<close>)
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ then obtain U where U: "openin X U" "a \<in> U" and subU: "U \<subseteq> topspace X"
+ and Uless: "\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>/2"
+ by (metis R half_gt_zero openin_subset)
+ then obtain x where x: "x \<in> S" "x \<in> U" "x \<noteq> a" and fx: "f x \<in> mball b (\<epsilon>/2)"
+ using \<open>b \<in> \<Inter>\<C>\<close>
+ apply (simp add: \<C>_def F_def closure_of_def del: divide_const_simps)
+ by (metis Diff_iff Int_iff centre_in_mball_iff in_mball openin_mball singletonI zero_less_numeral)
+ moreover
+ have "d (f y) b < \<epsilon>" if "y \<in> U" "y \<noteq> a" "y \<in> S" for y
+ proof -
+ have "d (f x) (f y) < \<epsilon>/2"
+ using Uless that x by force
+ moreover have "d b (f x) < \<epsilon>/2"
+ using fx by simp
+ ultimately show ?thesis
+ using triangle [of b "f x" "f y"] subU that \<open>b \<in> M\<close> commute fim fx by fastforce
+ qed
+ ultimately show "\<forall>\<^sub>F x in atin_within X a S. f x \<in> M \<and> d (f x) b < \<epsilon>"
+ using fim U
+ apply (simp add: eventually_atin eventually_within_imp del: divide_const_simps flip: image_subset_iff_funcset)
+ by (smt (verit, del_insts) Diff_iff Int_iff imageI insertI1 openin_subset subsetD)
+ qed
+ then show ?thesis ..
+ qed
+ ultimately
+ show ?thesis
+ by (meson True \<open>M \<noteq> {}\<close> in_derived_set_of)
+ next
+ case False
+ have "(\<exists>l. limitin mtopology f l (atin_within X a S))"
+ by (metis \<open>M \<noteq> {}\<close> False derived_set_of_trivial_limit equals0I limitin_trivial topspace_mtopology)
+ moreover have "\<forall>e>0. \<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < e)"
+ by (metis Diff_iff False IntE True in_derived_set_of insert_iff)
+ ultimately show ?thesis
+ using limitin_mspace by blast
+ qed
+ next
+ case False
+ then show ?thesis
+ by (metis derived_set_of_trivial_limit ex_in_conv in_derived_set_of limitin_mspace limitin_trivial topspace_mtopology)
+ qed
+qed
+
+text \<open>The HOL Light proof uses some ugly tricks to share common parts of what are two separate proofs for the two cases\<close>
+lemma (in Metric_space) gdelta_in_points_of_convergence_within:
+ assumes "mcomplete"
+ and f: "continuous_map (subtopology X S) mtopology f \<or> t1_space X \<and> f \<in> S \<rightarrow> M"
+ shows "gdelta_in X {x \<in> topspace X. \<exists>l. limitin mtopology f l (atin_within X x S)}"
+proof -
+ have fim: "f \<in> (topspace X \<inter> S) \<rightarrow> M"
+ using continuous_map_image_subset_topspace f by force
+ show ?thesis
+ proof (cases "M={}")
+ case True
+ then show ?thesis
+ by (smt (verit) Collect_cong empty_def empty_iff gdelta_in_empty limitin_mspace)
+ next
+ case False
+ define A where "A \<equiv> {a \<in> topspace X. \<forall>\<epsilon>>0. \<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>)}"
+ have "gdelta_in X A"
+ using f
+ proof (elim disjE conjE)
+ assume cm: "continuous_map (subtopology X S) mtopology f"
+ define C where "C \<equiv> \<lambda>r. \<Union>{U. openin X U \<and> (\<forall>x \<in> S\<inter>U. \<forall>y \<in> S\<inter>U. d (f x) (f y) < r)}"
+ define B where "B \<equiv> (\<Inter>n. C(inverse(Suc n)))"
+ define D where "D \<equiv> (\<Inter> (C ` {0<..}))"
+ have "D=B"
+ unfolding B_def C_def D_def
+ apply (intro Inter_eq_Inter_inverse_Suc Sup_subset_mono)
+ by (smt (verit, ccfv_threshold) Collect_mono_iff)
+ have "B \<subseteq> topspace X"
+ using openin_subset by (force simp add: B_def C_def)
+ have "(countable intersection_of openin X) B"
+ unfolding B_def C_def
+ by (intro relative_to_inc countable_intersection_of_Inter countable_intersection_of_inc) auto
+ then have "gdelta_in X B"
+ unfolding gdelta_in_def by (intro relative_to_subset_inc \<open>B \<subseteq> topspace X\<close>)
+ moreover have "A=D"
+ proof (intro equalityI subsetI)
+ fix a
+ assume x: "a \<in> A"
+ then have "a \<in> topspace X"
+ using A_def by blast
+ show "a \<in> D"
+ proof (clarsimp simp: D_def C_def \<open>a \<in> topspace X\<close>)
+ fix \<epsilon>::real assume "\<epsilon> > 0"
+ then obtain U where "openin X U" "a \<in> U" and U: "(\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>)"
+ using x by (force simp: A_def)
+ show "\<exists>T. openin X T \<and> (\<forall>x\<in>S \<inter> T. \<forall>y\<in>S \<inter> T. d (f x) (f y) < \<epsilon>) \<and> a \<in> T"
+ proof (cases "a \<in> S")
+ case True
+ then obtain V where "openin X V" "a \<in> V" and V: "\<forall>x. x \<in> S \<and> x \<in> V \<longrightarrow> f a \<in> M \<and> f x \<in> M \<and> d (f a) (f x) < \<epsilon>"
+ using \<open>a \<in> topspace X\<close> \<open>\<epsilon> > 0\<close> cm
+ by (force simp add: continuous_map_to_metric openin_subtopology_alt Ball_def)
+ show ?thesis
+ proof (intro exI conjI strip)
+ show "openin X (U \<inter> V)"
+ using \<open>openin X U\<close> \<open>openin X V\<close> by blast
+ show "a \<in> U \<inter> V"
+ using \<open>a \<in> U\<close> \<open>a \<in> V\<close> by blast
+ show "\<And>x y. \<lbrakk>x \<in> S \<inter> (U \<inter> V); y \<in> S \<inter> (U \<inter> V)\<rbrakk> \<Longrightarrow> d (f x) (f y) < \<epsilon>"
+ by (metis DiffI Int_iff U V commute singletonD)
+ qed
+ next
+ case False then show ?thesis
+ using U \<open>a \<in> U\<close> \<open>openin X U\<close> by auto
+ qed
+ qed
+ next
+ fix x
+ assume x: "x \<in> D"
+ then have "x \<in> topspace X"
+ using \<open>B \<subseteq> topspace X\<close> \<open>D=B\<close> by blast
+ with x show "x \<in> A"
+ apply (clarsimp simp: D_def C_def A_def)
+ by (meson DiffD1 greaterThan_iff)
+ qed
+ ultimately show ?thesis
+ by (simp add: \<open>D=B\<close>)
+ next
+ assume "t1_space X" "f \<in> S \<rightarrow> M"
+ define C where "C \<equiv> \<lambda>r. \<Union>{U. openin X U \<and>
+ (\<exists>b \<in> topspace X. \<forall>x \<in> S\<inter>U - {b}. \<forall>y \<in> S\<inter>U - {b}. d (f x) (f y) < r)}"
+ define B where "B \<equiv> (\<Inter>n. C(inverse(Suc n)))"
+ define D where "D \<equiv> (\<Inter> (C ` {0<..}))"
+ have "D=B"
+ unfolding B_def C_def D_def
+ apply (intro Inter_eq_Inter_inverse_Suc Sup_subset_mono)
+ by (smt (verit, ccfv_threshold) Collect_mono_iff)
+ have "B \<subseteq> topspace X"
+ using openin_subset by (force simp add: B_def C_def)
+ have "(countable intersection_of openin X) B"
+ unfolding B_def C_def
+ by (intro relative_to_inc countable_intersection_of_Inter countable_intersection_of_inc) auto
+ then have "gdelta_in X B"
+ unfolding gdelta_in_def by (intro relative_to_subset_inc \<open>B \<subseteq> topspace X\<close>)
+ moreover have "A=D"
+ proof (intro equalityI subsetI)
+ fix x
+ assume x: "x \<in> D"
+ then have "x \<in> topspace X"
+ using \<open>B \<subseteq> topspace X\<close> \<open>D=B\<close> by blast
+ show "x \<in> A"
+ proof (clarsimp simp: A_def \<open>x \<in> topspace X\<close>)
+ fix \<epsilon> :: real
+ assume "\<epsilon>>0"
+ then obtain U b where "openin X U" "b \<in> topspace X"
+ and U: "\<forall>x\<in>S \<inter> U - {b}. \<forall>y\<in>S \<inter> U - {b}. d (f x) (f y) < \<epsilon>" and "x \<in> U"
+ using x by (auto simp: D_def C_def A_def Ball_def)
+ then have "openin X (U-{b})"
+ by (meson \<open>t1_space X\<close> t1_space_openin_delete_alt)
+ then show "\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>xa\<in>S \<inter> U - {x}. \<forall>y\<in>S \<inter> U - {x}. d (f xa) (f y) < \<epsilon>)"
+ using U \<open>openin X U\<close> \<open>x \<in> U\<close> by auto
+ qed
+ next
+ show "\<And>x. x \<in> A \<Longrightarrow> x \<in> D"
+ unfolding A_def D_def C_def
+ by clarsimp meson
+ qed
+ ultimately show ?thesis
+ by (simp add: \<open>D=B\<close>)
+ qed
+ then show ?thesis
+ by (simp add: A_def convergent_eq_zero_oscillation_gen False fim \<open>mcomplete\<close> cong: conj_cong)
+ qed
+qed
+
+
+lemma gdelta_in_points_of_convergence_within:
+ assumes Y: "completely_metrizable_space Y"
+ and f: "continuous_map (subtopology X S) Y f \<or> t1_space X \<and> f \<in> S \<rightarrow> topspace Y"
+ shows "gdelta_in X {x \<in> topspace X. \<exists>l. limitin Y f l (atin_within X x S)}"
+ using assms
+ unfolding completely_metrizable_space_def
+ using Metric_space.gdelta_in_points_of_convergence_within Metric_space.topspace_mtopology by fastforce
+
+
+lemma Lavrentiev_extension_gen:
+ assumes "S \<subseteq> topspace X" and Y: "completely_metrizable_space Y"
+ and contf: "continuous_map (subtopology X S) Y f"
+ obtains U g where "gdelta_in X U" "S \<subseteq> U"
+ "continuous_map (subtopology X (X closure_of S \<inter> U)) Y g"
+ "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+proof -
+ define U where "U \<equiv> {x \<in> topspace X. \<exists>l. limitin Y f l (atin_within X x S)}"
+ have "S \<subseteq> U"
+ using that contf limit_continuous_map_within subsetD [OF \<open>S \<subseteq> topspace X\<close>]
+ by (fastforce simp: U_def)
+ then have "S \<subseteq> X closure_of S \<inter> U"
+ by (simp add: \<open>S \<subseteq> topspace X\<close> closure_of_subset)
+ moreover
+ have "\<And>t. t \<in> X closure_of S \<inter> U - S \<Longrightarrow> \<exists>l. limitin Y f l (atin_within X t S)"
+ using U_def by blast
+ moreover have "regular_space Y"
+ by (simp add: Y completely_metrizable_imp_metrizable_space metrizable_imp_regular_space)
+ ultimately
+ obtain g where g: "continuous_map (subtopology X (X closure_of S \<inter> U)) Y g"
+ and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ using continuous_map_extension_pointwise_alt assms by blast
+ show thesis
+ proof
+ show "gdelta_in X U"
+ by (simp add: U_def Y contf gdelta_in_points_of_convergence_within)
+ show "continuous_map (subtopology X (X closure_of S \<inter> U)) Y g"
+ by (simp add: g)
+ qed (use \<open>S \<subseteq> U\<close> gf in auto)
+qed
+
+lemma Lavrentiev_extension:
+ assumes "S \<subseteq> topspace X"
+ and X: "metrizable_space X \<or> topspace X \<subseteq> X closure_of S"
+ and Y: "completely_metrizable_space Y"
+ and contf: "continuous_map (subtopology X S) Y f"
+ obtains U g where "gdelta_in X U" "S \<subseteq> U" "U \<subseteq> X closure_of S"
+ "continuous_map (subtopology X U) Y g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+proof -
+ obtain U g where "gdelta_in X U" "S \<subseteq> U"
+ and contg: "continuous_map (subtopology X (X closure_of S \<inter> U)) Y g"
+ and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ using Lavrentiev_extension_gen Y assms(1) contf by blast
+ define V where "V \<equiv> X closure_of S \<inter> U"
+ show thesis
+ proof
+ show "gdelta_in X V"
+ by (metis V_def X \<open>gdelta_in X U\<close> closed_imp_gdelta_in closedin_closure_of closure_of_subset_topspace gdelta_in_Int gdelta_in_topspace subset_antisym)
+ show "S \<subseteq> V"
+ by (simp add: V_def \<open>S \<subseteq> U\<close> assms(1) closure_of_subset)
+ show "continuous_map (subtopology X V) Y g"
+ by (simp add: V_def contg)
+ qed (auto simp: gf V_def)
+qed
+
+subsection\<open>Embedding in products and hence more about completely metrizable spaces\<close>
+
+lemma (in Metric_space) gdelta_homeomorphic_space_closedin_product:
+ assumes S: "\<And>i. i \<in> I \<Longrightarrow> openin mtopology (S i)"
+ obtains T where "closedin (prod_topology mtopology (powertop_real I)) T"
+ "subtopology mtopology (\<Inter>i \<in> I. S i) homeomorphic_space
+ subtopology (prod_topology mtopology (powertop_real I)) T"
+proof (cases "I={}")
+ case True
+ then have top: "topspace (prod_topology mtopology (powertop_real I)) = (M \<times> {(\<lambda>x. undefined)})"
+ by simp
+ show ?thesis
+ proof
+ show "closedin (prod_topology mtopology (powertop_real I)) (M \<times> {(\<lambda>x. undefined)})"
+ by (metis top closedin_topspace)
+ have "subtopology mtopology (\<Inter>(S ` I)) homeomorphic_space mtopology"
+ by (simp add: True product_topology_empty_discrete)
+ also have "\<dots> homeomorphic_space (prod_topology mtopology (powertop_real {}))"
+ by (metis PiE_empty_domain homeomorphic_space_sym prod_topology_homeomorphic_space_left topspace_product_topology)
+ finally
+ show "subtopology mtopology (\<Inter>(S ` I)) homeomorphic_space subtopology (prod_topology mtopology (powertop_real I)) (M \<times> {(\<lambda>x. undefined)})"
+ by (smt (verit) True subtopology_topspace top)
+ qed
+next
+ case False
+ have SM: "\<And>i. i \<in> I \<Longrightarrow> S i \<subseteq> M"
+ using assms openin_mtopology by blast
+ then have "(\<Inter>i \<in> I. S i) \<subseteq> M"
+ using False by blast
+ define dd where "dd \<equiv> \<lambda>i. if i\<notin>I \<or> S i = M then \<lambda>u. 1 else (\<lambda>u. INF x \<in> M - S i. d u x)"
+ have [simp]: "bdd_below (d u ` A)" for u A
+ by (meson bdd_belowI2 nonneg)
+ have cont_dd: "continuous_map (subtopology mtopology (S i)) euclidean (dd i)" if "i \<in> I" for i
+ proof -
+ have "dist (Inf (d x ` (M - S i))) (Inf (d y ` (M - S i))) \<le> d x y"
+ if "x \<in> S i" "x \<in> M" "y \<in> S i" "y \<in> M" "S i \<noteq> M" for x y
+ proof -
+ have [simp]: "\<not> M \<subseteq> S i"
+ using SM \<open>S i \<noteq> M\<close> \<open>i \<in> I\<close> by auto
+ have "\<And>u. \<lbrakk>u \<in> M; u \<notin> S i\<rbrakk> \<Longrightarrow> Inf (d x ` (M - S i)) \<le> d x y + d y u"
+ apply (clarsimp simp add: cInf_le_iff_less)
+ by (smt (verit) DiffI triangle \<open>x \<in> M\<close> \<open>y \<in> M\<close>)
+ then have "Inf (d x ` (M - S i)) - d x y \<le> Inf (d y ` (M - S i))"
+ by (force simp add: le_cInf_iff)
+ moreover
+ have "\<And>u. \<lbrakk>u \<in> M; u \<notin> S i\<rbrakk> \<Longrightarrow> Inf (d y ` (M - S i)) \<le> d x u + d x y"
+ apply (clarsimp simp add: cInf_le_iff_less)
+ by (smt (verit) DiffI triangle'' \<open>x \<in> M\<close> \<open>y \<in> M\<close>)
+ then have "Inf (d y ` (M - S i)) - d x y \<le> Inf (d x ` (M - S i))"
+ by (force simp add: le_cInf_iff)
+ ultimately show ?thesis
+ by (simp add: dist_real_def abs_le_iff)
+ qed
+ then have *: "Lipschitz_continuous_map (submetric Self (S i)) euclidean_metric (\<lambda>u. Inf (d u ` (M - S i)))"
+ unfolding Lipschitz_continuous_map_def by (force intro!: exI [where x=1])
+ then show ?thesis
+ using Lipschitz_continuous_imp_continuous_map [OF *]
+ by (simp add: dd_def Self_def mtopology_of_submetric )
+ qed
+ have dd_pos: "0 < dd i x" if "x \<in> S i" for i x
+ proof (clarsimp simp add: dd_def)
+ assume "i \<in> I" and "S i \<noteq> M"
+ have opeS: "openin mtopology (S i)"
+ by (simp add: \<open>i \<in> I\<close> assms)
+ then obtain r where "r>0" and r: "\<And>y. \<lbrakk>y \<in> M; d x y < r\<rbrakk> \<Longrightarrow> y \<in> S i"
+ by (meson \<open>x \<in> S i\<close> in_mball openin_mtopology subsetD)
+ then have "\<And>y. y \<in> M - S i \<Longrightarrow> d x y \<ge> r"
+ by (meson Diff_iff linorder_not_le)
+ then have "Inf (d x ` (M - S i)) \<ge> r"
+ by (meson Diff_eq_empty_iff SM \<open>S i \<noteq> M\<close> \<open>i \<in> I\<close> cINF_greatest set_eq_subset)
+ with \<open>r>0\<close> show "0 < Inf (d x ` (M - S i))" by simp
+ qed
+ define f where "f \<equiv> \<lambda>x. (x, \<lambda>i\<in>I. inverse(dd i x))"
+ define T where "T \<equiv> f ` (\<Inter>i \<in> I. S i)"
+ show ?thesis
+ proof
+ show "closedin (prod_topology mtopology (powertop_real I)) T"
+ unfolding closure_of_subset_eq [symmetric]
+ proof
+ show "T \<subseteq> topspace (prod_topology mtopology (powertop_real I))"
+ using False SM by (auto simp: T_def f_def)
+
+ have "(x,ds) \<in> T"
+ if \<section>: "\<And>U. \<lbrakk>(x, ds) \<in> U; openin (prod_topology mtopology (powertop_real I)) U\<rbrakk> \<Longrightarrow> \<exists>y\<in>T. y \<in> U"
+ and "x \<in> M" and ds: "ds \<in> I \<rightarrow>\<^sub>E UNIV" for x ds
+ proof -
+ have ope: "\<exists>x. x \<in> \<Inter>(S ` I) \<and> f x \<in> U \<times> V"
+ if "x \<in> U" and "ds \<in> V" and "openin mtopology U" and "openin (powertop_real I) V" for U V
+ using \<section> [of "U\<times>V"] that by (force simp add: T_def openin_prod_Times_iff)
+ have x_in_INT: "x \<in> \<Inter>(S ` I)"
+ proof clarify
+ fix i
+ assume "i \<in> I"
+ show "x \<in> S i"
+ proof (rule ccontr)
+ assume "x \<notin> S i"
+ have "openin (powertop_real I) {z \<in> topspace (powertop_real I). z i \<in> {ds i - 1 <..< ds i + 1}}"
+ proof (rule openin_continuous_map_preimage)
+ show "continuous_map (powertop_real I) euclidean (\<lambda>x. x i)"
+ by (metis \<open>i \<in> I\<close> continuous_map_product_projection)
+ qed auto
+ then obtain y where "y \<in> S i" "y \<in> M" and dxy: "d x y < inverse (\<bar>ds i\<bar> + 1)"
+ and intvl: "inverse (dd i y) \<in> {ds i - 1 <..< ds i + 1}"
+ using ope [of "mball x (inverse(abs(ds i) + 1))" "{z \<in> topspace(powertop_real I). z i \<in> {ds i - 1<..<ds i + 1}}"]
+ \<open>x \<in> M\<close> \<open>ds \<in> I \<rightarrow>\<^sub>E UNIV\<close> \<open>i \<in> I\<close>
+ by (fastforce simp add: f_def)
+ have "\<not> M \<subseteq> S i"
+ using \<open>x \<notin> S i\<close> \<open>x \<in> M\<close> by blast
+ have "inverse (\<bar>ds i\<bar> + 1) \<le> dd i y"
+ using intvl \<open>y \<in> S i\<close> dd_pos [of y i]
+ by (smt (verit, ccfv_threshold) greaterThanLessThan_iff inverse_inverse_eq le_imp_inverse_le)
+ also have "\<dots> \<le> d x y"
+ using \<open>i \<in> I\<close> \<open>\<not> M \<subseteq> S i\<close> \<open>x \<notin> S i\<close> \<open>x \<in> M\<close>
+ apply (simp add: dd_def cInf_le_iff_less)
+ using commute by force
+ finally show False
+ using dxy by linarith
+ qed
+ qed
+ moreover have "ds = (\<lambda>i\<in>I. inverse (dd i x))"
+ proof (rule PiE_ext [OF ds])
+ fix i
+ assume "i \<in> I"
+ define e where "e \<equiv> \<bar>ds i - inverse (dd i x)\<bar>"
+ { assume con: "e > 0"
+ have "continuous_map (subtopology mtopology (S i)) euclidean (\<lambda>x. inverse (dd i x))"
+ using dd_pos cont_dd \<open>i \<in> I\<close>
+ by (fastforce simp: intro!: continuous_map_real_inverse)
+ then have "openin (subtopology mtopology (S i))
+ {z \<in> topspace (subtopology mtopology (S i)).
+ inverse (dd i z) \<in> {inverse(dd i x) - e/2<..<inverse(dd i x) + e/2}}"
+ using openin_continuous_map_preimage open_greaterThanLessThan open_openin by blast
+ then obtain U where "openin mtopology U"
+ and U: "{z \<in> S i. inverse (dd i x) - e/2 < inverse (dd i z) \<and>
+ inverse (dd i z) < inverse (dd i x) + e/2}
+ = U \<inter> S i"
+ using SM \<open>i \<in> I\<close> by (auto simp: openin_subtopology)
+ have "x \<in> U"
+ using U x_in_INT \<open>i \<in> I\<close> con by fastforce
+ have "ds \<in> {z \<in> topspace (powertop_real I). z i \<in> {ds i - e / 2<..<ds i + e/2}}"
+ by (simp add: con ds)
+ moreover
+ have "openin (powertop_real I) {z \<in> topspace (powertop_real I). z i \<in> {ds i - e / 2<..<ds i + e/2}}"
+ proof (rule openin_continuous_map_preimage)
+ show "continuous_map (powertop_real I) euclidean (\<lambda>x. x i)"
+ by (metis \<open>i \<in> I\<close> continuous_map_product_projection)
+ qed auto
+ ultimately obtain y where "y \<in> \<Inter>(S ` I) \<and> f y \<in> U \<times> {z \<in> topspace (powertop_real I). z i \<in> {ds i - e / 2<..<ds i + e/2}}"
+ using ope \<open>x \<in> U\<close> \<open>openin mtopology U\<close> \<open>x \<in> U\<close>
+ by presburger
+ with \<open>i \<in> I\<close> U
+ have False unfolding set_eq_iff f_def e_def by simp (smt (verit) field_sum_of_halves)
+ }
+ then show "ds i = (\<lambda>i\<in>I. inverse (dd i x)) i"
+ using \<open>i \<in> I\<close> by (force simp: e_def)
+ qed auto
+ ultimately show ?thesis
+ by (auto simp: T_def f_def)
+ qed
+ then show "prod_topology mtopology (powertop_real I) closure_of T \<subseteq> T"
+ by (auto simp: closure_of_def)
+ qed
+ have eq: "(\<Inter>(S ` I) \<times> (I \<rightarrow>\<^sub>E UNIV) \<inter> f ` (M \<inter> \<Inter>(S ` I))) = (f ` \<Inter>(S ` I))"
+ using False SM by (force simp: f_def image_iff)
+ have "continuous_map (subtopology mtopology (\<Inter>(S ` I))) euclidean (dd i)" if "i \<in> I" for i
+ by (meson INT_lower cont_dd continuous_map_from_subtopology_mono that)
+ then have "continuous_map (subtopology mtopology (\<Inter>(S ` I))) (powertop_real I) (\<lambda>x. \<lambda>i\<in>I. inverse (dd i x))"
+ using dd_pos by (fastforce simp: continuous_map_componentwise intro!: continuous_map_real_inverse)
+ then have "embedding_map (subtopology mtopology (\<Inter>(S ` I))) (prod_topology (subtopology mtopology (\<Inter>(S ` I))) (powertop_real I)) f"
+ by (simp add: embedding_map_graph f_def)
+ moreover have "subtopology (prod_topology (subtopology mtopology (\<Inter>(S ` I))) (powertop_real I))
+ (f ` topspace (subtopology mtopology (\<Inter>(S ` I)))) =
+ subtopology (prod_topology mtopology (powertop_real I)) T"
+ by (simp add: prod_topology_subtopology subtopology_subtopology T_def eq)
+ ultimately
+ show "subtopology mtopology (\<Inter>(S ` I)) homeomorphic_space subtopology (prod_topology mtopology (powertop_real I)) T"
+ by (metis embedding_map_imp_homeomorphic_space)
+ qed
+qed
+
+
+lemma gdelta_homeomorphic_space_closedin_product:
+ assumes "metrizable_space X" and "\<And>i. i \<in> I \<Longrightarrow> openin X (S i)"
+ obtains T where "closedin (prod_topology X (powertop_real I)) T"
+ "subtopology X (\<Inter>i \<in> I. S i) homeomorphic_space
+ subtopology (prod_topology X (powertop_real I)) T"
+ using Metric_space.gdelta_homeomorphic_space_closedin_product
+ by (metis assms metrizable_space_def)
+
+lemma open_homeomorphic_space_closedin_product:
+ assumes "metrizable_space X" and "openin X S"
+ obtains T where "closedin (prod_topology X euclideanreal) T"
+ "subtopology X S homeomorphic_space
+ subtopology (prod_topology X euclideanreal) T"
+proof -
+ obtain T where cloT: "closedin (prod_topology X (powertop_real {()})) T"
+ and homT: "subtopology X S homeomorphic_space
+ subtopology (prod_topology X (powertop_real {()})) T"
+ using gdelta_homeomorphic_space_closedin_product [of X "{()}" "\<lambda>i. S"] assms
+ by auto
+ have "prod_topology X (powertop_real {()}) homeomorphic_space prod_topology X euclideanreal"
+ by (meson homeomorphic_space_prod_topology homeomorphic_space_refl homeomorphic_space_singleton_product)
+ then obtain f where f: "homeomorphic_map (prod_topology X (powertop_real {()})) (prod_topology X euclideanreal) f"
+ unfolding homeomorphic_space by metis
+ show thesis
+ proof
+ show "closedin (prod_topology X euclideanreal) (f ` T)"
+ using cloT f homeomorphic_map_closedness_eq by blast
+ moreover have "T = topspace (subtopology (prod_topology X (powertop_real {()})) T)"
+ by (metis cloT closedin_subset topspace_subtopology_subset)
+ ultimately show "subtopology X S homeomorphic_space subtopology (prod_topology X euclideanreal) (f ` T)"
+ by (smt (verit, best) closedin_subset f homT homeomorphic_map_subtopologies homeomorphic_space
+ homeomorphic_space_trans topspace_subtopology topspace_subtopology_subset)
+ qed
+qed
+
+lemma completely_metrizable_space_gdelta_in_alt:
+ assumes X: "completely_metrizable_space X"
+ and S: "(countable intersection_of openin X) S"
+ shows "completely_metrizable_space (subtopology X S)"
+proof -
+ obtain \<U> where "countable \<U>" "S = \<Inter>\<U>" and ope: "\<And>U. U \<in> \<U> \<Longrightarrow> openin X U"
+ using S by (force simp add: intersection_of_def)
+ then have \<U>: "completely_metrizable_space (powertop_real \<U>)"
+ by (simp add: completely_metrizable_space_euclidean completely_metrizable_space_product_topology)
+ obtain C where "closedin (prod_topology X (powertop_real \<U>)) C"
+ and sub: "subtopology X (\<Inter>\<U>) homeomorphic_space
+ subtopology (prod_topology X (powertop_real \<U>)) C"
+ by (metis gdelta_homeomorphic_space_closedin_product X completely_metrizable_imp_metrizable_space ope INF_identity_eq)
+ moreover have "completely_metrizable_space (prod_topology X (powertop_real \<U>))"
+ by (simp add: completely_metrizable_space_prod_topology X \<U>)
+ ultimately have "completely_metrizable_space (subtopology (prod_topology X (powertop_real \<U>)) C)"
+ using completely_metrizable_space_closedin by blast
+ then show ?thesis
+ using \<open>S = \<Inter>\<U>\<close> sub homeomorphic_completely_metrizable_space by blast
+qed
+
+lemma completely_metrizable_space_gdelta_in:
+ "\<lbrakk>completely_metrizable_space X; gdelta_in X S\<rbrakk>
+ \<Longrightarrow> completely_metrizable_space (subtopology X S)"
+ by (simp add: completely_metrizable_space_gdelta_in_alt gdelta_in_alt)
+
+lemma completely_metrizable_space_openin:
+ "\<lbrakk>completely_metrizable_space X; openin X S\<rbrakk>
+ \<Longrightarrow> completely_metrizable_space (subtopology X S)"
+ by (simp add: completely_metrizable_space_gdelta_in open_imp_gdelta_in)
+
+
+lemma (in Metric_space) locally_compact_imp_completely_metrizable_space:
+ assumes "locally_compact_space mtopology"
+ shows "completely_metrizable_space mtopology"
+proof -
+ obtain f :: "['a,'a] \<Rightarrow> real" and m' where
+ "mcomplete_of m'" and fim: "f \<in> M \<rightarrow> mspace m'"
+ and clo: "mtopology_of m' closure_of f ` M = mspace m'"
+ and d: "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> mdist m' (f x) (f y) = d x y"
+ by (metis metric_completion)
+ then have "embedding_map mtopology (mtopology_of m') f"
+ unfolding mtopology_of_def
+ by (metis Metric_space12.isometry_imp_embedding_map Metric_space12_mspace_mdist mdist_metric mspace_metric)
+ then have hom: "mtopology homeomorphic_space subtopology (mtopology_of m') (f ` M)"
+ by (metis embedding_map_imp_homeomorphic_space topspace_mtopology)
+ have "locally_compact_space (subtopology (mtopology_of m') (f ` M))"
+ using assms hom homeomorphic_locally_compact_space by blast
+ moreover have "Hausdorff_space (mtopology_of m')"
+ by (simp add: Metric_space.Hausdorff_space_mtopology mtopology_of_def)
+ ultimately have "openin (mtopology_of m') (f ` M)"
+ by (simp add: clo dense_locally_compact_openin_Hausdorff_space fim image_subset_iff_funcset)
+ then
+ have "completely_metrizable_space (subtopology (mtopology_of m') (f ` M))"
+ using \<open>mcomplete_of m'\<close> unfolding mcomplete_of_def mtopology_of_def
+ by (metis Metric_space.completely_metrizable_space_mtopology Metric_space_mspace_mdist completely_metrizable_space_openin )
+ then show ?thesis
+ using hom homeomorphic_completely_metrizable_space by blast
+qed
+
+lemma locally_compact_imp_completely_metrizable_space:
+ assumes "metrizable_space X" and "locally_compact_space X"
+ shows "completely_metrizable_space X"
+ by (metis Metric_space.locally_compact_imp_completely_metrizable_space assms metrizable_space_def)
+
+
+lemma completely_metrizable_space_imp_gdelta_in:
+ assumes X: "metrizable_space X" and "S \<subseteq> topspace X"
+ and XS: "completely_metrizable_space (subtopology X S)"
+ shows "gdelta_in X S"
+proof -
+ obtain U f where "gdelta_in X U" "S \<subseteq> U" and U: "U \<subseteq> X closure_of S"
+ and contf: "continuous_map (subtopology X U) (subtopology X S) f"
+ and fid: "\<And>x. x \<in> S \<Longrightarrow> f x = x"
+ using Lavrentiev_extension[of S X "subtopology X S" id] assms by auto
+ then have "f ` topspace (subtopology X U) \<subseteq> topspace (subtopology X S)"
+ using continuous_map_image_subset_topspace by blast
+ then have "f`U \<subseteq> S"
+ by (metis \<open>gdelta_in X U\<close> \<open>S \<subseteq> topspace X\<close> gdelta_in_subset topspace_subtopology_subset)
+ moreover
+ have "Hausdorff_space (subtopology X U)"
+ by (simp add: Hausdorff_space_subtopology X metrizable_imp_Hausdorff_space)
+ then have "\<And>x. x \<in> U \<Longrightarrow> f x = x"
+ using U fid contf forall_in_closure_of_eq [of _ "subtopology X U" S "subtopology X U" f id]
+ by (metis \<open>S \<subseteq> U\<close> closure_of_subtopology_open continuous_map_id continuous_map_in_subtopology id_apply inf.orderE subtopology_subtopology)
+ ultimately have "U \<subseteq> S"
+ by auto
+ then show ?thesis
+ using \<open>S \<subseteq> U\<close> \<open>gdelta_in X U\<close> by auto
+qed
+
+lemma completely_metrizable_space_eq_gdelta_in:
+ "\<lbrakk>completely_metrizable_space X; S \<subseteq> topspace X\<rbrakk>
+ \<Longrightarrow> completely_metrizable_space (subtopology X S) \<longleftrightarrow> gdelta_in X S"
+ using completely_metrizable_imp_metrizable_space completely_metrizable_space_gdelta_in completely_metrizable_space_imp_gdelta_in by blast
+
+lemma gdelta_in_eq_completely_metrizable_space:
+ "completely_metrizable_space X
+ \<Longrightarrow> gdelta_in X S \<longleftrightarrow> S \<subseteq> topspace X \<and> completely_metrizable_space (subtopology X S)"
+ by (metis completely_metrizable_space_eq_gdelta_in gdelta_in_alt)
+
end
--- a/src/HOL/Library/Equipollence.thy Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Library/Equipollence.thy Wed Jul 05 15:01:46 2023 +0200
@@ -18,6 +18,20 @@
lemma lepoll_empty_iff_empty [simp]: "A \<lesssim> {} \<longleftrightarrow> A = {}"
by (auto simp: lepoll_def)
+(*The HOL Light CARD_LE_RELATIONAL_FULL*)
+lemma lepoll_relational_full:
+ assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x. x \<in> A \<and> R x y"
+ and "\<And>x y y'. \<lbrakk>x \<in> A; y \<in> B; y' \<in> B; R x y; R x y'\<rbrakk> \<Longrightarrow> y = y'"
+ shows "B \<lesssim> A"
+proof -
+ obtain f where f: "\<And>y. y \<in> B \<Longrightarrow> f y \<in> A \<and> R (f y) y"
+ using assms by metis
+ with assms have "inj_on f B"
+ by (metis inj_onI)
+ with f show ?thesis
+ unfolding lepoll_def by blast
+qed
+
lemma eqpoll_iff_card_of_ordIso: "A \<approx> B \<longleftrightarrow> ordIso2 (card_of A) (card_of B)"
by (simp add: card_of_ordIso eqpoll_def)
@@ -190,6 +204,18 @@
lemma countable_lesspoll: "\<lbrakk>countable A; B \<prec> A\<rbrakk> \<Longrightarrow> countable B"
using countable_lepoll lesspoll_def by blast
+lemma lepoll_iff_card_le: "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> A \<lesssim> B \<longleftrightarrow> card A \<le> card B"
+ by (simp add: inj_on_iff_card_le lepoll_def)
+
+lemma lepoll_iff_finite_card: "A \<lesssim> {..<n::nat} \<longleftrightarrow> finite A \<and> card A \<le> n"
+ by (metis card_lessThan finite_lessThan finite_surj lepoll_iff lepoll_iff_card_le)
+
+lemma eqpoll_iff_finite_card: "A \<approx> {..<n::nat} \<longleftrightarrow> finite A \<and> card A = n"
+ by (metis card_lessThan eqpoll_finite_iff eqpoll_iff_card finite_lessThan)
+
+lemma lesspoll_iff_finite_card: "A \<prec> {..<n::nat} \<longleftrightarrow> finite A \<and> card A < n"
+ by (metis eqpoll_iff_finite_card lepoll_iff_finite_card lesspoll_def order_less_le)
+
subsection\<open>Mapping by an injection\<close>
lemma inj_on_image_eqpoll_self: "inj_on f A \<Longrightarrow> f ` A \<approx> A"
--- a/src/HOL/Library/Set_Idioms.thy Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Library/Set_Idioms.thy Wed Jul 05 15:01:46 2023 +0200
@@ -340,12 +340,8 @@
unfolding relative_to_def
by (metis Diff_Diff_Int Diff_eq double_compl inf.absorb_iff2)
-lemma relative_to_subset:
- "S \<subseteq> T \<and> P S \<Longrightarrow> (P relative_to T) S"
- unfolding relative_to_def by auto
-
lemma relative_to_subset_trans:
- "(P relative_to U) S \<and> S \<subseteq> T \<and> T \<subseteq> U \<Longrightarrow> (P relative_to T) S"
+ "\<lbrakk>(P relative_to U) S; S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (P relative_to T) S"
unfolding relative_to_def by auto
lemma relative_to_mono:
--- a/src/HOL/Real.thy Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Real.thy Wed Jul 05 15:01:46 2023 +0200
@@ -1095,7 +1095,6 @@
shows "x = 0"
by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc)
-
lemma inverse_Suc: "inverse (Suc n) > 0"
using of_nat_0_less_iff positive_imp_inverse_positive zero_less_Suc by blast
@@ -1117,6 +1116,24 @@
using order_le_less_trans by blast
qed
+(*HOL Light's FORALL_POS_MONO_1_EQ*)
+text \<open>On the relationship between two different ways of converting to 0\<close>
+lemma Inter_eq_Inter_inverse_Suc:
+ assumes "\<And>r' r. r' < r \<Longrightarrow> A r' \<subseteq> A r"
+ shows "\<Inter> (A ` {0<..}) = (\<Inter>n. A(inverse(Suc n)))"
+proof
+ have "x \<in> A \<epsilon>"
+ if x: "\<forall>n. x \<in> A (inverse (Suc n))" and "\<epsilon>>0" for x and \<epsilon> :: real
+ proof -
+ obtain n where "inverse (Suc n) < \<epsilon>"
+ using \<open>\<epsilon>>0\<close> reals_Archimedean by blast
+ with assms x show ?thesis
+ by blast
+ qed
+ then show "(\<Inter>n. A(inverse(Suc n))) \<subseteq> (\<Inter>\<epsilon>\<in>{0<..}. A \<epsilon>)"
+ by auto
+qed (use inverse_Suc in fastforce)
+
subsection \<open>Rationals\<close>
lemma Rats_abs_iff[simp]:
--- a/src/HOL/Transcendental.thy Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Transcendental.thy Wed Jul 05 15:01:46 2023 +0200
@@ -2716,42 +2716,48 @@
lemma floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
by (auto simp: floor_eq_iff powr_le_iff less_powr_iff)
-lemma floor_log_nat_eq_powr_iff: fixes b n k :: nat
- shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow>
- floor (log b (real k)) = n \<longleftrightarrow> b^n \<le> k \<and> k < b^(n+1)"
+lemma power_of_nat_log_ge: "b > 1 \<Longrightarrow> b ^ nat \<lceil>log b x\<rceil> \<ge> x"
+ by (smt (verit) less_log_of_power of_nat_ceiling)
+
+lemma floor_log_nat_eq_powr_iff:
+ fixes b n k :: nat
+ shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow> floor (log b (real k)) = n \<longleftrightarrow> b^n \<le> k \<and> k < b^(n+1)"
by (auto simp: floor_log_eq_powr_iff powr_add powr_realpow
of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
simp del: of_nat_power of_nat_mult)
-lemma floor_log_nat_eq_if: fixes b n k :: nat
+lemma floor_log_nat_eq_if:
+ fixes b n k :: nat
assumes "b^n \<le> k" "k < b^(n+1)" "b \<ge> 2"
- shows "floor (log b (real k)) = n"
-proof -
- have "k \<ge> 1" using assms(1,3) one_le_power[of b n] by linarith
- with assms show ?thesis by(simp add: floor_log_nat_eq_powr_iff)
-qed
-
-lemma ceiling_log_eq_powr_iff: "\<lbrakk> x > 0; b > 1 \<rbrakk>
- \<Longrightarrow> \<lceil>log b x\<rceil> = int k + 1 \<longleftrightarrow> b powr k < x \<and> x \<le> b powr (k + 1)"
-by (auto simp: ceiling_eq_iff powr_less_iff le_powr_iff)
-
-lemma ceiling_log_nat_eq_powr_iff: fixes b n k :: nat
- shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow>
- ceiling (log b (real k)) = int n + 1 \<longleftrightarrow> (b^n < k \<and> k \<le> b^(n+1))"
-using ceiling_log_eq_powr_iff
-by (auto simp: powr_add powr_realpow of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
- simp del: of_nat_power of_nat_mult)
-
-lemma ceiling_log_nat_eq_if: fixes b n k :: nat
+ shows "floor (log b (real k)) = n"
+proof -
+ have "k \<ge> 1"
+ using assms linorder_le_less_linear by force
+ with assms show ?thesis
+ by(simp add: floor_log_nat_eq_powr_iff)
+qed
+
+lemma ceiling_log_eq_powr_iff:
+ "\<lbrakk> x > 0; b > 1 \<rbrakk> \<Longrightarrow> \<lceil>log b x\<rceil> = int k + 1 \<longleftrightarrow> b powr k < x \<and> x \<le> b powr (k + 1)"
+ by (auto simp: ceiling_eq_iff powr_less_iff le_powr_iff)
+
+lemma ceiling_log_nat_eq_powr_iff:
+ fixes b n k :: nat
+ shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow> ceiling (log b (real k)) = int n + 1 \<longleftrightarrow> (b^n < k \<and> k \<le> b^(n+1))"
+ using ceiling_log_eq_powr_iff
+ by (auto simp: powr_add powr_realpow of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
+ simp del: of_nat_power of_nat_mult)
+
+lemma ceiling_log_nat_eq_if:
+ fixes b n k :: nat
assumes "b^n < k" "k \<le> b^(n+1)" "b \<ge> 2"
- shows "ceiling (log b (real k)) = int n + 1"
-proof -
- have "k \<ge> 1" using assms(1,3) one_le_power[of b n] by linarith
- with assms show ?thesis by(simp add: ceiling_log_nat_eq_powr_iff)
-qed
-
-lemma floor_log2_div2: fixes n :: nat assumes "n \<ge> 2"
-shows "floor(log 2 n) = floor(log 2 (n div 2)) + 1"
+ shows "\<lceil>log (real b) (real k)\<rceil> = int n + 1"
+ using assms ceiling_log_nat_eq_powr_iff by force
+
+lemma floor_log2_div2:
+ fixes n :: nat
+ assumes "n \<ge> 2"
+ shows "\<lfloor>log 2 (real n)\<rfloor> = \<lfloor>log 2 (n div 2)\<rfloor> + 1"
proof cases
assume "n=2" thus ?thesis by simp
next
@@ -2768,8 +2774,9 @@
show ?thesis by simp
qed
-lemma ceiling_log2_div2: assumes "n \<ge> 2"
-shows "ceiling(log 2 (real n)) = ceiling(log 2 ((n-1) div 2 + 1)) + 1"
+lemma ceiling_log2_div2:
+ assumes "n \<ge> 2"
+ shows "ceiling(log 2 (real n)) = ceiling(log 2 ((n-1) div 2 + 1)) + 1"
proof cases
assume "n=2" thus ?thesis by simp
next
@@ -2797,17 +2804,7 @@
lemma powr_int:
assumes "x > 0"
shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
-proof (cases "i < 0")
- case True
- have r: "x powr i = 1 / x powr (- i)"
- by (simp add: powr_minus field_simps)
- show ?thesis using \<open>i < 0\<close> \<open>x > 0\<close>
- by (simp add: r field_simps powr_realpow[symmetric])
-next
- case False
- then show ?thesis
- by (simp add: assms powr_realpow[symmetric])
-qed
+ by (simp add: assms inverse_eq_divide powr_real_of_int)
definition powr_real :: "real \<Rightarrow> real \<Rightarrow> real"
where [code_abbrev, simp]: "powr_real = Transcendental.powr"