# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1555519708 -3600
# Node ID 4900351361b0df419fe1c413250918a9dbd68298
# Parent  b67bab2b132c0f4f7f24b7b309516db920b1c5d1
Lindelöf spaces and supporting material

diff -r b67bab2b132c -r 4900351361b0 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -382,6 +382,10 @@
 lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
   by (simp add: closedin_def)
 
+lemma open_in_topspace_empty:
+   "topspace X = {} \<Longrightarrow> openin X S \<longleftrightarrow> S = {}"
+  by (simp add: openin_closedin_eq)
+
 lemma openin_imp_subset:
    "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
 by (metis Int_iff openin_subtopology subsetI)
@@ -1756,6 +1760,26 @@
      "open_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
   unfolding open_map_def by (simp add: openin_subset)
 
+lemma open_map_on_empty:
+   "topspace X = {} \<Longrightarrow> open_map X Y f"
+  by (metis empty_iff imageE in_mono open_map_def openin_subopen openin_subset)
+
+lemma closed_map_on_empty:
+   "topspace X = {} \<Longrightarrow> closed_map X Y f"
+  by (simp add: closed_map_def closedin_topspace_empty)
+
+lemma closed_map_const:
+   "closed_map X Y (\<lambda>x. c) \<longleftrightarrow> topspace X = {} \<or> closedin Y {c}"
+proof (cases "topspace X = {}")
+  case True
+  then show ?thesis
+    by (simp add: closed_map_on_empty)
+next
+  case False
+  then show ?thesis
+    by (auto simp: closed_map_def image_constant_conv)
+qed
+
 lemma open_map_imp_subset:
     "\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
   by (meson order_trans open_map_imp_subset_topspace subset_image_iff)
@@ -3220,6 +3244,10 @@
   unfolding compact_space_alt
   using openin_subset by fastforce
 
+lemma compactinD:
+  "\<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>"
+  by (auto simp: compactin_def)
+
 lemma compactin_euclidean_iff [simp]: "compactin euclidean S \<longleftrightarrow> compact S"
   by (simp add: compact_eq_Heine_Borel compactin_def) meson
 
@@ -3229,7 +3257,7 @@
   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>
     by auto
   show ?thesis
-    by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image exists_finite_subset_image)
+    by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image ex_finite_subset_image)
 qed
 
 lemma compactin_subspace: "compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> compact_space (subtopology X S)"
@@ -3411,7 +3439,7 @@
       by (auto simp: \<V>_def)
     moreover assume [unfolded compact_space_alt, rule_format, of \<V>]: "compact_space X"
     ultimately obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<U>" "topspace X \<subseteq> topspace X - \<Inter>\<F>"
-      by (auto simp: exists_finite_subset_image \<V>_def)
+      by (auto simp: ex_finite_subset_image \<V>_def)
     moreover have "\<F> \<noteq> {}"
       using \<F> \<open>topspace X \<noteq> {}\<close> by blast
     ultimately show "False"
@@ -3645,7 +3673,7 @@
    "embedding_map X (subtopology Y S) f \<longleftrightarrow> embedding_map X Y f \<and> f ` (topspace X) \<subseteq> S"
   apply (auto simp: embedding_map_def subtopology_subtopology Int_absorb1)
     apply (metis (no_types) homeomorphic_imp_surjective_map subtopology_subtopology subtopology_topspace topspace_subtopology)
-  apply (simp add: continuous_map_def homeomorphic_eq_everything_map topspace_subtopology)
+  apply (simp add: continuous_map_def homeomorphic_eq_everything_map)
   done
 
 lemma injective_open_imp_embedding_map:
@@ -3653,7 +3681,7 @@
   unfolding embedding_map_def
   apply (rule bijective_open_imp_homeomorphic_map)
   using continuous_map_in_subtopology apply blast
-    apply (auto simp: continuous_map_in_subtopology open_map_into_subtopology topspace_subtopology continuous_map)
+    apply (auto simp: continuous_map_in_subtopology open_map_into_subtopology continuous_map)
   done
 
 lemma injective_closed_imp_embedding_map:
@@ -3661,7 +3689,7 @@
   unfolding embedding_map_def
   apply (rule bijective_closed_imp_homeomorphic_map)
      apply (simp_all add: continuous_map_into_subtopology closed_map_into_subtopology)
-  apply (simp add: continuous_map inf.absorb_iff2 topspace_subtopology)
+  apply (simp add: continuous_map inf.absorb_iff2)
   done
 
 lemma embedding_map_imp_homeomorphic_space:
@@ -3669,6 +3697,11 @@
   unfolding embedding_map_def
   using homeomorphic_space by blast
 
+lemma embedding_imp_closed_map:
+   "\<lbrakk>embedding_map X Y f; closedin Y (f ` topspace X)\<rbrakk> \<Longrightarrow> closed_map X Y f"
+  unfolding closed_map_def
+  by (auto simp: closedin_closed_subtopology embedding_map_def homeomorphic_map_closedness_eq)
+
 
 subsection\<open>Retraction and section maps\<close>
 
@@ -4341,5 +4374,235 @@
   ultimately show "g x \<in> topspace (pullback_topology A f T2)"
     unfolding topspace_pullback_topology by blast
 qed
