src/HOL/Analysis/Abstract_Topology.thy

--- a/src/HOL/Analysis/Abstract_Topology.thy	Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue May 23 12:31:23 2023 +0100
@@ -269,6 +269,10 @@
   unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
   by auto
 
+lemma subset_openin_subtopology:
+   "\<lbrakk>openin X S; S \<subseteq> T\<rbrakk> \<Longrightarrow> openin (subtopology X T) S"
+  by (metis inf.orderE openin_subtopology)
+
 lemma openin_subtopology_Int:
    "openin X S \<Longrightarrow> openin (subtopology X T) (S \<inter> T)"
   using openin_subtopology by auto
@@ -296,6 +300,10 @@
   unfolding closedin_def topspace_subtopology
   by (auto simp: openin_subtopology)
 
+lemma closedin_subtopology_Int_closed:
+   "closedin X T \<Longrightarrow> closedin (subtopology X S) (S \<inter> T)"
+  using closedin_subtopology inf_commute by blast
+
 lemma closedin_subset_topspace:
    "\<lbrakk>closedin X S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology X T) S"
   using closedin_subtopology by fastforce
@@ -4808,6 +4816,18 @@
    "proper_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
   by (simp add: closed_map_imp_subset_topspace proper_map_def)
 
+lemma proper_map_restriction:
+  assumes "proper_map X Y f" "{x \<in> topspace X. f x \<in> V} = U"
+  shows "proper_map (subtopology X U) (subtopology Y V) f"
+proof -
+  have [simp]: "{x \<in> topspace X. f x \<in> V \<and> f x = y} = {x \<in> topspace X. f x = y}" 
+    if "y \<in> V" for y
+    using that by auto
+  show ?thesis
+    using assms unfolding proper_map_def using closed_map_restriction
+    by (force simp: compactin_subtopology)
+qed
+
 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"
@@ -4976,6 +4996,45 @@
    "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 (metis closed_Int_compactin closed_map_inclusion_eq inf.absorb_iff2 inj_on_id injective_imp_proper_eq_closed_map)
 
+lemma proper_map_into_subtopology:
+   "\<lbrakk>proper_map X Y f; f ` topspace X \<subseteq> C\<rbrakk> \<Longrightarrow> proper_map X (subtopology Y C) f"
+  by (simp add: closed_map_into_subtopology compactin_subtopology proper_map_alt)
+
+lemma proper_map_from_composition_left:
+  assumes gf: "proper_map X Z (g \<circ> f)" and contf: "continuous_map X Y f" and fim: "f ` topspace X = topspace Y"
+  shows "proper_map Y Z g"
+  unfolding proper_map_def
+proof (intro strip conjI)
+  show "closed_map Y Z g"
+    by (meson closed_map_from_composition_left gf contf fim proper_imp_closed_map)
+  fix z assume "z \<in> topspace Z"
+  have eq: "{y \<in> topspace Y. g y = z} = f ` {x \<in> topspace X. (g \<circ> f) x = z}"
+    using fim by force
+  show "compactin Y {x \<in> topspace Y. g x = z}"
+    unfolding eq
+  proof (rule image_compactin [OF _ contf])
+    show "compactin X {x \<in> topspace X. (g \<circ> f) x = z}"
+      using \<open>z \<in> topspace Z\<close> gf proper_map_def by fastforce
+  qed
+qed
+
+lemma proper_map_from_composition_right_inj:
+  assumes gf: "proper_map X Z (g \<circ> f)" and fim: "f ` topspace X \<subseteq> topspace Y" 
+    and contf: "continuous_map Y Z g" and inj: "inj_on g (topspace Y)"
+  shows "proper_map X Y f"
+  unfolding proper_map_def
+proof (intro strip conjI)
+  show "closed_map X Y f"
+    by (meson closed_map_from_composition_right assms proper_imp_closed_map)
+  fix y
+  assume "y \<in> topspace Y"
+  with fim inj have eq: "{x \<in> topspace X. f x = y} = {x \<in> topspace X. (g \<circ> f) x = g y}"
+    by (auto simp: image_subset_iff inj_onD)
+  show "compactin X {x \<in> topspace X. f x = y}"
+    unfolding eq
+    by (smt (verit) Collect_cong \<open>y \<in> topspace Y\<close> contf continuous_map_closedin gf proper_map_def)
+qed
+
 
 subsection\<open>Perfect maps (proper, continuous and surjective)\<close>
 
@@ -5021,4 +5080,11 @@
    "perfect_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
   by (simp add: perfect_map_def)
 
+lemma perfect_map_from_composition_left:
+  assumes "perfect_map X Z (g \<circ> f)" and "continuous_map X Y f"
+    and "continuous_map Y Z g" and "f ` topspace X = topspace Y"
+  shows "perfect_map Y Z g"
+  using assms unfolding perfect_map_def
+  by (metis image_comp proper_map_from_composition_left)
+
 end