--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy Sun Jul 02 14:28:20 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy Mon Jul 03 11:45:59 2023 +0100
@@ -1819,13 +1819,13 @@
qed
moreover
{ assume R: ?rhs
- then have fgim: "f ` topspace X \<subseteq> topspace X'" "g ` topspace Y \<subseteq> topspace Y'"
+ then have fgim: "f \<in> topspace X \<rightarrow> topspace X'" "g \<in> topspace Y \<rightarrow> topspace Y'"
and cm: "closed_map X X' f" "closed_map Y Y' g"
by (auto simp: proper_map_def closed_map_imp_subset_topspace)
have "closed_map (prod_topology X Y) (prod_topology X' Y') h"
unfolding closed_map_fibre_neighbourhood imp_conjL
proof (intro conjI strip)
- show "h ` topspace (prod_topology X Y) \<subseteq> topspace (prod_topology X' Y')"
+ show "h \<in> topspace (prod_topology X Y) \<rightarrow> topspace (prod_topology X' Y')"
unfolding h_def using fgim by auto
fix W w
assume W: "openin (prod_topology X Y) W"
@@ -1960,7 +1960,7 @@
"\<lbrakk>perfect_map X Z (g \<circ> f); f ` topspace X = topspace Y;
continuous_map X Y f; continuous_map Y Z g; inj_on g (topspace Y)\<rbrakk>
\<Longrightarrow> perfect_map X Y f"
- by (meson continuous_map_image_subset_topspace perfect_map_def proper_map_from_composition_right_inj)
+ by (meson continuous_map_openin_preimage_eq perfect_map_def proper_map_from_composition_right_inj)
subsection \<open>Regular spaces\<close>
@@ -2285,7 +2285,7 @@
fix C assume "closedin Z C"
then have "C \<subseteq> topspace Z"
by (simp add: closedin_subset)
- have "f ` topspace Z \<subseteq> topspace X" "g ` topspace Z \<subseteq> topspace Y"
+ have "f \<in> topspace Z \<rightarrow> topspace X" "g \<in> topspace Z \<rightarrow> topspace Y"
by (simp_all add: assms closed_map_imp_subset_topspace)
show "closedin (prod_topology X Y) ((\<lambda>x. (f x, g x)) ` C)"
unfolding closedin_def topspace_prod_topology
@@ -2293,7 +2293,7 @@
have "closedin Y (g ` C)"
using \<open>closedin Z C\<close> assms(3) closed_map_def by blast
with assms show "(\<lambda>x. (f x, g x)) ` C \<subseteq> topspace X \<times> topspace Y"
- using \<open>C \<subseteq> topspace Z\<close> \<open>f ` topspace Z \<subseteq> topspace X\<close> continuous_map_closedin subsetD by fastforce
+ by (smt (verit) SigmaI \<open>closedin Z C\<close> closed_map_def closedin_subset image_subset_iff)
have *: "\<exists>T. openin (prod_topology X Y) T \<and> (y1,y2) \<in> T \<and> T \<subseteq> topspace X \<times> topspace Y - (\<lambda>x. (f x, g x)) ` C"
if "(y1,y2) \<notin> (\<lambda>x. (f x, g x)) ` C" and y1: "y1 \<in> topspace X" and y2: "y2 \<in> topspace Y"
for y1 y2
@@ -5157,7 +5157,7 @@
qed
lemma closed_map_into_k_space:
- assumes "k_space Y" and fim: "f ` (topspace X) \<subseteq> topspace Y"
+ assumes "k_space Y" and fim: "f \<in> (topspace X) \<rightarrow> topspace Y"
and f: "\<And>K. compactin Y K
\<Longrightarrow> closed_map(subtopology X {x \<in> topspace X. f x \<in> K}) (subtopology Y K) f"
shows "closed_map X Y f"
@@ -5176,13 +5176,13 @@
qed
then show "closedin Y (f ` C)"
using \<open>k_space Y\<close> unfolding k_space
- by (meson \<open>closedin X C\<close> closedin_subset dual_order.trans fim image_mono)
+ by (meson \<open>closedin X C\<close> closedin_subset order.trans fim funcset_image subset_image_iff)
qed
text \<open>Essentially the same proof\<close>
lemma open_map_into_k_space:
- assumes "k_space Y" and fim: "f ` (topspace X) \<subseteq> topspace Y"
+ assumes "k_space Y" and fim: "f \<in> (topspace X) \<rightarrow> topspace Y"
and f: "\<And>K. compactin Y K
\<Longrightarrow> open_map (subtopology X {x \<in> topspace X. f x \<in> K}) (subtopology Y K) f"
shows "open_map X Y f"
@@ -5201,7 +5201,7 @@
qed
then show "openin Y (f ` C)"
using \<open>k_space Y\<close> unfolding k_space_open
- by (meson \<open>openin X C\<close> openin_subset dual_order.trans fim image_mono)
+ by (meson \<open>openin X C\<close> openin_subset order.trans fim funcset_image subset_image_iff)
qed
lemma quotient_map_into_k_space:
@@ -5255,7 +5255,7 @@
lemma open_map_into_k_space_eq:
assumes "k_space Y"
shows "open_map X Y f \<longleftrightarrow>
- f ` (topspace X) \<subseteq> topspace Y \<and>
+ f \<in> (topspace X) \<rightarrow> topspace Y \<and>
(\<forall>k. compactin Y k
\<longrightarrow> open_map (subtopology X {x \<in> topspace X. f x \<in> k}) (subtopology Y k) f)"
(is "?lhs=?rhs")
@@ -5269,7 +5269,7 @@
lemma closed_map_into_k_space_eq:
assumes "k_space Y"
shows "closed_map X Y f \<longleftrightarrow>
- f ` (topspace X) \<subseteq> topspace Y \<and>
+ f \<in> (topspace X) \<rightarrow> topspace Y \<and>
(\<forall>k. compactin Y k
\<longrightarrow> closed_map (subtopology X {x \<in> topspace X. f x \<in> k}) (subtopology Y k) f)"
(is "?lhs \<longleftrightarrow> ?rhs")
@@ -5281,7 +5281,7 @@
qed
lemma proper_map_into_k_space:
- assumes "k_space Y" and fim: "f ` (topspace X) \<subseteq> topspace Y"
+ assumes "k_space Y" and fim: "f \<in> (topspace X) \<rightarrow> topspace Y"
and f: "\<And>K. compactin Y K
\<Longrightarrow> proper_map (subtopology X {x \<in> topspace X. f x \<in> K})
(subtopology Y K) f"
@@ -5297,7 +5297,7 @@
lemma proper_map_into_k_space_eq:
assumes "k_space Y"
shows "proper_map X Y f \<longleftrightarrow>
- f ` (topspace X) \<subseteq> topspace Y \<and>
+ f \<in> (topspace X) \<rightarrow> topspace Y \<and>
(\<forall>K. compactin Y K
\<longrightarrow> proper_map (subtopology X {x \<in> topspace X. f x \<in> K}) (subtopology Y K) f)"
(is "?lhs \<longleftrightarrow> ?rhs")
@@ -5305,11 +5305,11 @@
show "?lhs \<Longrightarrow> ?rhs"
by (simp add: proper_map_imp_subset_topspace proper_map_restriction)
show "?rhs \<Longrightarrow> ?lhs"
- by (simp add: assms proper_map_into_k_space)
+ by (simp add: assms funcset_image proper_map_into_k_space)
qed
lemma compact_imp_proper_map:
- assumes "k_space Y" "kc_space Y" and fim: "f ` (topspace X) \<subseteq> topspace Y"
+ assumes "k_space Y" "kc_space Y" and fim: "f \<in> (topspace X) \<rightarrow> topspace Y"
and f: "continuous_map X Y f \<or> kc_space X"
and comp: "\<And>K. compactin Y K \<Longrightarrow> compactin X {x \<in> topspace X. f x \<in> K}"
shows "proper_map X Y f"
@@ -5325,12 +5325,12 @@
assumes "k_space Y" "kc_space Y"
and f: "continuous_map X Y f \<or> kc_space X"
shows "proper_map X Y f \<longleftrightarrow>
- f ` (topspace X) \<subseteq> topspace Y \<and>
+ f \<in> (topspace X) \<rightarrow> topspace Y \<and>
(\<forall>K. compactin Y K \<longrightarrow> compactin X {x \<in> topspace X. f x \<in> K})"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
show "?lhs \<Longrightarrow> ?rhs"
- by (simp add: proper_map_alt proper_map_imp_subset_topspace)
+ using \<open>k_space Y\<close> compactin_proper_map_preimage proper_map_into_k_space_eq by blast
qed (use assms compact_imp_proper_map in auto)
lemma compact_imp_perfect_map:
@@ -5338,7 +5338,7 @@
and "continuous_map X Y f"
and "\<And>K. compactin Y K \<Longrightarrow> compactin X {x \<in> topspace X. f x \<in> K}"
shows "perfect_map X Y f"
- by (simp add: assms compact_imp_proper_map perfect_map_def)
+ by (simp add: assms compact_imp_proper_map perfect_map_def flip: image_subset_iff_funcset)
end