+subsection\<open>Proper maps (not a priori assumed continuous) \<close>
+
+definition proper_map
+  where
+ "proper_map X Y f \<equiv>
+        closed_map X Y f \<and> (\<forall>y \<in> topspace Y. compactin X {x \<in> topspace X. f x = y})"
+
+lemma proper_imp_closed_map:
+   "proper_map X Y f \<Longrightarrow> closed_map X Y f"
+  by (simp add: proper_map_def)
+
+lemma proper_map_imp_subset_topspace:
+   "proper_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
+  by (simp add: closed_map_imp_subset_topspace proper_map_def)
+
+lemma closed_injective_imp_proper_map:
+  assumes f: "closed_map X Y f" and inj: "inj_on f (topspace X)"
+  shows "proper_map X Y f"
+  unfolding proper_map_def
+proof (clarsimp simp: f)
+  show "compactin X {x \<in> topspace X. f x = y}"
+    if "y \<in> topspace Y" for y
+  proof -
+    have "{x \<in> topspace X. f x = y} = {} \<or> (\<exists>a \<in> topspace X. {x \<in> topspace X. f x = y} = {a})"
+      using inj_on_eq_iff [OF inj] by auto
+    then show ?thesis
+      using that by (metis (no_types, lifting) compactin_empty compactin_sing)
+  qed
+qed
+
+lemma injective_imp_proper_eq_closed_map:
+   "inj_on f (topspace X) \<Longrightarrow> (proper_map X Y f \<longleftrightarrow> closed_map X Y f)"
+  using closed_injective_imp_proper_map proper_imp_closed_map by blast
+
+lemma homeomorphic_imp_proper_map:
+   "homeomorphic_map X Y f \<Longrightarrow> proper_map X Y f"
+  by (simp add: closed_injective_imp_proper_map homeomorphic_eq_everything_map)
+
+lemma compactin_proper_map_preimage:
+  assumes f: "proper_map X Y f" and "compactin Y K"
+  shows "compactin X {x. x \<in> topspace X \<and> f x \<in> K}"
+proof -
+  have "f ` (topspace X) \<subseteq> topspace Y"
+    by (simp add: f proper_map_imp_subset_topspace)
+  have *: "\<And>y. y \<in> topspace Y \<Longrightarrow> compactin X {x \<in> topspace X. f x = y}"
+    using f by (auto simp: proper_map_def)
+  show ?thesis
+    unfolding compactin_def
+  proof clarsimp
+    show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> {x \<in> topspace X. f x \<in> K} \<subseteq> \<Union>\<F>"
+      if \<U>: "\<forall>U\<in>\<U>. openin X U" and sub: "{x \<in> topspace X. f x \<in> K} \<subseteq> \<Union>\<U>"
+      for \<U>
+    proof -
+      have "\<forall>y \<in> K. \<exists>\<V>. finite \<V> \<and> \<V> \<subseteq> \<U>  \<and> {x \<in> topspace X. f x = y} \<subseteq> \<Union>\<V>"
+      proof
+        fix y
+        assume "y \<in> K"
+        then have "compactin X {x \<in> topspace X. f x = y}"
+          by (metis "*" \<open>compactin Y K\<close> compactin_subspace subsetD)
+        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>"
+          unfolding compactin_def using \<U> sub by fastforce
+      qed
+      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)"
+        by (metis (full_types))
+      define F where "F \<equiv> \<lambda>y. topspace Y - f ` (topspace X - \<Union>(\<V> y))"
+      have "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> F ` K \<and> K \<subseteq> \<Union>\<F>"
+      proof (rule compactinD [OF \<open>compactin Y K\<close>])
+        have "\<And>x. x \<in> K \<Longrightarrow> closedin Y (f ` (topspace X - \<Union>(\<V> x)))"
+          using f unfolding proper_map_def closed_map_def
+          by (meson \<U> \<V> openin_Union openin_closedin_eq subsetD)
+        then show "openin Y U" if "U \<in> F ` K" for U
+          using that by (auto simp: F_def)
+        show "K \<subseteq> \<Union>(F ` K)"
+          using \<V> \<open>compactin Y K\<close> unfolding F_def compactin_def by fastforce
+      qed
+      then obtain J where "finite J" "J \<subseteq> K" and J: "K \<subseteq> \<Union>(F ` J)"
+        by (auto simp: ex_finite_subset_image)
+      show ?thesis
+        unfolding F_def
+      proof (intro exI conjI)
+        show "finite (\<Union>(\<V> ` J))"
+          using \<V> \<open>J \<subseteq> K\<close> \<open>finite J\<close> by blast
+        show "\<Union>(\<V> ` J) \<subseteq> \<U>"
+          using \<V> \<open>J \<subseteq> K\<close> by blast
+        show "{x \<in> topspace X. f x \<in> K} \<subseteq> \<Union>(\<Union>(\<V> ` J))"
+          using J \<open>J \<subseteq> K\<close> unfolding F_def by auto
+      qed
+    qed
+  qed
+qed
+
+
+lemma compact_space_proper_map_preimage:
+  assumes f: "proper_map X Y f" and fim: "f ` (topspace X) = topspace Y" and "compact_space Y"
+  shows "compact_space X"
+proof -
+  have eq: "topspace X = {x \<in> topspace X. f x \<in> topspace Y}"
+    using fim by blast
+  moreover have "compactin Y (topspace Y)"
+    using \<open>compact_space Y\<close> compact_space_def by auto
+  ultimately show ?thesis
+    unfolding compact_space_def
+    using eq f compactin_proper_map_preimage by fastforce
+qed
+
+lemma proper_map_alt:
+   "proper_map X Y f \<longleftrightarrow>
+    closed_map X Y f \<and> (\<forall>K. compactin Y K \<longrightarrow> compactin X {x. x \<in> topspace X \<and> f x \<in> K})"
+  proof (intro iffI conjI allI impI)
+  show "compactin X {x \<in> topspace X. f x \<in> K}"
+    if "proper_map X Y f" and "compactin Y K" for K
+    using that by (simp add: compactin_proper_map_preimage)
+  show "proper_map X Y f"
+    if f: "closed_map X Y f \<and> (\<forall>K. compactin Y K \<longrightarrow> compactin X {x \<in> topspace X. f x \<in> K})"
+  proof -
+    have "compactin X {x \<in> topspace X. f x = y}" if "y \<in> topspace Y" for y
+    proof -
+      have "compactin X {x \<in> topspace X. f x \<in> {y}}"
+        using f compactin_sing that by fastforce
+      then show ?thesis
+        by auto
+    qed
+    with f show ?thesis
+      by (auto simp: proper_map_def)
+  qed
+qed (simp add: proper_imp_closed_map)
+
+lemma proper_map_on_empty:
+   "topspace X = {} \<Longrightarrow> proper_map X Y f"
+  by (auto simp: proper_map_def closed_map_on_empty)
+
+lemma proper_map_id [simp]:
+   "proper_map X X id"
+proof (clarsimp simp: proper_map_alt closed_map_id)
+  fix K
+  assume K: "compactin X K"
+  then have "{a \<in> topspace X. a \<in> K} = K"
+    by (simp add: compactin_subspace subset_antisym subset_iff)
+  then show "compactin X {a \<in> topspace X. a \<in> K}"
+    using K by auto
+qed
+
+lemma proper_map_compose:
+  assumes "proper_map X Y f" "proper_map Y Z g"
+  shows "proper_map X Z (g \<circ> f)"
+proof -
+  have "closed_map X Y f" and f: "\<And>K. compactin Y K \<Longrightarrow> compactin X {x \<in> topspace X. f x \<in> K}"
+    and "closed_map Y Z g" and g: "\<And>K. compactin Z K \<Longrightarrow> compactin Y {x \<in> topspace Y. g x \<in> K}"
+    using assms by (auto simp: proper_map_alt)
+  show ?thesis
+    unfolding proper_map_alt
+  proof (intro conjI allI impI)
+    show "closed_map X Z (g \<circ> f)"
+      using \<open>closed_map X Y f\<close> \<open>closed_map Y Z g\<close> closed_map_compose by blast
+    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
+      using \<open>closed_map X Y f\<close> closed_map_imp_subset_topspace by blast
+    then show "compactin X {x \<in> topspace X. (g \<circ> f) x \<in> K}"
+      if "compactin Z K" for K
+      using f [OF g [OF that]] by auto
+  qed
+qed
+
+lemma proper_map_const:
+   "proper_map X Y (\<lambda>x. c) \<longleftrightarrow> compact_space X \<and> (topspace X = {} \<or> closedin Y {c})"
+proof (cases "topspace X = {}")
+  case True
+  then show ?thesis
+    by (simp add: compact_space_topspace_empty proper_map_on_empty)
+next
+  case False
+  have *: "compactin X {x \<in> topspace X. c = y}" if "compact_space X" for y
+  proof (cases "c = y")
+    case True
+    then show ?thesis
+      using compact_space_def \<open>compact_space X\<close> by auto
+  qed auto
+  then show ?thesis
+    using closed_compactin closedin_subset
+    by (force simp: False proper_map_def closed_map_const compact_space_def)
+qed
+
+lemma proper_map_inclusion:
+   "s \<subseteq> topspace X
+        \<Longrightarrow> proper_map (subtopology X s) X id \<longleftrightarrow> closedin X s \<and> (\<forall>k. compactin X k \<longrightarrow> compactin X (s \<inter> k))"
+  by (auto simp: proper_map_alt closed_map_inclusion_eq inf.absorb_iff2 Collect_conj_eq compactin_subtopology intro: closed_Int_compactin)
+
+
+subsection\<open>Perfect maps (proper, continuous and surjective)\<close>
+
+definition perfect_map 
+  where "perfect_map X Y f \<equiv> continuous_map X Y f \<and> proper_map X Y f \<and> f ` (topspace X) = topspace Y"
+
+lemma homeomorphic_imp_perfect_map:
+   "homeomorphic_map X Y f \<Longrightarrow> perfect_map X Y f"
+  by (simp add: homeomorphic_eq_everything_map homeomorphic_imp_proper_map perfect_map_def)
+
+lemma perfect_imp_quotient_map:
+   "perfect_map X Y f \<Longrightarrow> quotient_map X Y f"
+  by (simp add: continuous_closed_imp_quotient_map perfect_map_def proper_map_def)
+
+lemma homeomorphic_eq_injective_perfect_map:
+   "homeomorphic_map X Y f \<longleftrightarrow> perfect_map X Y f \<and> inj_on f (topspace X)"
+  using homeomorphic_imp_perfect_map homeomorphic_map_def perfect_imp_quotient_map by blast
+
+lemma perfect_injective_eq_homeomorphic_map:
+   "perfect_map X Y f \<and> inj_on f (topspace X) \<longleftrightarrow> homeomorphic_map X Y f"
+  by (simp add: homeomorphic_eq_injective_perfect_map)
+
+lemma perfect_map_id [simp]: "perfect_map X X id"
+  by (simp add: homeomorphic_imp_perfect_map)
+
+lemma perfect_map_compose:
+   "\<lbrakk>perfect_map X Y f; perfect_map Y Z g\<rbrakk> \<Longrightarrow> perfect_map X Z (g \<circ> f)"
+  by (meson continuous_map_compose perfect_imp_quotient_map perfect_map_def proper_map_compose quotient_map_compose_eq quotient_map_def)
+
+lemma perfect_imp_continuous_map:
+   "perfect_map X Y f \<Longrightarrow> continuous_map X Y f"
+  using perfect_map_def by blast
+
+lemma perfect_imp_closed_map:
+   "perfect_map X Y f \<Longrightarrow> closed_map X Y f"
+  by (simp add: perfect_map_def proper_map_def)
+
+lemma perfect_imp_proper_map:
+   "perfect_map X Y f \<Longrightarrow> proper_map X Y f"
+  by (simp add: perfect_map_def)
+
+lemma perfect_imp_surjective_map:
+   "perfect_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
+  by (simp add: perfect_map_def)
 
 end
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -1107,7 +1107,7 @@
     "\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S"
   by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
 
