Lindelöf spaces and supporting material
authorpaulson <lp15@cam.ac.uk>
Wed Apr 17 17:48:28 2019 +0100 (6 days ago)
changeset 701784900351361b0
parent 70177 b67bab2b132c
child 70179 269dcea7426c
Lindelöf spaces and supporting material
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Abstract_Topology_2.thy
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Function_Topology.thy
src/HOL/Analysis/Lindelof_Spaces.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Product_Topology.thy
src/HOL/Analysis/T1_Spaces.thy
src/HOL/Finite_Set.thy
src/HOL/Homology/Simplices.thy
src/HOL/Library/Countable_Set.thy
src/HOL/Library/Infinite_Set.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Tue Apr 16 19:50:30 2019 +0000
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Wed Apr 17 17:48:28 2019 +0100
     1.3 @@ -382,6 +382,10 @@
     1.4  lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
     1.5    by (simp add: closedin_def)
     1.6  
     1.7 +lemma open_in_topspace_empty:
     1.8 +   "topspace X = {} \<Longrightarrow> openin X S \<longleftrightarrow> S = {}"
     1.9 +  by (simp add: openin_closedin_eq)
    1.10 +
    1.11  lemma openin_imp_subset:
    1.12     "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
    1.13  by (metis Int_iff openin_subtopology subsetI)
    1.14 @@ -1756,6 +1760,26 @@
    1.15       "open_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
    1.16    unfolding open_map_def by (simp add: openin_subset)
    1.17  
    1.18 +lemma open_map_on_empty:
    1.19 +   "topspace X = {} \<Longrightarrow> open_map X Y f"
    1.20 +  by (metis empty_iff imageE in_mono open_map_def openin_subopen openin_subset)
    1.21 +
    1.22 +lemma closed_map_on_empty:
    1.23 +   "topspace X = {} \<Longrightarrow> closed_map X Y f"
    1.24 +  by (simp add: closed_map_def closedin_topspace_empty)
    1.25 +
    1.26 +lemma closed_map_const:
    1.27 +   "closed_map X Y (\<lambda>x. c) \<longleftrightarrow> topspace X = {} \<or> closedin Y {c}"
    1.28 +proof (cases "topspace X = {}")
    1.29 +  case True
    1.30 +  then show ?thesis
    1.31 +    by (simp add: closed_map_on_empty)
    1.32 +next
    1.33 +  case False
    1.34 +  then show ?thesis
    1.35 +    by (auto simp: closed_map_def image_constant_conv)
    1.36 +qed
    1.37 +
    1.38  lemma open_map_imp_subset:
    1.39      "\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
    1.40    by (meson order_trans open_map_imp_subset_topspace subset_image_iff)
    1.41 @@ -3220,6 +3244,10 @@
    1.42    unfolding compact_space_alt
    1.43    using openin_subset by fastforce
    1.44  
    1.45 +lemma compactinD:
    1.46 +  "\<lbrakk>compactin X S; \<And>U. U \<in> \<U> \<Longrightarrow> openin X U; S \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow> \<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>"
    1.47 +  by (auto simp: compactin_def)
    1.48 +
    1.49  lemma compactin_euclidean_iff [simp]: "compactin euclidean S \<longleftrightarrow> compact S"
    1.50    by (simp add: compact_eq_Heine_Borel compactin_def) meson
    1.51  
    1.52 @@ -3229,7 +3257,7 @@
    1.53    have eq: "(\<forall>U \<in> \<U>. \<exists>Y. openin X Y \<and> U = Y \<inter> S) \<longleftrightarrow> \<U> \<subseteq> (\<lambda>Y. Y \<inter> S) ` {y. openin X y}" for \<U>
    1.54      by auto
    1.55    show ?thesis
    1.56 -    by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image exists_finite_subset_image)
    1.57 +    by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image ex_finite_subset_image)
    1.58  qed
    1.59  
    1.60  lemma compactin_subspace: "compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> compact_space (subtopology X S)"
    1.61 @@ -3411,7 +3439,7 @@
    1.62        by (auto simp: \<V>_def)
    1.63      moreover assume [unfolded compact_space_alt, rule_format, of \<V>]: "compact_space X"
    1.64      ultimately obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<U>" "topspace X \<subseteq> topspace X - \<Inter>\<F>"
    1.65 -      by (auto simp: exists_finite_subset_image \<V>_def)
    1.66 +      by (auto simp: ex_finite_subset_image \<V>_def)
    1.67      moreover have "\<F> \<noteq> {}"
    1.68        using \<F> \<open>topspace X \<noteq> {}\<close> by blast
    1.69      ultimately show "False"
    1.70 @@ -3645,7 +3673,7 @@
    1.71     "embedding_map X (subtopology Y S) f \<longleftrightarrow> embedding_map X Y f \<and> f ` (topspace X) \<subseteq> S"
    1.72    apply (auto simp: embedding_map_def subtopology_subtopology Int_absorb1)
    1.73      apply (metis (no_types) homeomorphic_imp_surjective_map subtopology_subtopology subtopology_topspace topspace_subtopology)
    1.74 -  apply (simp add: continuous_map_def homeomorphic_eq_everything_map topspace_subtopology)
    1.75 +  apply (simp add: continuous_map_def homeomorphic_eq_everything_map)
    1.76    done
    1.77  
    1.78  lemma injective_open_imp_embedding_map:
    1.79 @@ -3653,7 +3681,7 @@
    1.80    unfolding embedding_map_def
    1.81    apply (rule bijective_open_imp_homeomorphic_map)
    1.82    using continuous_map_in_subtopology apply blast
    1.83 -    apply (auto simp: continuous_map_in_subtopology open_map_into_subtopology topspace_subtopology continuous_map)
    1.84 +    apply (auto simp: continuous_map_in_subtopology open_map_into_subtopology continuous_map)
    1.85    done
    1.86  
    1.87  lemma injective_closed_imp_embedding_map:
    1.88 @@ -3661,7 +3689,7 @@
    1.89    unfolding embedding_map_def
    1.90    apply (rule bijective_closed_imp_homeomorphic_map)
    1.91       apply (simp_all add: continuous_map_into_subtopology closed_map_into_subtopology)
    1.92 -  apply (simp add: continuous_map inf.absorb_iff2 topspace_subtopology)
    1.93 +  apply (simp add: continuous_map inf.absorb_iff2)
    1.94    done
    1.95  
    1.96  lemma embedding_map_imp_homeomorphic_space:
    1.97 @@ -3669,6 +3697,11 @@
    1.98    unfolding embedding_map_def
    1.99    using homeomorphic_space by blast
   1.100  
   1.101 +lemma embedding_imp_closed_map:
   1.102 +   "\<lbrakk>embedding_map X Y f; closedin Y (f ` topspace X)\<rbrakk> \<Longrightarrow> closed_map X Y f"
   1.103 +  unfolding closed_map_def
   1.104 +  by (auto simp: closedin_closed_subtopology embedding_map_def homeomorphic_map_closedness_eq)
   1.105 +
   1.106  
   1.107  subsection\<open>Retraction and section maps\<close>
   1.108  
   1.109 @@ -4341,5 +4374,235 @@
   1.110    ultimately show "g x \<in> topspace (pullback_topology A f T2)"
   1.111      unfolding topspace_pullback_topology by blast
   1.112  qed
   1.113 +subsection\<open>Proper maps (not a priori assumed continuous) \<close>
   1.114 +
   1.115 +definition proper_map
   1.116 +  where
   1.117 + "proper_map X Y f \<equiv>
   1.118 +        closed_map X Y f \<and> (\<forall>y \<in> topspace Y. compactin X {x \<in> topspace X. f x = y})"
   1.119 +
   1.120 +lemma proper_imp_closed_map:
   1.121 +   "proper_map X Y f \<Longrightarrow> closed_map X Y f"
   1.122 +  by (simp add: proper_map_def)
   1.123 +
   1.124 +lemma proper_map_imp_subset_topspace:
   1.125 +   "proper_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
   1.126 +  by (simp add: closed_map_imp_subset_topspace proper_map_def)
   1.127 +
   1.128 +lemma closed_injective_imp_proper_map:
   1.129 +  assumes f: "closed_map X Y f" and inj: "inj_on f (topspace X)"
   1.130 +  shows "proper_map X Y f"
   1.131 +  unfolding proper_map_def
   1.132 +proof (clarsimp simp: f)
   1.133 +  show "compactin X {x \<in> topspace X. f x = y}"
   1.134 +    if "y \<in> topspace Y" for y
   1.135 +  proof -
   1.136 +    have "{x \<in> topspace X. f x = y} = {} \<or> (\<exists>a \<in> topspace X. {x \<in> topspace X. f x = y} = {a})"
   1.137 +      using inj_on_eq_iff [OF inj] by auto
   1.138 +    then show ?thesis
   1.139 +      using that by (metis (no_types, lifting) compactin_empty compactin_sing)
   1.140 +  qed
   1.141 +qed
   1.142 +
   1.143 +lemma injective_imp_proper_eq_closed_map:
   1.144 +   "inj_on f (topspace X) \<Longrightarrow> (proper_map X Y f \<longleftrightarrow> closed_map X Y f)"
   1.145 +  using closed_injective_imp_proper_map proper_imp_closed_map by blast
   1.146 +
   1.147 +lemma homeomorphic_imp_proper_map:
   1.148 +   "homeomorphic_map X Y f \<Longrightarrow> proper_map X Y f"
   1.149 +  by (simp add: closed_injective_imp_proper_map homeomorphic_eq_everything_map)
   1.150 +
   1.151 +lemma compactin_proper_map_preimage:
   1.152 +  assumes f: "proper_map X Y f" and "compactin Y K"
   1.153 +  shows "compactin X {x. x \<in> topspace X \<and> f x \<in> K}"
   1.154 +proof -
   1.155 +  have "f ` (topspace X) \<subseteq> topspace Y"
   1.156 +    by (simp add: f proper_map_imp_subset_topspace)
   1.157 +  have *: "\<And>y. y \<in> topspace Y \<Longrightarrow> compactin X {x \<in> topspace X. f x = y}"
   1.158 +    using f by (auto simp: proper_map_def)
   1.159 +  show ?thesis
   1.160 +    unfolding compactin_def
   1.161 +  proof clarsimp
   1.162 +    show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> {x \<in> topspace X. f x \<in> K} \<subseteq> \<Union>\<F>"
   1.163 +      if \<U>: "\<forall>U\<in>\<U>. openin X U" and sub: "{x \<in> topspace X. f x \<in> K} \<subseteq> \<Union>\<U>"
   1.164 +      for \<U>
   1.165 +    proof -
   1.166 +      have "\<forall>y \<in> K. \<exists>\<V>. finite \<V> \<and> \<V> \<subseteq> \<U>  \<and> {x \<in> topspace X. f x = y} \<subseteq> \<Union>\<V>"
   1.167 +      proof
   1.168 +        fix y
   1.169 +        assume "y \<in> K"
   1.170 +        then have "compactin X {x \<in> topspace X. f x = y}"
   1.171 +          by (metis "*" \<open>compactin Y K\<close> compactin_subspace subsetD)
   1.172 +        with \<open>y \<in> K\<close> show "\<exists>\<V>. finite \<V> \<and> \<V> \<subseteq> \<U>  \<and> {x \<in> topspace X. f x = y} \<subseteq> \<Union>\<V>"
   1.173 +          unfolding compactin_def using \<U> sub by fastforce
   1.174 +      qed
   1.175 +      then obtain \<V> where \<V>: "\<And>y. y \<in> K \<Longrightarrow> finite (\<V> y) \<and> \<V> y \<subseteq> \<U>  \<and> {x \<in> topspace X. f x = y} \<subseteq> \<Union>(\<V> y)"
   1.176 +        by (metis (full_types))
   1.177 +      define F where "F \<equiv> \<lambda>y. topspace Y - f ` (topspace X - \<Union>(\<V> y))"
   1.178 +      have "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> F ` K \<and> K \<subseteq> \<Union>\<F>"
   1.179 +      proof (rule compactinD [OF \<open>compactin Y K\<close>])
   1.180 +        have "\<And>x. x \<in> K \<Longrightarrow> closedin Y (f ` (topspace X - \<Union>(\<V> x)))"
   1.181 +          using f unfolding proper_map_def closed_map_def
   1.182 +          by (meson \<U> \<V> openin_Union openin_closedin_eq subsetD)
   1.183 +        then show "openin Y U" if "U \<in> F ` K" for U
   1.184 +          using that by (auto simp: F_def)
   1.185 +        show "K \<subseteq> \<Union>(F ` K)"
   1.186 +          using \<V> \<open>compactin Y K\<close> unfolding F_def compactin_def by fastforce
   1.187 +      qed
   1.188 +      then obtain J where "finite J" "J \<subseteq> K" and J: "K \<subseteq> \<Union>(F ` J)"
   1.189 +        by (auto simp: ex_finite_subset_image)
   1.190 +      show ?thesis
   1.191 +        unfolding F_def
   1.192 +      proof (intro exI conjI)
   1.193 +        show "finite (\<Union>(\<V> ` J))"
   1.194 +          using \<V> \<open>J \<subseteq> K\<close> \<open>finite J\<close> by blast
   1.195 +        show "\<Union>(\<V> ` J) \<subseteq> \<U>"
   1.196 +          using \<V> \<open>J \<subseteq> K\<close> by blast
   1.197 +        show "{x \<in> topspace X. f x \<in> K} \<subseteq> \<Union>(\<Union>(\<V> ` J))"
   1.198 +          using J \<open>J \<subseteq> K\<close> unfolding F_def by auto
   1.199 +      qed
   1.200 +    qed
   1.201 +  qed
   1.202 +qed
   1.203 +
   1.204 +
   1.205 +lemma compact_space_proper_map_preimage:
   1.206 +  assumes f: "proper_map X Y f" and fim: "f ` (topspace X) = topspace Y" and "compact_space Y"
   1.207 +  shows "compact_space X"
   1.208 +proof -
   1.209 +  have eq: "topspace X = {x \<in> topspace X. f x \<in> topspace Y}"
   1.210 +    using fim by blast
   1.211 +  moreover have "compactin Y (topspace Y)"
   1.212 +    using \<open>compact_space Y\<close> compact_space_def by auto
   1.213 +  ultimately show ?thesis
   1.214 +    unfolding compact_space_def
   1.215 +    using eq f compactin_proper_map_preimage by fastforce
   1.216 +qed
   1.217 +
   1.218 +lemma proper_map_alt:
   1.219 +   "proper_map X Y f \<longleftrightarrow>
   1.220 +    closed_map X Y f \<and> (\<forall>K. compactin Y K \<longrightarrow> compactin X {x. x \<in> topspace X \<and> f x \<in> K})"
   1.221 +  proof (intro iffI conjI allI impI)
   1.222 +  show "compactin X {x \<in> topspace X. f x \<in> K}"
   1.223 +    if "proper_map X Y f" and "compactin Y K" for K
   1.224 +    using that by (simp add: compactin_proper_map_preimage)
   1.225 +  show "proper_map X Y f"
   1.226 +    if f: "closed_map X Y f \<and> (\<forall>K. compactin Y K \<longrightarrow> compactin X {x \<in> topspace X. f x \<in> K})"
   1.227 +  proof -
   1.228 +    have "compactin X {x \<in> topspace X. f x = y}" if "y \<in> topspace Y" for y
   1.229 +    proof -
   1.230 +      have "compactin X {x \<in> topspace X. f x \<in> {y}}"
   1.231 +        using f compactin_sing that by fastforce
   1.232 +      then show ?thesis
   1.233 +        by auto
   1.234 +    qed
   1.235 +    with f show ?thesis
   1.236 +      by (auto simp: proper_map_def)
   1.237 +  qed
   1.238 +qed (simp add: proper_imp_closed_map)
   1.239 +
   1.240 +lemma proper_map_on_empty:
   1.241 +   "topspace X = {} \<Longrightarrow> proper_map X Y f"
   1.242 +  by (auto simp: proper_map_def closed_map_on_empty)
   1.243 +
   1.244 +lemma proper_map_id [simp]:
   1.245 +   "proper_map X X id"
   1.246 +proof (clarsimp simp: proper_map_alt closed_map_id)
   1.247 +  fix K
   1.248 +  assume K: "compactin X K"
   1.249 +  then have "{a \<in> topspace X. a \<in> K} = K"
   1.250 +    by (simp add: compactin_subspace subset_antisym subset_iff)
   1.251 +  then show "compactin X {a \<in> topspace X. a \<in> K}"
   1.252 +    using K by auto
   1.253 +qed
   1.254 +
   1.255 +lemma proper_map_compose:
   1.256 +  assumes "proper_map X Y f" "proper_map Y Z g"
   1.257 +  shows "proper_map X Z (g \<circ> f)"
   1.258 +proof -
   1.259 +  have "closed_map X Y f" and f: "\<And>K. compactin Y K \<Longrightarrow> compactin X {x \<in> topspace X. f x \<in> K}"
   1.260 +    and "closed_map Y Z g" and g: "\<And>K. compactin Z K \<Longrightarrow> compactin Y {x \<in> topspace Y. g x \<in> K}"
   1.261 +    using assms by (auto simp: proper_map_alt)
   1.262 +  show ?thesis
   1.263 +    unfolding proper_map_alt
   1.264 +  proof (intro conjI allI impI)
   1.265 +    show "closed_map X Z (g \<circ> f)"
   1.266 +      using \<open>closed_map X Y f\<close> \<open>closed_map Y Z g\<close> closed_map_compose by blast
   1.267 +    have "{x \<in> topspace X. g (f x) \<in> K} = {x \<in> topspace X. f x \<in> {b \<in> topspace Y. g b \<in> K}}" for K
   1.268 +      using \<open>closed_map X Y f\<close> closed_map_imp_subset_topspace by blast
   1.269 +    then show "compactin X {x \<in> topspace X. (g \<circ> f) x \<in> K}"
   1.270 +      if "compactin Z K" for K
   1.271 +      using f [OF g [OF that]] by auto
   1.272 +  qed
   1.273 +qed
   1.274 +
   1.275 +lemma proper_map_const:
   1.276 +   "proper_map X Y (\<lambda>x. c) \<longleftrightarrow> compact_space X \<and> (topspace X = {} \<or> closedin Y {c})"
   1.277 +proof (cases "topspace X = {}")
   1.278 +  case True
   1.279 +  then show ?thesis
   1.280 +    by (simp add: compact_space_topspace_empty proper_map_on_empty)
   1.281 +next
   1.282 +  case False
   1.283 +  have *: "compactin X {x \<in> topspace X. c = y}" if "compact_space X" for y
   1.284 +  proof (cases "c = y")
   1.285 +    case True
   1.286 +    then show ?thesis
   1.287 +      using compact_space_def \<open>compact_space X\<close> by auto
   1.288 +  qed auto
   1.289 +  then show ?thesis
   1.290 +    using closed_compactin closedin_subset
   1.291 +    by (force simp: False proper_map_def closed_map_const compact_space_def)
   1.292 +qed
   1.293 +
   1.294 +lemma proper_map_inclusion:
   1.295 +   "s \<subseteq> topspace X
   1.296 +        \<Longrightarrow> proper_map (subtopology X s) X id \<longleftrightarrow> closedin X s \<and> (\<forall>k. compactin X k \<longrightarrow> compactin X (s \<inter> k))"
   1.297 +  by (auto simp: proper_map_alt closed_map_inclusion_eq inf.absorb_iff2 Collect_conj_eq compactin_subtopology intro: closed_Int_compactin)
   1.298 +
   1.299 +
   1.300 +subsection\<open>Perfect maps (proper, continuous and surjective)\<close>
   1.301 +
   1.302 +definition perfect_map 
   1.303 +  where "perfect_map X Y f \<equiv> continuous_map X Y f \<and> proper_map X Y f \<and> f ` (topspace X) = topspace Y"
   1.304 +
   1.305 +lemma homeomorphic_imp_perfect_map:
   1.306 +   "homeomorphic_map X Y f \<Longrightarrow> perfect_map X Y f"
   1.307 +  by (simp add: homeomorphic_eq_everything_map homeomorphic_imp_proper_map perfect_map_def)
   1.308 +
   1.309 +lemma perfect_imp_quotient_map:
   1.310 +   "perfect_map X Y f \<Longrightarrow> quotient_map X Y f"
   1.311 +  by (simp add: continuous_closed_imp_quotient_map perfect_map_def proper_map_def)
   1.312 +
   1.313 +lemma homeomorphic_eq_injective_perfect_map:
   1.314 +   "homeomorphic_map X Y f \<longleftrightarrow> perfect_map X Y f \<and> inj_on f (topspace X)"
   1.315 +  using homeomorphic_imp_perfect_map homeomorphic_map_def perfect_imp_quotient_map by blast
   1.316 +
   1.317 +lemma perfect_injective_eq_homeomorphic_map:
   1.318 +   "perfect_map X Y f \<and> inj_on f (topspace X) \<longleftrightarrow> homeomorphic_map X Y f"
   1.319 +  by (simp add: homeomorphic_eq_injective_perfect_map)
   1.320 +
   1.321 +lemma perfect_map_id [simp]: "perfect_map X X id"
   1.322 +  by (simp add: homeomorphic_imp_perfect_map)
   1.323 +
   1.324 +lemma perfect_map_compose:
   1.325 +   "\<lbrakk>perfect_map X Y f; perfect_map Y Z g\<rbrakk> \<Longrightarrow> perfect_map X Z (g \<circ> f)"
   1.326 +  by (meson continuous_map_compose perfect_imp_quotient_map perfect_map_def proper_map_compose quotient_map_compose_eq quotient_map_def)
   1.327 +
   1.328 +lemma perfect_imp_continuous_map:
   1.329 +   "perfect_map X Y f \<Longrightarrow> continuous_map X Y f"
   1.330 +  using perfect_map_def by blast
   1.331 +
   1.332 +lemma perfect_imp_closed_map:
   1.333 +   "perfect_map X Y f \<Longrightarrow> closed_map X Y f"
   1.334 +  by (simp add: perfect_map_def proper_map_def)
   1.335 +
   1.336 +lemma perfect_imp_proper_map:
   1.337 +   "perfect_map X Y f \<Longrightarrow> proper_map X Y f"
   1.338 +  by (simp add: perfect_map_def)
   1.339 +
   1.340 +lemma perfect_imp_surjective_map:
   1.341 +   "perfect_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
   1.342 +  by (simp add: perfect_map_def)
   1.343  
   1.344  end
     2.1 --- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Apr 16 19:50:30 2019 +0000
     2.2 +++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Apr 17 17:48:28 2019 +0100
     2.3 @@ -1107,7 +1107,7 @@
     2.4      "\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S"
     2.5    by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
     2.6  
     2.7 -lemma retraction_imp_quotient_map:
     2.8 +lemma retraction_openin_vimage_iff:
     2.9    "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
    2.10    if retraction: "retraction S T r" and "U \<subseteq> T"
    2.11    using retraction apply (rule retractionE)
     3.1 --- a/src/HOL/Analysis/Analysis.thy	Tue Apr 16 19:50:30 2019 +0000
     3.2 +++ b/src/HOL/Analysis/Analysis.thy	Wed Apr 17 17:48:28 2019 +0100
     3.3 @@ -29,7 +29,7 @@
     3.4    Bounded_Continuous_Function
     3.5    Abstract_Topology
     3.6    Product_Topology
     3.7 -  T1_Spaces
     3.8 +  Lindelof_Spaces
     3.9    Infinite_Products
    3.10    Infinite_Set_Sum
    3.11    Weierstrass_Theorems
     4.1 --- a/src/HOL/Analysis/Function_Topology.thy	Tue Apr 16 19:50:30 2019 +0000
     4.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Wed Apr 17 17:48:28 2019 +0100
     4.3 @@ -1410,7 +1410,7 @@
     4.4      ultimately obtain \<C>' where "finite \<C>'" "\<C>' \<subseteq> \<B>'" "U \<subseteq> \<Union>\<C>'"
     4.5        using fin [of \<B>'] \<open>topspace X = U\<close> \<open>U \<subseteq> \<Union>\<B>\<close> by blast
     4.6      then show ?thesis
     4.7 -      unfolding \<B>' exists_finite_subset_image \<open>topspace X = U\<close> by auto
     4.8 +      unfolding \<B>' ex_finite_subset_image \<open>topspace X = U\<close> by auto
     4.9    qed
    4.10    show ?thesis
    4.11      apply (rule Alexander_subbase [where \<B> = "Collect ((\<lambda>x. x \<in> \<B>) relative_to (topspace X))"])
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Analysis/Lindelof_Spaces.thy	Wed Apr 17 17:48:28 2019 +0100
     5.3 @@ -0,0 +1,274 @@
     5.4 +section\<open>Lindelof spaces\<close>
     5.5 +
     5.6 +theory Lindelof_Spaces
     5.7 +imports T1_Spaces
     5.8 +begin
     5.9 +
    5.10 +definition Lindelof_space where
    5.11 +  "Lindelof_space X \<equiv>
    5.12 +        \<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> \<Union>\<U> = topspace X
    5.13 +            \<longrightarrow> (\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> \<Union>\<V> = topspace X)"
    5.14 +
    5.15 +lemma Lindelof_spaceD:
    5.16 +  "\<lbrakk>Lindelof_space X; \<And>U. U \<in> \<U> \<Longrightarrow> openin X U; \<Union>\<U> = topspace X\<rbrakk>
    5.17 +  \<Longrightarrow> \<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> \<Union>\<V> = topspace X"
    5.18 +  by (auto simp: Lindelof_space_def)
    5.19 +
    5.20 +lemma Lindelof_space_alt:
    5.21 +   "Lindelof_space X \<longleftrightarrow>
    5.22 +        (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<subseteq> \<Union>\<U>
    5.23 +             \<longrightarrow> (\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<V>))"
    5.24 +  unfolding Lindelof_space_def
    5.25 +  using openin_subset by fastforce
    5.26 +
    5.27 +lemma compact_imp_Lindelof_space:
    5.28 +   "compact_space X \<Longrightarrow> Lindelof_space X"
    5.29 +  unfolding Lindelof_space_def compact_space
    5.30 +  by (meson uncountable_infinite)
    5.31 +
    5.32 +lemma Lindelof_space_topspace_empty:
    5.33 +   "topspace X = {} \<Longrightarrow> Lindelof_space X"
    5.34 +  using compact_imp_Lindelof_space compact_space_topspace_empty by blast
    5.35 +
    5.36 +lemma Lindelof_space_Union:
    5.37 +  assumes \<U>: "countable \<U>" and lin: "\<And>U. U \<in> \<U> \<Longrightarrow> Lindelof_space (subtopology X U)"
    5.38 +  shows "Lindelof_space (subtopology X (\<Union>\<U>))"
    5.39 +proof -
    5.40 +  have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<F> \<and> \<Union>\<U> \<inter> \<Union>\<V> = topspace X \<inter> \<Union>\<U>"
    5.41 +    if \<F>: "\<F> \<subseteq> Collect (openin X)" and UF: "\<Union>\<U> \<inter> \<Union>\<F> = topspace X \<inter> \<Union>\<U>"
    5.42 +    for \<F>
    5.43 +  proof -
    5.44 +    have "\<And>U. \<lbrakk>U \<in> \<U>; U \<inter> \<Union>\<F> = topspace X \<inter> U\<rbrakk>
    5.45 +               \<Longrightarrow> \<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<F> \<and> U \<inter> \<Union>\<V> = topspace X \<inter> U"
    5.46 +      using lin \<F>
    5.47 +      unfolding Lindelof_space_def openin_subtopology_alt Ball_def subset_iff [symmetric]
    5.48 +      by (simp add: all_subset_image imp_conjL ex_countable_subset_image)
    5.49 +    then obtain g where g: "\<And>U. \<lbrakk>U \<in> \<U>; U \<inter> \<Union>\<F> = topspace X \<inter> U\<rbrakk>
    5.50 +                               \<Longrightarrow> countable (g U) \<and> (g U) \<subseteq> \<F> \<and> U \<inter> \<Union>(g U) = topspace X \<inter> U"
    5.51 +      by metis
    5.52 +    show ?thesis
    5.53 +    proof (intro exI conjI)
    5.54 +      show "countable (\<Union>(g ` \<U>))"
    5.55 +        using Int_commute UF g  by (fastforce intro: countable_UN [OF \<U>])
    5.56 +      show "\<Union>(g ` \<U>) \<subseteq> \<F>"
    5.57 +        using g UF by blast
    5.58 +      show "\<Union>\<U> \<inter> \<Union>(\<Union>(g ` \<U>)) = topspace X \<inter> \<Union>\<U>"
    5.59 +      proof
    5.60 +        show "\<Union>\<U> \<inter> \<Union>(\<Union>(g ` \<U>)) \<subseteq> topspace X \<inter> \<Union>\<U>"
    5.61 +          using g UF by blast
    5.62 +        show "topspace X \<inter> \<Union>\<U> \<subseteq> \<Union>\<U> \<inter> \<Union>(\<Union>(g ` \<U>))"
    5.63 +        proof clarsimp
    5.64 +          show "\<exists>y\<in>\<U>. \<exists>W\<in>g y. x \<in> W"
    5.65 +            if "x \<in> topspace X" "x \<in> V" "V \<in> \<U>" for x V
    5.66 +          proof -
    5.67 +            have "V \<inter> \<Union>\<F> = topspace X \<inter> V"
    5.68 +              using UF \<open>V \<in> \<U>\<close> by blast
    5.69 +            with that g [OF \<open>V \<in> \<U>\<close>]  show ?thesis by blast
    5.70 +          qed
    5.71 +        qed
    5.72 +      qed
    5.73 +    qed
    5.74 +  qed
    5.75 +  then show ?thesis
    5.76 +      unfolding Lindelof_space_def openin_subtopology_alt Ball_def subset_iff [symmetric]
    5.77 +      by (simp add: all_subset_image imp_conjL ex_countable_subset_image)
    5.78 +qed
    5.79 +
    5.80 +lemma countable_imp_Lindelof_space:
    5.81 +  assumes "countable(topspace X)"
    5.82 +  shows "Lindelof_space X"
    5.83 +proof -
    5.84 +  have "Lindelof_space (subtopology X (\<Union>x \<in> topspace X. {x}))"
    5.85 +  proof (rule Lindelof_space_Union)
    5.86 +    show "countable ((\<lambda>x. {x}) ` topspace X)"
    5.87 +      using assms by blast
    5.88 +    show "Lindelof_space (subtopology X U)"
    5.89 +      if "U \<in> (\<lambda>x. {x}) ` topspace X" for U
    5.90 +    proof -
    5.91 +      have "compactin X U"
    5.92 +        using that by force
    5.93 +      then show ?thesis
    5.94 +        by (meson compact_imp_Lindelof_space compact_space_subtopology)
    5.95 +    qed
    5.96 +  qed
    5.97 +  then show ?thesis
    5.98 +    by simp
    5.99 +qed
   5.100 +lemma Lindelof_space_subtopology:
   5.101 +   "Lindelof_space(subtopology X S) \<longleftrightarrow>
   5.102 +        (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<inter> S \<subseteq> \<Union>\<U>
   5.103 +            \<longrightarrow> (\<exists>V. countable V \<and> V \<subseteq> \<U> \<and> topspace X \<inter> S \<subseteq> \<Union>V))"
   5.104 +proof -
   5.105 +  have *: "(S \<inter> \<Union>\<U> = topspace X \<inter> S) = (topspace X \<inter> S \<subseteq> \<Union>\<U>)"
   5.106 +    if "\<And>x. x \<in> \<U> \<Longrightarrow> openin X x" for \<U>
   5.107 +    by (blast dest: openin_subset [OF that])
   5.108 +  moreover have "(\<V> \<subseteq> \<U> \<and> S \<inter> \<Union>\<V> = topspace X \<inter> S) = (\<V> \<subseteq> \<U> \<and> topspace X \<inter> S \<subseteq> \<Union>\<V>)"
   5.109 +    if "\<forall>x. x \<in> \<U> \<longrightarrow> openin X x" "topspace X \<inter> S \<subseteq> \<Union>\<U>" "countable \<V>" for \<U> \<V>
   5.110 +    using that * by blast
   5.111 +  ultimately show ?thesis
   5.112 +    unfolding Lindelof_space_def openin_subtopology_alt Ball_def
   5.113 +    apply (simp add: all_subset_image imp_conjL ex_countable_subset_image flip: subset_iff)
   5.114 +    apply (intro all_cong1 imp_cong ex_cong, auto)
   5.115 +    done
   5.116 +qed
   5.117 +
   5.118 +lemma Lindelof_space_subtopology_subset:
   5.119 +   "S \<subseteq> topspace X
   5.120 +        \<Longrightarrow> (Lindelof_space(subtopology X S) \<longleftrightarrow>
   5.121 +             (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> S \<subseteq> \<Union>\<U>
   5.122 +                 \<longrightarrow> (\<exists>V. countable V \<and> V \<subseteq> \<U> \<and> S \<subseteq> \<Union>V)))"
   5.123 +  by (metis Lindelof_space_subtopology topspace_subtopology topspace_subtopology_subset)
   5.124 +
   5.125 +lemma Lindelof_space_closedin_subtopology:
   5.126 +  assumes X: "Lindelof_space X" and clo: "closedin X S"
   5.127 +  shows "Lindelof_space (subtopology X S)"
   5.128 +proof -
   5.129 +  have "S \<subseteq> topspace X"
   5.130 +    by (simp add: clo closedin_subset)
   5.131 +  then show ?thesis
   5.132 +  proof (clarsimp simp add: Lindelof_space_subtopology_subset)
   5.133 +    show "\<exists>V. countable V \<and> V \<subseteq> \<F> \<and> S \<subseteq> \<Union>V"
   5.134 +      if "\<forall>U\<in>\<F>. openin X U" and "S \<subseteq> \<Union>\<F>" for \<F>
   5.135 +    proof -
   5.136 +      have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> insert (topspace X - S) \<F> \<and> \<Union>\<V> = topspace X"
   5.137 +      proof (rule Lindelof_spaceD [OF X, of "insert (topspace X - S) \<F>"])
   5.138 +        show "openin X U"
   5.139 +          if "U \<in> insert (topspace X - S) \<F>" for U
   5.140 +          using that \<open>\<forall>U\<in>\<F>. openin X U\<close> clo by blast
   5.141 +        show "\<Union>(insert (topspace X - S) \<F>) = topspace X"
   5.142 +          apply auto
   5.143 +          apply (meson in_mono openin_closedin_eq that(1))
   5.144 +          using UnionE \<open>S \<subseteq> \<Union>\<F>\<close> by auto
   5.145 +      qed
   5.146 +      then obtain \<V> where "countable \<V>" "\<V> \<subseteq> insert (topspace X - S) \<F>" "\<Union>\<V> = topspace X"
   5.147 +        by metis
   5.148 +      with \<open>S \<subseteq> topspace X\<close>
   5.149 +      show ?thesis
   5.150 +        by (rule_tac x="(\<V> - {topspace X - S})" in exI) auto
   5.151 +    qed
   5.152 +  qed
   5.153 +qed
   5.154 +
   5.155 +lemma Lindelof_space_continuous_map_image:
   5.156 +  assumes X: "Lindelof_space X" and f: "continuous_map X Y f" and fim: "f ` (topspace X) = topspace Y"
   5.157 +  shows "Lindelof_space Y"
   5.158 +proof -
   5.159 +  have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> \<Union>\<V> = topspace Y"
   5.160 +    if \<U>: "\<And>U. U \<in> \<U> \<Longrightarrow> openin Y U" and UU: "\<Union>\<U> = topspace Y" for \<U>
   5.161 +  proof -
   5.162 +    define \<V> where "\<V> \<equiv> (\<lambda>U. {x \<in> topspace X. f x \<in> U}) ` \<U>"
   5.163 +    have "\<And>V. V \<in> \<V> \<Longrightarrow> openin X V"
   5.164 +      unfolding \<V>_def using \<U> continuous_map f by fastforce
   5.165 +    moreover have "\<Union>\<V> = topspace X"
   5.166 +      unfolding \<V>_def using UU fim by fastforce
   5.167 +    ultimately have "\<exists>\<W>. countable \<W> \<and> \<W> \<subseteq> \<V> \<and> \<Union>\<W> = topspace X"
   5.168 +      using X by (simp add: Lindelof_space_def)
   5.169 +    then obtain \<C> where "countable \<C>" "\<C> \<subseteq> \<U>" and \<C>: "(\<Union>U\<in>\<C>. {x \<in> topspace X. f x \<in> U}) = topspace X"
   5.170 +      by (metis (no_types, lifting) \<V>_def countable_subset_image)
   5.171 +    moreover have "\<Union>\<C> = topspace Y"
   5.172 +    proof
   5.173 +      show "\<Union>\<C> \<subseteq> topspace Y"
   5.174 +        using UU \<C> \<open>\<C> \<subseteq> \<U>\<close> by fastforce
   5.175 +      have "y \<in> \<Union>\<C>" if "y \<in> topspace Y" for y
   5.176 +      proof -
   5.177 +        obtain x where "x \<in> topspace X" "y = f x"
   5.178 +          using that fim by (metis \<open>y \<in> topspace Y\<close> imageE)
   5.179 +        with \<C> show ?thesis by auto
   5.180 +      qed
   5.181 +      then show "topspace Y \<subseteq> \<Union>\<C>" by blast
   5.182 +    qed
   5.183 +    ultimately show ?thesis
   5.184 +      by blast
   5.185 +  qed
   5.186 +  then show ?thesis
   5.187 +    unfolding Lindelof_space_def
   5.188 +    by auto
   5.189 +qed
   5.190 +
   5.191 +lemma Lindelof_space_quotient_map_image:
   5.192 +   "\<lbrakk>quotient_map X Y q; Lindelof_space X\<rbrakk> \<Longrightarrow> Lindelof_space Y"
   5.193 +  by (meson Lindelof_space_continuous_map_image quotient_imp_continuous_map quotient_imp_surjective_map)
   5.194 +
   5.195 +lemma Lindelof_space_retraction_map_image:
   5.196 +   "\<lbrakk>retraction_map X Y r; Lindelof_space X\<rbrakk> \<Longrightarrow> Lindelof_space Y"
   5.197 +  using Abstract_Topology.retraction_imp_quotient_map Lindelof_space_quotient_map_image by blast
   5.198 +
   5.199 +lemma locally_finite_cover_of_Lindelof_space:
   5.200 +  assumes X: "Lindelof_space X" and UU: "topspace X \<subseteq> \<Union>\<U>" and fin: "locally_finite_in X \<U>"
   5.201 +  shows "countable \<U>"
   5.202 +proof -
   5.203 +  have UU_eq: "\<Union>\<U> = topspace X"
   5.204 +    by (meson UU fin locally_finite_in_def subset_antisym)
   5.205 +  obtain T where T: "\<And>x. x \<in> topspace X \<Longrightarrow> openin X (T x) \<and> x \<in> T x \<and> finite {U \<in> \<U>. U \<inter> T x \<noteq> {}}"
   5.206 +    using fin unfolding locally_finite_in_def by meson
   5.207 +  then obtain I where "countable I" "I \<subseteq> topspace X" and I: "topspace X \<subseteq> \<Union>(T ` I)"
   5.208 +    using X unfolding Lindelof_space_alt
   5.209 +    by (drule_tac x="image T (topspace X)" in spec) (auto simp: ex_countable_subset_image)
   5.210 +  show ?thesis
   5.211 +  proof (rule countable_subset)
   5.212 +    have "\<And>i. i \<in> I \<Longrightarrow> countable {U \<in> \<U>. U \<inter> T i \<noteq> {}}"
   5.213 +      using T
   5.214 +      by (meson \<open>I \<subseteq> topspace X\<close> in_mono uncountable_infinite)
   5.215 +    then show "countable (insert {} (\<Union>i\<in>I. {U \<in> \<U>. U \<inter> T i \<noteq> {}}))"
   5.216 +      by (simp add: \<open>countable I\<close>)
   5.217 +  qed (use UU_eq I in auto)
   5.218 +qed
   5.219 +
   5.220 +
   5.221 +lemma Lindelof_space_proper_map_preimage:
   5.222 +  assumes f: "proper_map X Y f" and Y: "Lindelof_space Y"
   5.223 +  shows "Lindelof_space X"
   5.224 +proof (clarsimp simp: Lindelof_space_alt)
   5.225 +  show "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<V>"
   5.226 +    if \<U>: "\<forall>U\<in>\<U>. openin X U" and sub_UU: "topspace X \<subseteq> \<Union>\<U>" for \<U>
   5.227 +  proof -
   5.228 +    have "\<exists>\<V>. finite \<V> \<and> \<V> \<subseteq> \<U> \<and> {x \<in> topspace X. f x = y} \<subseteq> \<Union>\<V>" if "y \<in> topspace Y" for y
   5.229 +    proof (rule compactinD)
   5.230 +      show "compactin X {x \<in> topspace X. f x = y}"
   5.231 +        using f proper_map_def that by fastforce
   5.232 +    qed (use sub_UU \<U> in auto)
   5.233 +    then obtain \<V> where \<V>: "\<And>y. y \<in> topspace Y \<Longrightarrow> finite (\<V> y) \<and> \<V> y \<subseteq> \<U> \<and> {x \<in> topspace X. f x = y} \<subseteq> \<Union>(\<V> y)"
   5.234 +      by meson
   5.235 +    define \<W> where "\<W> \<equiv> (\<lambda>y. topspace Y - image f (topspace X - \<Union>(\<V> y))) ` topspace Y"
   5.236 +    have "\<forall>U \<in> \<W>. openin Y U"
   5.237 +      using f \<U> \<V> unfolding \<W>_def proper_map_def closed_map_def
   5.238 +      by (simp add: closedin_diff openin_Union openin_diff subset_iff)
   5.239 +    moreover have "topspace Y \<subseteq> \<Union>\<W>"
   5.240 +      using \<V> unfolding \<W>_def by clarsimp fastforce
   5.241 +    ultimately have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<W> \<and> topspace Y \<subseteq> \<Union>\<V>"
   5.242 +      using Y by (simp add: Lindelof_space_alt)
   5.243 +    then obtain I where "countable I" "I \<subseteq> topspace Y"
   5.244 +      and I: "topspace Y \<subseteq> (\<Union>i\<in>I. topspace Y - f ` (topspace X - \<Union>(\<V> i)))"
   5.245 +      unfolding \<W>_def ex_countable_subset_image by metis
   5.246 +    show ?thesis
   5.247 +    proof (intro exI conjI)
   5.248 +      have "\<And>i. i \<in> I \<Longrightarrow> countable (\<V> i)"
   5.249 +        by (meson \<V> \<open>I \<subseteq> topspace Y\<close> in_mono uncountable_infinite)
   5.250 +      with \<open>countable I\<close> show "countable (\<Union>(\<V> ` I))"
   5.251 +        by auto
   5.252 +      show "\<Union>(\<V> ` I) \<subseteq> \<U>"
   5.253 +        using \<V> \<open>I \<subseteq> topspace Y\<close> by fastforce
   5.254 +      show "topspace X \<subseteq> \<Union>(\<Union>(\<V> ` I))"
   5.255 +      proof
   5.256 +        show "x \<in> \<Union> (\<Union> (\<V> ` I))" if "x \<in> topspace X" for x
   5.257 +        proof -
   5.258 +          have "f x \<in> topspace Y"
   5.259 +            by (meson f image_subset_iff proper_map_imp_subset_topspace that)
   5.260 +          then show ?thesis
   5.261 +            using that I by auto
   5.262 +        qed
   5.263 +      qed
   5.264 +    qed
   5.265 +  qed
   5.266 +qed
   5.267 +
   5.268 +lemma Lindelof_space_perfect_map_image:
   5.269 +   "\<lbrakk>Lindelof_space X; perfect_map X Y f\<rbrakk> \<Longrightarrow> Lindelof_space Y"
   5.270 +  using Lindelof_space_quotient_map_image perfect_imp_quotient_map by blast
   5.271 +
   5.272 +lemma Lindelof_space_perfect_map_image_eq:
   5.273 +   "perfect_map X Y f \<Longrightarrow> Lindelof_space X \<longleftrightarrow> Lindelof_space Y"
   5.274 +  using Lindelof_space_perfect_map_image Lindelof_space_proper_map_preimage perfect_map_def by blast
   5.275 +
   5.276 +end
   5.277 +
     6.1 --- a/src/HOL/Analysis/Path_Connected.thy	Tue Apr 16 19:50:30 2019 +0000
     6.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Wed Apr 17 17:48:28 2019 +0100
     6.3 @@ -2109,6 +2109,14 @@
     6.4      by (metis Int_absorb1 mem_Collect_eq path_component_of_equiv path_component_of_subset_topspace topspace_subtopology)
     6.5  qed
     6.6  
     6.7 +lemma path_connectedin_euclidean [simp]:
     6.8 +   "path_connectedin euclidean S \<longleftrightarrow> path_connected S"
     6.9 +  by (auto simp: path_connectedin_def path_connected_space_iff_path_component path_connected_component)
    6.10 +
    6.11 +lemma path_connected_space_euclidean_subtopology [simp]:
    6.12 +   "path_connected_space(subtopology euclidean S) \<longleftrightarrow> path_connected S"
    6.13 +  using path_connectedin_topspace by force
    6.14 +
    6.15  lemma Union_path_components_of:
    6.16       "\<Union>(path_components_of X) = topspace X"
    6.17    by (auto simp: path_components_of_def path_component_of_equiv)
     7.1 --- a/src/HOL/Analysis/Product_Topology.thy	Tue Apr 16 19:50:30 2019 +0000
     7.2 +++ b/src/HOL/Analysis/Product_Topology.thy	Wed Apr 17 17:48:28 2019 +0100
     7.3 @@ -455,6 +455,15 @@
     7.4    unfolding homeomorphic_maps_def continuous_map_prod_top
     7.5    by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
     7.6  
     7.7 +lemma homeomorphic_maps_swap:
     7.8 +   "homeomorphic_maps (prod_topology X Y) (prod_topology Y X)
     7.9 +                          (\<lambda>(x,y). (y,x)) (\<lambda>(y,x). (x,y))"
    7.10 +  by (auto simp: homeomorphic_maps_def case_prod_unfold continuous_map_fst continuous_map_pairedI continuous_map_snd)
    7.11 +
    7.12 +lemma homeomorphic_map_swap:
    7.13 +   "homeomorphic_map (prod_topology X Y) (prod_topology Y X) (\<lambda>(x,y). (y,x))"
    7.14 +  using homeomorphic_map_maps homeomorphic_maps_swap by metis
    7.15 +
    7.16  lemma embedding_map_graph:
    7.17     "embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
    7.18      (is "?lhs = ?rhs")
    7.19 @@ -474,7 +483,7 @@
    7.20      unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def
    7.21      by (rule_tac x=fst in exI)
    7.22         (auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology
    7.23 -                   continuous_map_fst topspace_subtopology)
    7.24 +                   continuous_map_fst)
    7.25  qed
    7.26  
    7.27  lemma homeomorphic_space_prod_topology:
     8.1 --- a/src/HOL/Analysis/T1_Spaces.thy	Tue Apr 16 19:50:30 2019 +0000
     8.2 +++ b/src/HOL/Analysis/T1_Spaces.thy	Wed Apr 17 17:48:28 2019 +0100
     8.3 @@ -475,6 +475,37 @@
     8.4      by (simp add: topology_eq)
     8.5  qed
     8.6  
     8.7 +lemma continuous_map_imp_closed_graph:
     8.8 +  assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y"
     8.9 +  shows "closedin (prod_topology X Y) ((\<lambda>x. (x,f x)) ` topspace X)"
    8.10 +  unfolding closedin_def
    8.11 +proof
    8.12 +  show "(\<lambda>x. (x, f x)) ` topspace X \<subseteq> topspace (prod_topology X Y)"
    8.13 +    using continuous_map_def f by fastforce
    8.14 +  show "openin (prod_topology X Y) (topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X)"
    8.15 +    unfolding openin_prod_topology_alt
    8.16 +  proof (intro allI impI)
    8.17 +    show "\<exists>U V. openin X U \<and> openin Y V \<and> x \<in> U \<and> y \<in> V \<and> U \<times> V \<subseteq> topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X"
    8.18 +      if "(x,y) \<in> topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X"
    8.19 +      for x y
    8.20 +    proof -
    8.21 +      have "x \<in> topspace X" "y \<in> topspace Y" "y \<noteq> f x"
    8.22 +        using that by auto
    8.23 +      moreover have "f x \<in> topspace Y"
    8.24 +        by (meson \<open>x \<in> topspace X\<close> continuous_map_def f)
    8.25 +      ultimately obtain U V where UV: "openin Y U" "openin Y V" "f x \<in> U" "y \<in> V" "disjnt U V"
    8.26 +        using Y Hausdorff_space_def by metis
    8.27 +      show ?thesis
    8.28 +      proof (intro exI conjI)
    8.29 +        show "openin X {x \<in> topspace X. f x \<in> U}"
    8.30 +          using \<open>openin Y U\<close> f openin_continuous_map_preimage by blast
    8.31 +        show "{x \<in> topspace X. f x \<in> U} \<times> V \<subseteq> topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X"
    8.32 +          using UV by (auto simp: disjnt_iff dest: openin_subset)
    8.33 +      qed (use UV \<open>x \<in> topspace X\<close> in auto)
    8.34 +    qed
    8.35 +  qed
    8.36 +qed
    8.37 +
    8.38  lemma continuous_imp_closed_map:
    8.39     "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f\<rbrakk> \<Longrightarrow> closed_map X Y f"
    8.40    by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin)
    8.41 @@ -529,8 +560,39 @@
    8.42    qed
    8.43  qed
    8.44  
    8.45 +lemma closed_map_paired_continuous_map_right:
    8.46 +   "\<lbrakk>continuous_map X Y f; Hausdorff_space Y\<rbrakk> \<Longrightarrow> closed_map X (prod_topology X Y) (\<lambda>x. (x,f x))"
    8.47 +  by (simp add: continuous_map_imp_closed_graph embedding_map_graph embedding_imp_closed_map)
    8.48  
    8.49 -lemma Hausdorff_space_euclidean: "Hausdorff_space (euclidean :: 'a::metric_space topology)"
    8.50 +lemma closed_map_paired_continuous_map_left:
    8.51 +  assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y"
    8.52 +  shows "closed_map X (prod_topology Y X) (\<lambda>x. (f x,x))"
    8.53 +proof -
    8.54 +  have eq: "(\<lambda>x. (f x,x)) = (\<lambda>(a,b). (b,a)) \<circ> (\<lambda>x. (x,f x))"
    8.55 +    by auto
    8.56 +  show ?thesis
    8.57 +    unfolding eq
    8.58 +  proof (rule closed_map_compose)
    8.59 +    show "closed_map X (prod_topology X Y) (\<lambda>x. (x, f x))"
    8.60 +      using Y closed_map_paired_continuous_map_right f by blast
    8.61 +    show "closed_map (prod_topology X Y) (prod_topology Y X) (\<lambda>(a, b). (b, a))"
    8.62 +      by (metis homeomorphic_map_swap homeomorphic_imp_closed_map)
    8.63 +  qed
    8.64 +qed
    8.65 +
    8.66 +lemma proper_map_paired_continuous_map_right:
    8.67 +   "\<lbrakk>continuous_map X Y f; Hausdorff_space Y\<rbrakk>
    8.68 +        \<Longrightarrow> proper_map X (prod_topology X Y) (\<lambda>x. (x,f x))"
    8.69 +  using closed_injective_imp_proper_map closed_map_paired_continuous_map_right
    8.70 +  by (metis (mono_tags, lifting) Pair_inject inj_onI)
    8.71 +
    8.72 +lemma proper_map_paired_continuous_map_left:
    8.73 +   "\<lbrakk>continuous_map X Y f; Hausdorff_space Y\<rbrakk>
    8.74 +        \<Longrightarrow> proper_map X (prod_topology Y X) (\<lambda>x. (f x,x))"
    8.75 +  using closed_injective_imp_proper_map closed_map_paired_continuous_map_left
    8.76 +  by (metis (mono_tags, lifting) Pair_inject inj_onI)
    8.77 +
    8.78 +lemma Hausdorff_space_euclidean [simp]: "Hausdorff_space (euclidean :: 'a::metric_space topology)"
    8.79  proof -
    8.80    have "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
    8.81      if "x \<noteq> y"
     9.1 --- a/src/HOL/Finite_Set.thy	Tue Apr 16 19:50:30 2019 +0000
     9.2 +++ b/src/HOL/Finite_Set.thy	Wed Apr 17 17:48:28 2019 +0100
     9.3 @@ -334,7 +334,7 @@
     9.4      using finite_subset_image [OF B] P by blast
     9.5  qed blast
     9.6  
     9.7 -lemma exists_finite_subset_image:
     9.8 +lemma ex_finite_subset_image:
     9.9    "(\<exists>B. finite B \<and> B \<subseteq> f ` A \<and> P B) \<longleftrightarrow> (\<exists>B. finite B \<and> B \<subseteq> A \<and> P (f ` B))"
    9.10  proof safe
    9.11    fix B :: "'a set"
    10.1 --- a/src/HOL/Homology/Simplices.thy	Tue Apr 16 19:50:30 2019 +0000
    10.2 +++ b/src/HOL/Homology/Simplices.thy	Wed Apr 17 17:48:28 2019 +0100
    10.3 @@ -2411,7 +2411,7 @@
    10.4      using compactin_standard_simplex [of p]
    10.5      unfolding compactin_def by force
    10.6    then obtain S where "finite S" and ssp: "S \<subseteq> standard_simplex p" "standard_simplex p \<subseteq> \<Union>(F ` S)"
    10.7 -    unfolding exists_finite_subset_image by (auto simp: exists_finite_subset_image)
    10.8 +    unfolding ex_finite_subset_image by (auto simp: ex_finite_subset_image)
    10.9    then have "S \<noteq> {}"
   10.10      by (auto simp: nonempty_standard_simplex)
   10.11    show ?thesis
    11.1 --- a/src/HOL/Library/Countable_Set.thy	Tue Apr 16 19:50:30 2019 +0000
    11.2 +++ b/src/HOL/Library/Countable_Set.thy	Wed Apr 17 17:48:28 2019 +0100
    11.3 @@ -195,6 +195,23 @@
    11.4  lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A"
    11.5    by (metis countable_image the_inv_into_onto)
    11.6  
    11.7 +lemma countable_image_inj_Int_vimage:
    11.8 +   "\<lbrakk>inj_on f S; countable A\<rbrakk> \<Longrightarrow> countable (S \<inter> f -` A)"
    11.9 +  by (meson countable_image_inj_on countable_subset image_subset_iff_subset_vimage inf_le2 inj_on_Int)
   11.10 +
   11.11 +lemma countable_image_inj_gen:
   11.12 +   "\<lbrakk>inj_on f S; countable A\<rbrakk> \<Longrightarrow> countable {x \<in> S. f x \<in> A}"
   11.13 +  using countable_image_inj_Int_vimage
   11.14 +  by (auto simp: vimage_def Collect_conj_eq)
   11.15 +
   11.16 +lemma countable_image_inj_eq:
   11.17 +   "inj_on f S \<Longrightarrow> countable(f ` S) \<longleftrightarrow> countable S"
   11.18 +  using countable_image_inj_on by blast
   11.19 +
   11.20 +lemma countable_image_inj:
   11.21 +   "\<lbrakk>countable A; inj f\<rbrakk> \<Longrightarrow> countable {x. f x \<in> A}"
   11.22 +  by (metis (mono_tags, lifting) countable_image_inj_eq countable_subset image_Collect_subsetI inj_on_inverseI the_inv_f_f)
   11.23 +
   11.24  lemma countable_UN[intro, simp]:
   11.25    fixes I :: "'i set" and A :: "'i => 'a set"
   11.26    assumes I: "countable I"
   11.27 @@ -320,6 +337,39 @@
   11.28    then show ?lhs by force
   11.29  qed
   11.30  
   11.31 +lemma ex_subset_image_inj:
   11.32 +   "(\<exists>T. T \<subseteq> f ` S \<and> P T) \<longleftrightarrow> (\<exists>T. T \<subseteq> S \<and> inj_on f T \<and> P (f ` T))"
   11.33 +  by (auto simp: subset_image_inj)
   11.34 +
   11.35 +lemma all_subset_image_inj:
   11.36 +   "(\<forall>T. T \<subseteq> f ` S \<longrightarrow> P T) \<longleftrightarrow> (\<forall>T. T \<subseteq> S \<and> inj_on f T \<longrightarrow> P(f ` T))"
   11.37 +  by (metis subset_image_inj)
   11.38 +
   11.39 +lemma ex_countable_subset_image_inj:
   11.40 +   "(\<exists>T. countable T \<and> T \<subseteq> f ` S \<and> P T) \<longleftrightarrow>
   11.41 +    (\<exists>T. countable T \<and> T \<subseteq> S \<and> inj_on f T \<and> P (f ` T))"
   11.42 +  by (metis countable_image_inj_eq subset_image_inj)
   11.43 +
   11.44 +lemma all_countable_subset_image_inj:
   11.45 +   "(\<forall>T. countable T \<and> T \<subseteq> f ` S \<longrightarrow> P T) \<longleftrightarrow> (\<forall>T. countable T \<and> T \<subseteq> S \<and> inj_on f T \<longrightarrow>P(f ` T))"
   11.46 +  by (metis countable_image_inj_eq subset_image_inj)
   11.47 +
   11.48 +lemma ex_countable_subset_image:
   11.49 +   "(\<exists>T. countable T \<and> T \<subseteq> f ` S \<and> P T) \<longleftrightarrow> (\<exists>T. countable T \<and> T \<subseteq> S \<and> P (f ` T))"
   11.50 +  by (metis countable_subset_image)
   11.51 +
   11.52 +lemma all_countable_subset_image:
   11.53 +   "(\<forall>T. countable T \<and> T \<subseteq> f ` S \<longrightarrow> P T) \<longleftrightarrow> (\<forall>T. countable T \<and> T \<subseteq> S \<longrightarrow> P(f ` T))"
   11.54 +  by (metis countable_subset_image)
   11.55 +
   11.56 +lemma countable_image_eq:
   11.57 +   "countable(f ` S) \<longleftrightarrow> (\<exists>T. countable T \<and> T \<subseteq> S \<and> f ` S = f ` T)"
   11.58 +  by (metis countable_image countable_image_inj_eq order_refl subset_image_inj)
   11.59 +
   11.60 +lemma countable_image_eq_inj:
   11.61 +   "countable(f ` S) \<longleftrightarrow> (\<exists>T. countable T \<and> T \<subseteq> S \<and> f ` S = f ` T \<and> inj_on f T)"
   11.62 +  by (metis countable_image_inj_eq order_refl subset_image_inj)
   11.63 +
   11.64  lemma infinite_countable_subset':
   11.65    assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C"
   11.66  proof -
    12.1 --- a/src/HOL/Library/Infinite_Set.thy	Tue Apr 16 19:50:30 2019 +0000
    12.2 +++ b/src/HOL/Library/Infinite_Set.thy	Wed Apr 17 17:48:28 2019 +0100
    12.3 @@ -8,6 +8,27 @@
    12.4    imports Main
    12.5  begin
    12.6  
    12.7 +lemma subset_image_inj:
    12.8 +  "S \<subseteq> f ` T \<longleftrightarrow> (\<exists>U. U \<subseteq> T \<and> inj_on f U \<and> S = f ` U)"
    12.9 +proof safe
   12.10 +  show "\<exists>U\<subseteq>T. inj_on f U \<and> S = f ` U"
   12.11 +    if "S \<subseteq> f ` T"
   12.12 +  proof -
   12.13 +    from that [unfolded subset_image_iff subset_iff]
   12.14 +    obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> x = f (g x)"
   12.15 +      unfolding image_iff by metis
   12.16 +    show ?thesis
   12.17 +    proof (intro exI conjI)
   12.18 +      show "g ` S \<subseteq> T"
   12.19 +        by (simp add: g image_subsetI)
   12.20 +      show "inj_on f (g ` S)"
   12.21 +        using g by (auto simp: inj_on_def)
   12.22 +      show "S = f ` (g ` S)"
   12.23 +        using g image_subset_iff by auto
   12.24 +    qed
   12.25 +  qed
   12.26 +qed blast
   12.27 +
   12.28  subsection \<open>The set of natural numbers is infinite\<close>
   12.29  
   12.30  lemma infinite_nat_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"