--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Mon Jul 03 16:46:37 2023 +0100
@@ -2645,7 +2645,7 @@
lemma continuous_map_uniform_limit_alt:
assumes contf: "\<forall>\<^sub>F \<xi> in F. continuous_map X mtopology (f \<xi>)"
- and gim: "g ` (topspace X) \<subseteq> M"
+ and gim: "g \<in> topspace X \<rightarrow> M"
and dfg: "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> \<forall>\<^sub>F \<xi> in F. \<forall>x \<in> topspace X. d (f \<xi> x) (g x) < \<epsilon>"
and nontriv: "\<not> trivial_limit F"
shows "continuous_map X mtopology g"
@@ -2653,7 +2653,7 @@
fix \<epsilon> :: real
assume "\<epsilon> > 0"
with gim dfg show "\<forall>\<^sub>F \<xi> in F. \<forall>x\<in>topspace X. g x \<in> M \<and> d (f \<xi> x) (g x) < \<epsilon>"
- by (simp add: image_subset_iff)
+ by (simp add: Pi_iff)
qed (use nontriv in auto)
@@ -2800,14 +2800,16 @@
lemma completely_metrizable_space_cbox: "completely_metrizable_space (top_of_set (cbox a b))"
using closed_closedin completely_metrizable_space_closedin completely_metrizable_space_euclidean by blast
+
lemma homeomorphic_completely_metrizable_space_aux:
assumes homXY: "X homeomorphic_space Y" and X: "completely_metrizable_space X"
shows "completely_metrizable_space Y"
proof -
obtain f g where hmf: "homeomorphic_map X Y f" and hmg: "homeomorphic_map Y X g"
- and fg: "(\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"
- and fim: "f ` (topspace X) = topspace Y" and gim: "g ` (topspace Y) = topspace X"
- by (smt (verit, best) homXY homeomorphic_imp_surjective_map homeomorphic_maps_map homeomorphic_space_def)
+ and fg: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x" "\<And>y. y \<in> topspace Y \<Longrightarrow> f(g y) = y"
+ and fim: "f \<in> topspace X \<rightarrow> topspace Y" and gim: "g \<in> topspace Y \<rightarrow> topspace X"
+ using homXY
+ using homeomorphic_space_unfold by blast
obtain M d where Md: "Metric_space M d" "Metric_space.mcomplete M d" and Xeq: "X = Metric_space.mtopology M d"
using X by (auto simp: completely_metrizable_space_def)
then interpret MX: Metric_space M d by metis
@@ -2816,7 +2818,7 @@
proof
show "(D x y = 0) \<longleftrightarrow> (x = y)" if "x \<in> topspace Y" "y \<in> topspace Y" for x y
unfolding D_def
- by (metis that MX.topspace_mtopology MX.zero Xeq fg gim imageI)
+ by (metis that MX.topspace_mtopology MX.zero Xeq fg gim Pi_iff)
show "D x z \<le> D x y +D y z"
if "x \<in> topspace Y" "y \<in> topspace Y" "z \<in> topspace Y" for x y z
using that MX.triangle Xeq gim by (auto simp: D_def)
@@ -2828,8 +2830,8 @@
show "Metric_space (topspace Y) D"
using MY.Metric_space_axioms by blast
have gball: "g ` MY.mball y r = MX.mball (g y) r" if "y \<in> topspace Y" for y r
- using that MX.topspace_mtopology Xeq gim
- unfolding MX.mball_def MY.mball_def by (auto simp: subset_iff image_iff D_def)
+ using that MX.topspace_mtopology Xeq gim hmg homeomorphic_imp_surjective_map
+ unfolding MX.mball_def MY.mball_def by (fastforce simp: D_def)
have "\<exists>r>0. MY.mball y r \<subseteq> S" if "openin Y S" and "y \<in> S" for S y
proof -
have "openin X (g`S)"
@@ -3783,16 +3785,16 @@
definition Lipschitz_continuous_map
where "Lipschitz_continuous_map \<equiv>
- \<lambda>m1 m2 f. f ` mspace m1 \<subseteq> mspace m2 \<and>
+ \<lambda>m1 m2 f. f \<in> mspace m1 \<rightarrow> mspace m2 \<and>
(\<exists>B. \<forall>x \<in> mspace m1. \<forall>y \<in> mspace m1. mdist m2 (f x) (f y) \<le> B * mdist m1 x y)"
lemma Lipschitz_continuous_map_image:
- "Lipschitz_continuous_map m1 m2 f \<Longrightarrow> f ` mspace m1 \<subseteq> mspace m2"
+ "Lipschitz_continuous_map m1 m2 f \<Longrightarrow> f \<in> mspace m1 \<rightarrow> mspace m2"
by (simp add: Lipschitz_continuous_map_def)
lemma Lipschitz_continuous_map_pos:
"Lipschitz_continuous_map m1 m2 f \<longleftrightarrow>
- f ` mspace m1 \<subseteq> mspace m2 \<and>
+ f \<in> mspace m1 \<rightarrow> mspace m2 \<and>
(\<exists>B>0. \<forall>x \<in> mspace m1. \<forall>y \<in> mspace m1. mdist m2 (f x) (f y) \<le> B * mdist m1 x y)"
proof -
have "B * mdist m1 x y \<le> (\<bar>B\<bar> + 1) * mdist m1 x y" "\<bar>B\<bar> + 1 > 0" for x y B
@@ -3805,15 +3807,14 @@
lemma Lipschitz_continuous_map_eq:
assumes "Lipschitz_continuous_map m1 m2 f" "\<And>x. x \<in> mspace m1 \<Longrightarrow> f x = g x"
shows "Lipschitz_continuous_map m1 m2 g"
- using Lipschitz_continuous_map_def assms
- by (metis (no_types, opaque_lifting) image_subset_iff)
+ using Lipschitz_continuous_map_def assms by (simp add: Lipschitz_continuous_map_pos Pi_iff)
lemma Lipschitz_continuous_map_from_submetric:
assumes "Lipschitz_continuous_map m1 m2 f"
shows "Lipschitz_continuous_map (submetric m1 S) m2 f"
unfolding Lipschitz_continuous_map_def
proof
- show "f ` mspace (submetric m1 S) \<subseteq> mspace m2"
+ show "f \<in> mspace (submetric m1 S) \<rightarrow> mspace m2"
using Lipschitz_continuous_map_pos assms by fastforce
qed (use assms in \<open>fastforce simp: Lipschitz_continuous_map_def\<close>)
@@ -3824,37 +3825,36 @@
lemma Lipschitz_continuous_map_into_submetric:
"Lipschitz_continuous_map m1 (submetric m2 S) f \<longleftrightarrow>
- f ` mspace m1 \<subseteq> S \<and> Lipschitz_continuous_map m1 m2 f"
+ f \<in> mspace m1 \<rightarrow> S \<and> Lipschitz_continuous_map m1 m2 f"
by (auto simp: Lipschitz_continuous_map_def)
lemma Lipschitz_continuous_map_const:
"Lipschitz_continuous_map m1 m2 (\<lambda>x. c) \<longleftrightarrow>
mspace m1 = {} \<or> c \<in> mspace m2"
- unfolding Lipschitz_continuous_map_def image_subset_iff
+ unfolding Lipschitz_continuous_map_def Pi_iff
by (metis all_not_in_conv mdist_nonneg mdist_zero mult_1)
lemma Lipschitz_continuous_map_id:
"Lipschitz_continuous_map m1 m1 (\<lambda>x. x)"
- by (metis Lipschitz_continuous_map_def image_ident mult_1 order_refl)
+ unfolding Lipschitz_continuous_map_def by (metis funcset_id mult_1 order_refl)
lemma Lipschitz_continuous_map_compose:
assumes f: "Lipschitz_continuous_map m1 m2 f" and g: "Lipschitz_continuous_map m2 m3 g"
shows "Lipschitz_continuous_map m1 m3 (g \<circ> f)"
- unfolding Lipschitz_continuous_map_def image_subset_iff
+ unfolding Lipschitz_continuous_map_def
proof
- show "\<forall>x\<in>mspace m1. (g \<circ> f) x \<in> mspace m3"
- by (metis Lipschitz_continuous_map_def assms comp_apply image_subset_iff)
+ show "g \<circ> f \<in> mspace m1 \<rightarrow> mspace m3"
+ by (smt (verit, best) Lipschitz_continuous_map_image Pi_iff comp_apply f g)
obtain B where B: "\<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m2 (f x) (f y) \<le> B * mdist m1 x y"
using assms unfolding Lipschitz_continuous_map_def by presburger
obtain C where "C>0" and C: "\<forall>x\<in>mspace m2. \<forall>y\<in>mspace m2. mdist m3 (g x) (g y) \<le> C * mdist m2 x y"
using assms unfolding Lipschitz_continuous_map_pos by metis
show "\<exists>B. \<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m3 ((g \<circ> f) x) ((g \<circ> f) y) \<le> B * mdist m1 x y"
- apply (rule_tac x="C*B" in exI)
- proof clarify
+ proof (intro strip exI)
fix x y
assume \<section>: "x \<in> mspace m1" "y \<in> mspace m1"
then have "mdist m3 ((g \<circ> f) x) ((g \<circ> f) y) \<le> C * mdist m2 (f x) (f y)"
- by (metis C Lipschitz_continuous_map_def f comp_apply image_subset_iff)
+ using C Lipschitz_continuous_map_image f by fastforce
also have "\<dots> \<le> C * B * mdist m1 x y"
by (simp add: "\<section>" B \<open>0 < C\<close>)
finally show "mdist m3 ((g \<circ> f) x) ((g \<circ> f) y) \<le> C * B * mdist m1 x y" .
@@ -3865,12 +3865,12 @@
definition uniformly_continuous_map
where "uniformly_continuous_map \<equiv>
- \<lambda>m1 m2 f. f ` mspace m1 \<subseteq> mspace m2 \<and>
+ \<lambda>m1 m2 f. f \<in> mspace m1 \<rightarrow> mspace m2 \<and>
(\<forall>\<epsilon>>0. \<exists>\<delta>>0. \<forall>x \<in> mspace m1. \<forall>y \<in> mspace m1.
mdist m1 y x < \<delta> \<longrightarrow> mdist m2 (f y) (f x) < \<epsilon>)"
-lemma uniformly_continuous_map_image:
- "uniformly_continuous_map m1 m2 f \<Longrightarrow> f ` mspace m1 \<subseteq> mspace m2"
+lemma uniformly_continuous_map_funspace:
+ "uniformly_continuous_map m1 m2 f \<Longrightarrow> f \<in> mspace m1 \<rightarrow> mspace m2"
by (simp add: uniformly_continuous_map_def)
lemma ucmap_A:
@@ -3898,7 +3898,7 @@
assumes \<section>: "\<And>\<rho> \<sigma> \<epsilon>. \<lbrakk>\<epsilon> > 0; range \<rho> \<subseteq> mspace m1; range \<sigma> \<subseteq> mspace m1;
((\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0)\<rbrakk>
\<Longrightarrow> \<exists>n. mdist m2 (f (\<rho> n)) (f (\<sigma> n)) < \<epsilon>"
- and fim: "f ` mspace m1 \<subseteq> mspace m2"
+ and fim: "f \<in> mspace m1 \<rightarrow> mspace m2"
shows "uniformly_continuous_map m1 m2 f"
proof -
{assume "\<not> (\<forall>\<epsilon>>0. \<exists>\<delta>>0. \<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m1 y x < \<delta> \<longrightarrow> mdist m2 (f y) (f x) < \<epsilon>)"
@@ -3921,13 +3921,13 @@
lemma uniformly_continuous_map_sequentially:
"uniformly_continuous_map m1 m2 f \<longleftrightarrow>
- f ` mspace m1 \<subseteq> mspace m2 \<and>
+ f \<in> mspace m1 \<rightarrow> mspace m2 \<and>
(\<forall>\<rho> \<sigma>. range \<rho> \<subseteq> mspace m1 \<and> range \<sigma> \<subseteq> mspace m1 \<and> (\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0
\<longrightarrow> (\<lambda>n. mdist m2 (f (\<rho> n)) (f (\<sigma> n))) \<longlonglongrightarrow> 0)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
show "?lhs \<Longrightarrow> ?rhs"
- by (simp add: ucmap_A uniformly_continuous_map_image)
+ by (simp add: ucmap_A uniformly_continuous_map_funspace)
show "?rhs \<Longrightarrow> ?lhs"
by (intro ucmap_B ucmap_C) auto
qed
@@ -3935,14 +3935,14 @@
lemma uniformly_continuous_map_sequentially_alt:
"uniformly_continuous_map m1 m2 f \<longleftrightarrow>
- f ` mspace m1 \<subseteq> mspace m2 \<and>
+ f \<in> mspace m1 \<rightarrow> mspace m2 \<and>
(\<forall>\<epsilon>>0. \<forall>\<rho> \<sigma>. range \<rho> \<subseteq> mspace m1 \<and> range \<sigma> \<subseteq> mspace m1 \<and>
((\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0)
\<longrightarrow> (\<exists>n. mdist m2 (f (\<rho> n)) (f (\<sigma> n)) < \<epsilon>))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
show "?lhs \<Longrightarrow> ?rhs"
- using uniformly_continuous_map_image by (intro conjI strip ucmap_B | force simp: ucmap_A)+
+ using uniformly_continuous_map_funspace by (intro conjI strip ucmap_B | fastforce simp: ucmap_A)+
show "?rhs \<Longrightarrow> ?lhs"
by (intro ucmap_C) auto
qed
@@ -3951,14 +3951,14 @@
lemma uniformly_continuous_map_eq:
"\<lbrakk>\<And>x. x \<in> mspace m1 \<Longrightarrow> f x = g x; uniformly_continuous_map m1 m2 f\<rbrakk>
\<Longrightarrow> uniformly_continuous_map m1 m2 g"
- by (simp add: uniformly_continuous_map_def)
+ by (simp add: uniformly_continuous_map_def Pi_iff)
lemma uniformly_continuous_map_from_submetric:
assumes "uniformly_continuous_map m1 m2 f"
shows "uniformly_continuous_map (submetric m1 S) m2 f"
unfolding uniformly_continuous_map_def
proof
- show "f ` mspace (submetric m1 S) \<subseteq> mspace m2"
+ show "f \<in> mspace (submetric m1 S) \<rightarrow> mspace m2"
using assms by (auto simp: uniformly_continuous_map_def)
qed (use assms in \<open>force simp: uniformly_continuous_map_def\<close>)
@@ -3969,23 +3969,23 @@
lemma uniformly_continuous_map_into_submetric:
"uniformly_continuous_map m1 (submetric m2 S) f \<longleftrightarrow>
- f ` mspace m1 \<subseteq> S \<and> uniformly_continuous_map m1 m2 f"
+ f \<in> mspace m1 \<rightarrow> S \<and> uniformly_continuous_map m1 m2 f"
by (auto simp: uniformly_continuous_map_def)
lemma uniformly_continuous_map_const:
"uniformly_continuous_map m1 m2 (\<lambda>x. c) \<longleftrightarrow>
mspace m1 = {} \<or> c \<in> mspace m2"
- unfolding uniformly_continuous_map_def image_subset_iff
+ unfolding uniformly_continuous_map_def Pi_iff
by (metis empty_iff equals0I mdist_zero)
lemma uniformly_continuous_map_id [simp]:
"uniformly_continuous_map m1 m1 (\<lambda>x. x)"
- by (metis image_ident order_refl uniformly_continuous_map_def)
+ by (metis funcset_id uniformly_continuous_map_def)
lemma uniformly_continuous_map_compose:
assumes f: "uniformly_continuous_map m1 m2 f" and g: "uniformly_continuous_map m2 m3 g"
shows "uniformly_continuous_map m1 m3 (g \<circ> f)"
- by (smt (verit, ccfv_threshold) comp_apply f g image_subset_iff uniformly_continuous_map_def)
+ by (smt (verit, ccfv_threshold) comp_apply f g Pi_iff uniformly_continuous_map_def)
lemma uniformly_continuous_map_real_const [simp]:
"uniformly_continuous_map m euclidean_metric (\<lambda>x. c)"
@@ -4009,9 +4009,9 @@
= Cauchy_continuous_on S f"
by (auto simp add: Cauchy_continuous_map_def Cauchy_continuous_on_def Cauchy_def Met_TC.subspace Metric_space.MCauchy_def)
-lemma Cauchy_continuous_map_image:
+lemma Cauchy_continuous_map_funspace:
assumes "Cauchy_continuous_map m1 m2 f"
- shows "f ` mspace m1 \<subseteq> mspace m2"
+ shows "f \<in> mspace m1 \<rightarrow> mspace m2"
proof clarsimp
fix x
assume "x \<in> mspace m1"
@@ -4042,14 +4042,14 @@
lemma Cauchy_continuous_map_into_submetric:
"Cauchy_continuous_map m1 (submetric m2 S) f \<longleftrightarrow>
- f ` mspace m1 \<subseteq> S \<and> Cauchy_continuous_map m1 m2 f" (is "?lhs \<longleftrightarrow> ?rhs")
+ f \<in> mspace m1 \<rightarrow> S \<and> Cauchy_continuous_map m1 m2 f" (is "?lhs \<longleftrightarrow> ?rhs")
proof -
have "?lhs \<Longrightarrow> Cauchy_continuous_map m1 m2 f"
by (simp add: Cauchy_continuous_map_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
moreover have "?rhs \<Longrightarrow> ?lhs"
- by (bestsimp simp add: Cauchy_continuous_map_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
+ by (auto simp: Cauchy_continuous_map_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
ultimately show ?thesis
- by (metis Cauchy_continuous_map_image le_inf_iff mspace_submetric)
+ by (metis Cauchy_continuous_map_funspace Int_iff funcsetI funcset_mem mspace_submetric)
qed
lemma Cauchy_continuous_map_const [simp]:
@@ -4060,7 +4060,7 @@
moreover have "c \<in> mspace m2 \<Longrightarrow> Cauchy_continuous_map m1 m2 (\<lambda>x. c)"
by (simp add: Cauchy_continuous_map_def o_def Metric_space.MCauchy_const [OF Metric_space_mspace_mdist])
ultimately show ?thesis
- using Cauchy_continuous_map_image by blast
+ using Cauchy_continuous_map_funspace by blast
qed
lemma Cauchy_continuous_map_id [simp]:
@@ -4076,7 +4076,7 @@
assumes "Lipschitz_continuous_map m1 m2 f"
shows "uniformly_continuous_map m1 m2 f"
proof -
- have "f ` mspace m1 \<subseteq> mspace m2"
+ have "f \<in> mspace m1 \<rightarrow> mspace m2"
by (simp add: Lipschitz_continuous_map_image assms)
moreover have "\<exists>\<delta>>0. \<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m1 y x < \<delta> \<longrightarrow> mdist m2 (f y) (f x) < \<epsilon>"
if "\<epsilon> > 0" for \<epsilon>
@@ -4097,7 +4097,7 @@
"uniformly_continuous_map m1 m2 f \<Longrightarrow> Cauchy_continuous_map m1 m2 f"
unfolding uniformly_continuous_map_def Cauchy_continuous_map_def
apply (simp add: image_subset_iff o_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
- by meson
+ by (metis funcset_mem)
lemma locally_Cauchy_continuous_map:
assumes "\<epsilon> > 0"
@@ -4137,7 +4137,7 @@
then have "\<sigma> n \<in> mball_of m1 (\<sigma> n) \<epsilon>"
by (simp add: Metric_space.centre_in_mball_iff Metric_space_mspace_mdist assms(1) mball_of_def)
then show "(f \<circ> \<sigma>) n \<in> mspace m2"
- using Cauchy_continuous_map_image [OF \<section> [of "\<sigma> n"]] \<open>\<sigma> n \<in> mspace m1\<close> by auto
+ using Cauchy_continuous_map_funspace [OF \<section> [of "\<sigma> n"]] \<open>\<sigma> n \<in> mspace m1\<close> by auto
qed
qed
@@ -4154,7 +4154,7 @@
unfolding limit_atin_sequentially
proof (intro conjI strip)
show "f x \<in> M2"
- using Cauchy_continuous_map_image \<open>x \<in> M1\<close> assms by fastforce
+ using Cauchy_continuous_map_funspace \<open>x \<in> M1\<close> assms by fastforce
fix \<sigma>
assume "range \<sigma> \<subseteq> M1 - {x} \<and> limitin M1.mtopology \<sigma> x sequentially"
then have "M1.MCauchy (\<lambda>n. if even n then \<sigma> (n div 2) else x)"
@@ -4221,8 +4221,8 @@
shows "uniformly_continuous_map m1 m2 f"
unfolding uniformly_continuous_map_sequentially_alt imp_conjL
proof (intro conjI strip)
- show "f ` mspace m1 \<subseteq> mspace m2"
- by (simp add: Cauchy_continuous_map_image f)
+ show "f \<in> mspace m1 \<rightarrow> mspace m2"
+ by (simp add: Cauchy_continuous_map_funspace f)
interpret M1: Metric_space "mspace m1" "mdist m1"
by (simp add: Metric_space_mspace_mdist)
interpret M2: Metric_space "mspace m2" "mdist m2"
@@ -4286,7 +4286,7 @@
lemma Lipschitz_continuous_map_projections:
"Lipschitz_continuous_map (prod_metric m1 m2) m1 fst"
"Lipschitz_continuous_map (prod_metric m1 m2) m2 snd"
- by (simp add: Lipschitz_continuous_map_def prod_dist_def;
+ by (simp add: Lipschitz_continuous_map_def prod_dist_def fst_Pi snd_Pi;
metis mult_numeral_1 real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2)+
lemma Lipschitz_continuous_map_pairwise:
@@ -4308,11 +4308,11 @@
show ?thesis
unfolding Lipschitz_continuous_map_pos
proof (intro exI conjI strip)
- have f1im: "f1 ` mspace m \<subseteq> mspace m1"
+ have f1im: "f1 \<in> mspace m \<rightarrow> mspace m1"
by (simp add: Lipschitz_continuous_map_image f1)
- moreover have f2im: "f2 ` mspace m \<subseteq> mspace m2"
+ moreover have f2im: "f2 \<in> mspace m \<rightarrow> mspace m2"
by (simp add: Lipschitz_continuous_map_image f2)
- ultimately show "(\<lambda>x. (f1 x, f2 x)) ` mspace m \<subseteq> mspace (prod_metric m1 m2)"
+ ultimately show "(\<lambda>x. (f1 x, f2 x)) \<in> mspace m \<rightarrow> mspace (prod_metric m1 m2)"
by auto
show "B1+B2 > 0"
using \<open>0 < B1\<close> \<open>0 < B2\<close> by linarith
@@ -4343,11 +4343,11 @@
show ?thesis
unfolding uniformly_continuous_map_def
proof (intro conjI strip)
- have f1im: "f1 ` mspace m \<subseteq> mspace m1"
- by (simp add: uniformly_continuous_map_image f1)
- moreover have f2im: "f2 ` mspace m \<subseteq> mspace m2"
- by (simp add: uniformly_continuous_map_image f2)
- ultimately show "(\<lambda>x. (f1 x, f2 x)) ` mspace m \<subseteq> mspace (prod_metric m1 m2)"
+ have f1im: "f1 \<in> mspace m \<rightarrow> mspace m1"
+ by (simp add: uniformly_continuous_map_funspace f1)
+ moreover have f2im: "f2 \<in> mspace m \<rightarrow> mspace m2"
+ by (simp add: uniformly_continuous_map_funspace f2)
+ ultimately show "(\<lambda>x. (f1 x, f2 x)) \<in> mspace m \<rightarrow> mspace (prod_metric m1 m2)"
by auto
fix \<epsilon>:: real
assume "\<epsilon> > 0"
@@ -4402,9 +4402,9 @@
assumes f: "Lipschitz_continuous_map m1 m2 f" and S: "Metric_space.mbounded (mspace m1) (mdist m1) S"
shows "Metric_space.mbounded (mspace m2) (mdist m2) (f`S)"
proof -
- obtain B where fim: "f ` mspace m1 \<subseteq> mspace m2"
+ obtain B where fim: "f \<in> mspace m1 \<rightarrow> mspace m2"
and "B>0" and B: "\<And>x y. \<lbrakk>x \<in> mspace m1; y \<in> mspace m1\<rbrakk> \<Longrightarrow> mdist m2 (f x) (f y) \<le> B * mdist m1 x y"
- by (meson Lipschitz_continuous_map_pos f)
+ by (metis Lipschitz_continuous_map_pos f)
show ?thesis
unfolding Metric_space.mbounded_alt_pos [OF Metric_space_mspace_mdist]
proof
@@ -4429,7 +4429,7 @@
have "S \<subseteq> mspace m1"
using S by (simp add: Metric_space.mtotally_bounded_sequentially[OF Metric_space_mspace_mdist])
then show "f ` S \<subseteq> mspace m2"
- using Cauchy_continuous_map_image f by blast
+ using Cauchy_continuous_map_funspace f by blast
fix \<sigma> :: "nat \<Rightarrow> 'b"
assume "range \<sigma> \<subseteq> f ` S"
then have "\<forall>n. \<exists>x. \<sigma> n = f x \<and> x \<in> S"
@@ -4448,11 +4448,11 @@
lemma Lipschitz_coefficient_pos:
assumes "x \<in> mspace m" "y \<in> mspace m" "f x \<noteq> f y"
- and "f ` mspace m \<subseteq> mspace m2"
+ and "f \<in> mspace m \<rightarrow> mspace m2"
and "\<And>x y. \<lbrakk>x \<in> mspace m; y \<in> mspace m\<rbrakk>
\<Longrightarrow> mdist m2 (f x) (f y) \<le> k * mdist m x y"
shows "0 < k"
- using assms by (smt (verit, best) image_subset_iff mdist_nonneg mdist_zero mult_nonpos_nonneg)
+ using assms by (smt (verit, best) Pi_iff mdist_nonneg mdist_zero mult_nonpos_nonneg)
lemma Lipschitz_continuous_map_metric:
"Lipschitz_continuous_map (prod_metric m m) euclidean_metric (\<lambda>(x,y). mdist m x y)"
@@ -4563,7 +4563,7 @@
subsection \<open>Isometries\<close>
lemma (in Metric_space12) isometry_imp_embedding_map:
- assumes fim: "f ` M1 \<subseteq> M2" and d: "\<And>x y. \<lbrakk>x \<in> M1; y \<in> M1\<rbrakk> \<Longrightarrow> d2 (f x) (f y) = d1 x y"
+ assumes fim: "f \<in> M1 \<rightarrow> M2" and d: "\<And>x y. \<lbrakk>x \<in> M1; y \<in> M1\<rbrakk> \<Longrightarrow> d2 (f x) (f y) = d1 x y"
shows "embedding_map M1.mtopology M2.mtopology f"
proof -
have "inj_on f M1"
@@ -4574,7 +4574,10 @@
unfolding homeomorphic_maps_def
proof (intro conjI; clarsimp)
show "continuous_map M1.mtopology (subtopology M2.mtopology (f ` M1)) f"
- by (metis M1.metric_continuous_map M1.topspace_mtopology M2.Metric_space_axioms continuous_map_into_subtopology d fim order_refl)
+ proof (rule continuous_map_into_subtopology)
+ show "continuous_map M1.mtopology M2.mtopology f"
+ by (metis M1.metric_continuous_map M2.Metric_space_axioms d fim image_subset_iff_funcset)
+ qed simp
have "Lipschitz_continuous_map (submetric (metric(M2,d2)) (f ` M1)) (metric(M1,d1)) g"
unfolding Lipschitz_continuous_map_def
proof (intro conjI exI strip; simp)
@@ -4595,7 +4598,8 @@
lemma (in Metric_space12) isometry_imp_homeomorphic_map:
assumes fim: "f ` M1 = M2" and d: "\<And>x y. \<lbrakk>x \<in> M1; y \<in> M1\<rbrakk> \<Longrightarrow> d2 (f x) (f y) = d1 x y"
shows "homeomorphic_map M1.mtopology M2.mtopology f"
- by (metis M1.topspace_mtopology M2.subtopology_mspace d embedding_map_def fim isometry_imp_embedding_map subsetI)
+ by (metis image_eqI M1.topspace_mtopology M2.subtopology_mspace d embedding_map_def fim isometry_imp_embedding_map Pi_iff)
+
subsection\<open>"Capped" equivalent bounded metrics and general product metrics\<close>
definition (in Metric_space) capped_dist where
@@ -5132,6 +5136,5 @@
"locally_connected_space(Euclidean_space n)"
by (simp add: locally_path_connected_Euclidean_space locally_path_connected_imp_locally_connected_space)
-
end
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy Mon Jul 03 16:46:37 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
--- a/src/HOL/Analysis/Abstract_Topology.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Mon Jul 03 16:46:37 2023 +0100
@@ -1703,24 +1703,24 @@
lemma continuous_map_from_subtopology:
- "continuous_map X X' f \<Longrightarrow> continuous_map (subtopology X S) X' f"
+ "continuous_map X Y f \<Longrightarrow> continuous_map (subtopology X S) Y f"
by (auto simp: continuous_map openin_subtopology)
lemma continuous_map_into_fulltopology:
- "continuous_map X (subtopology X' T) f \<Longrightarrow> continuous_map X X' f"
+ "continuous_map X (subtopology Y T) f \<Longrightarrow> continuous_map X Y f"
by (auto simp: continuous_map_in_subtopology)
lemma continuous_map_into_subtopology:
- "\<lbrakk>continuous_map X X' f; f ` topspace X \<subseteq> T\<rbrakk> \<Longrightarrow> continuous_map X (subtopology X' T) f"
+ "\<lbrakk>continuous_map X Y f; f \<in> topspace X \<rightarrow> T\<rbrakk> \<Longrightarrow> continuous_map X (subtopology Y T) f"
by (auto simp: continuous_map_in_subtopology)
lemma continuous_map_from_subtopology_mono:
- "\<lbrakk>continuous_map (subtopology X T) X' f; S \<subseteq> T\<rbrakk>
- \<Longrightarrow> continuous_map (subtopology X S) X' f"
+ "\<lbrakk>continuous_map (subtopology X T) Y f; S \<subseteq> T\<rbrakk>
+ \<Longrightarrow> continuous_map (subtopology X S) Y f"
by (metis inf.absorb_iff2 continuous_map_from_subtopology subtopology_subtopology)
lemma continuous_map_from_discrete_topology [simp]:
- "continuous_map (discrete_topology U) X f \<longleftrightarrow> f ` U \<subseteq> topspace X"
+ "continuous_map (discrete_topology U) X f \<longleftrightarrow> f \<in> U \<rightarrow> topspace X"
by (auto simp: continuous_map_def)
lemma continuous_map_iff_continuous [simp]: "continuous_map (top_of_set S) euclidean g = continuous_on S g"
@@ -1731,12 +1731,12 @@
lemma continuous_map_openin_preimage_eq:
"continuous_map X Y f \<longleftrightarrow>
- f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X (topspace X \<inter> f -` U))"
+ f \<in> (topspace X) \<rightarrow> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X (topspace X \<inter> f -` U))"
by (auto simp: continuous_map_def vimage_def Int_def)
lemma continuous_map_closedin_preimage_eq:
"continuous_map X Y f \<longleftrightarrow>
- f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. closedin Y U \<longrightarrow> closedin X (topspace X \<inter> f -` U))"
+ f \<in> (topspace X) \<rightarrow> topspace Y \<and> (\<forall>U. closedin Y U \<longrightarrow> closedin X (topspace X \<inter> f -` U))"
by (auto simp: continuous_map_closedin vimage_def Int_def)
lemma continuous_map_square_root: "continuous_map euclideanreal euclideanreal sqrt"
@@ -1759,7 +1759,7 @@
lemma\<^marker>\<open>tag important\<close> continuous_map_alt:
"continuous_map T1 T2 f
- = ((\<forall>U. openin T2 U \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)) \<and> f ` topspace T1 \<subseteq> topspace T2)"
+ = ((\<forall>U. openin T2 U \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)) \<and> f \<in> topspace T1 \<rightarrow> topspace T2)"
by (auto simp: continuous_map_def vimage_def image_def Collect_conj_eq inf_commute)
lemma continuous_map_open [intro]:
@@ -1782,8 +1782,8 @@
where "closed_map X1 X2 f \<equiv> \<forall>U. closedin X1 U \<longrightarrow> closedin X2 (f ` U)"
lemma open_map_imp_subset_topspace:
- "open_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
- unfolding open_map_def by (simp add: openin_subset)
+ "open_map X1 X2 f \<Longrightarrow> f \<in> (topspace X1) \<rightarrow> topspace X2"
+ unfolding open_map_def using openin_subset by fastforce
lemma open_map_on_empty:
"topspace X = {} \<Longrightarrow> open_map X Y f"
@@ -1798,8 +1798,8 @@
by (metis closed_map_def closed_map_on_empty closedin_empty closedin_topspace image_constant_conv)
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)
+ "\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f \<in> S \<rightarrow> topspace X2"
+ using open_map_imp_subset_topspace by fastforce
lemma topology_finer_open_id:
"(\<forall>S. openin X S \<longrightarrow> openin X' S) \<longleftrightarrow> open_map X X' id"
@@ -1826,11 +1826,11 @@
by (metis (no_types, lifting) image_comp open_map_def)
lemma closed_map_imp_subset_topspace:
- "closed_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
- by (simp add: closed_map_def closedin_subset)
+ "closed_map X1 X2 f \<Longrightarrow> f \<in> (topspace X1) \<rightarrow> topspace X2"
+ by (simp add: closed_map_def closedin_def image_subset_iff_funcset)
lemma closed_map_imp_subset:
- "\<lbrakk>closed_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
+ "\<lbrakk>closed_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f \<in> S \<rightarrow> topspace X2"
using closed_map_imp_subset_topspace by blast
lemma topology_finer_closed_id:
@@ -1863,21 +1863,21 @@
by (simp add: closed_map_inclusion_eq closedin_Int)
lemma open_map_into_subtopology:
- "\<lbrakk>open_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> open_map X (subtopology X' S) f"
+ "\<lbrakk>open_map X X' f; f \<in> topspace X \<rightarrow> S\<rbrakk> \<Longrightarrow> open_map X (subtopology X' S) f"
unfolding open_map_def openin_subtopology
using openin_subset by fastforce
lemma closed_map_into_subtopology:
- "\<lbrakk>closed_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> closed_map X (subtopology X' S) f"
+ "\<lbrakk>closed_map X X' f; f \<in> topspace X \<rightarrow> S\<rbrakk> \<Longrightarrow> closed_map X (subtopology X' S) f"
unfolding closed_map_def closedin_subtopology
using closedin_subset by fastforce
lemma open_map_into_discrete_topology:
- "open_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
+ "open_map X (discrete_topology U) f \<longleftrightarrow> f \<in> (topspace X) \<rightarrow> U"
unfolding open_map_def openin_discrete_topology using openin_subset by blast
lemma closed_map_into_discrete_topology:
- "closed_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
+ "closed_map X (discrete_topology U) f \<longleftrightarrow> f \<in> (topspace X) \<rightarrow> U"
unfolding closed_map_def closedin_discrete_topology using closedin_subset by blast
lemma bijective_open_imp_closed_map:
@@ -1930,8 +1930,8 @@
lemma closed_map_closure_of_image:
"closed_map X Y f \<longleftrightarrow>
- f ` topspace X \<subseteq> topspace Y \<and>
- (\<forall>S. S \<subseteq> topspace X \<longrightarrow> Y closure_of (f ` S) \<subseteq> image f (X closure_of S))" (is "?lhs=?rhs")
+ f \<in> topspace X \<rightarrow> topspace Y \<and>
+ (\<forall>S. S \<subseteq> topspace X \<longrightarrow> Y closure_of (f ` S) \<subseteq> f ` (X closure_of S))" (is "?lhs=?rhs")
proof
assume ?lhs
then show ?rhs
@@ -1953,12 +1953,12 @@
lemma open_map_interior_of_image_subset_gen:
"open_map X Y f \<longleftrightarrow>
- (f ` topspace X \<subseteq> topspace Y \<and> (\<forall>S. f ` (X interior_of S) \<subseteq> Y interior_of f ` S))"
- by (meson open_map_imp_subset_topspace open_map_interior_of_image_subset)
+ (f \<in> topspace X \<rightarrow> topspace Y \<and> (\<forall>S. f ` (X interior_of S) \<subseteq> Y interior_of f ` S))"
+ by (metis open_map_imp_subset_topspace open_map_interior_of_image_subset)
lemma open_map_preimage_neighbourhood:
"open_map X Y f \<longleftrightarrow>
- (f ` topspace X \<subseteq> topspace Y \<and>
+ (f \<in> topspace X \<rightarrow> topspace Y \<and>
(\<forall>U T. closedin X U \<and> T \<subseteq> topspace Y \<and>
{x \<in> topspace X. f x \<in> T} \<subseteq> U \<longrightarrow>
(\<exists>V. closedin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U)))" (is "?lhs=?rhs")
@@ -1966,7 +1966,7 @@
assume L: ?lhs
show ?rhs
proof (intro conjI strip)
- show "f ` topspace X \<subseteq> topspace Y"
+ show "f \<in> topspace X \<rightarrow> topspace Y"
by (simp add: \<open>open_map X Y f\<close> open_map_imp_subset_topspace)
next
fix U T
@@ -2000,7 +2000,7 @@
lemma closed_map_preimage_neighbourhood:
"closed_map X Y f \<longleftrightarrow>
- image f (topspace X) \<subseteq> topspace Y \<and>
+ f \<in> topspace X \<rightarrow> topspace Y \<and>
(\<forall>U T. openin X U \<and> T \<subseteq> topspace Y \<and>
{x \<in> topspace X. f x \<in> T} \<subseteq> U
\<longrightarrow> (\<exists>V. openin Y V \<and> T \<subseteq> V \<and>
@@ -2009,7 +2009,7 @@
assume L: ?lhs
show ?rhs
proof (intro conjI strip)
- show "f ` topspace X \<subseteq> topspace Y"
+ show "f \<in> topspace X \<rightarrow> topspace Y"
by (simp add: L closed_map_imp_subset_topspace)
next
fix U T
@@ -2042,13 +2042,13 @@
lemma closed_map_fibre_neighbourhood:
"closed_map X Y f \<longleftrightarrow>
- f ` (topspace X) \<subseteq> topspace Y \<and>
+ f \<in> (topspace X) \<rightarrow> topspace Y \<and>
(\<forall>U y. openin X U \<and> y \<in> topspace Y \<and> {x \<in> topspace X. f x = y} \<subseteq> U
\<longrightarrow> (\<exists>V. openin Y V \<and> y \<in> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U))"
unfolding closed_map_preimage_neighbourhood
proof (intro conj_cong refl all_cong1)
fix U
- assume "f ` topspace X \<subseteq> topspace Y"
+ assume "f \<in> topspace X \<rightarrow> topspace Y"
show "(\<forall>T. openin X U \<and> T \<subseteq> topspace Y \<and> {x \<in> topspace X. f x \<in> T} \<subseteq> U
\<longrightarrow> (\<exists>V. openin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U))
= (\<forall>y. openin X U \<and> y \<in> topspace Y \<and> {x \<in> topspace X. f x = y} \<subseteq> U
@@ -2083,8 +2083,8 @@
lemma open_map_in_subtopology:
"openin Y S
- \<Longrightarrow> (open_map X (subtopology Y S) f \<longleftrightarrow> open_map X Y f \<and> f ` (topspace X) \<subseteq> S)"
- by (metis le_inf_iff open_map_def open_map_imp_subset_topspace open_map_into_subtopology openin_trans_full topspace_subtopology)
+ \<Longrightarrow> open_map X (subtopology Y S) f \<longleftrightarrow> open_map X Y f \<and> f \<in> topspace X \<rightarrow> S"
+ by (metis image_subset_iff_funcset open_map_def open_map_into_subtopology openin_imp_subset openin_topspace openin_trans_full)
lemma open_map_from_open_subtopology:
"\<lbrakk>openin Y S; open_map X (subtopology Y S) f\<rbrakk> \<Longrightarrow> open_map X Y f"
@@ -2092,7 +2092,7 @@
lemma closed_map_in_subtopology:
"closedin Y S
- \<Longrightarrow> closed_map X (subtopology Y S) f \<longleftrightarrow> (closed_map X Y f \<and> f ` topspace X \<subseteq> S)"
+ \<Longrightarrow> closed_map X (subtopology Y S) f \<longleftrightarrow> (closed_map X Y f \<and> f \<in> topspace X \<rightarrow> S)"
by (metis closed_map_def closed_map_imp_subset_topspace closed_map_into_subtopology
closedin_closed_subtopology closedin_subset topspace_subtopology_subset)
@@ -2138,7 +2138,7 @@
qed
lemma closed_map_from_composition_right:
- assumes cmf: "closed_map X Z (g \<circ> f)" "f ` topspace X \<subseteq> topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)"
+ assumes cmf: "closed_map X Z (g \<circ> f)" "f \<in> topspace X \<rightarrow> topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)"
shows "closed_map X Y f"
unfolding closed_map_def
proof (intro strip)
@@ -2156,7 +2156,7 @@
text \<open>identical proof as the above\<close>
lemma open_map_from_composition_right:
- assumes "open_map X Z (g \<circ> f)" "f ` topspace X \<subseteq> topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)"
+ assumes "open_map X Z (g \<circ> f)" "f \<in> topspace X \<rightarrow> topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)"
shows "open_map X Y f"
unfolding open_map_def
proof (intro strip)
@@ -2733,8 +2733,8 @@
by (simp add: homeomorphic_eq_everything_map)
lemma homeomorphic_imp_surjective_map:
- "homeomorphic_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
- by (simp add: homeomorphic_eq_everything_map)
+ "homeomorphic_map X Y f \<Longrightarrow> f ` topspace X = topspace Y"
+ using homeomorphic_eq_everything_map by fastforce
lemma homeomorphic_imp_injective_map:
"homeomorphic_map X Y f \<Longrightarrow> inj_on f (topspace X)"
@@ -2899,13 +2899,13 @@
lemma all_openin_homeomorphic_image:
assumes "homeomorphic_map X Y f"
- shows "(\<forall>V. openin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> P(f ` U))"
- by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_openness openin_subset subset_image_iff)
+ shows "(\<forall>V. openin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> P(f ` U))"
+ by (metis (no_types, lifting) assms homeomorphic_eq_everything_map homeomorphic_map_openness openin_subset subset_image_iff)
lemma all_closedin_homeomorphic_image:
assumes "homeomorphic_map X Y f"
- shows "(\<forall>V. closedin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. closedin X U \<longrightarrow> P(f ` U))" (is "?lhs = ?rhs")
- by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_closedness closedin_subset subset_image_iff)
+ shows "(\<forall>V. closedin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. closedin X U \<longrightarrow> P(f ` U))"
+ by (metis (no_types, lifting) assms closedin_subset homeomorphic_eq_everything_map homeomorphic_map_closedness subset_image_iff)
lemma homeomorphic_map_derived_set_of:
@@ -3059,7 +3059,7 @@
lemma homeomorphic_empty_space:
"X homeomorphic_space Y \<Longrightarrow> topspace X = {} \<longleftrightarrow> topspace Y = {}"
- by (metis homeomorphic_imp_surjective_map homeomorphic_space image_is_empty)
+ by (metis homeomorphic_eq_everything_map homeomorphic_space image_is_empty)
lemma homeomorphic_empty_space_eq:
assumes "topspace X = {}"
@@ -3067,6 +3067,14 @@
unfolding homeomorphic_maps_def homeomorphic_space_def
by (metis assms continuous_map_on_empty continuous_map_closedin ex_in_conv)
+lemma homeomorphic_space_unfold:
+ assumes "X homeomorphic_space Y"
+ obtains f g where "homeomorphic_map X Y f" "homeomorphic_map Y X g"
+ and "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x" "\<And>y. y \<in> topspace Y \<Longrightarrow> f(g y) = y"
+ and "f \<in> topspace X \<rightarrow> topspace Y" "g \<in> topspace Y \<rightarrow> topspace X"
+ using assms unfolding homeomorphic_space_def homeomorphic_maps_map
+ by (smt (verit, best) Pi_I homeomorphic_imp_surjective_map image_eqI)
+
subsection\<open>Connected topological spaces\<close>
definition connected_space :: "'a topology \<Rightarrow> bool" where
@@ -3923,9 +3931,9 @@
have hm: "homeomorphic_map X (subtopology X' (f ` topspace X)) f" "homeomorphic_map X' (subtopology X'' (g ` topspace X')) g"
using assms by (auto simp: embedding_map_def)
then obtain C where "g ` topspace X' \<inter> C = (g \<circ> f) ` topspace X"
- by (metis homeomorphic_imp_surjective_map image_comp image_mono inf.absorb_iff2 topspace_subtopology)
+ using continuous_map_image_subset_topspace homeomorphic_imp_continuous_map by fastforce
then have "homeomorphic_map (subtopology X' (f ` topspace X)) (subtopology X'' ((g \<circ> f) ` topspace X)) g"
- by (metis hm homeomorphic_imp_surjective_map homeomorphic_map_subtopologies image_comp subtopology_subtopology topspace_subtopology)
+ by (metis hm homeomorphic_eq_everything_map homeomorphic_map_subtopologies image_comp subtopology_subtopology topspace_subtopology)
then show ?thesis
unfolding embedding_map_def
using hm(1) homeomorphic_map_compose by blast
@@ -3945,14 +3953,15 @@
lemma injective_open_imp_embedding_map:
"\<lbrakk>continuous_map X Y f; open_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
- unfolding embedding_map_def
- by (simp add: continuous_map_in_subtopology continuous_open_quotient_map eq_iff homeomorphic_map_def open_map_imp_subset open_map_into_subtopology)
+ unfolding embedding_map_def homeomorphic_map_def
+ by (simp add: image_subset_iff_funcset continuous_map_in_subtopology continuous_open_quotient_map eq_iff
+ open_map_imp_subset open_map_into_subtopology)
lemma injective_closed_imp_embedding_map:
"\<lbrakk>continuous_map X Y f; closed_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
- unfolding embedding_map_def
+ unfolding embedding_map_def homeomorphic_map_def
by (simp add: closed_map_imp_subset closed_map_into_subtopology continuous_closed_quotient_map
- continuous_map_in_subtopology dual_order.eq_iff homeomorphic_map_def)
+ continuous_map_in_subtopology dual_order.eq_iff image_subset_iff_funcset)
lemma embedding_map_imp_homeomorphic_space:
"embedding_map X Y f \<Longrightarrow> X homeomorphic_space (subtopology Y (f ` (topspace X)))"
@@ -4098,7 +4107,7 @@
lemma continuous_map_euclidean_top_of_set:
assumes eq: "f -` S = UNIV" and cont: "continuous_on UNIV f"
shows "continuous_map euclidean (top_of_set S) f"
- by (simp add: cont continuous_map_into_subtopology eq image_subset_iff_subset_vimage)
+ by (simp add: cont continuous_map_in_subtopology eq image_subset_iff_subset_vimage)
subsection\<^marker>\<open>tag unimportant\<close> \<open>Half-global and completely global cases\<close>
@@ -4256,36 +4265,32 @@
qed
lemma continuous_on_open_gen:
- assumes "f ` S \<subseteq> T"
+ assumes "f \<in> S \<rightarrow> T"
shows "continuous_on S f \<longleftrightarrow>
(\<forall>U. openin (top_of_set T) U
\<longrightarrow> openin (top_of_set S) (S \<inter> f -` U))"
(is "?lhs = ?rhs")
proof
assume ?lhs
- then show ?rhs
- by (clarsimp simp add: continuous_openin_preimage_eq openin_open)
- (metis Int_assoc assms image_subset_iff_subset_vimage inf.absorb_iff1)
+ with assms show ?rhs
+ apply (simp add: Pi_iff continuous_openin_preimage_eq openin_open)
+ by (metis inf.orderE inf_assoc subsetI vimageI vimage_Int)
next
assume R [rule_format]: ?rhs
show ?lhs
proof (clarsimp simp add: continuous_openin_preimage_eq)
- fix U::"'a set"
- assume "open U"
- then have "openin (top_of_set S) (S \<inter> f -` (U \<inter> T))"
- by (metis R inf_commute openin_open)
- then show "openin (top_of_set S) (S \<inter> f -` U)"
- by (metis Int_assoc Int_commute assms image_subset_iff_subset_vimage inf.absorb_iff2 vimage_Int)
+ show "\<And>T. open T \<Longrightarrow> openin (top_of_set S) (S \<inter> f -` T)"
+ by (metis (no_types) R assms image_subset_iff_funcset image_subset_iff_subset_vimage inf.orderE inf_assoc openin_open_Int vimage_Int)
qed
qed
lemma continuous_openin_preimage:
- "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (top_of_set T) U\<rbrakk>
+ "\<lbrakk>continuous_on S f; f \<in> S \<rightarrow> T; openin (top_of_set T) U\<rbrakk>
\<Longrightarrow> openin (top_of_set S) (S \<inter> f -` U)"
by (simp add: continuous_on_open_gen)
lemma continuous_on_closed_gen:
- assumes "f ` S \<subseteq> T"
+ assumes "f \<in> S \<rightarrow> T"
shows "continuous_on S f \<longleftrightarrow>
(\<forall>U. closedin (top_of_set T) U
\<longrightarrow> closedin (top_of_set S) (S \<inter> f -` U))"
@@ -4298,7 +4303,7 @@
qed
lemma continuous_closedin_preimage_gen:
- assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (top_of_set T) U"
+ assumes "continuous_on S f" "f \<in> S \<rightarrow> T" "closedin (top_of_set T) U"
shows "closedin (top_of_set S) (S \<inter> f -` U)"
using assms continuous_on_closed_gen by blast
@@ -4825,7 +4830,7 @@
by (simp add: proper_map_def)
lemma proper_map_imp_subset_topspace:
- "proper_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
+ "proper_map X Y f \<Longrightarrow> f \<in> (topspace X) \<rightarrow> topspace Y"
by (simp add: closed_map_imp_subset_topspace proper_map_def)
lemma proper_map_restriction:
@@ -4868,7 +4873,7 @@
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"
+ have "f \<in> (topspace X) \<rightarrow> 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)
@@ -5009,7 +5014,7 @@
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"
+ "\<lbrakk>proper_map X Y f; f \<in> topspace X \<rightarrow> 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:
@@ -5031,7 +5036,7 @@
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"
+ assumes gf: "proper_map X Z (g \<circ> f)" and fim: "f \<in> topspace X \<rightarrow> 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
@@ -5041,7 +5046,7 @@
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)
+ 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)
--- a/src/HOL/Analysis/Abstract_Topology_2.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Mon Jul 03 16:46:37 2023 +0100
@@ -575,7 +575,7 @@
subsection\<^marker>\<open>tag unimportant\<close>\<open>Quotient maps\<close>
lemma quotient_map_imp_continuous_open:
- assumes T: "f ` S \<subseteq> T"
+ assumes T: "f \<in> S \<rightarrow> T"
and ope: "\<And>U. U \<subseteq> T
\<Longrightarrow> (openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
openin (top_of_set T) U)"
@@ -587,7 +587,7 @@
qed
lemma quotient_map_imp_continuous_closed:
- assumes T: "f ` S \<subseteq> T"
+ assumes T: "f \<in> S \<rightarrow> T"
and ope: "\<And>U. U \<subseteq> T
\<Longrightarrow> (closedin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
closedin (top_of_set T) U)"
@@ -635,8 +635,8 @@
qed
lemma continuous_right_inverse_imp_quotient_map:
- assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
- and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
+ assumes contf: "continuous_on S f" and imf: "f \<in> S \<rightarrow> T"
+ and contg: "continuous_on T g" and img: "g \<in> T \<rightarrow> S"
and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
and U: "U \<subseteq> T"
shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
@@ -657,13 +657,13 @@
finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
assume ?lhs
then have *: "openin (top_of_set (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
- by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
+ by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self image_subset_iff_funcset)
show ?rhs
using g [OF *] eq by auto
next
assume rhs: ?rhs
show ?lhs
- by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
+ using assms continuous_openin_preimage rhs by blast
qed
qed
@@ -696,7 +696,7 @@
shows "continuous_map X Y g"
unfolding continuous_map_openin_preimage_eq
proof (intro conjI allI impI)
- show "g ` topspace X \<subseteq> topspace Y"
+ show "g \<in> topspace X \<rightarrow> topspace Y"
using g cont continuous_map_image_subset_topspace by fastforce
next
fix U
@@ -737,7 +737,7 @@
shows "continuous_map X Y g"
unfolding continuous_map_closedin_preimage_eq
proof (intro conjI allI impI)
- show "g ` topspace X \<subseteq> topspace Y"
+ show "g \<in> topspace X \<rightarrow> topspace Y"
using g cont continuous_map_image_subset_topspace by fastforce
next
fix U
@@ -885,7 +885,7 @@
definition\<^marker>\<open>tag important\<close> retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
where "retraction S T r \<longleftrightarrow>
- T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
+ T \<subseteq> S \<and> continuous_on S r \<and> r \<in> S \<rightarrow> T \<and> (\<forall>x\<in>T. r x = x)"
definition\<^marker>\<open>tag important\<close> retract_of (infixl "retract'_of" 50) where
"T retract_of S \<longleftrightarrow> (\<exists>r. retraction S T r)"
@@ -899,20 +899,20 @@
fixes S :: "'a::topological_space set"
and T :: "'b::topological_space set"
assumes contt: "continuous_on T i"
- and "i ` T \<subseteq> S"
+ and "i \<in> T \<rightarrow> S"
and contr: "continuous_on S r"
- and "r ` S \<subseteq> T"
+ and "r \<in> S \<rightarrow> T"
and ri: "\<And>y. y \<in> T \<Longrightarrow> r (i y) = y"
- and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
+ and FP: "\<And>f. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
and contg: "continuous_on T g"
- and "g ` T \<subseteq> T"
+ and "g \<in> T \<rightarrow> T"
obtains y where "y \<in> T" and "g y = y"
proof -
have "\<exists>x\<in>S. (i \<circ> g \<circ> r) x = x"
proof (rule FP)
show "continuous_on S (i \<circ> g \<circ> r)"
- by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset)
- show "(i \<circ> g \<circ> r) ` S \<subseteq> S"
+ by (metis assms(4) assms(8) contg continuous_on_compose continuous_on_subset contr contt funcset_image)
+ show "(i \<circ> g \<circ> r) \<in> S \<rightarrow> S"
using assms(2,4,8) by force
qed
then obtain x where x: "x \<in> S" "(i \<circ> g \<circ> r) x = x" ..
@@ -928,8 +928,8 @@
fixes S :: "'a::topological_space set"
and T :: "'b::topological_space set"
assumes "S homeomorphic T"
- shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow>
- (\<forall>g. continuous_on T g \<and> g ` T \<subseteq> T \<longrightarrow> (\<exists>y\<in>T. g y = y))"
+ shows "(\<forall>f. continuous_on S f \<and> f \<in> S \<rightarrow> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow>
+ (\<forall>g. continuous_on T g \<and> g \<in> T \<rightarrow> T \<longrightarrow> (\<exists>y\<in>T. g y = y))"
(is "?lhs = ?rhs")
proof -
obtain r i where r:
@@ -940,11 +940,11 @@
proof
assume ?lhs
with r show ?rhs
- by (metis invertible_fixpoint_property[of T i S r] order_refl)
+ by (smt (verit, del_insts) Pi_iff image_eqI invertible_fixpoint_property[of T i S r])
next
assume ?rhs
with r show ?lhs
- by (metis invertible_fixpoint_property[of S r T i] order_refl)
+ by (smt (verit, del_insts) Pi_iff image_eqI invertible_fixpoint_property[of S r T i])
qed
qed
@@ -952,9 +952,9 @@
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
and S :: "'a set"
assumes "T retract_of S"
- and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
+ and FP: "\<And>f. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
and contg: "continuous_on T g"
- and "g ` T \<subseteq> T"
+ and "g \<in> T \<rightarrow> T"
obtains y where "y \<in> T" and "g y = y"
proof -
obtain h where "retraction S T h"
@@ -962,23 +962,24 @@
then show ?thesis
unfolding retraction_def
using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
- by (metis assms(4) contg image_ident that)
+ by (smt (verit, del_insts) Pi_iff assms(4) contg subsetD that)
qed
lemma retraction:
- "retraction S T r \<longleftrightarrow>
- T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
- by (force simp: retraction_def)
+ "retraction S T r \<longleftrightarrow> T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
+ by (force simp: retraction_def simp flip: image_subset_iff_funcset)
lemma retractionE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close>
assumes "retraction S T r"
- obtains "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
+ obtains "T = r ` S" "r \<in> S \<rightarrow> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
proof (rule that)
from retraction [of S T r] assms
have "T \<subseteq> S" "continuous_on S r" "r ` S = T" and "\<forall>x \<in> T. r x = x"
by simp_all
- then show "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r"
- by simp_all
+ then show "r \<in> S \<rightarrow> S" "continuous_on S r"
+ by auto
+ then show "T = r ` S"
+ using \<open>r ` S = T\<close> by blast
from \<open>\<forall>x \<in> T. r x = x\<close> have "r x = x" if "x \<in> T" for x
using that by simp
with \<open>r ` S = T\<close> show "r (r x) = r x" if "x \<in> S" for x
@@ -987,7 +988,7 @@
lemma retract_ofE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close>
assumes "T retract_of S"
- obtains r where "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
+ obtains r where "T = r ` S" "r \<in> S \<rightarrow> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
proof -
from assms obtain r where "retraction S T r"
by (auto simp add: retract_of_def)
@@ -996,30 +997,31 @@
qed
lemma retract_of_imp_extensible:
- assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U"
- obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ assumes "S retract_of T" and "continuous_on S f" and "f \<in> S \<rightarrow> U"
+ obtains g where "continuous_on T g" "g \<in> T \<rightarrow> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof -
from \<open>S retract_of T\<close> obtain r where "retraction T S r"
by (auto simp add: retract_of_def)
- show thesis
- by (rule that [of "f \<circ> r"])
- (use \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> U\<close> \<open>retraction T S r\<close> in \<open>auto simp: continuous_on_compose2 retraction\<close>)
+ then have "continuous_on T (f \<circ> r)"
+ by (metis assms(2) continuous_on_compose retraction)
+ then show thesis
+ by (smt (verit, best) Pi_iff \<open>retraction T S r\<close> assms(3) comp_apply retraction_def that)
qed
lemma idempotent_imp_retraction:
- assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
+ assumes "continuous_on S f" and "f \<in> S \<rightarrow> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
shows "retraction S (f ` S) f"
-by (simp add: assms retraction)
+ by (simp add: assms funcset_image retraction)
lemma retraction_subset:
- assumes "retraction S T r" and "T \<subseteq> s'" and "s' \<subseteq> S"
- shows "retraction s' T r"
+ assumes "retraction S T r" and "T \<subseteq> S'" and "S' \<subseteq> S"
+ shows "retraction S' T r"
unfolding retraction_def
- by (metis assms continuous_on_subset image_mono retraction)
+ by (metis assms continuous_on_subset image_mono image_subset_iff_funcset retraction)
lemma retract_of_subset:
- assumes "T retract_of S" and "T \<subseteq> s'" and "s' \<subseteq> S"
- shows "T retract_of s'"
+ assumes "T retract_of S" and "T \<subseteq> S'" and "S' \<subseteq> S"
+ shows "T retract_of S'"
by (meson assms retract_of_def retraction_subset)
lemma retraction_refl [simp]: "retraction S S (\<lambda>x. x)"
@@ -1054,10 +1056,10 @@
assumes "S retract_of T"
shows "closedin (top_of_set T) S"
proof -
- obtain r where r: "S \<subseteq> T" "continuous_on T r" "r ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x"
+ obtain r where r: "S \<subseteq> T" "continuous_on T r" "r \<in> T \<rightarrow> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x"
using assms by (auto simp: retract_of_def retraction_def)
have "S = {x\<in>T. x = r x}"
- using r by auto
+ using r by force
also have "\<dots> = T \<inter> ((\<lambda>x. (x, r x)) -` ({y. \<exists>x. y = (x, x)}))"
unfolding vimage_def mem_Times_iff fst_conv snd_conv
using r
@@ -1088,14 +1090,14 @@
shows "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U" (is "?lhs = ?rhs")
proof
show "?lhs \<Longrightarrow> ?rhs"
- using r retraction_def retractionE
- by (smt (verit, best) continuous_right_inverse_imp_quotient_map retraction_subset \<open>U \<subseteq> T\<close>)
+ using r
+ by (smt (verit, del_insts) assms(2) continuous_right_inverse_imp_quotient_map image_subset_iff_funcset r retractionE retraction_def retraction_subset)
show "?rhs \<Longrightarrow> ?lhs"
- by (meson continuous_openin_preimage r retraction_def)
+ by (metis continuous_on_open r retraction)
qed
lemma retract_of_Times:
- "\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
+ "\<lbrakk>S retract_of S'; T retract_of T'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (S' \<times> T')"
apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
apply (rename_tac f g)
apply (rule_tac x="\<lambda>z. ((f \<circ> fst) z, (g \<circ> snd) z)" in exI)
@@ -1238,7 +1240,7 @@
lemma path_finish_in_topspace: "pathin X g \<Longrightarrow> g 1 \<in> topspace X"
by (force simp: pathin_def continuous_map)
-lemma path_image_subset_topspace: "pathin X g \<Longrightarrow> g ` ({0..1}) \<subseteq> topspace X"
+lemma path_image_subset_topspace: "pathin X g \<Longrightarrow> g \<in> ({0..1}) \<rightarrow> topspace X"
by (force simp: pathin_def continuous_map)
definition path_connected_space :: "'a topology \<Rightarrow> bool"
@@ -1262,9 +1264,9 @@
lemma path_connectedin:
"path_connectedin X S \<longleftrightarrow>
S \<subseteq> topspace X \<and>
- (\<forall>x \<in> S. \<forall>y \<in> S. \<exists>g. pathin X g \<and> g ` {0..1} \<subseteq> S \<and> g 0 = x \<and> g 1 = y)"
+ (\<forall>x \<in> S. \<forall>y \<in> S. \<exists>g. pathin X g \<and> g \<in> {0..1} \<rightarrow> S \<and> g 0 = x \<and> g 1 = y)"
unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology
- by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2)
+ by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2 flip: image_subset_iff_funcset)
lemma path_connectedin_topspace:
"path_connectedin X (topspace X) \<longleftrightarrow> path_connected_space X"
@@ -1310,21 +1312,21 @@
assumes f: "continuous_map X Y f" and S: "path_connectedin X S"
shows "path_connectedin Y (f ` S)"
proof -
- have fX: "f ` (topspace X) \<subseteq> topspace Y"
- by (metis f continuous_map_image_subset_topspace)
+ have fX: "f \<in> (topspace X) \<rightarrow> topspace Y"
+ using continuous_map_def f by fastforce
show ?thesis
unfolding path_connectedin
proof (intro conjI ballI; clarify?)
fix x
assume "x \<in> S"
show "f x \<in> topspace Y"
- by (meson S fX \<open>x \<in> S\<close> image_subset_iff path_connectedin_subset_topspace set_mp)
+ using S \<open>x \<in> S\<close> fX path_connectedin_subset_topspace by fastforce
next
fix x y
assume "x \<in> S" and "y \<in> S"
- then obtain g where g: "pathin X g" "g ` {0..1} \<subseteq> S" "g 0 = x" "g 1 = y"
+ then obtain g where g: "pathin X g" "g \<in> {0..1} \<rightarrow> S" "g 0 = x" "g 1 = y"
using S by (force simp: path_connectedin)
- show "\<exists>g. pathin Y g \<and> g ` {0..1} \<subseteq> f ` S \<and> g 0 = f x \<and> g 1 = f y"
+ show "\<exists>g. pathin Y g \<and> g \<in> {0..1} \<rightarrow> f ` S \<and> g 0 = f x \<and> g 1 = f y"
proof (intro exI conjI)
show "pathin Y (f \<circ> g)"
using \<open>pathin X g\<close> f pathin_compose by auto
@@ -1361,7 +1363,7 @@
shows "path_connectedin Y (f ` U) \<longleftrightarrow> path_connectedin X U"
unfolding path_connectedin_def
proof (intro conj_cong homeomorphic_path_connected_space)
- show "(f ` U \<subseteq> topspace Y) = (U \<subseteq> topspace X)"
+ show "f ` U \<subseteq> topspace Y \<longleftrightarrow> (U \<subseteq> topspace X)"
using assms homeomorphic_imp_surjective_map by blast
next
assume "U \<subseteq> topspace X"
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Jul 03 16:46:37 2023 +0100
@@ -24,7 +24,7 @@
assumes "contractible T" "S retract_of T"
shows "contractible S"
using assms
-apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with)
+apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with image_subset_iff_funcset)
apply (rule_tac x="r a" in exI)
apply (rule_tac x="r \<circ> h" in exI)
apply (intro conjI continuous_intros continuous_on_compose)
@@ -126,8 +126,8 @@
by (metis eq_id_iff homotopic_with_id2 topspace_euclidean_subtopology)
ultimately
show ?thesis
- unfolding homotopy_equivalent_space_def
- by (metis (no_types, lifting) continuous_map_subtopology_eu continuous_on_id' id_def image_id r retraction_def)
+ unfolding homotopy_equivalent_space_def
+ by (smt (verit, del_insts) continuous_map_id continuous_map_subtopology_eu id_def r retraction retraction_comp subset_refl)
qed
lemma deformation_retract:
@@ -1807,7 +1807,7 @@
and "convex S"
and "interior S \<noteq> {}"
and "continuous_on S f"
- and "f ` S \<subseteq> S"
+ and "f \<in> S \<rightarrow> S"
obtains x where "x \<in> S" and "f x = x"
proof -
let ?U = "cbox 0 One :: 'a set"
@@ -1824,8 +1824,7 @@
then have *: "interior ?U \<noteq> {}" by fast
have *: "?U homeomorphic S"
using homeomorphic_convex_compact[OF convex_box(1) compact_cbox * assms(2,1,3)] .
- have "\<forall>f. continuous_on ?U f \<and> f ` ?U \<subseteq> ?U \<longrightarrow>
- (\<exists>x\<in>?U. f x = x)"
+ have "\<forall>f. continuous_on ?U f \<and> f \<in> ?U \<rightarrow> ?U \<longrightarrow> (\<exists>x\<in>?U. f x = x)"
using brouwer_cube by auto
then show ?thesis
unfolding homeomorphic_fixpoint_property[OF *]
@@ -1839,7 +1838,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
assumes "e > 0"
and "continuous_on (cball a e) f"
- and "f ` cball a e \<subseteq> cball a e"
+ and "f \<in> cball a e \<rightarrow> cball a e"
obtains x where "x \<in> cball a e" and "f x = x"
using brouwer_weak[OF compact_cball convex_cball, of a e f]
unfolding interior_cball ball_eq_empty
@@ -1851,7 +1850,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
assumes S: "compact S" "convex S" "S \<noteq> {}"
and contf: "continuous_on S f"
- and fim: "f ` S \<subseteq> S"
+ and fim: "f \<in> S \<rightarrow> S"
obtains x where "x \<in> S" and "f x = x"
proof -
have "\<exists>e>0. S \<subseteq> cball 0 e"
@@ -1864,12 +1863,12 @@
show "continuous_on (cball 0 e) (f \<circ> closest_point S)"
by (meson assms closest_point_in_set compact_eq_bounded_closed contf continuous_on_closest_point
continuous_on_compose continuous_on_subset image_subsetI)
- show "(f \<circ> closest_point S) ` cball 0 e \<subseteq> cball 0 e"
- by clarsimp (metis S fim closest_point_exists(1) compact_eq_bounded_closed e(2) image_subset_iff mem_cball_0 subsetCE)
+ show "f \<circ> closest_point S \<in> cball 0 e \<rightarrow> cball 0 e"
+ by (smt (verit) Pi_iff assms(1) assms(3) closest_point_in_set comp_apply compact_eq_bounded_closed e(2) fim subset_eq)
qed (use assms in auto)
then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point S) x = x" ..
- have "x \<in> S"
- by (metis closest_point_in_set comp_apply compact_imp_closed fim image_eqI S(1) S(3) subset_iff x(2))
+ with S have "x \<in> S"
+ by (metis PiE closest_point_in_set comp_apply compact_imp_closed fim)
then have *: "closest_point S x = x"
by (rule closest_point_self)
show thesis
@@ -1877,7 +1876,7 @@
show "closest_point S x \<in> S"
by (simp add: "*" \<open>x \<in> S\<close>)
show "f (closest_point S x) = closest_point S x"
- using "*" x(2) by auto
+ using "*" x by auto
qed
qed
@@ -1897,14 +1896,13 @@
proof (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
show "continuous_on (frontier (cball a e)) ((-) (2 *\<^sub>R a))"
by (intro continuous_intros)
- show "(-) (2 *\<^sub>R a) ` frontier (cball a e) \<subseteq> frontier (cball a e)"
+ show "(-) (2 *\<^sub>R a) \<in> frontier (cball a e) \<rightarrow> frontier (cball a e)"
by clarsimp (metis "**" dist_norm norm_minus_cancel)
qed (auto simp: dist_norm intro: brouwer_ball[OF assms])
then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
by (auto simp: algebra_simps)
then have "a = x"
- unfolding scaleR_left_distrib[symmetric]
- by auto
+ unfolding scaleR_left_distrib[symmetric] by auto
then show False
using x assms by auto
qed
@@ -1977,7 +1975,7 @@
fixes S :: "'a::euclidean_space set"
assumes "bounded S" and fros: "frontier S \<subseteq> T"
and contf: "continuous_on (closure S) f"
- and fim: "f ` S \<subseteq> T"
+ and fim: "f \<in> S \<rightarrow> T"
and fid: "\<And>x. x \<in> T \<Longrightarrow> f x = x"
shows "S \<subseteq> T"
proof (rule ccontr)
@@ -1995,7 +1993,7 @@
using \<open>bounded S\<close> bounded_subset_ballD by blast
have notga: "g x \<noteq> a" for x
unfolding g_def using fros fim \<open>a \<notin> T\<close>
- by (metis Un_iff \<open>a \<in> S\<close> closure_Un_frontier fid imageI subset_eq)
+ by (metis PiE Un_iff \<open>a \<in> S\<close> closure_Un_frontier fid subsetD)
define h where "h \<equiv> (\<lambda>y. a + (B / norm(y - a)) *\<^sub>R (y - a)) \<circ> g"
have "\<not> (frontier (cball a B) retract_of (cball a B))"
by (metis no_retraction_cball \<open>0 < B\<close>)
@@ -2009,12 +2007,12 @@
show "continuous_on (cball a B) h"
unfolding h_def
by (intro continuous_intros) (use contg continuous_on_subset notga in auto)
- show "h ` cball a B \<subseteq> frontier (cball a B)"
+ show "h \<in> cball a B \<rightarrow> frontier (cball a B)"
using \<open>0 < B\<close> by (auto simp: h_def notga dist_norm)
show "\<And>x. x \<in> frontier (cball a B) \<Longrightarrow> h x = x"
- apply (auto simp: h_def algebra_simps)
- apply (simp add: vector_add_divide_simps notga)
- by (metis (no_types, opaque_lifting) B add.commute dist_commute dist_norm g_def mem_ball not_less_iff_gr_or_eq subset_eq)
+ using notga \<open>0 < B\<close>
+ apply (simp add: g_def h_def field_simps)
+ by (metis B dist_commute dist_norm mem_ball order_less_irrefl subset_eq)
qed
ultimately show False by simp
qed
@@ -2131,7 +2129,7 @@
using arelS relS rel_frontier_def by fastforce
show "continuous_on (T - {a}) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
using contdd by (simp add: o_def)
- show "(\<lambda>x. a + dd (x - a) *\<^sub>R (x - a)) ` (T - {a}) \<subseteq> rel_frontier S"
+ show "(\<lambda>x. a + dd (x - a) *\<^sub>R (x - a)) \<in> (T - {a}) \<rightarrow> rel_frontier S"
apply (auto simp: rel_frontier_def)
apply (metis Diff_subset add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def subset_iff)
by (metis DiffE add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def rev_subsetD)
@@ -2216,20 +2214,25 @@
subsubsection\<open>Borsuk-style characterization of separation\<close>
lemma continuous_on_Borsuk_map:
- "a \<notin> s \<Longrightarrow> continuous_on s (\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a))"
+ "a \<notin> S \<Longrightarrow> continuous_on S (\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a))"
by (rule continuous_intros | force)+
lemma Borsuk_map_into_sphere:
- "(\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a)) ` s \<subseteq> sphere 0 1 \<longleftrightarrow> (a \<notin> s)"
- by auto (metis eq_iff_diff_eq_0 left_inverse norm_eq_zero)
+ "(\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a)) \<in> S \<rightarrow> sphere 0 1 \<longleftrightarrow> (a \<notin> S)"
+proof -
+ have "\<And>x. \<lbrakk>a \<notin> S; x \<in> S\<rbrakk> \<Longrightarrow> inverse (norm (x - a)) * norm (x - a) = 1"
+ by (metis left_inverse norm_eq_zero right_minus_eq)
+ then show ?thesis
+ by force
+qed
lemma Borsuk_maps_homotopic_in_path_component:
- assumes "path_component (- s) a b"
- shows "homotopic_with_canon (\<lambda>x. True) s (sphere 0 1)
+ assumes "path_component (- S) a b"
+ shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
(\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a))
(\<lambda>x. inverse(norm(x - b)) *\<^sub>R (x - b))"
proof -
- obtain g where "path g" "path_image g \<subseteq> -s" "pathstart g = a" "pathfinish g = b"
+ obtain g where "path g" "path_image g \<subseteq> -S" "pathstart g = a" "pathfinish g = b"
using assms by (auto simp: path_component_def)
then show ?thesis
apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def)
@@ -2240,61 +2243,59 @@
lemma non_extensible_Borsuk_map:
fixes a :: "'a :: euclidean_space"
- assumes "compact s" and cin: "c \<in> components(- s)" and boc: "bounded c" and "a \<in> c"
- shows "\<not> (\<exists>g. continuous_on (s \<union> c) g \<and>
- g ` (s \<union> c) \<subseteq> sphere 0 1 \<and>
- (\<forall>x \<in> s. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))"
+ assumes "compact S" and cin: "C \<in> components(- S)" and boc: "bounded C" and "a \<in> C"
+ shows "\<not> (\<exists>g. continuous_on (S \<union> C) g \<and>
+ g \<in> (S \<union> C) \<rightarrow> sphere 0 1 \<and>
+ (\<forall>x \<in> S. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))"
proof -
- have "closed s" using assms by (simp add: compact_imp_closed)
- have "c \<subseteq> -s"
+ have "closed S" using assms by (simp add: compact_imp_closed)
+ have "C \<subseteq> -S"
using assms by (simp add: in_components_subset)
- with \<open>a \<in> c\<close> have "a \<notin> s" by blast
- then have ceq: "c = connected_component_set (- s) a"
- by (metis \<open>a \<in> c\<close> cin components_iff connected_component_eq)
- then have "bounded (s \<union> connected_component_set (- s) a)"
- using \<open>compact s\<close> boc compact_imp_bounded by auto
- with bounded_subset_ballD obtain r where "0 < r" and r: "(s \<union> connected_component_set (- s) a) \<subseteq> ball a r"
+ with \<open>a \<in> C\<close> have "a \<notin> S" by blast
+ then have ceq: "C = connected_component_set (- S) a"
+ by (metis \<open>a \<in> C\<close> cin components_iff connected_component_eq)
+ then have "bounded (S \<union> connected_component_set (- S) a)"
+ using \<open>compact S\<close> boc compact_imp_bounded by auto
+ with bounded_subset_ballD obtain r where "0 < r" and r: "(S \<union> connected_component_set (- S) a) \<subseteq> ball a r"
by blast
{ fix g
- assume "continuous_on (s \<union> c) g"
- "g ` (s \<union> c) \<subseteq> sphere 0 1"
- and [simp]: "\<And>x. x \<in> s \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
- then have [simp]: "\<And>x. x \<in> s \<union> c \<Longrightarrow> norm (g x) = 1"
+ assume "continuous_on (S \<union> C) g"
+ "g \<in> (S \<union> C) \<rightarrow> sphere 0 1"
+ and [simp]: "\<And>x. x \<in> S \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
+ then have norm_g1[simp]: "\<And>x. x \<in> S \<union> C \<Longrightarrow> norm (g x) = 1"
by force
- have cb_eq: "cball a r = (s \<union> connected_component_set (- s) a) \<union>
- (cball a r - connected_component_set (- s) a)"
+ have cb_eq: "cball a r = (S \<union> connected_component_set (- S) a) \<union>
+ (cball a r - connected_component_set (- S) a)"
using ball_subset_cball [of a r] r by auto
- have cont1: "continuous_on (s \<union> connected_component_set (- s) a)
+ have cont1: "continuous_on (S \<union> connected_component_set (- S) a)
(\<lambda>x. a + r *\<^sub>R g x)"
- using \<open>continuous_on (s \<union> c) g\<close> ceq
+ using \<open>continuous_on (S \<union> C) g\<close> ceq
by (intro continuous_intros) blast
- have cont2: "continuous_on (cball a r - connected_component_set (- s) a)
+ have cont2: "continuous_on (cball a r - connected_component_set (- S) a)
(\<lambda>x. a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
- by (rule continuous_intros | force simp: \<open>a \<notin> s\<close>)+
+ by (rule continuous_intros | force simp: \<open>a \<notin> S\<close>)+
have 1: "continuous_on (cball a r)
- (\<lambda>x. if connected_component (- s) a x
+ (\<lambda>x. if connected_component (- S) a x
then a + r *\<^sub>R g x
else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
apply (subst cb_eq)
apply (rule continuous_on_cases [OF _ _ cont1 cont2])
- using \<open>closed s\<close> ceq cin
+ using \<open>closed S\<close> ceq cin
by (force simp: closed_Diff open_Compl closed_Un_complement_component open_connected_component)+
- have 2: "(\<lambda>x. a + r *\<^sub>R g x) ` (cball a r \<inter> connected_component_set (- s) a)
+ have 2: "(\<lambda>x. a + r *\<^sub>R g x) ` (cball a r \<inter> connected_component_set (- S) a)
\<subseteq> sphere a r "
using \<open>0 < r\<close> by (force simp: dist_norm ceq)
have "retraction (cball a r) (sphere a r)
- (\<lambda>x. if x \<in> connected_component_set (- s) a
+ (\<lambda>x. if x \<in> connected_component_set (- S) a
then a + r *\<^sub>R g x
else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
- using \<open>0 < r\<close>
- apply (simp add: retraction_def dist_norm 1 2, safe)
- apply (force simp: dist_norm abs_if mult_less_0_iff divide_simps \<open>a \<notin> s\<close>)
- using r
- by (auto simp: dist_norm norm_minus_commute)
+ using \<open>0 < r\<close> \<open>a \<notin> S\<close> \<open>a \<in> C\<close> r
+ by (auto simp: norm_minus_commute retraction_def Pi_iff ceq dist_norm abs_if
+ mult_less_0_iff divide_simps 1 2)
then have False
using no_retraction_cball
[OF \<open>0 < r\<close>, of a, unfolded retract_of_def, simplified, rule_format,
- of "\<lambda>x. if x \<in> connected_component_set (- s) a
+ of "\<lambda>x. if x \<in> connected_component_set (- S) a
then a + r *\<^sub>R g x
else a + r *\<^sub>R inverse(norm(x - a)) *\<^sub>R (x - a)"]
by blast
--- a/src/HOL/Analysis/Fashoda_Theorem.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Mon Jul 03 16:46:37 2023 +0100
@@ -174,8 +174,8 @@
"(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
apply (rule compact_cbox convex_box)+
- unfolding interior_cbox
- apply (rule 1 2 3)+
+ unfolding interior_cbox image_subset_iff_funcset [symmetric]
+ apply (rule 1 2 3)+
apply blast
done
have "?F x \<noteq> 0"
--- a/src/HOL/Analysis/Further_Topology.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Mon Jul 03 16:46:37 2023 +0100
@@ -231,7 +231,7 @@
qed
have conT0: "continuous_on (T - {0}) (\<lambda>y. inverse(norm y) *\<^sub>R y)"
by (intro continuous_intros) auto
- have sub0T: "(\<lambda>y. y /\<^sub>R norm y) ` (T - {0}) \<subseteq> sphere 0 1 \<inter> T"
+ have sub0T: "(\<lambda>y. y /\<^sub>R norm y) \<in> (T - {0}) \<rightarrow> sphere 0 1 \<inter> T"
by (fastforce simp: assms(2) subspace_mul)
obtain c where homhc: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) h (\<lambda>x. c)"
proof
@@ -307,7 +307,7 @@
assumes "convex S" "bounded S" "convex T" "bounded T"
and affST: "aff_dim S < aff_dim T"
and contf: "continuous_on (rel_frontier S) f"
- and fim: "f ` (rel_frontier S) \<subseteq> rel_frontier T"
+ and fim: "f \<in> (rel_frontier S) \<rightarrow> rel_frontier T"
obtains c where "homotopic_with_canon (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
proof (cases "S = {}")
case True
@@ -319,7 +319,7 @@
proof (cases "T = {}")
case True
then show ?thesis
- using fim that by auto
+ using fim that by (simp add: Pi_iff)
next
case False
obtain T':: "'a set"
@@ -345,7 +345,7 @@
have "\<exists>c. homotopic_with_canon (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
using spheremap_lemma2 homotopy_eqv_cohomotopic_triviality_null[OF relS]
using homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim]
- by (metis \<open>S' \<subseteq> T'\<close> \<open>subspace S'\<close> \<open>subspace T'\<close> dimST')
+ by (metis \<open>S' \<subseteq> T'\<close> \<open>subspace S'\<close> \<open>subspace T'\<close> dimST' image_subset_iff_funcset)
with that show ?thesis by blast
qed
qed
@@ -353,7 +353,7 @@
lemma inessential_spheremap_lowdim:
fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space"
assumes
- "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \<subseteq> (sphere b s)"
+ "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f \<in> (sphere a r) \<rightarrow> (sphere b s)"
obtains c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
proof (cases "s \<le> 0")
case True then show ?thesis
@@ -505,7 +505,7 @@
using \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face_of_polytope_polytope poly polytope_imp_polyhedron by auto
ultimately have relf_sub: "rel_frontier D \<subseteq> \<Union> {E. E face_of C \<and> aff_dim E < p}"
by (simp add: rel_frontier_of_polyhedron Union_mono)
- then have him_relf: "h ` rel_frontier D \<subseteq> rel_frontier T"
+ then have him_relf: "h \<in> rel_frontier D \<rightarrow> rel_frontier T"
using \<open>C \<in> \<F>\<close> him by blast
have "convex D"
by (simp add: \<open>polyhedron D\<close> polyhedron_imp_convex)
@@ -516,9 +516,9 @@
then have *: "(\<exists>c. homotopic_with_canon (\<lambda>x. True) (rel_frontier D) (rel_frontier T) h (\<lambda>x. c)) =
(\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> rel_frontier T \<and>
(\<forall>x\<in>rel_frontier D. g x = h x))"
- by (simp add: assms rel_frontier_eq_empty him_relf nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier])
- have "(\<exists>c. homotopic_with_canon (\<lambda>x. True) (rel_frontier D) (rel_frontier T) h (\<lambda>x. c))"
- by (metis inessential_spheremap_lowdim_gen
+ by (simp add: assms image_subset_iff_funcset rel_frontier_eq_empty him_relf nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier])
+ have "\<exists>c. homotopic_with_canon (\<lambda>x. True) (rel_frontier D) (rel_frontier T) h (\<lambda>x. c)"
+ by (metis inessential_spheremap_lowdim_gen
[OF \<open>convex D\<close> \<open>bounded D\<close> \<open>convex T\<close> \<open>bounded T\<close> affD_lessT contDh him_relf])
then obtain g where contg: "continuous_on UNIV g"
and gim: "range g \<subseteq> rel_frontier T"
@@ -852,11 +852,11 @@
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X < aff_dim T"
and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
- and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
+ and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> rel_frontier T"
obtains g where "continuous_on (\<Union>\<F>) g"
"g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof -
- obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g ` V \<subseteq> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g \<in> V \<rightarrow> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
have "compact S"
by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact)
@@ -906,11 +906,11 @@
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> aff_dim T"
and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
- and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
+ and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> rel_frontier T"
obtains C g where "finite C" "disjnt C S" "continuous_on (\<Union>\<F> - C) g"
"g ` (\<Union>\<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof -
- obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g ` V \<subseteq> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g \<in> V \<rightarrow> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
have "compact S"
by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact)
@@ -974,13 +974,13 @@
assumes "compact S" "convex U" "bounded U"
and aff: "aff_dim T \<le> aff_dim U"
and "S \<subseteq> T" and contf: "continuous_on S f"
- and fim: "f ` S \<subseteq> rel_frontier U"
+ and fim: "f \<in> S \<rightarrow> rel_frontier U"
obtains K g where "finite K" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
- "g ` (T - K) \<subseteq> rel_frontier U"
+ "g \<in> (T - K) \<rightarrow> rel_frontier U"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof -
have "\<exists>K g. finite K \<and> disjnt K S \<and> continuous_on (T - K) g \<and>
- g ` (T - K) \<subseteq> rel_frontier U \<and> (\<forall>x \<in> S. g x = f x)"
+ g \<in> (T - K) \<rightarrow> rel_frontier U \<and> (\<forall>x \<in> S. g x = f x)"
if "affine T" "S \<subseteq> T" and aff: "aff_dim T \<le> aff_dim U" for T
proof (cases "S = {}")
case True
@@ -1089,7 +1089,8 @@
by (metis image_comp image_mono cpt_subset)
also have "... \<subseteq> rel_frontier U"
by (rule gim)
- finally show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) ` (T - K) \<subseteq> rel_frontier U" .
+ finally show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) \<in> (T - K) \<rightarrow> rel_frontier U"
+ by blast
show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) x = f x" if "x \<in> S" for x
proof -
have "(g \<circ> closest_point (cbox (- c) c \<inter> T)) x = g x"
@@ -1103,7 +1104,7 @@
qed
then obtain K g where "finite K" "disjnt K S"
and contg: "continuous_on (affine hull T - K) g"
- and gim: "g ` (affine hull T - K) \<subseteq> rel_frontier U"
+ and gim: "g \<in> (affine hull T - K) \<rightarrow> rel_frontier U"
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
by (metis aff affine_affine_hull aff_dim_affine_hull
order_trans [OF \<open>S \<subseteq> T\<close> hull_subset [of T affine]])
@@ -1123,14 +1124,14 @@
lemma extend_map_affine_to_sphere1:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::topological_space"
assumes "finite K" "affine U" and contf: "continuous_on (U - K) f"
- and fim: "f ` (U - K) \<subseteq> T"
+ and fim: "f \<in> (U - K) \<rightarrow> T"
and comps: "\<And>C. \<lbrakk>C \<in> components(U - S); C \<inter> K \<noteq> {}\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
and clo: "closedin (top_of_set U) S" and K: "disjnt K S" "K \<subseteq> U"
- obtains g where "continuous_on (U - L) g" "g ` (U - L) \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ obtains g where "continuous_on (U - L) g" "g \<in> (U - L) \<rightarrow> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof (cases "K = {}")
case True
then show ?thesis
- by (metis Diff_empty Diff_subset contf fim continuous_on_subset image_subsetI image_eqI subset_iff that)
+ by (metis DiffD1 Diff_empty Diff_subset PiE Pi_I contf continuous_on_subset fim that)
next
case False
have "S \<subseteq> U"
@@ -1194,7 +1195,7 @@
then obtain r where contr: "continuous_on (U - {a}) r"
and rim: "r ` (U - {a}) \<subseteq> sphere a d" "r ` (U - {a}) \<subseteq> U"
and req: "\<And>x. x \<in> sphere a d \<inter> U \<Longrightarrow> r x = x"
- using \<open>affine U\<close> by (auto simp: retract_of_def retraction_def hull_same)
+ using \<open>affine U\<close> by (force simp: retract_of_def retraction_def hull_same)
define j where "j \<equiv> \<lambda>x. if x \<in> ball a d then r x else x"
have kj: "\<And>x. x \<in> S \<Longrightarrow> k (j x) = x"
using \<open>C \<subseteq> U - S\<close> \<open>S \<subseteq> U\<close> \<open>ball a d \<inter> U \<subseteq> C\<close> j_def subC by auto
@@ -1256,7 +1257,7 @@
have ST: "\<And>x. x \<in> S \<Longrightarrow> (f \<circ> k \<circ> j) x \<in> T"
proof (simp add: kj)
show "\<And>x. x \<in> S \<Longrightarrow> f x \<in> T"
- using K unfolding disjnt_iff by (metis DiffI \<open>S \<subseteq> U\<close> subsetD fim image_subset_iff)
+ using K \<open>S \<subseteq> U\<close> fT unfolding disjnt_iff by auto
qed
moreover have "(f \<circ> k \<circ> j) x \<in> T" if "x \<in> C" "x \<noteq> a" "x \<notin> S" for x
proof -
@@ -1410,7 +1411,7 @@
using image_mono order_trans by blast
moreover have "f ` ((U - L) \<inter> (S \<union> \<Union>G)) \<subseteq> T"
using fim SUG by blast
- ultimately show "(\<lambda>x. if x \<in> S \<union> \<Union>G then f x else g x) ` (U - L) \<subseteq> T"
+ ultimately show "(\<lambda>x. if x \<in> S \<union> \<Union>G then f x else g x) \<in> (U - L) \<rightarrow> T"
by force
show "\<And>x. x \<in> S \<Longrightarrow> (if x \<in> S \<union> \<Union>G then f x else g x) = f x"
by (simp add: F_def G_def)
@@ -1423,15 +1424,15 @@
assumes "compact S" "convex U" "bounded U" "affine T" "S \<subseteq> T"
and affTU: "aff_dim T \<le> aff_dim U"
and contf: "continuous_on S f"
- and fim: "f ` S \<subseteq> rel_frontier U"
+ and fim: "f \<in> S \<rightarrow> rel_frontier U"
and ovlap: "\<And>C. C \<in> components(T - S) \<Longrightarrow> C \<inter> L \<noteq> {}"
obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S"
- "continuous_on (T - K) g" "g ` (T - K) \<subseteq> rel_frontier U"
+ "continuous_on (T - K) g" "g \<in> (T - K) \<rightarrow> rel_frontier U"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof -
obtain K g where K: "finite K" "K \<subseteq> T" "disjnt K S"
and contg: "continuous_on (T - K) g"
- and gim: "g ` (T - K) \<subseteq> rel_frontier U"
+ and gim: "g \<in> (T - K) \<rightarrow> rel_frontier U"
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using assms extend_map_affine_to_sphere_cofinite_simple by metis
have "(\<exists>y C. C \<in> components (T - S) \<and> x \<in> C \<and> y \<in> C \<and> y \<in> L)" if "x \<in> K" for x
@@ -1446,7 +1447,7 @@
then obtain \<xi> where \<xi>: "\<And>x. x \<in> K \<Longrightarrow> \<exists>C. C \<in> components (T - S) \<and> x \<in> C \<and> \<xi> x \<in> C \<and> \<xi> x \<in> L"
by metis
obtain h where conth: "continuous_on (T - \<xi> ` K) h"
- and him: "h ` (T - \<xi> ` K) \<subseteq> rel_frontier U"
+ and him: "h \<in> (T - \<xi> ` K) \<rightarrow> rel_frontier U"
and hg: "\<And>x. x \<in> S \<Longrightarrow> h x = g x"
proof (rule extend_map_affine_to_sphere1 [OF \<open>finite K\<close> \<open>affine T\<close> contg gim, of S "\<xi> ` K"])
show cloTS: "closedin (top_of_set T) S"
@@ -1475,10 +1476,10 @@
assumes SUT: "compact S" "convex U" "bounded U" "affine T" "S \<subseteq> T"
and aff: "aff_dim T \<le> aff_dim U"
and contf: "continuous_on S f"
- and fim: "f ` S \<subseteq> rel_frontier U"
+ and fim: "f \<in> S \<rightarrow> rel_frontier U"
and dis: "\<And>C. \<lbrakk>C \<in> components(T - S); bounded C\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
- "g ` (T - K) \<subseteq> rel_frontier U"
+ "g \<in> (T - K) \<rightarrow> rel_frontier U"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof (cases "S = {}")
case True
@@ -1615,8 +1616,8 @@
have "g (closest_point (cbox (- c) c \<inter> T) x) \<in> rel_frontier U"
if "x \<in> T" "x \<in> K \<longrightarrow> x \<notin> cbox (- b - One) (b + One)" for x
using gim [THEN subsetD] that cloTK by blast
- then show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) ` (T - K \<inter> cbox (- (b + One)) (b + One))
- \<subseteq> rel_frontier U"
+ then show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) \<in> (T - K \<inter> cbox (- (b + One)) (b + One))
+ \<rightarrow> rel_frontier U"
by force
show "\<And>x. x \<in> S \<Longrightarrow> (g \<circ> closest_point (cbox (- c) c \<inter> T)) x = f x"
by simp (metis (mono_tags, lifting) IntI \<open>S \<subseteq> T\<close> cT_ne clo_cT closest_point_refl gf subsetD S_sub_cc)
@@ -1629,23 +1630,26 @@
assumes SUT: "compact S" "affine T" "S \<subseteq> T"
and aff: "aff_dim T \<le> DIM('b)" and "0 \<le> r"
and contf: "continuous_on S f"
- and fim: "f ` S \<subseteq> sphere a r"
+ and fim: "f \<in> S \<rightarrow> sphere a r"
and dis: "\<And>C. \<lbrakk>C \<in> components(T - S); bounded C\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
- "g ` (T - K) \<subseteq> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ "g \<in> (T - K) \<rightarrow> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof (cases "r = 0")
case True
with fim show ?thesis
by (rule_tac K="{}" and g = "\<lambda>x. a" in that) (auto)
next
case False
- with assms have "0 < r" by auto
- then have "aff_dim T \<le> aff_dim (cball a r)"
- by (simp add: aff aff_dim_cball)
- then show ?thesis
- using extend_map_affine_to_sphere_cofinite_gen
- [OF \<open>compact S\<close> convex_cball bounded_cball \<open>affine T\<close> \<open>S \<subseteq> T\<close> _ contf]
- using fim by (fastforce simp: assms False that dest: dis)
+ show thesis
+ proof (rule extend_map_affine_to_sphere_cofinite_gen
+ [OF \<open>compact S\<close> convex_cball bounded_cball \<open>affine T\<close> \<open>S \<subseteq> T\<close> _ contf])
+ have "0 < r"
+ using assms False by auto
+ then show "aff_dim T \<le> aff_dim (cball a r)"
+ by (simp add: aff aff_dim_cball)
+ show "f \<in> S \<rightarrow> rel_frontier (cball a r)"
+ by (simp add: False fim)
+ qed (use dis False that in auto)
qed
corollary extend_map_UNIV_to_sphere_cofinite:
@@ -1653,10 +1657,10 @@
assumes "DIM('a) \<le> DIM('b)" and "0 \<le> r"
and "compact S"
and "continuous_on S f"
- and "f ` S \<subseteq> sphere a r"
+ and "f \<in> S \<rightarrow> sphere a r"
and "\<And>C. \<lbrakk>C \<in> components(- S); bounded C\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
obtains K g where "finite K" "K \<subseteq> L" "disjnt K S" "continuous_on (- K) g"
- "g ` (- K) \<subseteq> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ "g \<in> (- K) \<rightarrow> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using extend_map_affine_to_sphere_cofinite
[OF \<open>compact S\<close> affine_UNIV subset_UNIV] assms
by (metis Compl_eq_Diff_UNIV aff_dim_UNIV of_nat_le_iff)
@@ -1666,9 +1670,9 @@
assumes aff: "DIM('a) \<le> DIM('b)" and "0 \<le> r"
and SUT: "compact S"
and contf: "continuous_on S f"
- and fim: "f ` S \<subseteq> sphere a r"
+ and fim: "f \<in> S \<rightarrow> sphere a r"
and dis: "\<And>C. C \<in> components(- S) \<Longrightarrow> \<not> bounded C"
- obtains g where "continuous_on UNIV g" "g ` UNIV \<subseteq> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ obtains g where "continuous_on UNIV g" "g \<in> UNIV \<rightarrow> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using extend_map_UNIV_to_sphere_cofinite [OF aff \<open>0 \<le> r\<close> \<open>compact S\<close> contf fim, of "{}"]
by (metis Compl_empty_eq dis subset_empty)
@@ -1677,7 +1681,7 @@
fixes S :: "'a::euclidean_space set"
assumes "compact S"
shows "(\<forall>c \<in> components(- S). \<not>bounded c) \<longleftrightarrow>
- (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
+ (\<forall>f. continuous_on S f \<and> f \<in> S \<rightarrow> sphere (0::'a) 1
\<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
(is "?lhs = ?rhs")
proof
@@ -1685,14 +1689,14 @@
show ?rhs
proof clarify
fix f :: "'a \<Rightarrow> 'a"
- assume contf: "continuous_on S f" and fim: "f ` S \<subseteq> sphere 0 1"
- obtain g where contg: "continuous_on UNIV g" and gim: "range g \<subseteq> sphere 0 1"
+ assume contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> sphere 0 1"
+ obtain g where contg: "continuous_on UNIV g" and gim: "g \<in> UNIV \<rightarrow> sphere 0 1"
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
by (rule extend_map_UNIV_to_sphere_no_bounded_component [OF _ _ \<open>compact S\<close> contf fim L]) auto
then obtain c where c: "homotopic_with_canon (\<lambda>h. True) UNIV (sphere 0 1) g (\<lambda>x. c)"
- using contractible_UNIV nullhomotopic_from_contractible by blast
+ by (metis contractible_UNIV nullhomotopic_from_contractible)
then show "\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)"
- by (metis assms compact_imp_closed contf contg contractible_empty fim gf gim nullhomotopic_from_contractible nullhomotopic_into_sphere_extension)
+ by (metis assms compact_imp_closed contf contg contractible_empty fim gf gim nullhomotopic_from_contractible nullhomotopic_into_sphere_extension image_subset_iff_funcset)
qed
next
assume R [rule_format]: ?rhs
@@ -1717,7 +1721,7 @@
fixes S :: "'a::euclidean_space set"
assumes "compact S" and 2: "2 \<le> DIM('a)"
shows "connected(- S) \<longleftrightarrow>
- (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
+ (\<forall>f. continuous_on S f \<and> f \<in> S \<rightarrow> sphere (0::'a) 1
\<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
(is "?lhs = ?rhs")
proof
@@ -2881,7 +2885,7 @@
corollary homotopy_eqv_simple_connectedness:
fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
shows "S homotopy_eqv T \<Longrightarrow> simply_connected S \<longleftrightarrow> simply_connected T"
- by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality)
+ by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality image_subset_iff_funcset)
subsection\<open>Homeomorphism of simple closed curves to circles\<close>
@@ -3673,10 +3677,10 @@
then obtain g where contg: "continuous_on S g" and f: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
by metis
obtain a where "homotopic_with_canon (\<lambda>h. True) S (- {of_real 0}) (exp \<circ> g) (\<lambda>x. a)"
- proof (rule nullhomotopic_through_contractible [OF contg subset_UNIV _ _ contractible_UNIV])
+ proof (rule nullhomotopic_through_contractible [OF contg _ _ _ contractible_UNIV])
show "continuous_on (UNIV::complex set) exp"
by (intro continuous_intros)
- show "range exp \<subseteq> - {0}"
+ show "exp \<in> UNIV \<rightarrow> -{of_real 0}"
by auto
qed force
then have "homotopic_with_canon (\<lambda>h. True) S (- {0}) f (\<lambda>t. a)"
@@ -3719,11 +3723,11 @@
proof (rule nullhomotopic_through_contractible)
show "continuous_on S (complex_of_real \<circ> g)"
by (intro conjI contg continuous_intros)
- show "(complex_of_real \<circ> g) ` S \<subseteq> \<real>"
+ show "(complex_of_real \<circ> g) \<in> S \<rightarrow> \<real>"
by auto
show "continuous_on \<real> (exp \<circ> (*)\<i>)"
by (intro continuous_intros)
- show "(exp \<circ> (*)\<i>) ` \<real> \<subseteq> sphere 0 1"
+ show "(exp \<circ> (*)\<i>) \<in> \<real> \<rightarrow> sphere 0 1"
by (auto simp: complex_is_Real_iff)
qed (auto simp: convex_Reals convex_imp_contractible)
moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> (*)\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
@@ -4012,7 +4016,7 @@
proof -
obtain c where hom: "homotopic_with_canon (\<lambda>h. True) S (-{0}) f (\<lambda>x. c)"
using nullhomotopic_from_contractible assms
- by (metis imageE subset_Compl_singleton)
+ by (metis imageE subset_Compl_singleton image_subset_iff_funcset)
then show ?thesis
by (metis inessential_eq_continuous_logarithm that)
qed
@@ -4023,7 +4027,7 @@
and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
obtains g where "continuous_on S g" "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
using covering_space_lift [OF covering_space_exp_punctured_plane S contf]
- by (metis (full_types) f imageE subset_Compl_singleton)
+ by (metis (full_types) f imageE subset_Compl_singleton image_subset_iff_funcset)
lemma continuous_logarithm_on_cball:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
@@ -4077,7 +4081,7 @@
lemma inessential_spheremap_2_aux:
fixes f :: "'a::euclidean_space \<Rightarrow> complex"
assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f"
- and fim: "f `(sphere a r) \<subseteq> (sphere 0 1)"
+ and fim: "f \<in> (sphere a r) \<rightarrow> (sphere 0 1)"
obtains c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere 0 1) f (\<lambda>x. c)"
proof -
obtain g where contg: "continuous_on (sphere a r) g"
@@ -4095,7 +4099,8 @@
show "continuous_on (sphere a r) (Im \<circ> g)"
by (intro contg continuous_intros continuous_on_compose)
show "\<forall>x\<in>sphere a r. f x = exp (\<i> * complex_of_real ((Im \<circ> g) x))"
- using exp_eq_polar feq fim norm_exp_eq_Re by auto
+ using exp_eq_polar feq fim norm_exp_eq_Re
+ by (auto simp flip: image_subset_iff_funcset)
qed
with inessential_eq_continuous_logarithm_circle that show ?thesis
by metis
@@ -4104,7 +4109,7 @@
lemma inessential_spheremap_2:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2"
- and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \<subseteq> (sphere b s)"
+ and contf: "continuous_on (sphere a r) f" and fim: "f \<in> (sphere a r) \<rightarrow> (sphere b s)"
obtains c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
proof (cases "s \<le> 0")
case True
@@ -4118,20 +4123,20 @@
by (auto simp: homeomorphic_def)
then have conth: "continuous_on (sphere b s) h"
and contk: "continuous_on (sphere 0 1) k"
- and him: "h ` sphere b s \<subseteq> sphere 0 1"
- and kim: "k ` sphere 0 1 \<subseteq> sphere b s"
- by (simp_all add: homeomorphism_def)
+ and him: "h \<in> sphere b s \<rightarrow> sphere 0 1"
+ and kim: "k \<in> sphere 0 1 \<rightarrow> sphere b s"
+ by (force simp: homeomorphism_def)+
obtain c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere 0 1) (h \<circ> f) (\<lambda>x. c)"
proof (rule inessential_spheremap_2_aux [OF a2])
show "continuous_on (sphere a r) (h \<circ> f)"
- by (meson continuous_on_compose [OF contf] conth continuous_on_subset fim)
- show "(h \<circ> f) ` sphere a r \<subseteq> sphere 0 1"
+ by (meson contf conth continuous_on_compose continuous_on_subset fim image_subset_iff_funcset)
+ show "(h \<circ> f) \<in> sphere a r \<rightarrow> sphere 0 1"
using fim him by force
qed auto
then have "homotopic_with_canon (\<lambda>f. True) (sphere a r) (sphere b s) (k \<circ> (h \<circ> f)) (k \<circ> (\<lambda>x. c))"
by (rule homotopic_with_compose_continuous_left [OF _ contk kim])
moreover have "\<And>x. r = dist a x \<Longrightarrow> f x = k (h (f x))"
- by (metis fim hk homeomorphism_def image_subset_iff mem_sphere)
+ by (metis fim hk homeomorphism_def image_subset_iff mem_sphere image_subset_iff_funcset)
ultimately have "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. k c)"
by (auto intro: homotopic_with_eq)
then show ?thesis
@@ -4330,16 +4335,16 @@
definition\<^marker>\<open>tag important\<close> Borsukian where
"Borsukian S \<equiv>
- \<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
+ \<forall>f. continuous_on S f \<and> f \<in> S \<rightarrow> (- {0::complex})
\<longrightarrow> (\<exists>a. homotopic_with_canon (\<lambda>h. True) S (- {0}) f (\<lambda>x. a))"
lemma Borsukian_retraction_gen:
assumes "Borsukian S" "continuous_on S h" "h ` S = T"
- "continuous_on T k" "k ` T \<subseteq> S" "\<And>y. y \<in> T \<Longrightarrow> h(k y) = y"
+ "continuous_on T k" "k \<in> T \<rightarrow> S" "\<And>y. y \<in> T \<Longrightarrow> h(k y) = y"
shows "Borsukian T"
proof -
interpret R: Retracts S h T k
- using assms by (simp add: Retracts.intro)
+ using assms by (simp add: image_subset_iff_funcset Retracts.intro)
show ?thesis
using assms
apply (clarsimp simp add: Borsukian_def)
@@ -4348,7 +4353,7 @@
qed
lemma retract_of_Borsukian: "\<lbrakk>Borsukian T; S retract_of T\<rbrakk> \<Longrightarrow> Borsukian S"
- by (smt (verit) Borsukian_retraction_gen retract_of_def retraction retraction_def retraction_subset)
+ by (smt (verit) Borsukian_retraction_gen retract_of_def retraction retraction_def retraction_subset image_subset_iff_funcset)
lemma homeomorphic_Borsukian: "\<lbrakk>Borsukian S; S homeomorphic T\<rbrakk> \<Longrightarrow> Borsukian T"
using Borsukian_retraction_gen order_refl
@@ -4374,29 +4379,29 @@
and T :: "'b::real_normed_vector set"
assumes "S homotopy_eqv T"
shows "(Borsukian S \<longleftrightarrow> Borsukian T)"
- by (meson Borsukian_def assms homotopy_eqv_cohomotopic_triviality_null)
+ by (meson Borsukian_def assms homotopy_eqv_cohomotopic_triviality_null image_subset_iff_funcset)
lemma Borsukian_alt:
fixes S :: "'a::real_normed_vector set"
shows
"Borsukian S \<longleftrightarrow>
- (\<forall>f g. continuous_on S f \<and> f ` S \<subseteq> -{0} \<and>
- continuous_on S g \<and> g ` S \<subseteq> -{0}
+ (\<forall>f g. continuous_on S f \<and> f \<in> S \<rightarrow> -{0} \<and>
+ continuous_on S g \<and> g \<in> S \<rightarrow> -{0}
\<longrightarrow> homotopic_with_canon (\<lambda>h. True) S (- {0::complex}) f g)"
unfolding Borsukian_def homotopic_triviality
- by (simp add: path_connected_punctured_universe)
+ by (force simp add: path_connected_punctured_universe)
lemma Borsukian_continuous_logarithm:
fixes S :: "'a::real_normed_vector set"
shows "Borsukian S \<longleftrightarrow>
- (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
+ (\<forall>f. continuous_on S f \<and> f \<in> S \<rightarrow> (- {0::complex})
\<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))))"
by (simp add: Borsukian_def inessential_eq_continuous_logarithm)
lemma Borsukian_continuous_logarithm_circle:
fixes S :: "'a::real_normed_vector set"
shows "Borsukian S \<longleftrightarrow>
- (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
+ (\<forall>f. continuous_on S f \<and> f \<in> S \<rightarrow> sphere (0::complex) 1
\<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))))"
(is "?lhs = ?rhs")
proof
@@ -4405,12 +4410,12 @@
next
assume RHS [rule_format]: ?rhs
show ?lhs
- proof (clarsimp simp: Borsukian_continuous_logarithm)
+ proof (clarsimp simp: Borsukian_continuous_logarithm Pi_iff)
fix f :: "'a \<Rightarrow> complex"
- assume contf: "continuous_on S f" and 0: "0 \<notin> f ` S"
+ assume contf: "continuous_on S f" and 0: "\<forall>i\<in>S. f i \<noteq> 0"
then have "continuous_on S (\<lambda>x. f x / complex_of_real (cmod (f x)))"
by (intro continuous_intros) auto
- moreover have "(\<lambda>x. f x / complex_of_real (cmod (f x))) ` S \<subseteq> sphere 0 1"
+ moreover have "(\<lambda>x. f x / complex_of_real (cmod (f x))) \<in> S \<rightarrow> sphere 0 1"
using 0 by (auto simp: norm_divide)
ultimately obtain g where contg: "continuous_on S g"
and fg: "\<forall>x \<in> S. f x / complex_of_real (cmod (f x)) = exp(g x)"
@@ -4431,7 +4436,7 @@
lemma Borsukian_continuous_logarithm_circle_real:
fixes S :: "'a::real_normed_vector set"
shows "Borsukian S \<longleftrightarrow>
- (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
+ (\<forall>f. continuous_on S f \<and> f \<in> S \<rightarrow> sphere (0::complex) 1
\<longrightarrow> (\<exists>g. continuous_on S (complex_of_real \<circ> g) \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x)))))"
(is "?lhs = ?rhs")
proof
@@ -4439,11 +4444,11 @@
show ?rhs
proof (clarify)
fix f :: "'a \<Rightarrow> complex"
- assume "continuous_on S f" and f01: "f ` S \<subseteq> sphere 0 1"
+ assume "continuous_on S f" and f01: "f \<in> S \<rightarrow> sphere 0 1"
then obtain g where contg: "continuous_on S g" and "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
using LHS by (auto simp: Borsukian_continuous_logarithm_circle)
then have "\<forall>x\<in>S. f x = exp (\<i> * complex_of_real ((Im \<circ> g) x))"
- using f01 exp_eq_polar norm_exp_eq_Re by auto
+ using f01 exp_eq_polar norm_exp_eq_Re by (fastforce simp: Pi_iff)
then show "\<exists>g. continuous_on S (complex_of_real \<circ> g) \<and> (\<forall>x\<in>S. f x = exp (\<i> * complex_of_real (g x)))"
by (rule_tac x="Im \<circ> g" in exI) (force intro: continuous_intros contg)
qed
@@ -4452,7 +4457,7 @@
show ?lhs
proof (clarsimp simp: Borsukian_continuous_logarithm_circle)
fix f :: "'a \<Rightarrow> complex"
- assume "continuous_on S f" and f01: "f ` S \<subseteq> sphere 0 1"
+ assume "continuous_on S f" and f01: "f \<in> S \<rightarrow> sphere 0 1"
then obtain g where contg: "continuous_on S (complex_of_real \<circ> g)" and "\<And>x. x \<in> S \<Longrightarrow> f x = exp(\<i> * of_real(g x))"
by (metis RHS)
then show "\<exists>g. continuous_on S g \<and> (\<forall>x\<in>S. f x = exp (g x))"
@@ -4463,17 +4468,18 @@
lemma Borsukian_circle:
fixes S :: "'a::real_normed_vector set"
shows "Borsukian S \<longleftrightarrow>
- (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
+ (\<forall>f. continuous_on S f \<and> f \<in> S \<rightarrow> sphere (0::complex) 1
\<longrightarrow> (\<exists>a. homotopic_with_canon (\<lambda>h. True) S (sphere (0::complex) 1) f (\<lambda>x. a)))"
by (simp add: inessential_eq_continuous_logarithm_circle Borsukian_continuous_logarithm_circle_real)
lemma contractible_imp_Borsukian: "contractible S \<Longrightarrow> Borsukian S"
- by (meson Borsukian_def nullhomotopic_from_contractible)
+ by (meson Borsukian_def nullhomotopic_from_contractible image_subset_iff_funcset)
lemma simply_connected_imp_Borsukian:
fixes S :: "'a::real_normed_vector set"
shows "\<lbrakk>simply_connected S; locally path_connected S\<rbrakk> \<Longrightarrow> Borsukian S"
- by (metis (no_types, lifting) Borsukian_continuous_logarithm continuous_logarithm_on_simply_connected image_eqI subset_Compl_singleton)
+ by (smt (verit, del_insts) continuous_logarithm_on_simply_connected Borsukian_continuous_logarithm_circle
+ PiE mem_sphere_0 norm_eq_zero zero_neq_one)
lemma starlike_imp_Borsukian:
fixes S :: "'a::real_normed_vector set"
@@ -4504,19 +4510,19 @@
\<lbrakk>continuous_on S f; continuous_on T g; \<And>x. x \<in> S \<and> x \<in> T \<Longrightarrow> f x = g x\<rbrakk>
\<Longrightarrow> continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then f x else g x)"
shows "Borsukian(S \<union> T)"
-proof (clarsimp simp add: Borsukian_continuous_logarithm)
+proof (clarsimp simp add: Borsukian_continuous_logarithm Pi_iff)
fix f :: "'a \<Rightarrow> complex"
- assume contf: "continuous_on (S \<union> T) f" and 0: "0 \<notin> f ` (S \<union> T)"
+ assume contf: "continuous_on (S \<union> T) f" and 0: "\<forall>i\<in>S \<union> T. f i \<noteq> 0"
then have contfS: "continuous_on S f" and contfT: "continuous_on T f"
using continuous_on_subset by auto
have "\<lbrakk>continuous_on S f; f ` S \<subseteq> -{0}\<rbrakk> \<Longrightarrow> \<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))"
using BS by (auto simp: Borsukian_continuous_logarithm)
then obtain g where contg: "continuous_on S g" and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
- using "0" contfS by blast
+ using "0" contfS by force
have "\<lbrakk>continuous_on T f; f ` T \<subseteq> -{0}\<rbrakk> \<Longrightarrow> \<exists>g. continuous_on T g \<and> (\<forall>x \<in> T. f x = exp(g x))"
using BT by (auto simp: Borsukian_continuous_logarithm)
then obtain h where conth: "continuous_on T h" and fh: "\<And>x. x \<in> T \<Longrightarrow> f x = exp(h x)"
- using "0" contfT by blast
+ using "0" contfT by force
show "\<exists>g. continuous_on (S \<union> T) g \<and> (\<forall>x\<in>S \<union> T. f x = exp (g x))"
proof (cases "S \<inter> T = {}")
case True
@@ -4592,9 +4598,9 @@
assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T"
and "compact S" and conn: "\<And>y. y \<in> T \<Longrightarrow> connected {x. x \<in> S \<and> f x = y}"
shows "Borsukian T"
-proof (clarsimp simp add: Borsukian_continuous_logarithm)
+proof (clarsimp simp: Borsukian_continuous_logarithm Pi_iff)
fix g :: "'b \<Rightarrow> complex"
- assume contg: "continuous_on T g" and 0: "0 \<notin> g ` T"
+ assume contg: "continuous_on T g" and 0: "\<forall>i\<in>T. g i \<noteq> 0"
have "continuous_on S (g \<circ> f)"
using contf contg continuous_on_compose fim by blast
moreover have "(g \<circ> f) ` S \<subseteq> -{0}"
@@ -4631,7 +4637,7 @@
proof (rule continuous_from_closed_graph [of "h ` S"])
show "compact (h ` S)"
by (simp add: \<open>compact S\<close> compact_continuous_image conth)
- show "(h \<circ> f') ` T \<subseteq> h ` S"
+ show "(h \<circ> f') \<in> T \<rightarrow> h ` S"
by (auto simp: f')
have "h x = h (f' (f x))" if "x \<in> S" for x
using * [of "f x"] fim that unfolding constant_on_def by clarsimp (metis f' imageI right_minus_eq)
@@ -4660,10 +4666,10 @@
shows "Borsukian T"
proof (clarsimp simp add: Borsukian_continuous_logarithm_circle_real)
fix g :: "'b \<Rightarrow> complex"
- assume contg: "continuous_on T g" and gim: "g ` T \<subseteq> sphere 0 1"
+ assume contg: "continuous_on T g" and gim: "g \<in> T \<rightarrow> sphere 0 1"
have "continuous_on S (g \<circ> f)"
using contf contg continuous_on_compose fim by blast
- moreover have "(g \<circ> f) ` S \<subseteq> sphere 0 1"
+ moreover have "(g \<circ> f) \<in> S \<rightarrow> sphere 0 1"
using fim gim by auto
ultimately obtain h where cont_cxh: "continuous_on S (complex_of_real \<circ> h)"
and gfh: "\<And>x. x \<in> S \<Longrightarrow> (g \<circ> f) x = exp(\<i> * of_real(h x))"
@@ -4677,7 +4683,8 @@
show "continuous_on {x \<in> S. f x = y} h"
by (rule continuous_on_subset [OF conth]) auto
have "compact (S \<inter> f -` {y})"
- by (rule proper_map_from_compact [OF contf _ \<open>compact S\<close>, of T]) (simp_all add: fim that)
+ using that proper_map_from_compact [OF contf _ \<open>compact S\<close>] fim
+ by force
then show "compact {x \<in> S. f x = y}"
by (auto simp: vimage_def Int_def)
qed
@@ -4985,7 +4992,7 @@
with qV qW show ?thesis by force
qed
obtain g where contg: "continuous_on U g"
- and circle: "g ` U \<subseteq> sphere 0 1"
+ and circle: "g \<in> U \<rightarrow> sphere 0 1"
and S: "\<And>x. x \<in> S \<Longrightarrow> g x = exp(pi * \<i> * q x)"
and T: "\<And>x. x \<in> T \<Longrightarrow> g x = 1 / exp(pi * \<i> * q x)"
proof
@@ -5415,7 +5422,7 @@
proof (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ homotopic_with_symD [OF a]])
show "closedin (top_of_set UNIV) S"
using assms by auto
- show "range (\<lambda>t. a) \<subseteq> - {0}"
+ show "(\<lambda>t. a) \<in> UNIV \<rightarrow> - {0}"
using a homotopic_with_imp_subset2 False by blast
qed (use anr that in \<open>force+\<close>)
then show ?thesis
--- a/src/HOL/Analysis/Homeomorphism.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy Mon Jul 03 16:46:37 2023 +0100
@@ -1112,10 +1112,10 @@
fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
assumes cov: "covering_space c p S"
and eq: "g1 a = g2 a"
- and f: "continuous_on T f" "f ` T \<subseteq> S"
- and g1: "continuous_on T g1" "g1 ` T \<subseteq> c"
+ and f: "continuous_on T f" "f \<in> T \<rightarrow> S"
+ and g1: "continuous_on T g1" "g1 \<in> T \<rightarrow> c"
and fg1: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
- and g2: "continuous_on T g2" "g2 ` T \<subseteq> c"
+ and g2: "continuous_on T g2" "g2 \<in> T \<rightarrow> c"
and fg2: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
and u_compt: "U \<in> components T" and "a \<in> U" "x \<in> U"
shows "g1 x = g2 x"
@@ -1175,9 +1175,9 @@
fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
assumes "covering_space c p S"
"g1 a = g2 a"
- "continuous_on T f" "f ` T \<subseteq> S"
- "continuous_on T g1" "g1 ` T \<subseteq> c" "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
- "continuous_on T g2" "g2 ` T \<subseteq> c" "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
+ "continuous_on T f" "f \<in> T \<rightarrow> S"
+ "continuous_on T g1" "g1 \<in> T \<rightarrow> c" "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
+ "continuous_on T g2" "g2 \<in> T \<rightarrow> c" "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
"connected T" "a \<in> T" "x \<in> T"
shows "g1 x = g2 x"
using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
@@ -1315,11 +1315,11 @@
and h :: "real \<times> 'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S"
and conth: "continuous_on ({0..1} \<times> U) h"
- and him: "h ` ({0..1} \<times> U) \<subseteq> S"
+ and him: "h \<in> ({0..1} \<times> U) \<rightarrow> S"
and heq: "\<And>y. y \<in> U \<Longrightarrow> h (0,y) = p(f y)"
- and contf: "continuous_on U f" and fim: "f ` U \<subseteq> C"
+ and contf: "continuous_on U f" and fim: "f \<in> U \<rightarrow> C"
obtains k where "continuous_on ({0..1} \<times> U) k"
- "k ` ({0..1} \<times> U) \<subseteq> C"
+ "k \<in> ({0..1} \<times> U) \<rightarrow> C"
"\<And>y. y \<in> U \<Longrightarrow> k(0, y) = f y"
"\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p(k z)"
proof -
@@ -1459,7 +1459,7 @@
proof (rule continuous_openin_preimage [OF _ _ opeC'])
show "continuous_on V (k \<circ> Pair (n/N))"
by (intro continuous_intros continuous_on_subset [OF contk], auto)
- show "(k \<circ> Pair (n/N)) ` V \<subseteq> C"
+ show "(k \<circ> Pair (n/N)) \<in> V \<rightarrow> C"
using kim by (auto simp: \<open>y \<in> V\<close> W)
qed
obtain N' where opeUN': "openin (top_of_set U) N'"
@@ -1633,19 +1633,19 @@
using*V by (simp add: \<open>y \<in> V i\<close> \<open>y \<in> V j\<close> that)
show conth_y: "continuous_on ({0..1} \<times> {y}) h"
using VU \<open>y \<in> V j\<close> that by (auto intro: continuous_on_subset [OF conth])
- show "h ` ({0..1} \<times> {y}) \<subseteq> S"
+ show "h \<in> ({0..1} \<times> {y}) \<rightarrow> S"
using \<open>y \<in> V i\<close> assms(3) VU that by fastforce
show "continuous_on ({0..1} \<times> {y}) (fs i)"
using continuous_on_subset [OF contfs] \<open>i \<in> U\<close>
by (simp add: \<open>y \<in> V i\<close> subset_iff)
- show "fs i ` ({0..1} \<times> {y}) \<subseteq> C"
+ show "fs i \<in> ({0..1} \<times> {y}) \<rightarrow> C"
using "*" \<open>y \<in> V i\<close> \<open>i \<in> U\<close> by fastforce
show "\<And>x. x \<in> {0..1} \<times> {y} \<Longrightarrow> h x = p (fs i x)"
using "*" \<open>y \<in> V i\<close> \<open>i \<in> U\<close> by blast
show "continuous_on ({0..1} \<times> {y}) (fs j)"
using continuous_on_subset [OF contfs] \<open>j \<in> U\<close>
by (simp add: \<open>y \<in> V j\<close> subset_iff)
- show "fs j ` ({0..1} \<times> {y}) \<subseteq> C"
+ show "fs j \<in> ({0..1} \<times> {y}) \<rightarrow> C"
using "*" \<open>y \<in> V j\<close> \<open>j \<in> U\<close> by fastforce
show "\<And>x. x \<in> {0..1} \<times> {y} \<Longrightarrow> h x = p (fs j x)"
using "*" \<open>y \<in> V j\<close> \<open>j \<in> U\<close> by blast
@@ -1660,7 +1660,7 @@
qed force
show ?thesis
proof
- show "k ` ({0..1} \<times> U) \<subseteq> C"
+ show "k \<in> ({0..1} \<times> U) \<rightarrow> C"
using V*k VU by fastforce
show "\<And>y. y \<in> U \<Longrightarrow> k (0, y) = f y"
by (simp add: V*k)
@@ -1674,11 +1674,11 @@
and h :: "'c::real_normed_vector \<times> real \<Rightarrow> 'b"
assumes cov: "covering_space C p S"
and conth: "continuous_on (U \<times> {0..1}) h"
- and him: "h ` (U \<times> {0..1}) \<subseteq> S"
+ and him: "h \<in> (U \<times> {0..1}) \<rightarrow> S"
and heq: "\<And>y. y \<in> U \<Longrightarrow> h (y,0) = p(f y)"
- and contf: "continuous_on U f" and fim: "f ` U \<subseteq> C"
+ and contf: "continuous_on U f" and fim: "f \<in> U \<rightarrow> C"
obtains k where "continuous_on (U \<times> {0..1}) k"
- "k ` (U \<times> {0..1}) \<subseteq> C"
+ "k \<in> (U \<times> {0..1}) \<rightarrow> C"
"\<And>y. y \<in> U \<Longrightarrow> k(y, 0) = f y"
"\<And>z. z \<in> U \<times> {0..1} \<Longrightarrow> h z = p(k z)"
proof -
@@ -1701,13 +1701,13 @@
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and g:: "'c::real_normed_vector \<Rightarrow> 'a"
assumes cov: "covering_space C p S"
and contg: "continuous_on U g"
- and gim: "g ` U \<subseteq> C"
+ and gim: "g \<in> U \<rightarrow> C"
and pgeq: "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
and hom: "homotopic_with_canon (\<lambda>x. True) U S f f'"
obtains g' where "continuous_on U g'" "image g' U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g' y) = f' y"
proof -
obtain h where conth: "continuous_on ({0..1::real} \<times> U) h"
- and him: "h ` ({0..1} \<times> U) \<subseteq> S"
+ and him: "h \<in> ({0..1} \<times> U) \<rightarrow> S"
and h0: "\<And>x. h(0, x) = f x"
and h1: "\<And>x. h(1, x) = f' x"
using hom by (auto simp: homotopic_with_def)
@@ -1717,7 +1717,7 @@
and kim: "k ` ({0..1} \<times> U) \<subseteq> C"
and k0: "\<And>y. y \<in> U \<Longrightarrow> k(0, y) = g y"
and heq: "\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p(k z)"
- using covering_space_lift_homotopy [OF cov conth him _ contg gim] by metis
+ using covering_space_lift_homotopy [OF cov conth him _ contg gim] by (metis image_subset_iff_funcset)
show ?thesis
proof
show "continuous_on U (k \<circ> Pair 1)"
@@ -1743,7 +1743,7 @@
then obtain b where b: "b \<in> C" "p b = a"
using covering_space_imp_surjective [OF cov] homotopic_with_imp_subset2 [OF hom]
by auto
- then have gim: "(\<lambda>y. b) ` U \<subseteq> C"
+ then have gim: "(\<lambda>y. b) \<in> U \<rightarrow> C"
by blast
show ?thesis
proof (rule covering_space_lift_homotopic_function [OF cov continuous_on_const gim])
@@ -1770,7 +1770,7 @@
proof (rule covering_space_lift_homotopy [OF cov, of "{undefined}" "g \<circ> fst"])
show "continuous_on ({0..1::real} \<times> {undefined::'c}) (g \<circ> fst)"
using \<open>path g\<close> by (intro continuous_intros) (simp add: path_def)
- show "(g \<circ> fst) ` ({0..1} \<times> {undefined}) \<subseteq> S"
+ show "(g \<circ> fst) \<in> ({0..1} \<times> {undefined}) \<rightarrow> S"
using pag by (auto simp: path_image_def)
show "(g \<circ> fst) (0, y) = p a" if "y \<in> {undefined}" for y::'c
by (metis comp_def fst_conv pas pathstart_def)
@@ -1815,13 +1815,13 @@
proof -
obtain h :: "real \<times> real \<Rightarrow> 'b"
where conth: "continuous_on ({0..1} \<times> {0..1}) h"
- and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
+ and him: "h \<in> ({0..1} \<times> {0..1}) \<rightarrow> S"
and h0: "\<And>x. h (0, x) = g1 x" and h1: "\<And>x. h (1, x) = g2 x"
and heq0: "\<And>t. t \<in> {0..1} \<Longrightarrow> h (t, 0) = g1 0"
and heq1: "\<And>t. t \<in> {0..1} \<Longrightarrow> h (t, 1) = g1 1"
- using hom by (auto simp: homotopic_paths_def homotopic_with_def pathstart_def pathfinish_def)
+ using hom by (auto simp: homotopic_paths_def homotopic_with_def pathstart_def pathfinish_def image_subset_iff_funcset)
obtain k where contk: "continuous_on ({0..1} \<times> {0..1}) k"
- and kim: "k ` ({0..1} \<times> {0..1}) \<subseteq> C"
+ and kim: "k \<in> ({0..1} \<times> {0..1}) \<rightarrow> C"
and kh2: "\<And>y. y \<in> {0..1} \<Longrightarrow> k (y, 0) = h2 0"
and hpk: "\<And>z. z \<in> {0..1} \<times> {0..1} \<Longrightarrow> h z = p (k z)"
proof (rule covering_space_lift_homotopy_alt [OF cov conth him])
@@ -1830,11 +1830,11 @@
qed (use path_image_def pih2 in \<open>fastforce+\<close>)
have contg1: "continuous_on {0..1} g1" and contg2: "continuous_on {0..1} g2"
using \<open>path g1\<close> \<open>path g2\<close> path_def by blast+
- have g1im: "g1 ` {0..1} \<subseteq> S" and g2im: "g2 ` {0..1} \<subseteq> S"
+ have g1im: "g1 \<in> {0..1} \<rightarrow> S" and g2im: "g2 \<in> {0..1} \<rightarrow> S"
using path_image_def pig1 pig2 by auto
have conth1: "continuous_on {0..1} h1" and conth2: "continuous_on {0..1} h2"
using \<open>path h1\<close> \<open>path h2\<close> path_def by blast+
- have h1im: "h1 ` {0..1} \<subseteq> C" and h2im: "h2 ` {0..1} \<subseteq> C"
+ have h1im: "h1 \<in> {0..1} \<rightarrow> C" and h2im: "h2 \<in> {0..1} \<rightarrow> C"
using path_image_def pih1 pih2 by auto
show ?thesis
unfolding homotopic_paths pathstart_def pathfinish_def
@@ -1911,13 +1911,13 @@
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" and "a \<in> C" "z \<in> U"
and U: "path_connected U" "locally path_connected U"
- and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
+ and contf: "continuous_on U f" and fim: "f \<in> U \<rightarrow> S"
and feq: "f z = p a"
and hom: "\<And>r. \<lbrakk>path r; path_image r \<subseteq> U; pathstart r = z; pathfinish r = z\<rbrakk>
\<Longrightarrow> \<exists>q. path q \<and> path_image q \<subseteq> C \<and>
pathstart q = a \<and> pathfinish q = a \<and>
homotopic_paths S (f \<circ> r) (p \<circ> q)"
- obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
+ obtains g where "continuous_on U g" "g \<in> U \<rightarrow> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
proof -
have *: "\<exists>g h. path g \<and> path_image g \<subseteq> U \<and>
pathstart g = z \<and> pathfinish g = y \<and>
@@ -1934,7 +1934,7 @@
show "path (f \<circ> g)"
using \<open>path g\<close> \<open>path_image g \<subseteq> U\<close> contf continuous_on_subset path_continuous_image by blast
show "path_image (f \<circ> g) \<subseteq> S"
- by (metis \<open>path_image g \<subseteq> U\<close> fim image_mono path_image_compose subset_trans)
+ by (metis \<open>path_image g \<subseteq> U\<close> fim image_mono path_image_compose subset_trans image_subset_iff_funcset)
show "pathstart (f \<circ> g) = p a"
by (simp add: feq pastg pathstart_compose)
qed auto
@@ -1975,11 +1975,11 @@
show "g ` (*\<^sub>R) 2 ` {0..1/2} \<subseteq> U"
using g path_image_def by fastforce
qed auto
- show "(f \<circ> g \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> S"
- using g(2) path_image_def fim by fastforce
- show "(h \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> C"
+ show "(f \<circ> g \<circ> (*\<^sub>R) 2) \<in> {0..1/2} \<rightarrow> S"
+ using g(2) fim by (fastforce simp: path_image_def image_subset_iff_funcset)
+ show "(h \<circ> (*\<^sub>R) 2) \<in> {0..1/2} \<rightarrow> C"
using h path_image_def by fastforce
- show "q' ` {0..1/2} \<subseteq> C"
+ show "q' \<in> {0..1/2} \<rightarrow> C"
using \<open>path_image q' \<subseteq> C\<close> path_image_def by fastforce
show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> (*\<^sub>R) 2) x = p (q' x)"
by (auto simp: joinpaths_def pq'_eq)
@@ -2000,11 +2000,11 @@
show "reversepath g' ` (\<lambda>t. 2 *\<^sub>R t - 1) ` {1/2<..1} \<subseteq> U"
using g' by (auto simp: path_image_def reversepath_def)
qed (use g' in auto)
- show "(f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) ` {1/2<..1} \<subseteq> S"
+ show "(f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) \<in> {1/2<..1} \<rightarrow> S"
using g'(2) path_image_def fim by (auto simp: image_subset_iff path_image_def reversepath_def)
- show "q' ` {1/2<..1} \<subseteq> C"
+ show "q' \<in> {1/2<..1} \<rightarrow> C"
using \<open>path_image q' \<subseteq> C\<close> path_image_def by fastforce
- show "(reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) ` {1/2<..1} \<subseteq> C"
+ show "(reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) \<in> {1/2<..1} \<rightarrow> C"
using h' by (simp add: path_image_def reversepath_def subset_eq)
show "\<And>x. x \<in> {1/2<..1} \<Longrightarrow> (f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) x = p (q' x)"
by (auto simp: joinpaths_def pq'_eq)
@@ -2036,7 +2036,7 @@
using*[OF \<open>y \<in> U\<close>] by (metis l atLeastAtMost_iff order_refl pathfinish_def zero_le_one)
show "l z = a"
using l [of "linepath z z" z "linepath a a"] by (auto simp: assms)
- show LC: "l ` U \<subseteq> C"
+ show LC: "l \<in> U \<rightarrow> C"
by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE)
have "\<exists>T. openin (top_of_set U) T \<and> y \<in> T \<and> T \<subseteq> U \<inter> l -` X"
if X: "openin (top_of_set C) X" and "y \<in> U" "l y \<in> X" for X y
@@ -2080,7 +2080,8 @@
have "openin (top_of_set S) (W \<inter> p' -` (W' \<inter> X))"
proof (rule openin_trans)
show "openin (top_of_set W) (W \<inter> p' -` (W' \<inter> X))"
- using X \<open>W' \<subseteq> C\<close> by (intro continuous_openin_preimage [OF contp' p'im]) (auto simp: openin_open)
+ using X \<open>W' \<subseteq> C\<close>
+ by (metis continuous_on_open contp' homUW' homeomorphism_image2 inf.assoc inf.orderE openin_open)
show "openin (top_of_set S) W"
using WV by blast
qed
@@ -2154,6 +2155,7 @@
qed
qed
then show "continuous_on U l"
+ using vimage_eq openin_subopen continuous_on_open_gen [OF LC]
by (metis IntD1 IntD2 vimage_eq openin_subopen continuous_on_open_gen [OF LC])
qed
qed
@@ -2163,11 +2165,11 @@
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
and U: "path_connected U" "locally path_connected U"
- and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
+ and contf: "continuous_on U f" and fim: "f \<in> U \<rightarrow> S"
and feq: "f z = p a"
and hom: "\<And>r. \<lbrakk>path r; path_image r \<subseteq> U; pathstart r = z; pathfinish r = z\<rbrakk>
\<Longrightarrow> \<exists>b. homotopic_paths S (f \<circ> r) (linepath b b)"
- obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
+ obtains g where "continuous_on U g" "g \<in> U \<rightarrow> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
proof (rule covering_space_lift_general [OF cov U contf fim feq])
fix r
assume "path r" "path_image r \<subseteq> U" "pathstart r = z" "pathfinish r = z"
@@ -2190,9 +2192,9 @@
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
and scU: "simply_connected U" and lpcU: "locally path_connected U"
- and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
+ and contf: "continuous_on U f" and fim: "f \<in> U \<rightarrow> S"
and feq: "f z = p a"
- obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
+ obtains g where "continuous_on U g" "g \<in> U \<rightarrow> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
proof (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
show "path_connected U"
using scU simply_connected_eq_contractible_loop_some by blast
@@ -2211,8 +2213,8 @@
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S"
and U: "simply_connected U" "locally path_connected U"
- and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
- obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
+ and contf: "continuous_on U f" and fim: "f \<in> U \<rightarrow> S"
+ obtains g where "continuous_on U g" "g \<in> U \<rightarrow> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
proof (cases "U = {}")
case True
with that show ?thesis by auto
@@ -2220,7 +2222,7 @@
case False
then obtain z where "z \<in> U" by blast
then obtain a where "a \<in> C" "f z = p a"
- by (metis cov covering_space_imp_surjective fim image_iff image_subset_iff)
+ by (metis cov covering_space_imp_surjective fim image_iff Pi_iff)
then show ?thesis
by (metis that covering_space_lift_strong [OF cov _ \<open>z \<in> U\<close> U contf fim])
qed
--- a/src/HOL/Analysis/Homotopy.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Homotopy.thy Mon Jul 03 16:46:37 2023 +0100
@@ -124,6 +124,14 @@
"homotopic_with_canon P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
+lemma homotopic_with_imp_funspace1:
+ "homotopic_with_canon P X Y f g \<Longrightarrow> f \<in> X \<rightarrow> Y"
+ using homotopic_with_imp_subset1 by blast
+
+lemma homotopic_with_imp_funspace2:
+ "homotopic_with_canon P X Y f g \<Longrightarrow> g \<in> X \<rightarrow> Y"
+ using homotopic_with_imp_subset2 by blast
+
lemma homotopic_with_subset_left:
"\<lbrakk>homotopic_with_canon P X Y f g; Z \<subseteq> X\<rbrakk> \<Longrightarrow> homotopic_with_canon P Z Y f g"
unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward)
@@ -150,7 +158,7 @@
have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j"
proof -
have "continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} \<times> topspace X)) ?j"
- by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff)
+ by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff flip: image_subset_iff_funcset)
then show ?thesis
by (simp add: prod_topology_subtopology(1))
qed
@@ -262,14 +270,14 @@
by (metis assms homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps homotopic_with_trans)
proposition homotopic_with_compose_continuous_right:
- "\<lbrakk>homotopic_with_canon (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
+ "\<lbrakk>homotopic_with_canon (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h \<in> W \<rightarrow> X\<rbrakk>
\<Longrightarrow> homotopic_with_canon p W Y (f \<circ> h) (g \<circ> h)"
- by (simp add: homotopic_with_compose_continuous_map_right)
+ by (simp add: homotopic_with_compose_continuous_map_right image_subset_iff_funcset)
proposition homotopic_with_compose_continuous_left:
- "\<lbrakk>homotopic_with_canon (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
+ "\<lbrakk>homotopic_with_canon (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h \<in> Y \<rightarrow> Z\<rbrakk>
\<Longrightarrow> homotopic_with_canon p X Z (h \<circ> f) (h \<circ> g)"
- by (simp add: homotopic_with_compose_continuous_map_left)
+ by (simp add: homotopic_with_compose_continuous_map_left image_subset_iff_funcset)
lemma homotopic_from_subtopology:
"homotopic_with P X X' f g \<Longrightarrow> homotopic_with P (subtopology X S) X' f g"
@@ -397,15 +405,15 @@
text\<open>Homotopic triviality implicitly incorporates path-connectedness.\<close>
lemma homotopic_triviality:
- shows "(\<forall>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
- continuous_on S g \<and> g ` S \<subseteq> T
+ shows "(\<forall>f g. continuous_on S f \<and> f \<in> S \<rightarrow> T \<and>
+ continuous_on S g \<and> g \<in> S \<rightarrow> T
\<longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g) \<longleftrightarrow>
(S = {} \<or> path_connected T) \<and>
- (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> T \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)))"
+ (\<forall>f. continuous_on S f \<and> f \<in> S \<rightarrow> T \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)))"
(is "?lhs = ?rhs")
proof (cases "S = {} \<or> T = {}")
case True then show ?thesis
- by (auto simp: homotopic_on_emptyI)
+ by (auto simp: homotopic_on_emptyI simp flip: image_subset_iff_funcset)
next
case False show ?thesis
proof
@@ -418,7 +426,7 @@
using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto
qed
moreover
- have "\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)" if "continuous_on S f" "f ` S \<subseteq> T" for f
+ have "\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)" if "continuous_on S f" "f \<in> S \<rightarrow> T" for f
using False LHS continuous_on_const that by blast
ultimately show ?rhs
by (simp add: path_connected_component)
@@ -429,9 +437,9 @@
show ?lhs
proof clarify
fix f g
- assume "continuous_on S f" "f ` S \<subseteq> T" "continuous_on S g" "g ` S \<subseteq> T"
+ assume "continuous_on S f" "f \<in> S \<rightarrow> T" "continuous_on S g" "g \<in> S \<rightarrow> T"
obtain c d where c: "homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)" and d: "homotopic_with_canon (\<lambda>x. True) S T g (\<lambda>x. d)"
- using False \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> T\<close> RHS \<open>continuous_on S g\<close> \<open>g ` S \<subseteq> T\<close> by blast
+ using RHS \<open>continuous_on S f\<close> \<open>continuous_on S g\<close> \<open>f \<in> S \<rightarrow> T\<close> \<open>g \<in> S \<rightarrow> T\<close> by presburger
with T have "path_component T c d"
by (metis False ex_in_conv homotopic_with_imp_subset2 image_subset_iff path_connected_component)
then have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. c) (\<lambda>x. d)"
@@ -454,7 +462,7 @@
lemma homotopic_paths:
"homotopic_paths S p q \<longleftrightarrow>
(\<exists>h. continuous_on ({0..1} \<times> {0..1}) h \<and>
- h ` ({0..1} \<times> {0..1}) \<subseteq> S \<and>
+ h \<in> ({0..1} \<times> {0..1}) \<rightarrow> S \<and>
(\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
(\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
(\<forall>t \<in> {0..1::real}. pathstart(h \<circ> Pair t) = pathstart p \<and>
@@ -500,7 +508,7 @@
assumes "path p"
and pips: "path_image p \<subseteq> S"
and contf: "continuous_on {0..1} f"
- and f01:"f ` {0..1} \<subseteq> {0..1}"
+ and f01 :"f \<in> {0..1} \<rightarrow> {0..1}"
and [simp]: "f(0) = 0" "f(1) = 1"
and q: "\<And>t. t \<in> {0..1} \<Longrightarrow> q(t) = p(f t)"
shows "homotopic_paths S p q"
@@ -508,15 +516,15 @@
have contp: "continuous_on {0..1} p"
by (metis \<open>path p\<close> path_def)
then have "continuous_on {0..1} (p \<circ> f)"
- using contf continuous_on_compose continuous_on_subset f01 by blast
+ by (meson assms(4) contf continuous_on_compose continuous_on_subset image_subset_iff_funcset)
then have "path q"
by (simp add: path_def) (metis q continuous_on_cong)
have piqs: "path_image q \<subseteq> S"
- by (metis (no_types, opaque_lifting) pips f01 image_subset_iff path_image_def q)
+ by (smt (verit, ccfv_threshold) Pi_iff assms(2) assms(4) assms(7) image_subset_iff path_defs(4))
have fb0: "\<And>a b. \<lbrakk>0 \<le> a; a \<le> 1; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> (1 - a) * f b + a * b"
using f01 by force
have fb1: "\<lbrakk>0 \<le> a; a \<le> 1; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> (1 - a) * f b + a * b \<le> 1" for a b
- using f01 [THEN subsetD, of "f b"] by (simp add: convex_bound_le)
+ by (intro convex_bound_le) (use f01 in auto)
have "homotopic_paths S q p"
proof (rule homotopic_paths_trans)
show "homotopic_paths S q (p \<circ> f)"
@@ -585,9 +593,9 @@
done
proposition homotopic_paths_continuous_image:
- "\<lbrakk>homotopic_paths S f g; continuous_on S h; h ` S \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t (h \<circ> f) (h \<circ> g)"
+ "\<lbrakk>homotopic_paths S f g; continuous_on S h; h \<in> S \<rightarrow> t\<rbrakk> \<Longrightarrow> homotopic_paths t (h \<circ> f) (h \<circ> g)"
unfolding homotopic_paths_def
- by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose)
+ by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose image_subset_iff_funcset)
subsection\<open>Group properties for homotopy of paths\<close>
@@ -711,9 +719,9 @@
by (auto intro: homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]])
proposition homotopic_loops_continuous_image:
- "\<lbrakk>homotopic_loops S f g; continuous_on S h; h ` S \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t (h \<circ> f) (h \<circ> g)"
+ "\<lbrakk>homotopic_loops S f g; continuous_on S h; h \<in> S \<rightarrow> t\<rbrakk> \<Longrightarrow> homotopic_loops t (h \<circ> f) (h \<circ> g)"
unfolding homotopic_loops_def
- by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def)
+ by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def image_subset_iff_funcset)
subsection\<open>Relations between the two variants of homotopy\<close>
@@ -731,11 +739,11 @@
have pip: "path_image p \<subseteq> S" by (metis assms homotopic_loops_imp_subset)
let ?A = "{0..1::real} \<times> {0..1::real}"
obtain h where conth: "continuous_on ?A h"
- and hs: "h ` ?A \<subseteq> S"
+ and hs: "h \<in> ?A \<rightarrow> S"
and h0[simp]: "\<And>x. x \<in> {0..1} \<Longrightarrow> h(0,x) = p x"
and h1[simp]: "\<And>x. x \<in> {0..1} \<Longrightarrow> h(1,x) = a"
and ends: "\<And>t. t \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair t) = pathstart (h \<circ> Pair t)"
- using assms by (auto simp: homotopic_loops homotopic_with)
+ using assms by (auto simp: homotopic_loops homotopic_with image_subset_iff_funcset)
have conth0: "path (\<lambda>u. h (u, 0))"
unfolding path_def
proof (rule continuous_on_compose [of _ _ h, unfolded o_def])
@@ -783,12 +791,13 @@
+++ subpath (fst y) 0 (\<lambda>u. h (u, 0))) (snd y)"
have "continuous_on ?A ?h"
by (intro continuous_on_homotopic_join_lemma; simp add: path_defs joinpaths_def subpath_def conth c1 c2)
- moreover have "?h ` ?A \<subseteq> S"
+ moreover have "?h \<in> ?A \<rightarrow> S"
+ using hs
unfolding joinpaths_def subpath_def
- by (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] adhoc_le)
+ by (force simp: algebra_simps mult_le_one mult_left_le intro: adhoc_le)
ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))
(top_of_set S) ?h"
- by (simp add: subpath_reversepath)
+ by (simp add: subpath_reversepath image_subset_iff_funcset)
qed (use ploop in \<open>simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2\<close>)
moreover have "homotopic_paths S ((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>u. h (u, 0)))
(linepath (pathstart p) (pathstart p))"
@@ -999,7 +1008,7 @@
show "continuous_on {0..1} ?f"
unfolding split_01
by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def dest!: t2)+
- show "?f ` {0..1} \<subseteq> {0..1}"
+ show "?f \<in> {0..1} \<rightarrow> {0..1}"
using False assms
by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2)
show "(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)" if "t \<in> {0..1}" for t
@@ -1057,12 +1066,12 @@
assumes "path_component S a b"
shows "homotopic_loops S (linepath a a) (linepath b b)"
proof -
- obtain g :: "real \<Rightarrow> 'a" where g: "continuous_on {0..1} g" "g ` {0..1} \<subseteq> S" "g 0 = a" "g 1 = b"
+ obtain g :: "real \<Rightarrow> 'a" where g: "continuous_on {0..1} g" "g \<in> {0..1} \<rightarrow> S" "g 0 = a" "g 1 = b"
using assms by (auto simp: path_defs)
then have "continuous_on ({0..1} \<times> {0..1}) (g \<circ> fst)"
by (fastforce intro!: continuous_intros)+
with g show ?thesis
- by (auto simp: homotopic_loops_def homotopic_with_def path_defs image_subset_iff)
+ by (auto simp: homotopic_loops_def homotopic_with_def path_defs Pi_iff)
qed
lemma homotopic_loops_imp_path_component_value:
@@ -1289,39 +1298,39 @@
lemma nullhomotopic_through_contractible:
fixes S :: "_::topological_space set"
- assumes f: "continuous_on S f" "f ` S \<subseteq> T"
- and g: "continuous_on T g" "g ` T \<subseteq> U"
+ assumes f: "continuous_on S f" "f \<in> S \<rightarrow> T"
+ and g: "continuous_on T g" "g \<in> T \<rightarrow> U"
and T: "contractible T"
obtains c where "homotopic_with_canon (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
proof -
obtain b where b: "homotopic_with_canon (\<lambda>x. True) T T id (\<lambda>x. b)"
using assms by (force simp: contractible_def)
have "homotopic_with_canon (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
- by (metis Abstract_Topology.continuous_map_subtopology_eu b g homotopic_with_compose_continuous_map_left)
+ by (metis b continuous_map_subtopology_eu g homotopic_with_compose_continuous_map_left image_subset_iff_funcset)
then have "homotopic_with_canon (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
- by (simp add: f homotopic_with_compose_continuous_map_right)
+ by (simp add: f homotopic_with_compose_continuous_map_right image_subset_iff_funcset)
then show ?thesis
by (simp add: comp_def that)
qed
lemma nullhomotopic_into_contractible:
- assumes f: "continuous_on S f" "f ` S \<subseteq> T"
+ assumes f: "continuous_on S f" "f \<in> S \<rightarrow> T"
and T: "contractible T"
obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
by (rule nullhomotopic_through_contractible [OF f, of id T]) (use assms in auto)
lemma nullhomotopic_from_contractible:
- assumes f: "continuous_on S f" "f ` S \<subseteq> T"
+ assumes f: "continuous_on S f" "f \<in> S \<rightarrow> T"
and S: "contractible S"
obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
by (auto simp: comp_def intro: nullhomotopic_through_contractible [OF continuous_on_id _ f S])
lemma homotopic_through_contractible:
fixes S :: "_::real_normed_vector set"
- assumes "continuous_on S f1" "f1 ` S \<subseteq> T"
- "continuous_on T g1" "g1 ` T \<subseteq> U"
- "continuous_on S f2" "f2 ` S \<subseteq> T"
- "continuous_on T g2" "g2 ` T \<subseteq> U"
+ assumes "continuous_on S f1" "f1 \<in> S \<rightarrow> T"
+ "continuous_on T g1" "g1 \<in> T \<rightarrow> U"
+ "continuous_on S f2" "f2 \<in> S \<rightarrow> T"
+ "continuous_on T g2" "g2 \<in> T \<rightarrow> U"
"contractible T" "path_connected U"
shows "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
proof -
@@ -1346,8 +1355,8 @@
lemma homotopic_into_contractible:
fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
- assumes f: "continuous_on S f" "f ` S \<subseteq> T"
- and g: "continuous_on S g" "g ` S \<subseteq> T"
+ assumes f: "continuous_on S f" "f \<in> S \<rightarrow> T"
+ and g: "continuous_on S g" "g \<in> S \<rightarrow> T"
and T: "contractible T"
shows "homotopic_with_canon (\<lambda>h. True) S T f g"
using homotopic_through_contractible [of S f T id T g id]
@@ -1355,8 +1364,8 @@
lemma homotopic_from_contractible:
fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
- assumes f: "continuous_on S f" "f ` S \<subseteq> T"
- and g: "continuous_on S g" "g ` S \<subseteq> T"
+ assumes f: "continuous_on S f" "f \<in> S \<rightarrow> T"
+ and g: "continuous_on S g" "g \<in> S \<rightarrow> T"
and "contractible S" "path_connected T"
shows "homotopic_with_canon (\<lambda>h. True) S T f g"
using homotopic_through_contractible [of S id S f T id g]
@@ -1478,15 +1487,15 @@
shows "contractible (S \<times> T)"
proof -
obtain a h where conth: "continuous_on ({0..1} \<times> S) h"
- and hsub: "h ` ({0..1} \<times> S) \<subseteq> S"
+ and hsub: "h \<in> ({0..1} \<times> S) \<rightarrow> S"
and [simp]: "\<And>x. x \<in> S \<Longrightarrow> h (0, x) = x"
and [simp]: "\<And>x. x \<in> S \<Longrightarrow> h (1::real, x) = a"
- using S by (auto simp: contractible_def homotopic_with)
+ using S by (force simp: contractible_def homotopic_with)
obtain b k where contk: "continuous_on ({0..1} \<times> T) k"
- and ksub: "k ` ({0..1} \<times> T) \<subseteq> T"
+ and ksub: "k \<in> ({0..1} \<times> T) \<rightarrow> T"
and [simp]: "\<And>x. x \<in> T \<Longrightarrow> k (0, x) = x"
and [simp]: "\<And>x. x \<in> T \<Longrightarrow> k (1::real, x) = b"
- using T by (auto simp: contractible_def homotopic_with)
+ using T by (force simp: contractible_def homotopic_with)
show ?thesis
apply (simp add: contractible_def homotopic_with)
apply (rule exI [where x=a])
@@ -3210,7 +3219,7 @@
by (rule hom)
then have "homotopic_with_canon Q U t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
- using Q by (auto simp: conth imh)
+ using Q conth imh by force+
then show ?thesis
proof (rule homotopic_with_eq; simp)
show "\<And>h k. (\<And>x. x \<in> U \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
@@ -3240,7 +3249,7 @@
by (metis hom)
then have "homotopic_with_canon Q U t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
- using Q by (auto simp: conth imh)
+ using Q conth imh by force+
then have "homotopic_with_canon Q U t f (\<lambda>x. h c)"
proof (rule homotopic_with_eq)
show "\<And>x. x \<in> topspace (top_of_set U) \<Longrightarrow> f x = (h \<circ> (k \<circ> f)) x"
@@ -3281,7 +3290,7 @@
by (rule hom)
then have "homotopic_with_canon Q t U (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
- using Q by (auto simp: contk imk)
+ using Q contk imk by force+
then show ?thesis
proof (rule homotopic_with_eq)
show "f x = (f \<circ> h \<circ> k) x" "g x = (g \<circ> h \<circ> k) x"
@@ -3312,7 +3321,7 @@
proof (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
show "\<And>h. \<lbrakk>continuous_map (top_of_set S) (top_of_set U) h; P h\<rbrakk> \<Longrightarrow> Q (h \<circ> k)"
using Q by auto
- qed (auto simp: contk imk)
+ qed (use contk imk in force)+
moreover have "homotopic_with_canon Q t U f (\<lambda>x. c)"
using homotopic_with_eq [OF \<section>] feq Qeq by fastforce
ultimately show ?thesis
@@ -3789,15 +3798,10 @@
(infix "homotopy'_eqv" 50)
where "S homotopy_eqv T \<equiv> top_of_set S homotopy_equivalent_space top_of_set T"
-
-
-
-
lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
unfolding homeomorphic_def homeomorphism_def homotopy_equivalent_space_def
by (metis continuous_map_subtopology_eu homotopic_with_id2 openin_imp_subset openin_subtopology_self topspace_euclidean_subtopology)
-
lemma homotopy_eqv_inj_linear_image:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "linear f" "inj f"
@@ -3814,25 +3818,25 @@
and T :: "'b::real_normed_vector set"
and U :: "'c::real_normed_vector set"
assumes "S homotopy_eqv T"
- and f: "continuous_on U f" "f ` U \<subseteq> T"
- and g: "continuous_on U g" "g ` U \<subseteq> T"
- and homUS: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
- continuous_on U g; g ` U \<subseteq> S\<rbrakk>
+ and f: "continuous_on U f" "f \<in> U \<rightarrow> T"
+ and g: "continuous_on U g" "g \<in> U \<rightarrow> T"
+ and homUS: "\<And>f g. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S;
+ continuous_on U g; g \<in> U \<rightarrow> S\<rbrakk>
\<Longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g"
shows "homotopic_with_canon (\<lambda>x. True) U T f g"
proof -
- obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
- and k: "continuous_on T k" "k ` T \<subseteq> S"
+ obtain h k where h: "continuous_on S h" "h \<in> S \<rightarrow> T"
+ and k: "continuous_on T k" "k \<in> T \<rightarrow> S"
and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
"homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
- using assms by (auto simp: homotopy_equivalent_space_def)
+ using assms by (force simp: homotopy_equivalent_space_def image_subset_iff_funcset)
have "homotopic_with_canon (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
proof (rule homUS)
show "continuous_on U (k \<circ> f)" "continuous_on U (k \<circ> g)"
- using continuous_on_compose continuous_on_subset f g k by blast+
+ using continuous_on_compose continuous_on_subset f g k by (metis funcset_image)+
qed (use f g k in \<open>(force simp: o_def)+\<close> )
then have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
- by (rule homotopic_with_compose_continuous_left; simp add: h)
+ by (simp add: h homotopic_with_compose_continuous_map_left image_subset_iff_funcset)
moreover have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
by (rule homotopic_with_compose_continuous_right [where X=T and Y=T]; simp add: hom f)
moreover have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
@@ -3847,11 +3851,11 @@
and T :: "'b::real_normed_vector set"
and U :: "'c::real_normed_vector set"
assumes "S homotopy_eqv T"
- shows "(\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> S \<and>
- continuous_on U g \<and> g ` U \<subseteq> S
+ shows "(\<forall>f g. continuous_on U f \<and> f \<in> U \<rightarrow> S \<and>
+ continuous_on U g \<and> g \<in> U \<rightarrow> S
\<longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g) \<longleftrightarrow>
- (\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> T \<and>
- continuous_on U g \<and> g ` U \<subseteq> T
+ (\<forall>f g. continuous_on U f \<and> f \<in> U \<rightarrow> T \<and>
+ continuous_on U g \<and> g \<in> U \<rightarrow> T
\<longrightarrow> homotopic_with_canon (\<lambda>x. True) U T f g)"
(is "?lhs = ?rhs")
proof
@@ -3873,20 +3877,20 @@
and T :: "'b::real_normed_vector set"
and U :: "'c::real_normed_vector set"
assumes "S homotopy_eqv T"
- and f: "continuous_on T f" "f ` T \<subseteq> U"
- and homSU: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U\<rbrakk>
+ and f: "continuous_on T f" "f \<in> T \<rightarrow> U"
+ and homSU: "\<And>f. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> U\<rbrakk>
\<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) S U f (\<lambda>x. c)"
obtains c where "homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. c)"
proof -
- obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
- and k: "continuous_on T k" "k ` T \<subseteq> S"
+ obtain h k where h: "continuous_on S h" "h \<in> S \<rightarrow> T"
+ and k: "continuous_on T k" "k \<in> T \<rightarrow> S"
and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
"homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
- using assms by (auto simp: homotopy_equivalent_space_def)
+ using assms by (force simp: homotopy_equivalent_space_def image_subset_iff_funcset)
obtain c where "homotopic_with_canon (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
proof (rule exE [OF homSU])
show "continuous_on S (f \<circ> h)"
- using continuous_on_compose continuous_on_subset f h by blast
+ by (metis continuous_on_compose continuous_on_subset f h funcset_image)
qed (use f h in force)
then have "homotopic_with_canon (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
by (rule homotopic_with_compose_continuous_right [where X=S]) (use k in auto)
@@ -3902,9 +3906,9 @@
and T :: "'b::real_normed_vector set"
and U :: "'c::real_normed_vector set"
assumes "S homotopy_eqv T"
- shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> U
+ shows "(\<forall>f. continuous_on S f \<and> f \<in> S \<rightarrow> U
\<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow>
- (\<forall>f. continuous_on T f \<and> f ` T \<subseteq> U
+ (\<forall>f. continuous_on T f \<and> f \<in> T \<rightarrow> U
\<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. c)))"
by (rule iffI; metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_equivalent_space_sym)
@@ -3914,20 +3918,20 @@
and T :: "'b::real_normed_vector set"
and U :: "'c::real_normed_vector set"
assumes "S homotopy_eqv T"
- and f: "continuous_on U f" "f ` U \<subseteq> T"
- and homSU: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
+ and f: "continuous_on U f" "f \<in> U \<rightarrow> T"
+ and homSU: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S\<rbrakk>
\<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c)"
shows "\<exists>c. homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)"
proof -
- obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
- and k: "continuous_on T k" "k ` T \<subseteq> S"
+ obtain h k where h: "continuous_on S h" "h \<in> S \<rightarrow> T"
+ and k: "continuous_on T k" "k \<in> T \<rightarrow> S"
and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
"homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
- using assms by (auto simp: homotopy_equivalent_space_def)
+ using assms by (force simp: homotopy_equivalent_space_def image_subset_iff_funcset)
obtain c::'a where "homotopic_with_canon (\<lambda>x. True) U S (k \<circ> f) (\<lambda>x. c)"
proof (rule exE [OF homSU [of "k \<circ> f"]])
show "continuous_on U (k \<circ> f)"
- using continuous_on_compose continuous_on_subset f k by blast
+ using continuous_on_compose continuous_on_subset f k by (metis funcset_image)
qed (use f k in force)
then have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
by (rule homotopic_with_compose_continuous_left [where Y=S]) (use h in auto)
@@ -3943,9 +3947,9 @@
and T :: "'b::real_normed_vector set"
and U :: "'c::real_normed_vector set"
assumes "S homotopy_eqv T"
- shows "(\<forall>f. continuous_on U f \<and> f ` U \<subseteq> S
+ shows "(\<forall>f. continuous_on U f \<and> f \<in> U \<rightarrow> S
\<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c))) \<longleftrightarrow>
- (\<forall>f. continuous_on U f \<and> f ` U \<subseteq> T
+ (\<forall>f. continuous_on U f \<and> f \<in> U \<rightarrow> T
\<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)))"
by (rule iffI; metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_equivalent_space_sym)
--- a/src/HOL/Analysis/Lindelof_Spaces.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy Mon Jul 03 16:46:37 2023 +0100
@@ -253,7 +253,7 @@
show "x \<in> \<Union> (\<Union> (\<V> ` I))" if "x \<in> topspace X" for x
proof -
have "f x \<in> topspace Y"
- by (meson f image_subset_iff proper_map_imp_subset_topspace that)
+ using f proper_map_imp_subset_topspace that by fastforce
then show ?thesis
using that I by auto
qed
--- a/src/HOL/Analysis/Lipschitz.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Mon Jul 03 16:46:37 2023 +0100
@@ -125,8 +125,8 @@
proof
show "?lhs \<Longrightarrow> ?rhs"
by (force simp add: Lipschitz_continuous_map_pos lipschitz_on_def less_le_not_le)
- show "?rhs \<Longrightarrow> ?lhs"
- by (metis Lipschitz_continuous_map_def lipschitz_onD mdist_euclidean_metric mspace_euclidean_metric top_greatest)
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (auto simp: Lipschitz_continuous_map_def lipschitz_on_def)
qed
subsubsection \<open>Continuity\<close>
--- a/src/HOL/Analysis/Path_Connected.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Mon Jul 03 16:46:37 2023 +0100
@@ -1484,7 +1484,7 @@
lemma path_connectedin_iff_path_connected_real [simp]:
"path_connectedin euclideanreal S \<longleftrightarrow> path_connected S"
- by (simp add: path_connectedin path_connected_def path_defs)
+ by (simp add: path_connectedin path_connected_def path_defs image_subset_iff_funcset)
lemma path_connected_component: "path_connected S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. path_component S x y)"
unfolding path_connected_def path_component_def by auto
@@ -1929,12 +1929,12 @@
definition path_components_of :: "'a topology \<Rightarrow> 'a set set"
where "path_components_of X \<equiv> path_component_of_set X ` topspace X"
-lemma pathin_canon_iff: "pathin (top_of_set T) g \<longleftrightarrow> path g \<and> g ` {0..1} \<subseteq> T"
- by (simp add: path_def pathin_def)
+lemma pathin_canon_iff: "pathin (top_of_set T) g \<longleftrightarrow> path g \<and> g \<in> {0..1} \<rightarrow> T"
+ by (simp add: path_def pathin_def image_subset_iff_funcset)
lemma path_component_of_canon_iff [simp]:
"path_component_of (top_of_set T) a b \<longleftrightarrow> path_component T a b"
- by (simp add: path_component_of_def pathin_canon_iff path_defs)
+ by (simp add: path_component_of_def pathin_canon_iff path_defs image_subset_iff_funcset)
lemma path_component_in_topspace:
"path_component_of X x y \<Longrightarrow> x \<in> topspace X \<and> y \<in> topspace X"
--- a/src/HOL/Analysis/Retracts.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Retracts.thy Mon Jul 03 16:46:37 2023 +0100
@@ -100,7 +100,7 @@
proof (simp add: retraction_def retract_of_def, intro exI conjI)
show "continuous_on U (g \<circ> h')"
by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1)
- show "(g \<circ> h') ` U \<subseteq> S'"
+ show "(g \<circ> h') \<in> U \<rightarrow> S'"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>S'. (g \<circ> h') x = x"
by clarsimp (metis h'h hom homeomorphism_def)
@@ -136,7 +136,7 @@
proof (simp add: retraction_def retract_of_def, intro exI conjI)
show "continuous_on U (g \<circ> h')"
by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1)
- show "(g \<circ> h') ` U \<subseteq> T"
+ show "(g \<circ> h') \<in> U \<rightarrow> T"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>T. (g \<circ> h') x = x"
by clarsimp (metis h'h hom homeomorphism_def)
@@ -173,11 +173,11 @@
lemma ANR_imp_absolute_neighbourhood_extensor:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes "ANR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
+ assumes "ANR S" and contf: "continuous_on T f" and "f \<in> T \<rightarrow> S"
and cloUT: "closedin (top_of_set U) T"
obtains V g where "T \<subseteq> V" "openin (top_of_set U) V"
"continuous_on V g"
- "g ` V \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
+ "g \<in> V \<rightarrow> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
proof -
have "aff_dim S < int (DIM('b \<times> real))"
using aff_dim_le_DIM [of S] by simp
@@ -194,7 +194,7 @@
obtain g h where homgh: "homeomorphism S S' g h"
using hom by (force simp: homeomorphic_def)
have "continuous_on (f ` T) g"
- by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def homgh)
+ by (metis PiE assms(3) continuous_on_subset homeomorphism_cont1 homgh image_subset_iff)
then have contgf: "continuous_on T (g \<circ> f)"
by (intro continuous_on_compose contf)
have gfTC: "(g \<circ> f) ` T \<subseteq> C"
@@ -202,7 +202,7 @@
have "g ` S = S'"
by (metis (no_types) homeomorphism_def homgh)
then show ?thesis
- by (metis (no_types) assms(3) cloCS closedin_def image_comp image_mono order.trans topspace_euclidean_subtopology)
+ by (metis PiE assms(3) cloCS closedin_def image_comp image_mono image_subset_iff order.trans topspace_euclidean_subtopology)
qed
obtain f' where contf': "continuous_on U f'"
and "f' ` U \<subseteq> C"
@@ -211,10 +211,10 @@
show ?thesis
proof (rule_tac V = "U \<inter> f' -` D" and g = "h \<circ> r \<circ> f'" in that)
show "T \<subseteq> U \<inter> f' -` D"
- using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
+ using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f \<in> T \<rightarrow> S\<close> eq homeomorphism_image1 homgh
by fastforce
show ope: "openin (top_of_set U) (U \<inter> f' -` D)"
- using \<open>f' ` U \<subseteq> C\<close> by (auto simp: opD contf' continuous_openin_preimage)
+ by (meson \<open>f' ` U \<subseteq> C\<close> contf' continuous_openin_preimage image_subset_iff_funcset opD)
have conth: "continuous_on (r ` f' ` (U \<inter> f' -` D)) h"
proof (rule continuous_on_subset [of S'])
show "continuous_on S' h"
@@ -222,12 +222,12 @@
qed (use \<open>r ` D \<subseteq> S'\<close> in blast)
show "continuous_on (U \<inter> f' -` D) (h \<circ> r \<circ> f')"
by (blast intro: continuous_on_compose conth continuous_on_subset [OF contr] continuous_on_subset [OF contf'])
- show "(h \<circ> r \<circ> f') ` (U \<inter> f' -` D) \<subseteq> S"
+ show "(h \<circ> r \<circ> f') \<in> (U \<inter> f' -` D) \<rightarrow> S"
using \<open>homeomorphism S S' g h\<close> \<open>f' ` U \<subseteq> C\<close> \<open>r ` D \<subseteq> S'\<close>
by (auto simp: homeomorphism_def)
show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
- using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> eq
- by (auto simp: rid homeomorphism_def)
+ using \<open>homeomorphism S S' g h\<close> \<open>f \<in> T \<rightarrow> S\<close> eq
+ by (metis PiE comp_apply homeomorphism_def image_iff rid)
qed
qed
@@ -240,7 +240,7 @@
proof -
obtain g h where hom: "homeomorphism S S' g h"
using assms by (force simp: homeomorphic_def)
- obtain h: "continuous_on S' h" " h ` S' \<subseteq> S"
+ obtain h: "continuous_on S' h" " h \<in> S' \<rightarrow> S"
using hom homeomorphism_def by blast
from ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo]
obtain V h' where "S' \<subseteq> V" and opUV: "openin (top_of_set U) V"
@@ -251,7 +251,7 @@
proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>S' \<subseteq> V\<close>)
show "continuous_on V (g \<circ> h')"
by (meson continuous_on_compose continuous_on_subset h'(1) h'(2) hom homeomorphism_cont1)
- show "(g \<circ> h') ` V \<subseteq> S'"
+ show "(g \<circ> h') \<in> V \<rightarrow> S'"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>S'. (g \<circ> h') x = x"
by clarsimp (metis h'h hom homeomorphism_def)
@@ -269,29 +269,29 @@
corollary neighbourhood_extension_into_ANR:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T" and "ANR T" "closed S"
+ assumes contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> T" and "ANR T" "closed S"
obtains V g where "S \<subseteq> V" "open V" "continuous_on V g"
- "g ` V \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ "g \<in> V \<rightarrow> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf fim]
by (metis \<open>closed S\<close> closed_closedin open_openin subtopology_UNIV)
lemma absolute_neighbourhood_extensor_imp_ANR:
fixes S :: "'a::euclidean_space set"
assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
- \<And>U T. \<lbrakk>continuous_on T f; f ` T \<subseteq> S;
+ \<And>U T. \<lbrakk>continuous_on T f; f \<in> T \<rightarrow> S;
closedin (top_of_set U) T\<rbrakk>
\<Longrightarrow> \<exists>V g. T \<subseteq> V \<and> openin (top_of_set U) V \<and>
- continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)"
+ continuous_on V g \<and> g \<in> V \<rightarrow> S \<and> (\<forall>x \<in> T. g x = f x)"
shows "ANR S"
proof (clarsimp simp: ANR_def)
fix U and T :: "('a * real) set"
assume "S homeomorphic T" and clo: "closedin (top_of_set U) T"
then obtain g h where hom: "homeomorphism S T g h"
by (force simp: homeomorphic_def)
- obtain h: "continuous_on T h" " h ` T \<subseteq> S"
+ obtain h: "continuous_on T h" " h \<in> T \<rightarrow> S"
using hom homeomorphism_def by blast
obtain V h' where "T \<subseteq> V" and opV: "openin (top_of_set U) V"
- and h': "continuous_on V h'" "h' ` V \<subseteq> S"
+ and h': "continuous_on V h'" "h' \<in> V \<rightarrow> S"
and h'h: "\<forall>x\<in>T. h' x = h x"
using assms [OF h clo] by blast
have [simp]: "T \<subseteq> U"
@@ -299,9 +299,9 @@
have "T retract_of V"
proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>T \<subseteq> V\<close>)
show "continuous_on V (g \<circ> h')"
- by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1)
- show "(g \<circ> h') ` V \<subseteq> T"
- using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
+ by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_def image_subset_iff_funcset)
+ show "(g \<circ> h') \<in> V \<rightarrow> T"
+ using h' hom homeomorphism_image1 by fastforce
show "\<forall>x\<in>T. (g \<circ> h') x = x"
by clarsimp (metis h'h hom homeomorphism_def)
qed
@@ -313,10 +313,10 @@
fixes S :: "'a::euclidean_space set"
shows "ANR S \<longleftrightarrow>
(\<forall>f :: 'a * real \<Rightarrow> 'a.
- \<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
+ \<forall>U T. continuous_on T f \<longrightarrow> f \<in> T \<rightarrow> S \<longrightarrow>
closedin (top_of_set U) T \<longrightarrow>
(\<exists>V g. T \<subseteq> V \<and> openin (top_of_set U) V \<and>
- continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)))" (is "_ = ?rhs")
+ continuous_on V g \<and> g \<in> V \<rightarrow> S \<and> (\<forall>x \<in> T. g x = f x)))" (is "_ = ?rhs")
proof
assume "ANR S" then show ?rhs
by (metis ANR_imp_absolute_neighbourhood_extensor)
@@ -431,7 +431,7 @@
by (metis \<open>retraction X S r\<close> image_mono image_subset_iff_subset_vimage inf_le2 retraction)
qed
qed
- show "(f \<circ> r \<circ> h) ` (W \<inter> h -` X) \<subseteq> S'"
+ show "(f \<circ> r \<circ> h) \<in> (W \<inter> h -` X) \<rightarrow> S'"
using \<open>retraction X S r\<close> hom
by (auto simp: retraction_def homeomorphism_def)
show "\<forall>x\<in>S'. (f \<circ> r \<circ> h) x = x"
@@ -529,15 +529,15 @@
by (auto simp: contractible_def homotopic_with_def)
then have "a \<in> S"
by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one)
- have "\<exists>g. continuous_on W g \<and> g ` W \<subseteq> S \<and> (\<forall>x\<in>T. g x = f x)"
- if f: "continuous_on T f" "f ` T \<subseteq> S"
+ have "\<exists>g. continuous_on W g \<and> g \<in> W \<rightarrow> S \<and> (\<forall>x\<in>T. g x = f x)"
+ if f: "continuous_on T f" "f \<in> T \<rightarrow> S"
and WT: "closedin (top_of_set W) T"
for W T and f :: "'a \<times> real \<Rightarrow> 'a"
proof -
obtain U g
where "T \<subseteq> U" and WU: "openin (top_of_set W) U"
and contg: "continuous_on U g"
- and "g ` U \<subseteq> S" and gf: "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
+ and "g \<in> U \<rightarrow> S" and gf: "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor \<open>ANR S\<close>, rule_format, OF f WT]
by auto
have WWU: "closedin (top_of_set W) (W - U)"
@@ -570,7 +570,7 @@
show "continuous_on (W - V') g"
by (metis Diff_subset_conv \<open>W - U \<subseteq> V'\<close> contg continuous_on_subset Un_commute)
show "(\<lambda>x. (j x, g x)) ` (W - V') \<subseteq> {0..1} \<times> S"
- using j \<open>g ` U \<subseteq> S\<close> \<open>W - U \<subseteq> V'\<close> by fastforce
+ using j \<open>g \<in> U \<rightarrow> S\<close> \<open>W - U \<subseteq> V'\<close> by fastforce
qed
show "continuous_on W (\<lambda>x. if x \<in> W - V then a else h (j x, g x))"
proof (subst Weq, rule continuous_on_cases_local)
@@ -583,12 +583,12 @@
have "j(x, y) \<in> {0..1}"
using j that by blast
moreover have "g(x, y) \<in> S"
- using \<open>V' \<inter> V = {}\<close> \<open>W - U \<subseteq> V'\<close> \<open>g ` U \<subseteq> S\<close> that by fastforce
+ using \<open>V' \<inter> V = {}\<close> \<open>W - U \<subseteq> V'\<close> \<open>g \<in> U \<rightarrow> S\<close> that by fastforce
ultimately show ?thesis
using hS by blast
qed
- with \<open>a \<in> S\<close> \<open>g ` U \<subseteq> S\<close>
- show "(\<lambda>x. if x \<in> W - V then a else h (j x, g x)) ` W \<subseteq> S"
+ with \<open>a \<in> S\<close> \<open>g \<in> U \<rightarrow> S\<close>
+ show "(\<lambda>x. if x \<in> W - V then a else h (j x, g x)) \<in> W \<rightarrow> S"
by auto
next
show "\<forall>x\<in>T. (if x \<in> W - V then a else h (j x, g x)) = f x"
@@ -596,7 +596,7 @@
qed
qed
then show ?lhs
- by (simp add: AR_eq_absolute_extensor)
+ by (simp add: AR_eq_absolute_extensor image_subset_iff_funcset)
qed
@@ -606,17 +606,17 @@
shows "ANR S"
proof (clarsimp simp add: ANR_eq_absolute_neighbourhood_extensor)
fix f::"'a \<times> real \<Rightarrow> 'a" and U W
- assume W: "continuous_on W f" "f ` W \<subseteq> S" "closedin (top_of_set U) W"
- then obtain r where "S \<subseteq> T" and r: "continuous_on T r" "r ` T \<subseteq> S" "\<forall>x\<in>S. r x = x" "continuous_on W f" "f ` W \<subseteq> S"
+ assume W: "continuous_on W f" "f \<in> W \<rightarrow> S" "closedin (top_of_set U) W"
+ then obtain r where "S \<subseteq> T" and r: "continuous_on T r" "r \<in> T \<rightarrow> S" "\<forall>x\<in>S. r x = x" "continuous_on W f" "f \<in> W \<rightarrow> S"
"closedin (top_of_set U) W"
- by (meson ST retract_of_def retraction_def)
+ by (metis ST retract_of_def retraction_def)
then have "f ` W \<subseteq> T"
by blast
- with W obtain V g where V: "W \<subseteq> V" "openin (top_of_set U) V" "continuous_on V g" "g ` V \<subseteq> T" "\<forall>x\<in>W. g x = f x"
- by (metis ANR_imp_absolute_neighbourhood_extensor \<open>ANR T\<close>)
- with r have "continuous_on V (r \<circ> g) \<and> (r \<circ> g) ` V \<subseteq> S \<and> (\<forall>x\<in>W. (r \<circ> g) x = f x)"
- by (metis (no_types, lifting) comp_apply continuous_on_compose continuous_on_subset image_subset_iff)
- then show "\<exists>V. W \<subseteq> V \<and> openin (top_of_set U) V \<and> (\<exists>g. continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x\<in>W. g x = f x))"
+ with W obtain V g where V: "W \<subseteq> V" "openin (top_of_set U) V" "continuous_on V g" "g \<in> V \<rightarrow> T" "\<forall>x\<in>W. g x = f x"
+ by (smt (verit) ANR_imp_absolute_neighbourhood_extensor Pi_I assms(1) funcset_mem image_subset_iff_funcset)
+ with r have "continuous_on V (r \<circ> g) \<and> (r \<circ> g) \<in> V \<rightarrow> S \<and> (\<forall>x\<in>W. (r \<circ> g) x = f x)"
+ by (smt (verit, del_insts) Pi_iff comp_apply continuous_on_compose continuous_on_subset image_subset_iff_funcset)
+ then show "\<exists>V. W \<subseteq> V \<and> openin (top_of_set U) V \<and> (\<exists>g. continuous_on V g \<and> g \<in> V \<rightarrow> S \<and> (\<forall>x\<in>W. g x = f x))"
by (meson V)
qed
@@ -775,7 +775,8 @@
show ?thesis
apply (simp add: retract_of_def retraction_def \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close>)
apply (rule_tac x="\<lambda>x. if x \<in> S' then g x else h x" in exI)
- using ST UST \<open>S \<subseteq> S'\<close> \<open>S' \<inter> T' = W\<close> \<open>T \<subseteq> T'\<close> cont geqr heqr r_def by auto
+ using ST UST \<open>S \<subseteq> S'\<close> \<open>S' \<inter> T' = W\<close> \<open>T \<subseteq> T'\<close> cont geqr heqr r_def
+ by (smt (verit, del_insts) IntI Pi_I Un_iff image_subset_iff r0 subsetD)
qed
@@ -883,14 +884,14 @@
have "W0 \<subseteq> U"
using \<open>W \<subseteq> U\<close> cloWW0 closedin_subset by fastforce
obtain r0
- where "S \<inter> T \<subseteq> W0" and contr0: "continuous_on W0 r0" and "r0 ` W0 \<subseteq> S \<inter> T"
+ where "S \<inter> T \<subseteq> W0" and contr0: "continuous_on W0 r0" and "r0 \<in> W0 \<rightarrow> S \<inter> T"
and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
using ret by (force simp: retract_of_def retraction_def)
have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin)
define r where "r \<equiv> \<lambda>x. if x \<in> W0 then r0 x else x"
have "r ` (W0 \<union> S) \<subseteq> S" "r ` (W0 \<union> T) \<subseteq> T"
- using \<open>r0 ` W0 \<subseteq> S \<inter> T\<close> r_def by auto
+ using \<open>r0 \<in> W0 \<rightarrow> S \<inter> T\<close> r_def by auto
have contr: "continuous_on (W0 \<union> (S \<union> T)) r"
unfolding r_def
proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
@@ -907,21 +908,21 @@
closedin_Un closedin_imp_subset closedin_trans)
obtain W1 g where "W0 \<union> S \<subseteq> W1" and contg: "continuous_on W1 g"
and opeSW1: "openin (top_of_set S') W1"
- and "g ` W1 \<subseteq> S" and geqr: "\<And>x. x \<in> W0 \<union> S \<Longrightarrow> g x = r x"
- proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> _ \<open>r ` (W0 \<union> S) \<subseteq> S\<close> cloS'WS])
+ and "g \<in> W1 \<rightarrow> S" and geqr: "\<And>x. x \<in> W0 \<union> S \<Longrightarrow> g x = r x"
+ proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> _ _ cloS'WS])
show "continuous_on (W0 \<union> S) r"
using continuous_on_subset contr sup_assoc by blast
- qed auto
+ qed (use \<open>r ` (W0 \<union> S) \<subseteq> S\<close> in auto)
have cloT'WT: "closedin (top_of_set T') (W0 \<union> T)"
by (meson closedin_subset_trans UT cloUT' \<open>T \<subseteq> T'\<close> \<open>W \<subseteq> T'\<close> cloUW cloWW0
closedin_Un closedin_imp_subset closedin_trans)
obtain W2 h where "W0 \<union> T \<subseteq> W2" and conth: "continuous_on W2 h"
and opeSW2: "openin (top_of_set T') W2"
and "h ` W2 \<subseteq> T" and heqr: "\<And>x. x \<in> W0 \<union> T \<Longrightarrow> h x = r x"
- proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> _ \<open>r ` (W0 \<union> T) \<subseteq> T\<close> cloT'WT])
+ proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> _ _ cloT'WT])
show "continuous_on (W0 \<union> T) r"
using continuous_on_subset contr sup_assoc by blast
- qed auto
+ qed (use \<open>r ` (W0 \<union> T) \<subseteq> T\<close> in auto)
have "S' \<inter> T' = W"
by (force simp: S'_def T'_def W_def)
obtain O1 O2 where O12: "open O1" "W1 = S' \<inter> O1" "open O2" "W2 = T' \<inter> O2"
@@ -961,12 +962,12 @@
using continuous_on_cases_local [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]]
by simp
show "?gh ` (?WW1 \<union> ?WW2) \<subseteq> S \<union> T"
- using \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<inter> T' = W\<close> \<open>g ` W1 \<subseteq> S\<close> \<open>h ` W2 \<subseteq> T\<close> \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close>
+ using \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<inter> T' = W\<close> \<open>g \<in> W1 \<rightarrow> S\<close> \<open>h ` W2 \<subseteq> T\<close> \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close>
by (auto simp add: image_subset_iff)
qed
then show "S \<union> T retract_of ?WW1 \<union> ?WW2"
using \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close> ST opeUU0 U0
- by (auto simp: retract_of_def retraction_def)
+ by (auto simp: retract_of_def retraction_def image_subset_iff_funcset)
qed
qed
@@ -1025,17 +1026,17 @@
shows "ANR S"
proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
fix f :: "'a \<times> real \<Rightarrow> 'a" and U C
- assume contf: "continuous_on C f" and fim: "f ` C \<subseteq> S"
+ assume contf: "continuous_on C f" and fim: "f \<in> C \<rightarrow> S"
and cloUC: "closedin (top_of_set U) C"
- have "f ` C \<subseteq> T"
+ have "f \<in> C \<rightarrow> T"
using fim opeTS openin_imp_subset by blast
obtain W g where "C \<subseteq> W"
and UW: "openin (top_of_set U) W"
and contg: "continuous_on W g"
- and gim: "g ` W \<subseteq> T"
+ and gim: "g \<in> W \<rightarrow> T"
and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
- using ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf \<open>f ` C \<subseteq> T\<close> cloUC] fim by auto
- show "\<exists>V g. C \<subseteq> V \<and> openin (top_of_set U) V \<and> continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x\<in>C. g x = f x)"
+ using ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf \<open>f \<in> C \<rightarrow> T\<close> cloUC] fim by auto
+ show "\<exists>V g. C \<subseteq> V \<and> openin (top_of_set U) V \<and> continuous_on V g \<and> g \<in> V \<rightarrow> S \<and> (\<forall>x\<in>C. g x = f x)"
proof (intro exI conjI)
show "C \<subseteq> W \<inter> g -` S"
using \<open>C \<subseteq> W\<close> fim geq by blast
@@ -1043,7 +1044,7 @@
by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans)
show "continuous_on (W \<inter> g -` S) g"
by (blast intro: continuous_on_subset [OF contg])
- show "g ` (W \<inter> g -` S) \<subseteq> S"
+ show "g \<in> (W \<inter> g -` S) \<rightarrow> S"
using gim by blast
show "\<forall>x\<in>C. g x = f x"
using geq by blast
@@ -1217,7 +1218,7 @@
assumes "ANR S" "ANR T" shows "ANR(S \<times> T)"
proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
fix f :: " ('a \<times> 'b) \<times> real \<Rightarrow> 'a \<times> 'b" and U C
- assume "continuous_on C f" and fim: "f ` C \<subseteq> S \<times> T"
+ assume "continuous_on C f" and fim: "f \<in> C \<rightarrow> S \<times> T"
and cloUC: "closedin (top_of_set U) C"
have contf1: "continuous_on C (fst \<circ> f)"
by (simp add: \<open>continuous_on C f\<close> continuous_on_fst)
@@ -1227,23 +1228,23 @@
and gim: "g ` W1 \<subseteq> S"
and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = (fst \<circ> f) x"
proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> contf1 _ cloUC])
- show "(fst \<circ> f) ` C \<subseteq> S"
- using fim by auto
+ show "(fst \<circ> f) \<in> C \<rightarrow> S"
+ using fim by force
qed auto
have contf2: "continuous_on C (snd \<circ> f)"
by (simp add: \<open>continuous_on C f\<close> continuous_on_snd)
obtain W2 h where "C \<subseteq> W2"
and UW2: "openin (top_of_set U) W2"
and conth: "continuous_on W2 h"
- and him: "h ` W2 \<subseteq> T"
+ and him: "h \<in> W2 \<rightarrow> T"
and heq: "\<And>x. x \<in> C \<Longrightarrow> h x = (snd \<circ> f) x"
proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf2 _ cloUC])
- show "(snd \<circ> f) ` C \<subseteq> T"
- using fim by auto
+ show "(snd \<circ> f) \<in> C \<rightarrow> T"
+ using fim by force
qed auto
show "\<exists>V g. C \<subseteq> V \<and>
openin (top_of_set U) V \<and>
- continuous_on V g \<and> g ` V \<subseteq> S \<times> T \<and> (\<forall>x\<in>C. g x = f x)"
+ continuous_on V g \<and> g \<in> V \<rightarrow> S \<times> T \<and> (\<forall>x\<in>C. g x = f x)"
proof (intro exI conjI)
show "C \<subseteq> W1 \<inter> W2"
by (simp add: \<open>C \<subseteq> W1\<close> \<open>C \<subseteq> W2\<close>)
@@ -1251,7 +1252,7 @@
by (simp add: UW1 UW2 openin_Int)
show "continuous_on (W1 \<inter> W2) (\<lambda>x. (g x, h x))"
by (metis (no_types) contg conth continuous_on_Pair continuous_on_subset inf_commute inf_le1)
- show "(\<lambda>x. (g x, h x)) ` (W1 \<inter> W2) \<subseteq> S \<times> T"
+ show "(\<lambda>x. (g x, h x)) \<in> (W1 \<inter> W2) \<rightarrow> S \<times> T"
using gim him by blast
show "(\<forall>x\<in>C. (g x, h x) = f x)"
using geq heq by auto
@@ -1710,7 +1711,7 @@
assumes cloTS: "closedin (top_of_set T) S"
and anr: "(ANR S \<and> ANR T) \<or> ANR U"
and contf: "continuous_on T f"
- and "f ` T \<subseteq> U"
+ and "f \<in> T \<rightarrow> U"
and "homotopic_with_canon (\<lambda>x. True) S U f g"
obtains g' where "homotopic_with_canon (\<lambda>x. True) T U f g'"
"continuous_on T g'" "image g' T \<subseteq> U"
@@ -1718,9 +1719,9 @@
proof -
have "S \<subseteq> T" using assms closedin_imp_subset by blast
obtain h where conth: "continuous_on ({0..1} \<times> S) h"
- and him: "h ` ({0..1} \<times> S) \<subseteq> U"
+ and him: "h \<in> ({0..1} \<times> S) \<rightarrow> U"
and [simp]: "\<And>x. h(0, x) = f x" "\<And>x. h(1::real, x) = g x"
- using assms by (auto simp: homotopic_with_def)
+ using assms by (fastforce simp: homotopic_with_def)
define h' where "h' \<equiv> \<lambda>z. if snd z \<in> S then h z else (f \<circ> snd) z"
define B where "B \<equiv> {0::real} \<times> T \<union> {0..1} \<times> S"
have clo0T: "closedin (top_of_set ({0..1} \<times> T)) ({0::real} \<times> T)"
@@ -1744,9 +1745,9 @@
then have conth': "continuous_on B h'"
by (simp add: h'_def B_def Un_commute [of "{0} \<times> T"])
have "image h' B \<subseteq> U"
- using \<open>f ` T \<subseteq> U\<close> him by (auto simp: h'_def B_def)
+ using \<open>f \<in> T \<rightarrow> U\<close> him by (auto simp: h'_def B_def)
obtain V k where "B \<subseteq> V" and opeTV: "openin (top_of_set ({0..1} \<times> T)) V"
- and contk: "continuous_on V k" and kim: "k ` V \<subseteq> U"
+ and contk: "continuous_on V k" and kim: "k \<in> V \<rightarrow> U"
and keq: "\<And>x. x \<in> B \<Longrightarrow> k x = h' x"
using anr
proof
@@ -1770,14 +1771,15 @@
moreover have "(h' \<circ> r) ` V \<subseteq> U"
by (metis \<open>h' ` B \<subseteq> U\<close> image_comp retractionE that(2))
ultimately show ?thesis
- using Vk [of V "h' \<circ> r"] by (metis comp_apply retraction that)
+ using Vk [of V "h' \<circ> r"] by (metis comp_apply retraction image_subset_iff_funcset that)
qed
show thesis
by (meson "*" ANR_imp_neighbourhood_retract \<open>ANR B\<close> clo0TB retract_of_def)
next
assume "ANR U"
- with ANR_imp_absolute_neighbourhood_extensor \<open>h' ` B \<subseteq> U\<close> clo0TB conth' that
- show ?thesis by blast
+ with ANR_imp_absolute_neighbourhood_extensor \<open>h' ` B \<subseteq> U\<close> clo0TB conth' image_subset_iff_funcset that
+ show ?thesis
+ by (smt (verit) Pi_I funcset_mem)
qed
define S' where "S' \<equiv> {x. \<exists>u::real. u \<in> {0..1} \<and> (u, x::'a) \<in> {0..1} \<times> T - V}"
have "closedin (top_of_set T) S'"
@@ -1827,7 +1829,7 @@
fix t
assume "t \<in> T"
show "k (a t, t) \<in> U"
- by (metis \<open>t \<in> T\<close> image_subset_iff inV kim not_one_le_zero linear mult_cancel_right1)
+ by (metis \<open>t \<in> T\<close> image_subset_iff inV kim not_one_le_zero linear mult_cancel_right1 image_subset_iff_funcset)
qed
show "\<And>x. x \<in> S \<Longrightarrow> k (a x, x) = g x"
by (simp add: B_def a1 h'_def keq)
@@ -1854,7 +1856,7 @@
then obtain g where "continuous_on UNIV g" "range g \<subseteq> T"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof (rule Borsuk_homotopy_extension_homotopic)
- show "range (\<lambda>x. c) \<subseteq> T"
+ show "(\<lambda>x. c) \<in> UNIV \<rightarrow> T"
using \<open>S \<noteq> {}\<close> c homotopic_with_imp_subset1 by fastforce
qed (use assms c in auto)
then show ?rhs by blast
@@ -1956,7 +1958,7 @@
by (metis convex_imp_contractible convex_ball)
show "continuous_on (ball 0 r) (\<lambda>x. inverse(norm (x - b)) *\<^sub>R (x - b))"
by (rule continuous_on_Borsuk_map [OF bnot])
- show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) ` ball 0 r \<subseteq> sphere 0 1"
+ show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) \<in> ball 0 r \<rightarrow> sphere 0 1"
using bnot Borsuk_map_into_sphere by blast
qed blast
ultimately have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. (x - a) /\<^sub>R norm (x - a)) (\<lambda>x. c)"
@@ -1979,9 +1981,10 @@
assume notcc: "\<not> connected_component (- S) a b"
let ?T = "S \<union> connected_component_set (- S) a"
have "\<nexists>g. continuous_on (S \<union> connected_component_set (- S) a) g \<and>
- g ` (S \<union> connected_component_set (- S) a) \<subseteq> sphere 0 1 \<and>
+ g \<in> (S \<union> connected_component_set (- S) a) \<rightarrow> sphere 0 1 \<and>
(\<forall>x\<in>S. g x = (x - a) /\<^sub>R norm (x - a))"
- by (simp add: \<open>a \<notin> S\<close> componentsI non_extensible_Borsuk_map [OF \<open>compact S\<close> _ boc])
+ using non_extensible_Borsuk_map [OF \<open>compact S\<close> _ boc] \<open>a \<notin> S\<close>
+ by (simp add: componentsI)
moreover obtain g where "continuous_on (S \<union> connected_component_set (- S) a) g"
"g ` (S \<union> connected_component_set (- S) a) \<subseteq> sphere 0 1"
"\<And>x. x \<in> S \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
@@ -1990,7 +1993,7 @@
by (simp add: \<open>compact S\<close> closed_subset compact_imp_closed)
show "continuous_on ?T (\<lambda>x. (x - b) /\<^sub>R norm (x - b))"
by (simp add: \<open>b \<notin> S\<close> notcc continuous_on_Borsuk_map)
- show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) ` ?T \<subseteq> sphere 0 1"
+ show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) \<in> ?T \<rightarrow> sphere 0 1"
by (simp add: \<open>b \<notin> S\<close> notcc Borsuk_map_into_sphere)
show "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) (\<lambda>x. (x - a) /\<^sub>R norm (x - a))"
@@ -2073,12 +2076,12 @@
lemma extension_from_component:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes S: "locally connected S \<or> compact S" and "ANR U"
- and C: "C \<in> components S" and contf: "continuous_on C f" and fim: "f ` C \<subseteq> U"
- obtains g where "continuous_on S g" "g ` S \<subseteq> U" "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
+ and C: "C \<in> components S" and contf: "continuous_on C f" and fim: "f \<in> C \<rightarrow> U"
+ obtains g where "continuous_on S g" "g \<in> S \<rightarrow> U" "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
proof -
obtain T g where ope: "openin (top_of_set S) T"
and clo: "closedin (top_of_set S) T"
- and "C \<subseteq> T" and contg: "continuous_on T g" and gim: "g ` T \<subseteq> U"
+ and "C \<subseteq> T" and contg: "continuous_on T g" and gim: "g \<in> T \<rightarrow> U"
and gf: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
using S
proof
@@ -2089,7 +2092,7 @@
assume "compact S"
then obtain W g where "C \<subseteq> W" and opeW: "openin (top_of_set S) W"
and contg: "continuous_on W g"
- and gim: "g ` W \<subseteq> U" and gf: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
+ and gim: "g \<in> W \<rightarrow> U" and gf: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
using ANR_imp_absolute_neighbourhood_extensor [of U C f S] C \<open>ANR U\<close> closedin_component contf fim by blast
then obtain V where "open V" and V: "W = S \<inter> V"
by (auto simp: openin_open)
@@ -2103,13 +2106,13 @@
by (meson \<open>compact K\<close> \<open>compact S\<close> closedin_compact_eq opeK openin_imp_subset)
show "continuous_on K g"
by (metis Int_subset_iff V \<open>K \<subseteq> V\<close> contg continuous_on_subset opeK openin_subtopology subset_eq)
- show "g ` K \<subseteq> U"
+ show "g \<in> K \<rightarrow> U"
using V \<open>K \<subseteq> V\<close> gim opeK openin_imp_subset by fastforce
qed (use opeK gf \<open>C \<subseteq> K\<close> in auto)
qed
- obtain h where "continuous_on S h" "h ` S \<subseteq> U" "\<And>x. x \<in> T \<Longrightarrow> h x = g x"
+ obtain h where "continuous_on S h" "h \<in> S \<rightarrow> U" "\<And>x. x \<in> T \<Longrightarrow> h x = g x"
using extension_from_clopen
- by (metis C bot.extremum_uniqueI clo contg gim fim image_is_empty in_components_nonempty ope)
+ by (metis C bot.extremum_uniqueI clo contg gim fim image_is_empty in_components_nonempty ope image_subset_iff_funcset)
then show ?thesis
by (metis \<open>C \<subseteq> T\<close> gf subset_eq that)
qed
@@ -2198,9 +2201,9 @@
obtain W k where W: "({0,1} \<times> S) \<union> ({0..1} \<times> T) \<subseteq> W"
and opeW: "openin (top_of_set ({0..1} \<times> S)) W"
and contk: "continuous_on W k"
- and kim: "k ` W \<subseteq> U"
+ and kim: "k \<in> W \<rightarrow> U"
and kh': "\<And>x. x \<in> ({0,1} \<times> S) \<union> ({0..1} \<times> T) \<Longrightarrow> k x = h' x"
- by (metis ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR U\<close>, of "({0,1} \<times> S) \<union> ({0..1} \<times> T)" h' "{0..1} \<times> S"])
+ by (metis ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR U\<close>, of "({0,1} \<times> S) \<union> ({0..1} \<times> T)" h' "{0..1} \<times> S"] image_subset_iff_funcset)
obtain T' where opeT': "openin (top_of_set S) T'"
and "T \<subseteq> T'" and TW: "{0..1} \<times> T' \<subseteq> W"
using tube_lemma_gen [of "{0..1::real}" T S W] W \<open>T \<subseteq> S\<close> opeW by auto
@@ -2377,11 +2380,11 @@
fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set"
assumes S: "locally connected S \<or> compact S" and "ANR T"
shows
- "(\<forall>f g. continuous_on S f \<longrightarrow> f ` S \<subseteq> T \<longrightarrow> continuous_on S g \<longrightarrow> g ` S \<subseteq> T \<longrightarrow>
+ "(\<forall>f g. continuous_on S f \<longrightarrow> f \<in> S \<rightarrow> T \<longrightarrow> continuous_on S g \<longrightarrow> g \<in> S \<rightarrow> T \<longrightarrow>
homotopic_with_canon (\<lambda>x. True) S T f g)
\<longleftrightarrow>
(\<forall>C\<in>components S.
- \<forall>f g. continuous_on C f \<longrightarrow> f ` C \<subseteq> T \<longrightarrow> continuous_on C g \<longrightarrow> g ` C \<subseteq> T \<longrightarrow>
+ \<forall>f g. continuous_on C f \<longrightarrow> f \<in> C \<rightarrow> T \<longrightarrow> continuous_on C g \<longrightarrow> g \<in> C \<rightarrow> T \<longrightarrow>
homotopic_with_canon (\<lambda>x. True) C T f g)"
(is "?lhs = ?rhs")
proof
@@ -2389,11 +2392,11 @@
show ?rhs
proof clarify
fix C f g
- assume contf: "continuous_on C f" and fim: "f ` C \<subseteq> T"
- and contg: "continuous_on C g" and gim: "g ` C \<subseteq> T" and C: "C \<in> components S"
- obtain f' where contf': "continuous_on S f'" and f'im: "f' ` S \<subseteq> T" and f'f: "\<And>x. x \<in> C \<Longrightarrow> f' x = f x"
+ assume contf: "continuous_on C f" and fim: "f \<in> C \<rightarrow> T"
+ and contg: "continuous_on C g" and gim: "g \<in> C \<rightarrow> T" and C: "C \<in> components S"
+ obtain f' where contf': "continuous_on S f'" and f'im: "f' \<in> S \<rightarrow> T" and f'f: "\<And>x. x \<in> C \<Longrightarrow> f' x = f x"
using extension_from_component [OF S \<open>ANR T\<close> C contf fim] by metis
- obtain g' where contg': "continuous_on S g'" and g'im: "g' ` S \<subseteq> T" and g'g: "\<And>x. x \<in> C \<Longrightarrow> g' x = g x"
+ obtain g' where contg': "continuous_on S g'" and g'im: "g' \<in> S \<rightarrow> T" and g'g: "\<And>x. x \<in> C \<Longrightarrow> g' x = g x"
using extension_from_component [OF S \<open>ANR T\<close> C contg gim] by metis
have "homotopic_with_canon (\<lambda>x. True) C T f' g'"
using L [OF contf' f'im contg' g'im] homotopic_with_subset_left C in_components_subset by fastforce
@@ -2405,11 +2408,11 @@
show ?lhs
proof clarify
fix f g
- assume contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
- and contg: "continuous_on S g" and gim: "g ` S \<subseteq> T"
+ assume contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> T"
+ and contg: "continuous_on S g" and gim: "g \<in> S \<rightarrow> T"
moreover have "homotopic_with_canon (\<lambda>x. True) C T f g" if "C \<in> components S" for C
- using R [OF that]
- by (meson contf contg continuous_on_subset fim gim image_mono in_components_subset order.trans that)
+ using R [OF that] contf contg continuous_on_subset fim gim in_components_subset
+ by (smt (verit, del_insts) Pi_anti_mono subsetD that)
ultimately show "homotopic_with_canon (\<lambda>x. True) S T f g"
by (subst homotopic_on_components_eq [OF S \<open>ANR T\<close>]) auto
qed
--- a/src/HOL/Analysis/Starlike.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Starlike.thy Mon Jul 03 16:46:37 2023 +0100
@@ -4202,7 +4202,7 @@
lemma proper_map_from_compact:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T" and "compact S"
+ assumes contf: "continuous_on S f" and imf: "f \<in> S \<rightarrow> T" and "compact S"
"closedin (top_of_set T) K"
shows "compact (S \<inter> f -` K)"
by (rule closedin_compact [OF \<open>compact S\<close>] continuous_closedin_preimage_gen assms)+
@@ -5820,7 +5820,7 @@
lemma continuous_closed_graph_eq:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes "compact T" and fim: "f ` S \<subseteq> T"
+ assumes "compact T" and fim: "f \<in> S \<rightarrow> T"
shows "continuous_on S f \<longleftrightarrow>
closedin (top_of_set (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"
(is "?lhs = ?rhs")
@@ -5848,7 +5848,7 @@
lemma continuous_from_closed_graph:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes "compact T" and fim: "f ` S \<subseteq> T" and clo: "closed ((\<lambda>x. Pair x (f x)) ` S)"
+ assumes "compact T" and fim: "f \<in> S \<rightarrow> T" and clo: "closed ((\<lambda>x. Pair x (f x)) ` S)"
shows "continuous_on S f"
using fim clo
by (auto intro: closed_subset simp: continuous_closed_graph_eq [OF \<open>compact T\<close> fim])
--- a/src/HOL/Analysis/Urysohn.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Analysis/Urysohn.thy Mon Jul 03 16:46:37 2023 +0100
@@ -2516,8 +2516,9 @@
show ?thesis
unfolding Lipschitz_continuous_map_pos
proof
- show "f ` mspace (submetric m1 T) \<subseteq> mspace m2"
- by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist mtopology_of_def mtopology_of_submetric)
+ show "f \<in> mspace (submetric m1 T) \<rightarrow> mspace m2"
+ by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist mtopology_of_def
+ mtopology_of_submetric image_subset_iff_funcset)
define X where "X \<equiv> prod_topology (subtopology L.M1.mtopology T) (subtopology L.M1.mtopology T)"
obtain B::real where "B > 0" and B: "\<forall>(x,y) \<in> S\<times>S. mdist m2 (f x) (f y) \<le> B * mdist m1 x y"
using lcf \<open>S \<subseteq> mspace m1\<close> by (force simp: Lipschitz_continuous_map_pos)
@@ -2608,8 +2609,9 @@
show ?thesis
unfolding uniformly_continuous_map_def
proof (intro conjI strip)
- show "f ` mspace (submetric m1 T) \<subseteq> mspace m2"
- by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist mtopology_of_def mtopology_of_submetric)
+ show "f \<in> mspace (submetric m1 T) \<rightarrow> mspace m2"
+ by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist
+ mtopology_of_def mtopology_of_submetric image_subset_iff_funcset)
fix \<epsilon>::real
assume "\<epsilon> > 0"
then obtain \<delta> where "\<delta>>0" and \<delta>: "\<forall>(x,y) \<in> S\<times>S. mdist m1 x y < \<delta> \<longrightarrow> mdist m2 (f x) (f y) \<le> \<epsilon>/2"
@@ -3143,7 +3145,7 @@
lemma mspace_cfunspace [simp]:
"mspace (cfunspace X m) =
- {f. f ` topspace X \<subseteq> mspace m \<and> f \<in> extensional (topspace X) \<and>
+ {f. f \<in> topspace X \<rightarrow> mspace m \<and> f \<in> extensional (topspace X) \<and>
Metric_space.mbounded (mspace m) (mdist m) (f ` (topspace X)) \<and>
continuous_map X (mtopology_of m) f}"
by (auto simp: cfunspace_def Metric_space.fspace_def)
@@ -3278,7 +3280,7 @@
assume g: "range \<sigma> \<subseteq> mspace (cfunspace X Self) \<and> limitin F.mtopology \<sigma> g sequentially"
show "g \<in> mspace (cfunspace X Self)"
proof (simp add: mtopology_of_def, intro conjI)
- show "g ` topspace X \<subseteq> M" "g \<in> extensional (topspace X)" "mbounded (g ` topspace X)"
+ show "g \<in> topspace X \<rightarrow> M" "g \<in> extensional (topspace X)" "mbounded (g ` topspace X)"
using g F.limitin_mspace by (force simp: fspace_def)+
show "continuous_map X mtopology g"
using * g by blast
@@ -3296,7 +3298,7 @@
obtains f :: "['a,'a] \<Rightarrow> real" and S where
"S \<subseteq> mspace(funspace M euclidean_metric)"
"mcomplete_of (submetric (funspace M euclidean_metric) S)"
- "f ` M \<subseteq> S"
+ "f \<in> M \<rightarrow> S"
"mtopology_of(funspace M euclidean_metric) closure_of f ` M = S"
"\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk>
\<Longrightarrow> mdist (funspace M euclidean_metric) (f x) (f y) = d x y"
@@ -3337,7 +3339,7 @@
using Metric_space.mcomplete_funspace Met_TC.Metric_space_axioms by (fastforce simp: mcomplete_of_def)
ultimately show "mcomplete_of (submetric (funspace M euclidean_metric) S)"
by (simp add: S.closedin_eq_mcomplete mcomplete_of_def)
- show "f ` M \<subseteq> S"
+ show "f \<in> M \<rightarrow> S"
using S_def fim in_closure_of m'_def by fastforce
show "mtopology_of (funspace M euclidean_metric) closure_of f ` M = S"
by (auto simp: f_def S_def mtopology_of_def)
@@ -3363,14 +3365,14 @@
lemma (in Metric_space) metric_completion:
obtains f :: "['a,'a] \<Rightarrow> real" and m' where
"mcomplete_of m'"
- "f ` M \<subseteq> mspace m' "
+ "f \<in> M \<rightarrow> mspace m' "
"mtopology_of m' closure_of f ` M = mspace m'"
"\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> mdist m' (f x) (f y) = d x y"
proof -
obtain f :: "['a,'a] \<Rightarrow> real" and S where
Ssub: "S \<subseteq> mspace(funspace M euclidean_metric)"
and mcom: "mcomplete_of (submetric (funspace M euclidean_metric) S)"
- and fim: "f ` M \<subseteq> S"
+ and fim: "f \<in> M \<rightarrow> S"
and eqS: "mtopology_of(funspace M euclidean_metric) closure_of f ` M = S"
and eqd: "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> mdist (funspace M euclidean_metric) (f x) (f y) = d x y"
using metric_completion_explicit by metis
@@ -3379,11 +3381,11 @@
proof
show "mcomplete_of m'"
by (simp add: mcom m'_def)
- show "f ` M \<subseteq> mspace m'"
+ show "f \<in> M \<rightarrow> mspace m'"
using Ssub fim m'_def by auto
show "mtopology_of m' closure_of f ` M = mspace m'"
using eqS fim Ssub
- by (force simp: m'_def mtopology_of_submetric closure_of_subtopology Int_absorb1)
+ by (force simp: m'_def mtopology_of_submetric closure_of_subtopology Int_absorb1 image_subset_iff_funcset)
show "mdist m' (f x) (f y) = d x y" if "x \<in> M" and "y \<in> M" for x y
using that eqd m'_def by force
qed
@@ -3400,10 +3402,10 @@
then interpret Metric_space M d by simp
obtain f :: "['a,'a] \<Rightarrow> real" and m' where
"mcomplete_of m'"
- and fim: "f ` M \<subseteq> mspace m' "
+ and fim: "f \<in> M \<rightarrow> mspace m' "
and m': "mtopology_of m' closure_of f ` M = mspace m'"
and eqd: "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> mdist m' (f x) (f y) = d x y"
- by (meson metric_completion)
+ by (metis metric_completion)
show thesis
proof
show "completely_metrizable_space (mtopology_of m')"
@@ -3412,7 +3414,8 @@
by (metis Metric_space_mspace_mdist)
show "embedding_map X (mtopology_of m') f"
using Metric_space12.isometry_imp_embedding_map
- by (metis Metric_space12_def Metric_space_axioms Metric_space_mspace_mdist Xeq eqd fim mtopology_of_def)
+ by (metis Metric_space12_def Metric_space_axioms Metric_space_mspace_mdist Xeq eqd fim
+ mtopology_of_def)
show "(mtopology_of m') closure_of f ` topspace X = topspace (mtopology_of m')"
by (simp add: Xeq m')
qed
@@ -3424,7 +3427,7 @@
lemma (in Metric_space) contraction_imp_unique_fixpoint:
assumes "f x = x" "f y = y"
- and "f ` M \<subseteq> M"
+ and "f \<in> M \<rightarrow> M"
and "k < 1"
and "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> d (f x) (f y) \<le> k * d x y"
and "x \<in> M" "y \<in> M"
@@ -3433,7 +3436,7 @@
text \<open>Banach Fixed-Point Theorem (aka, Contraction Mapping Principle)\<close>
lemma (in Metric_space) Banach_fixedpoint_thm:
- assumes mcomplete and "M \<noteq> {}" and fim: "f ` M \<subseteq> M"
+ assumes mcomplete and "M \<noteq> {}" and fim: "f \<in> M \<rightarrow> M"
and "k < 1"
and con: "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> d (f x) (f y) \<le> k * d x y"
obtains x where "x \<in> M" "f x = x"
@@ -3444,7 +3447,7 @@
proof (cases "\<forall>x \<in> M. f x = f a")
case True
then show ?thesis
- by (metis \<open>a \<in> M\<close> fim image_subset_iff that)
+ by (metis \<open>a \<in> M\<close> fim image_subset_iff image_subset_iff_funcset that)
next
case False
then obtain b where "b \<in> M" and b: "f b \<noteq> f a"
@@ -3472,7 +3475,7 @@
fix \<epsilon>::real
assume "\<epsilon>>0"
with \<open>k < 1\<close> \<open>f a \<noteq> a\<close> \<open>a \<in> M\<close> fim have gt0: "((1 - k) * \<epsilon>) / d a (f a) > 0"
- by (fastforce simp: divide_simps)
+ by (fastforce simp: divide_simps Pi_iff)
obtain N where "k^N < ((1-k) * \<epsilon>) / d a (f a)"
using real_arch_pow_inv [OF gt0 \<open>k < 1\<close>] by blast
then have N: "\<And>n. n \<ge> N \<Longrightarrow> k^n < ((1-k) * \<epsilon>) / d a (f a)"
@@ -3992,11 +3995,11 @@
shows "embedding_map X
(product_topology (\<lambda>f. top_of_set {0..1::real})
(mspace (submetric (cfunspace X euclidean_metric)
- {f. f ` topspace X \<subseteq> {0..1}})) )
- (\<lambda>x. \<lambda>f \<in> mspace (submetric (cfunspace X euclidean_metric) {f. f ` topspace X \<subseteq> {0..1}}).
+ {f. f \<in> topspace X \<rightarrow> {0..1}})) )
+ (\<lambda>x. \<lambda>f \<in> mspace (submetric (cfunspace X euclidean_metric) {f. f \<in> topspace X \<rightarrow> {0..1}}).
f x)"
proof -
- define K where "K \<equiv> mspace(submetric (cfunspace X euclidean_metric) {f. f ` topspace X \<subseteq> {0..1::real}})"
+ define K where "K \<equiv> mspace(submetric (cfunspace X euclidean_metric) {f. f \<in> topspace X \<rightarrow> {0..1::real}})"
define e where "e \<equiv> \<lambda>x. \<lambda>f\<in>K. f x"
have "e x \<noteq> e y" if xy: "x \<noteq> y" "x \<in> topspace X" "y \<in> topspace X" for x y
proof -
@@ -4023,14 +4026,14 @@
assume "e x \<in> K \<rightarrow>\<^sub>E {0..1}" and "x \<in> topspace X" and "openin X U" and "x \<in> U"
then obtain g where contg: "continuous_map X (top_of_set {0..1}) g" and "g x = 0"
and gim: "g ` (topspace X - U) \<subseteq> {1::real}"
- using \<open>completely_regular_space X\<close> unfolding completely_regular_space_def
+ using \<open>completely_regular_space X\<close> unfolding completely_regular_space_def
by (metis Diff_iff openin_closedin_eq)
then have "bounded (g ` topspace X)"
by (meson bounded_closed_interval bounded_subset continuous_map_in_subtopology)
- moreover have "g ` topspace X \<subseteq> {0..1}"
- using contg by (simp add: continuous_map_in_subtopology)
+ moreover have "g \<in> topspace X \<rightarrow> {0..1}"
+ using contg by (simp add: continuous_map_def)
ultimately have g_in_K: "restrict g (topspace X) \<in> K"
- using contg by (simp add: K_def continuous_map_in_subtopology)
+ using contg by (force simp add: K_def continuous_map_in_subtopology)
have "openin (top_of_set {0..1}) {0..<1::real}"
using open_real_greaterThanLessThan[of "-1" 1] by (force simp: openin_open)
moreover have "e x \<in> (\<Pi>\<^sub>E f\<in>K. if f = restrict g (topspace X) then {0..<1} else {0..1})"
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy Mon Jul 03 16:46:37 2023 +0100
@@ -1145,7 +1145,7 @@
lemma covering_space_lift_is_holomorphic:
assumes cov: "covering_space C p S"
and C: "open C" "p holomorphic_on C"
- and holf: "f holomorphic_on U" and fim: "f ` U \<subseteq> S" and gim: "g ` U \<subseteq> C"
+ and holf: "f holomorphic_on U" and fim: "f \<in> U \<rightarrow> S" and gim: "g \<in> U \<rightarrow> C"
and contg: "continuous_on U g" and pg_f: "\<And>x. x \<in> U \<Longrightarrow> p(g x) = f x"
shows "g holomorphic_on U"
unfolding holomorphic_on_def
@@ -1161,7 +1161,7 @@
then have "\<And>W. W \<in> \<V> \<Longrightarrow> open W \<and> W \<subseteq> C"
by (metis \<open>open C\<close> inf_le1 open_Int openin_open)
then obtain V where "V \<in> \<V>" "g z \<in> V" "open V" "V \<subseteq> C"
- by (metis IntI UnionE image_subset_iff vimageI UV \<open>f z \<in> T\<close> \<open>z \<in> U\<close> gim pg_f)
+ by (metis IntI UnionE image_subset_iff vimageI UV \<open>f z \<in> T\<close> \<open>z \<in> U\<close> gim pg_f image_subset_iff_funcset)
have holp: "p holomorphic_on V"
using \<open>V \<subseteq> C\<close> \<open>p holomorphic_on C\<close> holomorphic_on_subset by blast
moreover have injp: "inj_on p V"
@@ -1201,15 +1201,14 @@
lemma covering_space_lift_holomorphic:
assumes cov: "covering_space C p S"
and C: "open C" "p holomorphic_on C"
- and f: "f holomorphic_on U" "f ` U \<subseteq> S"
+ and f: "f holomorphic_on U" "f \<in> U \<rightarrow> S"
and U: "simply_connected U" "locally path_connected U"
- obtains g where "g holomorphic_on U" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
+ obtains g where "g holomorphic_on U" "g \<in> U \<rightarrow> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
proof -
- obtain g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
- using covering_space_lift [OF cov U]
- using f holomorphic_on_imp_continuous_on by blast
+ obtain g where "continuous_on U g" "g \<in> U \<rightarrow> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
+ using covering_space_lift [OF cov U] f holomorphic_on_imp_continuous_on by blast
then show ?thesis
- by (metis C cov covering_space_lift_is_holomorphic f that)
+ by (metis C cov covering_space_lift_is_holomorphic f image_subset_iff_funcset that)
qed
subsection\<open>The Schwarz Lemma\<close>
--- a/src/HOL/Complex_Analysis/Riemann_Mapping.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Complex_Analysis/Riemann_Mapping.thy Mon Jul 03 16:46:37 2023 +0100
@@ -1624,7 +1624,7 @@
qed
show "continuous_on UNIV (\<lambda>w. \<zeta> + exp w)"
by (rule continuous_intros)+
- show "range (\<lambda>w. \<zeta> + exp w) \<subseteq> -{\<zeta>}"
+ show "(\<lambda>w. \<zeta> + exp w) \<in> UNIV \<rightarrow> -{\<zeta>}"
by auto
qed
then have "homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} (-{\<zeta>}) p (\<lambda>x. \<zeta> + 1)"
--- a/src/HOL/Library/FuncSet.thy Sun Jul 02 20:41:07 2023 +0200
+++ b/src/HOL/Library/FuncSet.thy Mon Jul 03 16:46:37 2023 +0100
@@ -148,9 +148,10 @@
by (auto simp: Pi_def)
lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
- apply auto
- apply (metis PiE fun_upd_apply)
- by force
+ using mk_disjoint_insert by fastforce
+
+lemma fst_Pi: "fst \<in> A \<times> B \<rightarrow> A" and snd_Pi: "snd \<in> A \<times> B \<rightarrow> B"
+ by auto
subsection \<open>Composition With a Restricted Domain: \<^term>\<open>compose\<close>\<close>