-lemma retraction_imp_quotient_map:
+lemma retraction_openin_vimage_iff:
   "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
   if retraction: "retraction S T r" and "U \<subseteq> T"
   using retraction apply (rule retractionE)
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Analysis/Analysis.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -29,7 +29,7 @@
   Bounded_Continuous_Function
   Abstract_Topology
   Product_Topology
-  T1_Spaces
+  Lindelof_Spaces
   Infinite_Products
   Infinite_Set_Sum
   Weierstrass_Theorems
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -1410,7 +1410,7 @@
     ultimately obtain \<C>' where "finite \<C>'" "\<C>' \<subseteq> \<B>'" "U \<subseteq> \<Union>\<C>'"
       using fin [of \<B>'] \<open>topspace X = U\<close> \<open>U \<subseteq> \<Union>\<B>\<close> by blast
     then show ?thesis
-      unfolding \<B>' exists_finite_subset_image \<open>topspace X = U\<close> by auto
+      unfolding \<B>' ex_finite_subset_image \<open>topspace X = U\<close> by auto
   qed
   show ?thesis
     apply (rule Alexander_subbase [where \<B> = "Collect ((\<lambda>x. x \<in> \<B>) relative_to (topspace X))"])
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Analysis/Lindelof_Spaces.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -0,0 +1,274 @@
+section\<open>Lindelof spaces\<close>
+
+theory Lindelof_Spaces
+imports T1_Spaces
+begin
+
+definition Lindelof_space where
+  "Lindelof_space X \<equiv>
+        \<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> \<Union>\<U> = topspace X
+            \<longrightarrow> (\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> \<Union>\<V> = topspace X)"
+
+lemma Lindelof_spaceD:
+  "\<lbrakk>Lindelof_space X; \<And>U. U \<in> \<U> \<Longrightarrow> openin X U; \<Union>\<U> = topspace X\<rbrakk>
+  \<Longrightarrow> \<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> \<Union>\<V> = topspace X"
+  by (auto simp: Lindelof_space_def)
+
+lemma Lindelof_space_alt:
+   "Lindelof_space X \<longleftrightarrow>
+        (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<subseteq> \<Union>\<U>
+             \<longrightarrow> (\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<V>))"
+  unfolding Lindelof_space_def
+  using openin_subset by fastforce
+
+lemma compact_imp_Lindelof_space:
+   "compact_space X \<Longrightarrow> Lindelof_space X"
+  unfolding Lindelof_space_def compact_space
+  by (meson uncountable_infinite)
+
+lemma Lindelof_space_topspace_empty:
+   "topspace X = {} \<Longrightarrow> Lindelof_space X"
+  using compact_imp_Lindelof_space compact_space_topspace_empty by blast
+
+lemma Lindelof_space_Union:
+  assumes \<U>: "countable \<U>" and lin: "\<And>U. U \<in> \<U> \<Longrightarrow> Lindelof_space (subtopology X U)"
+  shows "Lindelof_space (subtopology X (\<Union>\<U>))"
+proof -
+  have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<F> \<and> \<Union>\<U> \<inter> \<Union>\<V> = topspace X \<inter> \<Union>\<U>"
+    if \<F>: "\<F> \<subseteq> Collect (openin X)" and UF: "\<Union>\<U> \<inter> \<Union>\<F> = topspace X \<inter> \<Union>\<U>"
+    for \<F>
+  proof -
+    have "\<And>U. \<lbrakk>U \<in> \<U>; U \<inter> \<Union>\<F> = topspace X \<inter> U\<rbrakk>
+               \<Longrightarrow> \<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<F> \<and> U \<inter> \<Union>\<V> = topspace X \<inter> U"
+      using lin \<F>
+      unfolding Lindelof_space_def openin_subtopology_alt Ball_def subset_iff [symmetric]
+      by (simp add: all_subset_image imp_conjL ex_countable_subset_image)
+    then obtain g where g: "\<And>U. \<lbrakk>U \<in> \<U>; U \<inter> \<Union>\<F> = topspace X \<inter> U\<rbrakk>
+                               \<Longrightarrow> countable (g U) \<and> (g U) \<subseteq> \<F> \<and> U \<inter> \<Union>(g U) = topspace X \<inter> U"
+      by metis
+    show ?thesis
+    proof (intro exI conjI)
+      show "countable (\<Union>(g ` \<U>))"
+        using Int_commute UF g  by (fastforce intro: countable_UN [OF \<U>])
+      show "\<Union>(g ` \<U>) \<subseteq> \<F>"
+        using g UF by blast
+      show "\<Union>\<U> \<inter> \<Union>(\<Union>(g ` \<U>)) = topspace X \<inter> \<Union>\<U>"
+      proof
+        show "\<Union>\<U> \<inter> \<Union>(\<Union>(g ` \<U>)) \<subseteq> topspace X \<inter> \<Union>\<U>"
+          using g UF by blast
+        show "topspace X \<inter> \<Union>\<U> \<subseteq> \<Union>\<U> \<inter> \<Union>(\<Union>(g ` \<U>))"
+        proof clarsimp
+          show "\<exists>y\<in>\<U>. \<exists>W\<in>g y. x \<in> W"
+            if "x \<in> topspace X" "x \<in> V" "V \<in> \<U>" for x V
+          proof -
+            have "V \<inter> \<Union>\<F> = topspace X \<inter> V"
+              using UF \<open>V \<in> \<U>\<close> by blast
+            with that g [OF \<open>V \<in> \<U>\<close>]  show ?thesis by blast
+          qed
+        qed
+      qed
+    qed
+  qed
+  then show ?thesis
+      unfolding Lindelof_space_def openin_subtopology_alt Ball_def subset_iff [symmetric]
+      by (simp add: all_subset_image imp_conjL ex_countable_subset_image)
+qed
+
+lemma countable_imp_Lindelof_space:
+  assumes "countable(topspace X)"
+  shows "Lindelof_space X"
+proof -
+  have "Lindelof_space (subtopology X (\<Union>x \<in> topspace X. {x}))"
+  proof (rule Lindelof_space_Union)
+    show "countable ((\<lambda>x. {x}) ` topspace X)"
+      using assms by blast
+    show "Lindelof_space (subtopology X U)"
+      if "U \<in> (\<lambda>x. {x}) ` topspace X" for U
+    proof -
+      have "compactin X U"
+        using that by force
+      then show ?thesis
+        by (meson compact_imp_Lindelof_space compact_space_subtopology)
+    qed
+  qed
+  then show ?thesis
+    by simp
+qed
+lemma Lindelof_space_subtopology:
+   "Lindelof_space(subtopology X S) \<longleftrightarrow>
+        (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<inter> S \<subseteq> \<Union>\<U>
+            \<longrightarrow> (\<exists>V. countable V \<and> V \<subseteq> \<U> \<and> topspace X \<inter> S \<subseteq> \<Union>V))"
+proof -
+  have *: "(S \<inter> \<Union>\<U> = topspace X \<inter> S) = (topspace X \<inter> S \<subseteq> \<Union>\<U>)"
+    if "\<And>x. x \<in> \<U> \<Longrightarrow> openin X x" for \<U>
+    by (blast dest: openin_subset [OF that])
+  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>)"
+    if "\<forall>x. x \<in> \<U> \<longrightarrow> openin X x" "topspace X \<inter> S \<subseteq> \<Union>\<U>" "countable \<V>" for \<U> \<V>
+    using that * by blast
+  ultimately show ?thesis
+    unfolding Lindelof_space_def openin_subtopology_alt Ball_def
+    apply (simp add: all_subset_image imp_conjL ex_countable_subset_image flip: subset_iff)
+    apply (intro all_cong1 imp_cong ex_cong, auto)
+    done
+qed
+
+lemma Lindelof_space_subtopology_subset:
+   "S \<subseteq> topspace X
+        \<Longrightarrow> (Lindelof_space(subtopology X S) \<longleftrightarrow>
+             (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> S \<subseteq> \<Union>\<U>
+                 \<longrightarrow> (\<exists>V. countable V \<and> V \<subseteq> \<U> \<and> S \<subseteq> \<Union>V)))"
+  by (metis Lindelof_space_subtopology topspace_subtopology topspace_subtopology_subset)
+
+lemma Lindelof_space_closedin_subtopology:
+  assumes X: "Lindelof_space X" and clo: "closedin X S"
+  shows "Lindelof_space (subtopology X S)"
+proof -
+  have "S \<subseteq> topspace X"
+    by (simp add: clo closedin_subset)
+  then show ?thesis
+  proof (clarsimp simp add: Lindelof_space_subtopology_subset)
+    show "\<exists>V. countable V \<and> V \<subseteq> \<F> \<and> S \<subseteq> \<Union>V"
+      if "\<forall>U\<in>\<F>. openin X U" and "S \<subseteq> \<Union>\<F>" for \<F>
+    proof -
+      have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> insert (topspace X - S) \<F> \<and> \<Union>\<V> = topspace X"
+      proof (rule Lindelof_spaceD [OF X, of "insert (topspace X - S) \<F>"])
+        show "openin X U"
+          if "U \<in> insert (topspace X - S) \<F>" for U
+          using that \<open>\<forall>U\<in>\<F>. openin X U\<close> clo by blast
+        show "\<Union>(insert (topspace X - S) \<F>) = topspace X"
+          apply auto
+          apply (meson in_mono openin_closedin_eq that(1))
+          using UnionE \<open>S \<subseteq> \<Union>\<F>\<close> by auto
+      qed
+      then obtain \<V> where "countable \<V>" "\<V> \<subseteq> insert (topspace X - S) \<F>" "\<Union>\<V> = topspace X"
+        by metis
+      with \<open>S \<subseteq> topspace X\<close>
+      show ?thesis
+        by (rule_tac x="(\<V> - {topspace X - S})" in exI) auto
+    qed
+  qed
+qed
+
+lemma Lindelof_space_continuous_map_image:
+  assumes X: "Lindelof_space X" and f: "continuous_map X Y f" and fim: "f ` (topspace X) = topspace Y"
+  shows "Lindelof_space Y"
+proof -
+  have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> \<Union>\<V> = topspace Y"
+    if \<U>: "\<And>U. U \<in> \<U> \<Longrightarrow> openin Y U" and UU: "\<Union>\<U> = topspace Y" for \<U>
+  proof -
+    define \<V> where "\<V> \<equiv> (\<lambda>U. {x \<in> topspace X. f x \<in> U}) ` \<U>"
+    have "\<And>V. V \<in> \<V> \<Longrightarrow> openin X V"
+      unfolding \<V>_def using \<U> continuous_map f by fastforce
+    moreover have "\<Union>\<V> = topspace X"
+      unfolding \<V>_def using UU fim by fastforce
+    ultimately have "\<exists>\<W>. countable \<W> \<and> \<W> \<subseteq> \<V> \<and> \<Union>\<W> = topspace X"
+      using X by (simp add: Lindelof_space_def)
+    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"
+      by (metis (no_types, lifting) \<V>_def countable_subset_image)
+    moreover have "\<Union>\<C> = topspace Y"
+    proof
+      show "\<Union>\<C> \<subseteq> topspace Y"
+        using UU \<C> \<open>\<C> \<subseteq> \<U>\<close> by fastforce
+      have "y \<in> \<Union>\<C>" if "y \<in> topspace Y" for y
+      proof -
+        obtain x where "x \<in> topspace X" "y = f x"
+          using that fim by (metis \<open>y \<in> topspace Y\<close> imageE)
+        with \<C> show ?thesis by auto
+      qed
+      then show "topspace Y \<subseteq> \<Union>\<C>" by blast
+    qed
+    ultimately show ?thesis
+      by blast
+  qed
+  then show ?thesis
+    unfolding Lindelof_space_def
+    by auto
+qed
+
+lemma Lindelof_space_quotient_map_image:
+   "\<lbrakk>quotient_map X Y q; Lindelof_space X\<rbrakk> \<Longrightarrow> Lindelof_space Y"
+  by (meson Lindelof_space_continuous_map_image quotient_imp_continuous_map quotient_imp_surjective_map)
+
+lemma Lindelof_space_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; Lindelof_space X\<rbrakk> \<Longrightarrow> Lindelof_space Y"
+  using Abstract_Topology.retraction_imp_quotient_map Lindelof_space_quotient_map_image by blast
+
+lemma locally_finite_cover_of_Lindelof_space:
+  assumes X: "Lindelof_space X" and UU: "topspace X \<subseteq> \<Union>\<U>" and fin: "locally_finite_in X \<U>"
+  shows "countable \<U>"
+proof -
+  have UU_eq: "\<Union>\<U> = topspace X"
+    by (meson UU fin locally_finite_in_def subset_antisym)
+  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> {}}"
+    using fin unfolding locally_finite_in_def by meson
+  then obtain I where "countable I" "I \<subseteq> topspace X" and I: "topspace X \<subseteq> \<Union>(T ` I)"
+    using X unfolding Lindelof_space_alt
+    by (drule_tac x="image T (topspace X)" in spec) (auto simp: ex_countable_subset_image)
+  show ?thesis
+  proof (rule countable_subset)
+    have "\<And>i. i \<in> I \<Longrightarrow> countable {U \<in> \<U>. U \<inter> T i \<noteq> {}}"
+      using T
+      by (meson \<open>I \<subseteq> topspace X\<close> in_mono uncountable_infinite)
+    then show "countable (insert {} (\<Union>i\<in>I. {U \<in> \<U>. U \<inter> T i \<noteq> {}}))"
+      by (simp add: \<open>countable I\<close>)
+  qed (use UU_eq I in auto)
+qed
+
+
+lemma Lindelof_space_proper_map_preimage:
+  assumes f: "proper_map X Y f" and Y: "Lindelof_space Y"
+  shows "Lindelof_space X"
+proof (clarsimp simp: Lindelof_space_alt)
+  show "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<V>"
+    if \<U>: "\<forall>U\<in>\<U>. openin X U" and sub_UU: "topspace X \<subseteq> \<Union>\<U>" for \<U>
+  proof -
+    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
+    proof (rule compactinD)
+      show "compactin X {x \<in> topspace X. f x = y}"
+        using f proper_map_def that by fastforce
+    qed (use sub_UU \<U> in auto)
+    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)"
+      by meson
+    define \<W> where "\<W> \<equiv> (\<lambda>y. topspace Y - image f (topspace X - \<Union>(\<V> y))) ` topspace Y"
+    have "\<forall>U \<in> \<W>. openin Y U"
+      using f \<U> \<V> unfolding \<W>_def proper_map_def closed_map_def
+      by (simp add: closedin_diff openin_Union openin_diff subset_iff)
+    moreover have "topspace Y \<subseteq> \<Union>\<W>"
+      using \<V> unfolding \<W>_def by clarsimp fastforce
+    ultimately have "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<W> \<and> topspace Y \<subseteq> \<Union>\<V>"
+      using Y by (simp add: Lindelof_space_alt)
+    then obtain I where "countable I" "I \<subseteq> topspace Y"
+      and I: "topspace Y \<subseteq> (\<Union>i\<in>I. topspace Y - f ` (topspace X - \<Union>(\<V> i)))"
+      unfolding \<W>_def ex_countable_subset_image by metis
+    show ?thesis
+    proof (intro exI conjI)
+      have "\<And>i. i \<in> I \<Longrightarrow> countable (\<V> i)"
+        by (meson \<V> \<open>I \<subseteq> topspace Y\<close> in_mono uncountable_infinite)
+      with \<open>countable I\<close> show "countable (\<Union>(\<V> ` I))"
+        by auto
+      show "\<Union>(\<V> ` I) \<subseteq> \<U>"
+        using \<V> \<open>I \<subseteq> topspace Y\<close> by fastforce
+      show "topspace X \<subseteq> \<Union>(\<Union>(\<V> ` I))"
+      proof
+        show "x \<in> \<Union> (\<Union> (\<V> ` I))" if "x \<in> topspace X" for x
+        proof -
+          have "f x \<in> topspace Y"
+            by (meson f image_subset_iff proper_map_imp_subset_topspace that)
+          then show ?thesis
+            using that I by auto
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma Lindelof_space_perfect_map_image:
+   "\<lbrakk>Lindelof_space X; perfect_map X Y f\<rbrakk> \<Longrightarrow> Lindelof_space Y"
+  using Lindelof_space_quotient_map_image perfect_imp_quotient_map by blast
+
+lemma Lindelof_space_perfect_map_image_eq:
+   "perfect_map X Y f \<Longrightarrow> Lindelof_space X \<longleftrightarrow> Lindelof_space Y"
+  using Lindelof_space_perfect_map_image Lindelof_space_proper_map_preimage perfect_map_def by blast
+
+end
+
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -2109,6 +2109,14 @@
     by (metis Int_absorb1 mem_Collect_eq path_component_of_equiv path_component_of_subset_topspace topspace_subtopology)
 qed
 
