--- a/src/HOL/Analysis/Abstract_Topology.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Thu Apr 18 06:19:30 2019 +0200
@@ -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
--- a/src/HOL/Analysis/Abstract_Topology_2.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Thu Apr 18 06:19:30 2019 +0200
@@ -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)
--- a/src/HOL/Analysis/Analysis.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Analysis/Analysis.thy Thu Apr 18 06:19:30 2019 +0200
@@ -29,7 +29,7 @@
Bounded_Continuous_Function
Abstract_Topology
Product_Topology
- T1_Spaces
+ Lindelof_Spaces
Infinite_Products
Infinite_Set_Sum
Weierstrass_Theorems
--- a/src/HOL/Analysis/Function_Topology.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Analysis/Function_Topology.thy Thu Apr 18 06:19:30 2019 +0200
@@ -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))"])
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy Thu Apr 18 06:19:30 2019 +0200
@@ -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
+
--- a/src/HOL/Analysis/Path_Connected.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Thu Apr 18 06:19:30 2019 +0200
@@ -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)
--- a/src/HOL/Analysis/Product_Topology.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Analysis/Product_Topology.thy Thu Apr 18 06:19:30 2019 +0200
@@ -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:
--- a/src/HOL/Analysis/T1_Spaces.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Analysis/T1_Spaces.thy Thu Apr 18 06:19:30 2019 +0200
@@ -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"
--- a/src/HOL/Finite_Set.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Finite_Set.thy Thu Apr 18 06:19:30 2019 +0200
@@ -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"
--- a/src/HOL/Hilbert_Choice.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Hilbert_Choice.thy Thu Apr 18 06:19:30 2019 +0200
@@ -562,6 +562,27 @@
shows "inv f = g"
using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
+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)"
+ by (auto simp add: image_iff Bex_def choice_iff')
+ 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>Other Consequences of Hilbert's Epsilon\<close>
--- a/src/HOL/Homology/Simplices.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Homology/Simplices.thy Thu Apr 18 06:19:30 2019 +0200
@@ -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
--- a/src/HOL/Library/Countable_Set.thy Wed Apr 17 21:48:56 2019 +0200
+++ b/src/HOL/Library/Countable_Set.thy Thu Apr 18 06:19:30 2019 +0200
@@ -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 -