--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy Wed Jul 12 23:11:59 2023 +0100
@@ -109,7 +109,7 @@
lemma cm_Euclidean_space_iff_continuous_on:
"continuous_map (subtopology (Euclidean_space m) S) (Euclidean_space n) f
\<longleftrightarrow> continuous_on (topspace (subtopology (Euclidean_space m) S)) f \<and>
- f ` (topspace (subtopology (Euclidean_space m) S)) \<subseteq> topspace (Euclidean_space n)"
+ f \<in> (topspace (subtopology (Euclidean_space m) S)) \<rightarrow> topspace (Euclidean_space n)"
(is "?P \<longleftrightarrow> ?Q \<and> ?R")
proof -
have ?Q if ?P
--- a/src/HOL/Analysis/Abstract_Limits.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Limits.thy Wed Jul 12 23:11:59 2023 +0100
@@ -178,7 +178,7 @@
shows "limitin Y (g \<circ> f) (g l) F"
proof -
have "g l \<in> topspace Y"
- by (meson assms continuous_map_def limitin_topspace)
+ by (meson assms continuous_map f image_eqI in_mono limitin_def)
moreover
have "\<And>U. \<lbrakk>\<forall>V. openin X V \<and> l \<in> V \<longrightarrow> (\<forall>\<^sub>F x in F. f x \<in> V); openin Y U; g l \<in> U\<rbrakk>
\<Longrightarrow> \<forall>\<^sub>F x in F. g (f x) \<in> U"
@@ -194,14 +194,14 @@
definition topcontinuous_at where
"topcontinuous_at X Y f x \<longleftrightarrow>
x \<in> topspace X \<and>
- (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+ f \<in> topspace X \<rightarrow> topspace Y \<and>
(\<forall>V. openin Y V \<and> f x \<in> V
\<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y \<in> U. f y \<in> V)))"
lemma topcontinuous_at_atin:
"topcontinuous_at X Y f x \<longleftrightarrow>
x \<in> topspace X \<and>
- (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+ f \<in> topspace X \<rightarrow> topspace Y \<and>
limitin Y f (f x) (atin X x)"
unfolding topcontinuous_at_def
by (fastforce simp add: limitin_atin)+
--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Wed Jul 12 23:11:59 2023 +0100
@@ -2583,7 +2583,7 @@
proof
show "?lhs \<Longrightarrow> ?rhs"
unfolding continuous_map_eq_topcontinuous_at topcontinuous_at_def
- by (metis centre_in_mball_iff openin_mball topspace_mtopology)
+ by (metis PiE centre_in_mball_iff openin_mball topspace_mtopology)
next
assume R: ?rhs
then have "\<forall>x\<in>topspace X. f x \<in> M"
@@ -2598,7 +2598,7 @@
lemma continuous_map_from_metric:
"continuous_map mtopology X f \<longleftrightarrow>
- f ` M \<subseteq> topspace X \<and>
+ f \<in> M \<rightarrow> topspace X \<and>
(\<forall>a \<in> M. \<forall>U. openin X U \<and> f a \<in> U \<longrightarrow> (\<exists>r>0. \<forall>x. x \<in> M \<and> d a x < r \<longrightarrow> f x \<in> U))"
proof (cases "f ` M \<subseteq> topspace X")
case True
@@ -2607,7 +2607,7 @@
next
case False
then show ?thesis
- by (simp add: continuous_map_eq_image_closure_subset_gen)
+ by (simp add: continuous_map_def image_subset_iff_funcset)
qed
text \<open>An abstract formulation, since the limits do not have to be sequential\<close>
@@ -2671,7 +2671,7 @@
proof -
have "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>l. limitin mtopology (\<lambda>n. f n x) l sequentially"
using \<open>mcomplete\<close> [unfolded mcomplete, rule_format] assms
- by (smt (verit) contf continuous_map_def eventually_mono topspace_mtopology)
+ by (smt (verit) contf continuous_map_def eventually_mono topspace_mtopology Pi_iff)
then obtain g where g: "\<And>x. x \<in> topspace X \<Longrightarrow> limitin mtopology (\<lambda>n. f n x) (g x) sequentially"
by metis
show thesis
@@ -5107,14 +5107,14 @@
qed
-lemma metrizable_space_product_topology:
+proposition metrizable_space_product_topology:
"metrizable_space (product_topology X I) \<longleftrightarrow>
topspace (product_topology X I) = {} \<or>
countable {i \<in> I. \<not> (\<exists>a. topspace(X i) \<subseteq> {a})} \<and>
(\<forall>i \<in> I. metrizable_space (X i))"
by (metis (mono_tags, lifting) empty_metrizable_space metrizable_topology_A metrizable_topology_B metrizable_topology_D)
-lemma completely_metrizable_space_product_topology:
+proposition completely_metrizable_space_product_topology:
"completely_metrizable_space (product_topology X I) \<longleftrightarrow>
topspace (product_topology X I) = {} \<or>
countable {i \<in> I. \<not> (\<exists>a. topspace(X i) \<subseteq> {a})} \<and>
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy Wed Jul 12 23:11:59 2023 +0100
@@ -894,7 +894,8 @@
qed
subsection \<open>Neigbourhood bases EXTRAS\<close>
-(* Neigbourhood bases (useful for "local" properties of various kind). *)
+
+text \<open>Neigbourhood bases: useful for "local" properties of various kinds\<close>
lemma openin_topology_neighbourhood_base_unique:
"openin X = arbitrary union_of P \<longleftrightarrow>
@@ -1192,7 +1193,7 @@
assumes "continuous_map X Y f" "t0_space Y" and x: "x \<in> topspace X"
shows "f (Kolmogorov_quotient X x) = f x"
using assms unfolding continuous_map_def t0_space_def
- by (smt (verit, ccfv_SIG) Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace x mem_Collect_eq)
+ by (smt (verit, ccfv_threshold) Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace PiE mem_Collect_eq)
lemma t0_space_Kolmogorov_quotient:
"t0_space (subtopology X (Kolmogorov_quotient X ` topspace X))"
@@ -1239,7 +1240,7 @@
have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S; Kolmogorov_quotient X x = Kolmogorov_quotient X y\<rbrakk> \<Longrightarrow> f x = f y"
using assms
apply (simp add: Kolmogorov_quotient_eq t0_space_def continuous_map_def Int_absorb1 openin_subtopology)
- by (smt (verit, del_insts) Int_iff mem_Collect_eq)
+ by (smt (verit, del_insts) Int_iff mem_Collect_eq Pi_iff)
then obtain g where g: "continuous_map (subtopology X (Kolmogorov_quotient X ` S)) Y g"
"g ` (topspace X \<inter> Kolmogorov_quotient X ` S) = f ` S"
"\<And>x. x \<in> S \<Longrightarrow> g (Kolmogorov_quotient X x) = f x"
@@ -1321,7 +1322,7 @@
obtain r where r: "continuous_map X (subtopology X S) r" "\<forall>x\<in>S. r x = x"
using assms by (meson retract_of_space_def)
then have \<section>: "S = {x \<in> topspace X. r x = x}"
- using S retract_of_space_imp_subset by (force simp: continuous_map_def)
+ using S retract_of_space_imp_subset by (force simp: continuous_map_def Pi_iff)
show ?thesis
unfolding \<section>
using r continuous_map_into_fulltopology assms
@@ -1345,7 +1346,8 @@
assume ?rhs
then show ?lhs
unfolding homeomorphic_maps_def
- by (smt (verit, ccfv_threshold) continuous_map_eq continuous_map_subtopology_fst embedding_map_def embedding_map_graph homeomorphic_eq_everything_map image_cong image_iff prod.collapse prod.inject)
+ by (smt (verit, del_insts) continuous_map_eq continuous_map_subtopology_fst embedding_map_def
+ embedding_map_graph homeomorphic_eq_everything_map image_cong image_iff prod.sel(1))
qed
@@ -1663,9 +1665,8 @@
have "continuous_map (subtopology X A) (subtopology Y K) f" if "kc_space X"
unfolding continuous_map_closedin
proof (intro conjI strip)
- show "f x \<in> topspace (subtopology Y K)"
- if "x \<in> topspace (subtopology X A)" for x
- using that A_def K compactin_subset_topspace by auto
+ show "f \<in> topspace (subtopology X A) \<rightarrow> topspace (subtopology Y K)"
+ using A_def K compactin_subset_topspace by fastforce
next
fix C
assume C: "closedin (subtopology Y K) C"
@@ -1927,7 +1928,7 @@
using proper_map_paired [OF assms] by (simp add: o_def)
lemma proper_map_from_composition_right:
- assumes "Hausdorff_space Y" "proper_map X Z (g \<circ> f)" and "continuous_map X Y f"
+ assumes "Hausdorff_space Y" "proper_map X Z (g \<circ> f)" and contf: "continuous_map X Y f"
and contg: "continuous_map Y Z g"
shows "proper_map X Y f"
proof -
@@ -1935,7 +1936,7 @@
have "proper_map X Y (fst \<circ> (\<lambda>x. (f x, (g \<circ> f) x)))"
proof (rule proper_map_compose)
have [simp]: "x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y" for x
- by (meson assms(3) continuous_map_def)
+ using contf continuous_map_preimage_topspace by auto
show "proper_map X YZ (\<lambda>x. (f x, (g \<circ> f) x))"
unfolding YZ_def
using assms
@@ -2558,7 +2559,8 @@
using \<open>closed_map X Y f\<close> \<open>closedin X C\<close> \<open>openin X U2\<close> closed_map_def by blast
moreover
have "f x \<in> topspace Y - f ` (C - U2)"
- using \<open>closedin X C\<close> \<open>continuous_map X Y f\<close> \<open>x \<in> topspace X\<close> closedin_subset continuous_map_def subV by fastforce
+ using \<open>closedin X C\<close> \<open>continuous_map X Y f\<close> \<open>x \<in> topspace X\<close> closedin_subset continuous_map_def subV
+ by (fastforce simp: Pi_iff)
ultimately
obtain V1 V2 where VV: "openin Y V1" "openin Y V2" "f x \<in> V1"
and subV2: "f ` (C - U2) \<subseteq> V2" and "disjnt V1 V2"
@@ -3213,7 +3215,7 @@
assume x: "x \<in> topspace X"
then obtain U K where "openin X' U" "compactin X' K" "f x \<in> U" "U \<subseteq> K"
using assms unfolding locally_compact_space_def perfect_map_def
- by (metis (no_types, lifting) continuous_map_closedin)
+ by (metis (no_types, lifting) continuous_map_closedin Pi_iff)
show "\<exists>U K. openin X U \<and> compactin X K \<and> x \<in> U \<and> U \<subseteq> K"
proof (intro exI conjI)
have "continuous_map X X' f"
@@ -3433,7 +3435,7 @@
by (auto simp: retraction_maps_def)
show "S \<subseteq> {x \<in> topspace Y. r' x \<in> U}" "T \<subseteq> {x \<in> topspace Y. r' x \<in> V}"
using openin_continuous_map_preimage UV r' \<open>closedin Y S\<close> \<open>closedin Y T\<close>
- by (auto simp add: closedin_def continuous_map_closedin retraction_maps_def subset_iff)
+ by (auto simp add: closedin_def continuous_map_closedin retraction_maps_def subset_iff Pi_iff)
show "disjnt {x \<in> topspace Y. r' x \<in> U} {x \<in> topspace Y. r' x \<in> V}"
using \<open>disjnt U V\<close> by (auto simp: disjnt_def)
qed
@@ -4293,7 +4295,7 @@
unfolding quasi_component_of_def
proof (intro strip conjI)
show "f x \<in> topspace Y" "f y \<in> topspace Y"
- using assms by (simp_all add: continuous_map_def quasi_component_of_def)
+ using assms by (simp_all add: continuous_map_def quasi_component_of_def Pi_iff)
fix T
assume "closedin Y T \<and> openin Y T"
with assms show "(f x \<in> T) = (f y \<in> T)"
--- a/src/HOL/Analysis/Abstract_Topology.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Wed Jul 12 23:11:59 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
--- a/src/HOL/Analysis/Abstract_Topology_2.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Wed Jul 12 23:11:59 2023 +0100
@@ -872,7 +872,7 @@
show "continuous_map (subtopology X ?T) Y g"
by (simp add: contg)
have "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> X closure_of {x \<in> topspace X. p x \<in> topspace Z - U}"
- by (smt (verit, del_insts) DiffI mem_Collect_eq subset_iff closure_of_mono continuous_map_closedin contp)
+ by (smt (verit) Collect_mono_iff DiffI closure_of_mono continuous_map contp image_subset_iff)
then show "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> ?T"
by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]])
qed
@@ -1352,7 +1352,7 @@
lemma homeomorphic_path_connected_space_imp:
"\<lbrakk>path_connected_space X; X homeomorphic_space Y\<rbrakk> \<Longrightarrow> path_connected_space Y"
unfolding homeomorphic_space_def homeomorphic_maps_def
- by (metis (no_types, opaque_lifting) continuous_map_closedin continuous_map_image_subset_topspace imageI order_class.order.antisym path_connectedin_continuous_map_image path_connectedin_topspace subsetI)
+ by (smt (verit, ccfv_threshold) homeomorphic_imp_surjective_map homeomorphic_maps_def homeomorphic_maps_map path_connectedin_continuous_map_image path_connectedin_topspace)
lemma homeomorphic_path_connected_space:
"X homeomorphic_space Y \<Longrightarrow> path_connected_space X \<longleftrightarrow> path_connected_space Y"
--- a/src/HOL/Analysis/Function_Topology.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Function_Topology.thy Wed Jul 12 23:11:59 2023 +0100
@@ -490,10 +490,10 @@
using H(2) \<open>J \<subseteq> I\<close> \<open>finite J\<close> assms(1) by blast
ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
next
- have "f ` topspace T1 \<subseteq> topspace (product_topology T I)"
- using assms continuous_map_def by fastforce
+ have "f \<in> topspace T1 \<rightarrow> topspace (product_topology T I)"
+ using assms continuous_map_funspace by (force simp: Pi_iff)
then show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
- by (simp add: product_topology_def)
+ by (fastforce simp add: product_topology_def Pi_iff)
qed
lemma continuous_map_product_then_coordinatewise [intro]:
--- a/src/HOL/Analysis/Path_Connected.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Wed Jul 12 23:11:59 2023 +0100
@@ -4026,7 +4026,7 @@
qed auto
qed
then show "continuous_map (top_of_set ?S) X g"
- by (simp add: continuous_map_def gf)
+ by (simp add: "1" continuous_map)
qed (auto simp: gf)
qed
qed
--- a/src/HOL/Analysis/Product_Topology.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Product_Topology.thy Wed Jul 12 23:11:59 2023 +0100
@@ -190,7 +190,7 @@
have f: "f x = (?g x, ?h x)" for x
by auto
show ?thesis
- proof (cases "(\<forall>x \<in> topspace Z. ?g x \<in> topspace X) \<and> (\<forall>x \<in> topspace Z. ?h x \<in> topspace Y)")
+ proof (cases "?g \<in> topspace Z \<rightarrow> topspace X \<and> ?h \<in> topspace Z \<rightarrow> topspace Y")
case True
show ?thesis
proof safe
@@ -199,7 +199,7 @@
unfolding continuous_map_def using True that
apply clarify
apply (drule_tac x="U \<times> topspace Y" in spec)
- by (simp add: openin_prod_Times_iff mem_Times_iff cong: conj_cong)
+ by (auto simp: openin_prod_Times_iff mem_Times_iff Pi_iff cong: conj_cong)
with True show "continuous_map Z X (fst \<circ> f)"
by (auto simp: continuous_map_def)
next
@@ -208,7 +208,7 @@
unfolding continuous_map_def using True that
apply clarify
apply (drule_tac x="topspace X \<times> V" in spec)
- by (simp add: openin_prod_Times_iff mem_Times_iff cong: conj_cong)
+ by (simp add: openin_prod_Times_iff mem_Times_iff Pi_iff cong: conj_cong)
with True show "continuous_map Z Y (snd \<circ> f)"
by (auto simp: continuous_map_def)
next
@@ -227,9 +227,9 @@
done
qed
show "continuous_map Z (prod_topology X Y) f"
- using True by (simp add: continuous_map_def openin_prod_topology_alt mem_Times_iff *)
+ using True by (force simp: continuous_map_def openin_prod_topology_alt mem_Times_iff *)
qed
- qed (auto simp: continuous_map_def)
+ qed (force simp: continuous_map_def)
qed
lemma continuous_map_paired:
@@ -402,7 +402,7 @@
using \<C> by simp
obtain \<U> \<V> where \<U>: "\<And>U. U \<in> \<U> \<Longrightarrow> openin X U" "\<Y>' = (\<lambda>U. U \<times> topspace Y) ` \<U>"
and \<V>: "\<And>V. V \<in> \<V> \<Longrightarrow> openin Y V" "\<X>' = (\<lambda>V. topspace X \<times> V) ` \<V>"
- using XY by (clarsimp simp add: \<X>_def \<Y>_def subset_image_iff) (force simp add: subset_iff)
+ using XY by (clarsimp simp add: \<X>_def \<Y>_def subset_image_iff) (force simp: subset_iff)
have "\<exists>\<D>. finite \<D> \<and> \<D> \<subseteq> \<X>' \<union> \<Y>' \<and> topspace X \<times> topspace Y \<subseteq> \<Union> \<D>"
proof -
have "topspace X \<subseteq> \<Union>\<U> \<or> topspace Y \<subseteq> \<Union>\<V>"
@@ -463,7 +463,7 @@
show "(finite intersection_of (\<lambda>x. x \<in> \<X> \<or> x \<in> \<Y>)) (U \<times> V)"
apply (simp add: intersection_of_def \<X>_def \<Y>_def)
apply (rule_tac x="{(U \<times> topspace Y),(topspace X \<times> V)}" in exI)
- using \<open>openin X U\<close> \<open>openin Y V\<close> openin_subset UV apply (fastforce simp add:)
+ using \<open>openin X U\<close> \<open>openin Y V\<close> openin_subset UV apply (fastforce simp:)
done
qed
ultimately show ?thesis
@@ -489,12 +489,18 @@
lemma homeomorphic_maps_prod:
"homeomorphic_maps (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y)) (\<lambda>(x,y). (f' x, g' y)) \<longleftrightarrow>
- topspace(prod_topology X Y) = {} \<and>
- topspace(prod_topology X' Y') = {} \<or>
- homeomorphic_maps X X' f f' \<and>
- homeomorphic_maps Y Y' g g'"
+ topspace(prod_topology X Y) = {} \<and> topspace(prod_topology X' Y') = {}
+ \<or> homeomorphic_maps X X' f f' \<and> homeomorphic_maps Y Y' g g'" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
unfolding homeomorphic_maps_def continuous_map_prod_top
- by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
+ by (auto simp: continuous_map_on_empty continuous_map_on_empty2 ball_conj_distrib)
+next
+ show "?rhs \<Longrightarrow> ?lhs"
+ unfolding homeomorphic_maps_def
+ by (auto simp: continuous_map_prod_top continuous_map_on_empty continuous_map_on_empty2)
+qed
+
lemma homeomorphic_maps_swap:
"homeomorphic_maps (prod_topology X Y) (prod_topology Y X)
--- a/src/HOL/Analysis/T1_Spaces.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/T1_Spaces.thy Wed Jul 12 23:11:59 2023 +0100
@@ -451,7 +451,8 @@
fix x y
assume x: "x \<in> topspace X" and y: "y \<in> topspace X" and "x \<noteq> y"
then obtain U V where "openin Y U" "openin Y V" "f x \<in> U" "f y \<in> V" "disjnt U V"
- using assms unfolding Hausdorff_space_def continuous_map_def by (meson inj_onD)
+ using assms
+ by (smt (verit, ccfv_threshold) Hausdorff_space_def continuous_map image_subset_iff inj_on_def)
show "\<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
proof (intro exI conjI)
show "openin X {x \<in> topspace X. f x \<in> U}"
@@ -501,12 +502,12 @@
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"
+ have "x \<in> topspace X" and y: "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
+ then have "f x \<in> topspace Y"
+ using continuous_map_image_subset_topspace f by blast
+ then obtain U V where UV: "openin Y U" "openin Y V" "f x \<in> U" "y \<in> V" "disjnt U V"
+ using Y y Hausdorff_space_def by metis
show ?thesis
proof (intro exI conjI)
show "openin X {x \<in> topspace X. f x \<in> U}"
@@ -547,10 +548,8 @@
show "continuous_map (subtopology Y (f ` (topspace X))) X g"
unfolding continuous_map_closedin
proof (intro conjI ballI allI impI)
- fix x
- assume "x \<in> topspace (subtopology Y (f ` topspace X))"
- then show "g x \<in> topspace X"
- by (auto simp: gf)
+ show "g \<in> topspace (subtopology Y (f ` topspace X)) \<rightarrow> topspace X"
+ using gf by auto
next
fix C
assume C: "closedin X C"
--- a/src/HOL/Analysis/Urysohn.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Urysohn.thy Wed Jul 12 23:11:59 2023 +0100
@@ -380,7 +380,7 @@
and ga: "g ` SA \<subseteq> {- d}" and gb: "g ` SB \<subseteq> {d}"
using Urysohn_lemma \<open>normal_space X\<close> by metis
then have g_le_d: "\<And>x. x \<in> topspace X \<Longrightarrow> \<bar>g x\<bar> \<le> d"
- by (simp add: abs_le_iff continuous_map_def minus_le_iff)
+ by (fastforce simp: abs_le_iff continuous_map_def minus_le_iff)
have g_eq_d: "\<And>x. \<lbrakk>x \<in> S; f x - h x \<le> -d\<rbrakk> \<Longrightarrow> g x = -d"
using ga by (auto simp: SA_def)
have g_eq_negd: "\<And>x. \<lbrakk>x \<in> S; f x - h x \<ge> d\<rbrakk> \<Longrightarrow> g x = d"
--- a/src/HOL/Homology/Brouwer_Degree.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Homology/Brouwer_Degree.thy Wed Jul 12 23:11:59 2023 +0100
@@ -1026,7 +1026,7 @@
have rimeq: "r ` (topspace (subtopology (nsphere n) {x. x k \<le> 0}) \<inter> {x. x k = 0})
= topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {x. x k = 0}"
using continuous_map_eq_topcontinuous_at continuous_map_nsphere_reflection topcontinuous_at_atin
- by (fastforce simp: r_def)
+ by (fastforce simp: r_def Pi_iff)
show "?f \<in> iso ?G (relative_homology_group p (subtopology (nsphere n) {x. x k \<ge> 0}) {x. x k = 0})"
using homeomorphic_map_relative_homology_iso [OF hmrs Int_lower1 rimeq]
by (metis hom_induced_restrict relative_homology_group_restrict)
--- a/src/HOL/Homology/Homology_Groups.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Homology/Homology_Groups.thy Wed Jul 12 23:11:59 2023 +0100
@@ -508,8 +508,8 @@
hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
\<in> carrier (relative_homology_group p Y T)"
for p X S Y f T c
- using hom_carrier [OF 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]]
- by (simp add: image_subset_iff subtopology_restrict continuous_map_def)
+ using hom_carrier [OF 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]]
+ continuous_map_image_subset_topspace by fastforce
have inhom: "(\<lambda>c. if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
c \<in> carrier (relative_homology_group p X S)
then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
@@ -530,10 +530,10 @@
proof (cases "continuous_map X Y f")
case True
then have "f ` (topspace X \<inter> S) \<subseteq> topspace Y"
- by (meson IntE continuous_map_def image_subsetI)
+ using continuous_map_image_subset_topspace by blast
then show ?thesis
using True False that
- using 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]
+ using 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]
by (simp add: 4 continuous_map_image_subset_topspace hom_mult not_less group.is_monoid monoid.m_closed Int_left_absorb)
qed (simp add: group.is_monoid)
qed
@@ -543,7 +543,7 @@
f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
for p X S Y T f c
using 2 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p c]
- by simp (meson IntE continuous_map_def image_subsetI)
+ continuous_map_image_subset_topspace by fastforce
show ?thesis
apply (rule_tac x="\<lambda>p X S Y T f c.
if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
--- a/src/HOL/Homology/Invariance_of_Domain.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Homology/Invariance_of_Domain.thy Wed Jul 12 23:11:59 2023 +0100
@@ -54,7 +54,7 @@
moreover have "topspace (nsphere n) \<inter> {f. f n = 0} = topspace (nsphere (n - Suc 0))"
by (metis subt_eq topspace_subtopology)
ultimately show ?thesis
- using cmr continuous_map_def by fastforce
+ using fim by auto
qed
then have fimeq: "f ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff)
@@ -623,7 +623,7 @@
using rm_ret [OF \<open>squashable 0 UNIV\<close>] by auto
then have "ret 0 x \<in> topspace (Euclidean_space n)"
if "x \<in> topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x
- using that by (simp add: continuous_map_def retraction_maps_def)
+ using that by (metis continuous_map_image_subset_topspace image_subset_iff retraction_maps_def)
then show "(ret 0) ` (lo \<inter> hi) \<subseteq> topspace (Euclidean_space n) - S"
by (auto simp: local.cong ret_def hi_def lo_def)
show "homotopic_with (\<lambda>h. h ` (lo \<inter> hi) \<subseteq> lo \<inter> hi) (Euclidean_space (Suc n)) (Euclidean_space (Suc n)) (ret 0) id"
@@ -1353,7 +1353,7 @@
have "openin (Euclidean_space n) (h ` e ` {- r<..<r})"
unfolding 1
proof (subst homeomorphic_map_openness [OF hom_e', symmetric])
- show "h ` e ` {- r<..<r} \<subseteq> topspace (Euclidean_space 1)"
+ show hesub: "h ` e ` {- r<..<r} \<subseteq> topspace (Euclidean_space 1)"
using "1" C_def \<open>\<And>r. B r \<subseteq> C r\<close> cmh continuous_map_image_subset_topspace eBr by fastforce
have cont: "continuous_on {- r<..<r} (e' \<circ> h \<circ> e)"
proof (intro continuous_on_compose)
@@ -1365,12 +1365,10 @@
by (auto simp: eBr \<open>\<And>r. B r \<subseteq> C r\<close>) (auto simp: B_def)
with cmh show "continuous_on (e ` {- r<..<r}) h"
by (meson cm_Euclidean_space_iff_continuous_on continuous_on_subset)
- have "h ` (e ` {- r<..<r}) \<subseteq> topspace ?E"
- using subCr cmh by (simp add: continuous_map_def image_subset_iff)
- moreover have "continuous_on (topspace ?E) e'"
+ have "continuous_on (topspace ?E) e'"
by (metis "1" continuous_map_Euclidean_space_iff hom_ee' homeomorphic_maps_def)
- ultimately show "continuous_on (h ` e ` {- r<..<r}) e'"
- by (simp add: e'_def continuous_on_subset)
+ then show "continuous_on (h ` e ` {- r<..<r}) e'"
+ using hesub by (simp add: 1 e'_def continuous_on_subset)
qed
show "openin euclideanreal (e' ` h ` e ` {- r<..<r})"
using injective_eq_1d_open_map_UNIV [OF cont] inj by (simp add: image_image is_interval_1)
--- a/src/HOL/Homology/Simplices.thy Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Homology/Simplices.thy Wed Jul 12 23:11:59 2023 +0100
@@ -699,7 +699,7 @@
"\<lbrakk>singular_simplex p X c;
\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk>
\<Longrightarrow> simplex_map p f c = simplex_map p g c"
- by (auto simp: singular_simplex_def simplex_map_def continuous_map_def)
+ by (auto simp: singular_simplex_def simplex_map_def continuous_map_def Pi_iff)
lemma simplex_map_id_gen:
"\<lbrakk>singular_simplex p X c;
@@ -879,14 +879,14 @@
have "continuous_map (subtopology (product_topology (\<lambda>n. euclideanreal) UNIV) (standard_simplex p)) X f"
using \<open>singular_simplex p X f\<close> singular_simplex_def by blast
then have "\<And>c. c \<notin> standard_simplex p \<or> f c = a"
- by (simp add: assms continuous_map_def)
+ by (simp add: assms continuous_map_def Pi_iff)
then show ?thesis
by (metis (no_types) L extensional_restrict restrict_ext singular_simplex_def)
qed
next
assume ?rhs
with assms show ?lhs
- by (auto simp: singular_simplex_def topspace_subtopology)
+ by (auto simp: singular_simplex_def)
qed
lemma singular_chain_singleton:
--- a/src/HOL/ROOT Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/ROOT Wed Jul 12 23:11:59 2023 +0100
@@ -98,7 +98,7 @@
document_files "root.bib" "root.tex"
session "HOL-Analysis" (main timing) in Analysis = HOL +
- options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+ options [timeout=1800, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
document_variants = "document:manual=-proof,-ML,-unimportant"]
sessions
"HOL-Library"
@@ -111,7 +111,7 @@
"root.bib"
session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" +
- options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+ options [timeout=300, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
document_variants = "document:manual=-proof,-ML,-unimportant"]
theories
Complex_Analysis
@@ -125,7 +125,7 @@
Metric_Arith_Examples
session "HOL-Homology" (timing) in Homology = "HOL-Analysis" +
- options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+ options [timeout=300, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
document_variants = "document:manual=-proof,-ML,-unimportant"]
sessions
"HOL-Algebra"
@@ -322,6 +322,7 @@
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
"
+ options [timeout = 300]
sessions
"HOL-Algebra"
theories
@@ -846,6 +847,7 @@
ATP_Problem_Import
session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
+ options [timeout = 600]
sessions
"HOL-Combinatorics"
theories