+lemma path_connectedin_euclidean [simp]:
+   "path_connectedin euclidean S \<longleftrightarrow> path_connected S"
+  by (auto simp: path_connectedin_def path_connected_space_iff_path_component path_connected_component)
+
+lemma path_connected_space_euclidean_subtopology [simp]:
+   "path_connected_space(subtopology euclidean S) \<longleftrightarrow> path_connected S"
+  using path_connectedin_topspace by force
+
 lemma Union_path_components_of:
      "\<Union>(path_components_of X) = topspace X"
   by (auto simp: path_components_of_def path_component_of_equiv)
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Analysis/Product_Topology.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -455,6 +455,15 @@
   unfolding homeomorphic_maps_def continuous_map_prod_top
   by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
 
+lemma homeomorphic_maps_swap:
+   "homeomorphic_maps (prod_topology X Y) (prod_topology Y X)
+                          (\<lambda>(x,y). (y,x)) (\<lambda>(y,x). (x,y))"
+  by (auto simp: homeomorphic_maps_def case_prod_unfold continuous_map_fst continuous_map_pairedI continuous_map_snd)
+
+lemma homeomorphic_map_swap:
+   "homeomorphic_map (prod_topology X Y) (prod_topology Y X) (\<lambda>(x,y). (y,x))"
+  using homeomorphic_map_maps homeomorphic_maps_swap by metis
+
 lemma embedding_map_graph:
    "embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
     (is "?lhs = ?rhs")
