--- 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