--- a/src/HOL/Analysis/Abstract_Topology.thy Mon Jul 10 18:48:22 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Tue Jul 11 20:21:58 2023 +0100
@@ -1454,7 +1454,7 @@
definition continuous_map where
"continuous_map X Y f \<equiv>
- (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+ f \<in> topspace X \<rightarrow> topspace Y \<and>
(\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
lemma continuous_map:
@@ -1466,17 +1466,24 @@
"continuous_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
by (auto simp: continuous_map_def)
+lemma continuous_map_funspace:
+ "continuous_map X Y f \<Longrightarrow> f \<in> topspace X \<rightarrow> topspace Y"
+ by (auto simp: continuous_map_def)
+
lemma continuous_map_on_empty: "topspace X = {} \<Longrightarrow> continuous_map X Y f"
by (auto simp: continuous_map_def)
+lemma continuous_map_on_empty2: "topspace Y = {} \<Longrightarrow> continuous_map X Y f \<longleftrightarrow> topspace X = {}"
+ by (auto simp: continuous_map_def)
+
lemma continuous_map_closedin:
"continuous_map X Y f \<longleftrightarrow>
- (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+ f \<in> topspace X \<rightarrow> topspace Y \<and>
(\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
proof -
have "(\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}) =
(\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
- if "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
+ if "f \<in> topspace X \<rightarrow> topspace Y"
proof -
have eq: "{x \<in> topspace X. f x \<in> topspace Y \<and> f x \<notin> C} = (topspace X - {x \<in> topspace X. f x \<in> C})" for C
using that by blast
@@ -1555,9 +1562,7 @@
shows "continuous_map X Y f"
unfolding continuous_map_closedin
proof (intro conjI ballI allI impI)
- fix x
- assume "x \<in> topspace X"
- then show "f x \<in> topspace Y"
+ show "f \<in> topspace X \<rightarrow> topspace Y"
using assms closure_of_subset_topspace by fastforce
next
fix C
@@ -1588,9 +1593,9 @@
lemma continuous_map_eq_image_closure_subset_gen:
"continuous_map X Y f \<longleftrightarrow>
- f ` (topspace X) \<subseteq> topspace Y \<and>
+ f \<in> topspace X \<rightarrow> topspace Y \<and>
(\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
- using continuous_map_subset_aux1 continuous_map_subset_aux2 continuous_map_image_subset_topspace by metis
+ by (meson Pi_iff continuous_map continuous_map_eq_image_closure_subset image_subset_iff)
lemma continuous_map_closure_preimage_subset:
"continuous_map X Y f
@@ -1650,15 +1655,13 @@
shows "continuous_map X X'' (g \<circ> f)"
unfolding continuous_map_def
proof (intro conjI ballI allI impI)
- fix x
- assume "x \<in> topspace X"
- then show "(g \<circ> f) x \<in> topspace X''"
+ show "g \<circ> f \<in> topspace X \<rightarrow> topspace X''"
using assms unfolding continuous_map_def by force
next
fix U
assume "openin X'' U"
have eq: "{x \<in> topspace X. (g \<circ> f) x \<in> U} = {x \<in> topspace X. f x \<in> {y. y \<in> topspace X' \<and> g y \<in> U}}"
- by auto (meson f continuous_map_def)
+ using continuous_map_image_subset_topspace f by force
show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U}"
unfolding eq
using assms unfolding continuous_map_def
@@ -1672,7 +1675,7 @@
have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
using assms by auto
show ?thesis
- using assms by (simp add: continuous_map_def eq)
+ using assms by (force simp add: continuous_map_def eq)
qed
lemma restrict_continuous_map [simp]:
@@ -2327,8 +2330,8 @@
shows "continuous_map X' X'' g"
unfolding quotient_map_def continuous_map_def
proof (intro conjI ballI allI impI)
- show "\<And>x'. x' \<in> topspace X' \<Longrightarrow> g x' \<in> topspace X''"
- using assms unfolding quotient_map_def
+ show "g \<in> topspace X' \<rightarrow> topspace X''"
+ using assms unfolding quotient_map_def Pi_iff
by (metis (no_types, opaque_lifting) continuous_map_image_subset_topspace image_comp image_subset_iff)
next
fix U'' :: "'c set"
@@ -2657,7 +2660,7 @@
\<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>y. y \<in> topspace Y \<Longrightarrow> g y = g' y\<rbrakk>
\<Longrightarrow> homeomorphic_maps X Y f' g'"
unfolding homeomorphic_maps_def
- by (metis continuous_map_eq continuous_map_eq_image_closure_subset_gen image_subset_iff)
+ by (metis continuous_map_eq continuous_map_image_subset_topspace image_subset_iff)
lemma homeomorphic_maps_sym:
"homeomorphic_maps X Y f g \<longleftrightarrow> homeomorphic_maps Y X g f"
@@ -2711,7 +2714,7 @@
homeomorphic_maps Y X'' g k
\<Longrightarrow> homeomorphic_maps X X'' (g \<circ> f) (h \<circ> k)"
unfolding homeomorphic_maps_def
- by (auto simp: continuous_map_compose; simp add: continuous_map_def)
+ by (auto simp: continuous_map_compose; simp add: continuous_map_def Pi_iff)
lemma homeomorphic_eq_everything_map:
"homeomorphic_map X Y f \<longleftrightarrow>
@@ -2784,11 +2787,13 @@
show ?rhs
proof (intro conjI bijective_open_imp_homeomorphic_map L)
show "open_map X Y f"
- using L using open_eq_continuous_inverse_map [of concl: X Y f g] by (simp add: continuous_map_def)
+ using L using open_eq_continuous_inverse_map [of concl: X Y f g]
+ by (simp add: continuous_map_def Pi_iff)
show "open_map Y X g"
- using L using open_eq_continuous_inverse_map [of concl: Y X g f] by (simp add: continuous_map_def)
+ using L using open_eq_continuous_inverse_map [of concl: Y X g f]
+ by (simp add: continuous_map_def Pi_iff)
show "f ` topspace X = topspace Y" "g ` topspace Y = topspace X"
- using L by (force simp: continuous_map_closedin)+
+ using L by (force simp: continuous_map_closedin Pi_iff)+
show "inj_on f (topspace X)" "inj_on g (topspace Y)"
using L unfolding inj_on_def by metis+
qed
@@ -3020,7 +3025,7 @@
have "f ` (topspace X \<inter> S) \<subseteq> topspace Y \<inter> T"
using S hom homeomorphic_imp_surjective_map by fastforce
then show "f ` (topspace X \<inter> S) = topspace Y \<inter> T"
- using that unfolding homeomorphic_maps_def continuous_map_def
+ using that unfolding homeomorphic_maps_def continuous_map_def Pi_iff
by (smt (verit, del_insts) Int_iff S image_iff subsetI subset_antisym)
qed
then show ?thesis
@@ -3064,8 +3069,8 @@
lemma homeomorphic_empty_space_eq:
assumes "topspace X = {}"
shows "X homeomorphic_space Y \<longleftrightarrow> topspace Y = {}"
- unfolding homeomorphic_maps_def homeomorphic_space_def
- by (metis assms continuous_map_on_empty continuous_map_closedin ex_in_conv)
+ using assms
+ by (auto simp: homeomorphic_maps_def homeomorphic_space_def continuous_map_def)
lemma homeomorphic_space_unfold:
assumes "X homeomorphic_space Y"
@@ -3993,7 +3998,8 @@
lemma retraction_maps_eq:
"\<lbrakk>retraction_maps X Y f g; \<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>x. x \<in> topspace Y \<Longrightarrow> g x = g' x\<rbrakk>
\<Longrightarrow> retraction_maps X Y f' g'"
- unfolding retraction_maps_def by (metis (no_types, lifting) continuous_map_def continuous_map_eq)
+ unfolding retraction_maps_def
+ by (metis continuous_map_eq continuous_map_image_subset_topspace image_subset_iff)
lemma section_map_eq:
"\<lbrakk>section_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> section_map X Y g"
@@ -4012,8 +4018,8 @@
proof
assume ?lhs
then obtain g where "homeomorphic_maps X Y f g"
- unfolding homeomorphic_maps_def retraction_map_def section_map_def
- by (smt (verit, best) continuous_map_def retraction_maps_def)
+ unfolding homeomorphic_maps_def retraction_map_def section_map_def
+ by (smt (verit) Pi_iff continuous_map_def retraction_maps_def)
then show ?rhs
using homeomorphic_map_maps by blast
next
@@ -4034,7 +4040,7 @@
unfolding quotient_map_def
proof (intro conjI subsetI allI impI)
show "f ` topspace X = topspace Y"
- using assms by (force simp: retraction_map_def retraction_maps_def continuous_map_def)
+ using assms by (force simp: retraction_map_def retraction_maps_def continuous_map_def Pi_iff)
next
fix U
assume U: "U \<subseteq> topspace Y"
@@ -4043,12 +4049,13 @@
"openin Y {x \<in> topspace Y. g x \<in> {x \<in> topspace X. f x \<in> U}}" for g
using openin_subopen U that by fastforce
then show "openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
- using assms by (auto simp: retraction_map_def retraction_maps_def continuous_map_def)
+ using assms by (auto simp: retraction_map_def retraction_maps_def continuous_map_def Pi_iff)
qed
lemma retraction_maps_compose:
"\<lbrakk>retraction_maps X Y f f'; retraction_maps Y Z g g'\<rbrakk> \<Longrightarrow> retraction_maps X Z (g \<circ> f) (f' \<circ> g')"
- by (clarsimp simp: retraction_maps_def continuous_map_compose) (simp add: continuous_map_def)
+ unfolding retraction_maps_def
+ by (smt (verit, ccfv_threshold) comp_apply continuous_map_compose continuous_map_image_subset_topspace image_subset_iff)
lemma retraction_map_compose:
"\<lbrakk>retraction_map X Y f; retraction_map Y Z g\<rbrakk> \<Longrightarrow> retraction_map X Z (g \<circ> f)"
@@ -4567,16 +4574,16 @@
assumes P: "openin Y = arbitrary union_of P"
shows
"continuous_map X Y f \<longleftrightarrow>
- (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and> (\<forall>U. P U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
+ f \<in> topspace X \<rightarrow> topspace Y \<and> (\<forall>U. P U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
(is "?lhs=?rhs")
proof
assume L: ?lhs
- then have "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
- by (meson continuous_map_def)
+ then have "f \<in> topspace X \<rightarrow> topspace Y"
+ by (simp add: continuous_map_funspace)
moreover have "\<And>U. P U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
using L assms continuous_map openin_topology_base_unique by fastforce
ultimately show ?rhs by auto
-qed (simp add: assms continuous_map_into_topology_base)
+qed (simp add: assms Pi_iff continuous_map_into_topology_base)
lemma continuous_map_into_topology_subbase:
fixes U P
@@ -4613,13 +4620,13 @@
assumes "Y = topology(arbitrary union_of (finite intersection_of P relative_to U))"
shows
"continuous_map X Y f \<longleftrightarrow>
- (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and> (\<forall>U. P U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
+ f \<in> topspace X \<rightarrow> topspace Y \<and> (\<forall>U. P U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
(is "?lhs=?rhs")
proof
assume L: ?lhs
show ?rhs
proof (intro conjI strip)
- show "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
+ show "f \<in> topspace X \<rightarrow> topspace Y"
using L continuous_map_def by fastforce
fix V
assume "P V"
@@ -5048,8 +5055,9 @@
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: Pi_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)
+ using contf gf \<open>y \<in> topspace Y\<close>
+ unfolding eq continuous_map_def proper_map_def
+ by blast
qed