@@ -474,7 +483,7 @@
     unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def
     by (rule_tac x=fst in exI)
        (auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology
-                   continuous_map_fst topspace_subtopology)
+                   continuous_map_fst)
 qed
 
 lemma homeomorphic_space_prod_topology:
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Analysis/T1_Spaces.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -475,6 +475,37 @@
     by (simp add: topology_eq)
 qed
 
+lemma continuous_map_imp_closed_graph:
+  assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y"
+  shows "closedin (prod_topology X Y) ((\<lambda>x. (x,f x)) ` topspace X)"
+  unfolding closedin_def
+proof
+  show "(\<lambda>x. (x, f x)) ` topspace X \<subseteq> topspace (prod_topology X Y)"
+    using continuous_map_def f by fastforce
+  show "openin (prod_topology X Y) (topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X)"
+    unfolding openin_prod_topology_alt
+  proof (intro allI impI)
+    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"
+      if "(x,y) \<in> topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X"
+      for x y
+    proof -
+      have "x \<in> topspace X" "y \<in> topspace Y" "y \<noteq> f x"
+        using that by auto
+      moreover have "f x \<in> topspace Y"
+        by (meson \<open>x \<in> topspace X\<close> continuous_map_def f)
+      ultimately obtain U V where UV: "openin Y U" "openin Y V" "f x \<in> U" "y \<in> V" "disjnt U V"
+        using Y Hausdorff_space_def by metis
+      show ?thesis
+      proof (intro exI conjI)
+        show "openin X {x \<in> topspace X. f x \<in> U}"
+          using \<open>openin Y U\<close> f openin_continuous_map_preimage by blast
+        show "{x \<in> topspace X. f x \<in> U} \<times> V \<subseteq> topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X"
+          using UV by (auto simp: disjnt_iff dest: openin_subset)
+      qed (use UV \<open>x \<in> topspace X\<close> in auto)
+    qed
+  qed
+qed
+
 lemma continuous_imp_closed_map:
    "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f\<rbrakk> \<Longrightarrow> closed_map X Y f"
   by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin)
@@ -529,8 +560,39 @@
   qed
 qed
 
+lemma closed_map_paired_continuous_map_right:
+   "\<lbrakk>continuous_map X Y f; Hausdorff_space Y\<rbrakk> \<Longrightarrow> closed_map X (prod_topology X Y) (\<lambda>x. (x,f x))"
+  by (simp add: continuous_map_imp_closed_graph embedding_map_graph embedding_imp_closed_map)
 
-lemma Hausdorff_space_euclidean: "Hausdorff_space (euclidean :: 'a::metric_space topology)"
+lemma closed_map_paired_continuous_map_left:
+  assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y"
+  shows "closed_map X (prod_topology Y X) (\<lambda>x. (f x,x))"
+proof -
+  have eq: "(\<lambda>x. (f x,x)) = (\<lambda>(a,b). (b,a)) \<circ> (\<lambda>x. (x,f x))"
+    by auto
+  show ?thesis
+    unfolding eq
+  proof (rule closed_map_compose)
+    show "closed_map X (prod_topology X Y) (\<lambda>x. (x, f x))"
+      using Y closed_map_paired_continuous_map_right f by blast
+    show "closed_map (prod_topology X Y) (prod_topology Y X) (\<lambda>(a, b). (b, a))"
+      by (metis homeomorphic_map_swap homeomorphic_imp_closed_map)
+  qed
+qed
+
+lemma proper_map_paired_continuous_map_right:
+   "\<lbrakk>continuous_map X Y f; Hausdorff_space Y\<rbrakk>
+        \<Longrightarrow> proper_map X (prod_topology X Y) (\<lambda>x. (x,f x))"
+  using closed_injective_imp_proper_map closed_map_paired_continuous_map_right
+  by (metis (mono_tags, lifting) Pair_inject inj_onI)
+
+lemma proper_map_paired_continuous_map_left:
+   "\<lbrakk>continuous_map X Y f; Hausdorff_space Y\<rbrakk>
+        \<Longrightarrow> proper_map X (prod_topology Y X) (\<lambda>x. (f x,x))"
+  using closed_injective_imp_proper_map closed_map_paired_continuous_map_left
+  by (metis (mono_tags, lifting) Pair_inject inj_onI)
+
+lemma Hausdorff_space_euclidean [simp]: "Hausdorff_space (euclidean :: 'a::metric_space topology)"
 proof -
   have "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
     if "x \<noteq> y"
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Finite_Set.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -334,7 +334,7 @@
     using finite_subset_image [OF B] P by blast
 qed blast
 
-lemma exists_finite_subset_image:
+lemma ex_finite_subset_image:
   "(\<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))"
 proof safe
   fix B :: "'a set"
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Homology/Simplices.thy
--- a/src/HOL/Homology/Simplices.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Homology/Simplices.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -2411,7 +2411,7 @@
     using compactin_standard_simplex [of p]
     unfolding compactin_def by force
   then obtain S where "finite S" and ssp: "S \<subseteq> standard_simplex p" "standard_simplex p \<subseteq> \<Union>(F ` S)"
-    unfolding exists_finite_subset_image by (auto simp: exists_finite_subset_image)
+    unfolding ex_finite_subset_image by (auto simp: ex_finite_subset_image)
   then have "S \<noteq> {}"
     by (auto simp: nonempty_standard_simplex)
   show ?thesis
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Library/Countable_Set.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -195,6 +195,23 @@
 lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A"
   by (metis countable_image the_inv_into_onto)
 
+lemma countable_image_inj_Int_vimage:
+   "\<lbrakk>inj_on f S; countable A\<rbrakk> \<Longrightarrow> countable (S \<inter> f -` A)"
+  by (meson countable_image_inj_on countable_subset image_subset_iff_subset_vimage inf_le2 inj_on_Int)
+
+lemma countable_image_inj_gen:
+   "\<lbrakk>inj_on f S; countable A\<rbrakk> \<Longrightarrow> countable {x \<in> S. f x \<in> A}"
+  using countable_image_inj_Int_vimage
+  by (auto simp: vimage_def Collect_conj_eq)
+
+lemma countable_image_inj_eq:
+   "inj_on f S \<Longrightarrow> countable(f ` S) \<longleftrightarrow> countable S"
+  using countable_image_inj_on by blast
+
+lemma countable_image_inj:
+   "\<lbrakk>countable A; inj f\<rbrakk> \<Longrightarrow> countable {x. f x \<in> A}"
+  by (metis (mono_tags, lifting) countable_image_inj_eq countable_subset image_Collect_subsetI inj_on_inverseI the_inv_f_f)
+
 lemma countable_UN[intro, simp]:
   fixes I :: "'i set" and A :: "'i => 'a set"
   assumes I: "countable I"
@@ -320,6 +337,39 @@
   then show ?lhs by force
 qed
 
+lemma ex_subset_image_inj:
+   "(\<exists>T. T \<subseteq> f ` S \<and> P T) \<longleftrightarrow> (\<exists>T. T \<subseteq> S \<and> inj_on f T \<and> P (f ` T))"
+  by (auto simp: subset_image_inj)
+
+lemma all_subset_image_inj:
+   "(\<forall>T. T \<subseteq> f ` S \<longrightarrow> P T) \<longleftrightarrow> (\<forall>T. T \<subseteq> S \<and> inj_on f T \<longrightarrow> P(f ` T))"
+  by (metis subset_image_inj)
+
+lemma ex_countable_subset_image_inj:
+   "(\<exists>T. countable T \<and> T \<subseteq> f ` S \<and> P T) \<longleftrightarrow>
+    (\<exists>T. countable T \<and> T \<subseteq> S \<and> inj_on f T \<and> P (f ` T))"
+  by (metis countable_image_inj_eq subset_image_inj)
+
+lemma all_countable_subset_image_inj:
+   "(\<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))"
+  by (metis countable_image_inj_eq subset_image_inj)
+
+lemma ex_countable_subset_image:
+   "(\<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))"
+  by (metis countable_subset_image)
+
+lemma all_countable_subset_image:
+   "(\<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))"
+  by (metis countable_subset_image)
+
+lemma countable_image_eq:
+   "countable(f ` S) \<longleftrightarrow> (\<exists>T. countable T \<and> T \<subseteq> S \<and> f ` S = f ` T)"
+  by (metis countable_image countable_image_inj_eq order_refl subset_image_inj)
+
+lemma countable_image_eq_inj:
+   "countable(f ` S) \<longleftrightarrow> (\<exists>T. countable T \<and> T \<subseteq> S \<and> f ` S = f ` T \<and> inj_on f T)"
+  by (metis countable_image_inj_eq order_refl subset_image_inj)
+
 lemma infinite_countable_subset':
   assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C"
 proof -
diff -r b67bab2b132c -r 4900351361b0 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Library/Infinite_Set.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -8,6 +8,27 @@
   imports Main
 begin
 
+lemma subset_image_inj:
+  "S \<subseteq> f ` T \<longleftrightarrow> (\<exists>U. U \<subseteq> T \<and> inj_on f U \<and> S = f ` U)"
+proof safe
+  show "\<exists>U\<subseteq>T. inj_on f U \<and> S = f ` U"
+    if "S \<subseteq> f ` T"
+  proof -
+    from that [unfolded subset_image_iff subset_iff]
+    obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> x = f (g x)"
+      unfolding image_iff by metis
+    show ?thesis
+    proof (intro exI conjI)
+      show "g ` S \<subseteq> T"
+        by (simp add: g image_subsetI)
+      show "inj_on f (g ` S)"
+        using g by (auto simp: inj_on_def)
+      show "S = f ` (g ` S)"
+        using g image_subset_iff by auto
+    qed
+  qed
+qed blast
+
 subsection \<open>The set of natural numbers is infinite\<close>
 
 lemma infinite_nat_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"