--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy Sun Mar 23 22:33:19 2025 +0000
@@ -81,13 +81,13 @@
"\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
\<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i + g x i)"
unfolding Euclidean_space_def continuous_map_in_subtopology
- by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_add)
+ by (auto simp: continuous_map_componentwise_UNIV Pi_iff continuous_map_add)
lemma continuous_map_Euclidean_space_diff [continuous_intros]:
"\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
\<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i - g x i)"
- unfolding Euclidean_space_def continuous_map_in_subtopology
- by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_diff)
+ unfolding Euclidean_space_def continuous_map_in_subtopology
+ by (auto simp: continuous_map_componentwise_UNIV Pi_iff continuous_map_diff)
lemma continuous_map_Euclidean_space_iff:
"continuous_map (Euclidean_space m) euclidean g
@@ -101,7 +101,7 @@
next
assume "continuous_on (topspace (Euclidean_space m)) g"
then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclidean g"
- by (metis (lifting) continuous_map_into_fulltopology continuous_map_subtopology_eu order_refl topspace_Euclidean_space)
+ by (simp add: topspace_Euclidean_space)
then show "continuous_map (Euclidean_space m) euclidean g"
by (simp add: Euclidean_space_def euclidean_product_topology)
qed
@@ -353,7 +353,7 @@
for k
unfolding case_prod_unfold o_def
by (intro continuous_map_into_fulltopology [OF continuous_map_fst] continuous_intros) auto
- moreover have "?h ` ({0..1} \<times> topspace (nsphere p)) \<subseteq> {x. \<forall>i\<ge>Suc p. x i = 0}"
+ moreover have "?h \<in> ({0..1} \<times> topspace (nsphere p)) \<rightarrow> {x. \<forall>i\<ge>Suc p. x i = 0}"
using continuous_map_image_subset_topspace [OF f]
by (auto simp: nsphere image_subset_iff a0)
moreover have "(\<lambda>i. 0) \<notin> ?h ` ({0..1} \<times> topspace (nsphere p))"
@@ -376,7 +376,8 @@
using eq unfolding * by (simp add: fun_eq_iff)
qed
ultimately show "continuous_map (prod_topology ?T01 (nsphere p)) ?Y ?h"
- by (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV)
+ unfolding Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
+ by (force simp flip: image_subset_iff_funcset)
next
have *: "\<lbrakk>\<forall>i\<ge>Suc p. x i = 0; x \<noteq> (\<lambda>i. 0)\<rbrakk> \<Longrightarrow> (\<Sum>j\<le>p. (x j)\<^sup>2) \<noteq> 0" for x :: "nat \<Rightarrow> real"
by (force simp: fun_eq_iff not_less_eq_eq sum_nonneg_eq_0_iff)--- a/src/HOL/Analysis/Abstract_Topology.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Sun Mar 23 22:33:19 2025 +0000
@@ -1567,12 +1567,12 @@
by (smt (verit, ccfv_threshold) assms continuous_map image_eqI image_subset_iff in_closure_of mem_Collect_eq)
qed
-lemma continuous_map_subset_aux1: "continuous_map X Y f \<Longrightarrow>
- (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+lemma continuous_map_subset_aux1:
+ "continuous_map X Y f \<Longrightarrow> (\<forall>S. f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
using continuous_map_image_closure_subset by blast
lemma continuous_map_subset_aux2:
- assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
+ assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S"
shows "continuous_map X Y f"
unfolding continuous_map_closedin
proof (intro conjI ballI allI impI)
@@ -1598,18 +1598,18 @@
qed
lemma continuous_map_eq_image_closure_subset:
- "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+ "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
lemma continuous_map_eq_image_closure_subset_alt:
- "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+ "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
lemma continuous_map_eq_image_closure_subset_gen:
"continuous_map X Y f \<longleftrightarrow>
f \<in> topspace X \<rightarrow> topspace Y \<and>
- (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
- by (meson Pi_iff continuous_map continuous_map_eq_image_closure_subset image_subset_iff)
+ (\<forall>S. f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
+ by (metis continuous_map_eq_image_closure_subset continuous_map_funspace)
lemma continuous_map_closure_preimage_subset:
"continuous_map X Y f
@@ -1697,16 +1697,18 @@
by (auto simp: elim!: continuous_map_eq)
lemma continuous_map_in_subtopology:
- "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f ` (topspace X) \<subseteq> S"
+ "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f \<in> (topspace X) \<rightarrow> S"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
show ?rhs
proof -
- have "\<And>A. f ` (X closure_of A) \<subseteq> subtopology X' S closure_of f ` A"
- by (meson L continuous_map_image_closure_subset)
+ have "\<And>A. f \<in> (X closure_of A) \<rightarrow> subtopology X' S closure_of f ` A"
+ by (metis L continuous_map_eq_image_closure_subset image_subset_iff_funcset)
then show ?thesis
- by (metis (no_types) closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace continuous_map_eq_image_closure_subset order.trans)
+ by (metis closure_of_subset_subtopology closure_of_subtopology_subset
+ closure_of_topspace continuous_map_eq_image_closure_subset
+ image_subset_iff_funcset subset_trans)
qed
next
assume R: ?rhs
@@ -3963,7 +3965,7 @@
proof
show "?lhs \<Longrightarrow> ?rhs"
unfolding embedding_map_def
- by (metis continuous_map_in_subtopology homeomorphic_imp_continuous_map inf_absorb2 subtopology_subtopology)
+ by (metis Int_subset_iff homeomorphic_imp_surjective_map inf_le1 subtopology_restrict subtopology_subtopology topspace_subtopology)
qed (simp add: embedding_map_def inf.absorb_iff2 subtopology_subtopology)
lemma injective_open_imp_embedding_map:
@@ -4118,13 +4120,13 @@
using assms continuous_on_closed by blast
lemma continuous_map_subtopology_eu [simp]:
- "continuous_map (top_of_set S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
+ "continuous_map (top_of_set S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h \<in> S \<rightarrow> T"
by (simp add: continuous_map_in_subtopology)
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_in_subtopology eq image_subset_iff_subset_vimage)
+ using cont continuous_map_iff_continuous2 continuous_map_into_subtopology eq by blast
subsection\<^marker>\<open>tag unimportant\<close> \<open>Half-global and completely global cases\<close>
@@ -4166,25 +4168,14 @@
by (metis Int_commute closedin_closed continuous_on_closed_invariant)
lemma continuous_open_preimage:
- assumes contf: "continuous_on S f" and "open S" "open T"
+ assumes "continuous_on S f" and "open S" "open T"
shows "open (S \<inter> f -` T)"
-proof-
- obtain U where "open U" "(S \<inter> f -` T) = S \<inter> U"
- using continuous_openin_preimage_gen[OF contf \<open>open T\<close>]
- unfolding openin_open by auto
- then show ?thesis
- using open_Int[of S U, OF \<open>open S\<close>] by auto
-qed
+ by (metis Int_commute assms continuous_on_open_vimage)
lemma continuous_closed_preimage:
- assumes contf: "continuous_on S f" and "closed S" "closed T"
+ assumes "continuous_on S f" and "closed S" "closed T"
shows "closed (S \<inter> f -` T)"
-proof-
- obtain U where "closed U" "(S \<inter> f -` T) = S \<inter> U"
- using continuous_closedin_preimage[OF contf \<open>closed T\<close>]
- unfolding closedin_closed by auto
- then show ?thesis using closed_Int[of S U, OF \<open>closed S\<close>] by auto
-qed
+ by (metis assms closed_vimage_Int inf_commute)
lemma continuous_open_vimage: "open S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` S)"
by (metis continuous_on_eq_continuous_within open_vimage) --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Mar 23 22:33:19 2025 +0000
@@ -97,12 +97,23 @@
by (metis locally_compact_closedin closedin_retract)
lemma homotopic_into_retract:
- "\<lbrakk>f \<in> S \<rightarrow> T; g \<in> S \<rightarrow> T; T retract_of U; homotopic_with_canon (\<lambda>x. True) S U f g\<rbrakk>
- \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g"
- apply (subst (asm) homotopic_with_def)
- apply (simp add: homotopic_with retract_of_def retraction_def Pi_iff, clarify)
- apply (rule_tac x="r \<circ> h" in exI)
- by (smt (verit, ccfv_SIG) comp_def continuous_on_compose continuous_on_subset image_subset_iff)
+ assumes fg: "f \<in> S \<rightarrow> T" "g \<in> S \<rightarrow> T"
+ assumes "T retract_of U"
+ assumes "homotopic_with_canon (\<lambda>x. True) S U f g"
+ shows "homotopic_with_canon (\<lambda>x. True) S T f g"
+proof -
+ obtain h r where r: "retraction U T r"
+ "continuous_on ({0..1::real} \<times> S) h"
+ and h: "h \<in> {0..1} \<times> S \<rightarrow> U \<and> (\<forall>x. h (0, x) = f x) \<and> (\<forall>x. h (1, x) = g x)"
+ using assms by (auto simp: homotopic_with_def retract_of_def)
+ then have "continuous_on ({0..1} \<times> S) (r \<circ> h)"
+ by (metis continuous_on_compose continuous_on_subset funcset_image
+ retraction_def)
+ then show ?thesis
+ using r fg h
+ apply (simp add: retraction homotopic_with Pi_iff)
+ by (smt (verit, best) imageI)
+qed
lemma retract_of_locally_connected:
assumes "locally connected T" "S retract_of T"
@@ -131,7 +142,8 @@
ultimately
show ?thesis
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)
+ by (meson continuous_map_from_subtopology_mono continuous_map_id
+ continuous_map_subtopology_eu r retraction_def)
qed
lemma deformation_retract:
@@ -2235,7 +2247,7 @@
have "continuous_on ({0..1} \<times> S) h"
unfolding h_def using g by (intro continuous_intros) (auto simp: path_defs)
moreover
- have "h ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
+ have "h \<in> ({0..1} \<times> S) \<rightarrow> sphere 0 1"
unfolding h_def using g by (auto simp: divide_simps path_defs)
ultimately show ?thesis
using g by (auto simp: h_def path_defs homotopic_with_def)--- a/src/HOL/Analysis/Further_Topology.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Sun Mar 23 22:33:19 2025 +0000
@@ -2743,7 +2743,8 @@
by (auto simp: Arg2pi_ge_0 Arg2pi_lt_2pi less_imp_le)
also have "... \<subseteq> S"
using him by blast
- finally show "(\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
+ finally show "(\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi))) \<in> {0..1} \<times> sphere 0 1 \<rightarrow> S"
+ by blast
qed (auto simp: h0 h1)
qed
--- a/src/HOL/Analysis/Homotopy.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Analysis/Homotopy.thy Sun Mar 23 22:33:19 2025 +0000
@@ -116,21 +116,21 @@
by (cases "t = 1") (simp_all add: assms)
qed auto
+lemma homotopic_with_imp_funspace1:
+ "homotopic_with_canon P X Y f g \<Longrightarrow> f \<in> X \<rightarrow> Y"
+ using homotopic_with_imp_continuous_maps by fastforce
+
lemma homotopic_with_imp_subset1:
"homotopic_with_canon P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
- by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
+ using homotopic_with_imp_funspace1 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_continuous_maps by force
lemma homotopic_with_imp_subset2:
"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
+ using homotopic_with_imp_funspace2 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"
@@ -485,10 +485,11 @@
lemma homotopic_paths_imp_subset:
"homotopic_paths S p q \<Longrightarrow> path_image p \<subseteq> S \<and> path_image q \<subseteq> S"
- by (metis (mono_tags) continuous_map_subtopology_eu homotopic_paths_def homotopic_with_imp_continuous_maps path_image_def)
+ by (simp add: homotopic_paths_def homotopic_with_imp_subset1 homotopic_with_imp_subset2
+ path_image_def)
proposition homotopic_paths_refl [simp]: "homotopic_paths S p p \<longleftrightarrow> path p \<and> path_image p \<subseteq> S"
- by (simp add: homotopic_paths_def path_def path_image_def)
+ by (auto simp add: homotopic_paths_def path_def path_image_def)
proposition homotopic_paths_sym: "homotopic_paths S p q \<Longrightarrow> homotopic_paths S q p"
by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)
@@ -684,7 +685,7 @@
lemma homotopic_loops:
"homotopic_loops S p q \<longleftrightarrow>
(\<exists>h. continuous_on ({0..1::real} \<times> {0..1}) h \<and>
- image 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}. pathfinish(h \<circ> Pair t) = pathstart(h \<circ> Pair t)))"
@@ -702,12 +703,13 @@
proposition homotopic_loops_imp_subset:
"homotopic_loops S p q \<Longrightarrow> path_image p \<subseteq> S \<and> path_image q \<subseteq> S"
unfolding homotopic_loops_def path_image_def
- by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
+ by (simp add: homotopic_with_imp_subset1 homotopic_with_imp_subset2)
proposition homotopic_loops_refl:
"homotopic_loops S p p \<longleftrightarrow>
path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p"
- by (simp add: homotopic_loops_def path_image_def path_def)
+ by (metis (mono_tags, lifting) homotopic_loops_def homotopic_paths_def
+ homotopic_paths_refl homotopic_with_refl)
proposition homotopic_loops_sym: "homotopic_loops S p q \<Longrightarrow> homotopic_loops S q p"
by (simp add: homotopic_loops_def homotopic_with_sym)
@@ -726,8 +728,9 @@
proposition homotopic_loops_eq:
"\<lbrakk>path p; path_image p \<subseteq> S; pathfinish p = pathstart p; \<And>t. t \<in> {0..1} \<Longrightarrow> p(t) = q(t)\<rbrakk>
\<Longrightarrow> homotopic_loops S p q"
- unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def
- by (auto intro: homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]])
+ unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def image_subset_iff_funcset
+ using homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]]
+ by fastforce
proposition homotopic_loops_continuous_image:
"\<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)"
@@ -1247,7 +1250,7 @@
using p1 p2 unfolding homotopic_loops
apply clarify
subgoal for h k
- by (rule_tac x="\<lambda>z. (h z, k z)" in exI) (force intro: continuous_intros simp: path_defs)
+ by (rule_tac x="\<lambda>z. (h z, k z)" in exI) (auto intro: continuous_intros simp: path_defs)
done
qed
with assms show ?thesis
@@ -3786,7 +3789,9 @@
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)
+ apply (erule ex_forward)+
+ by (metis continuous_map_subtopology_eu homotopic_with_id2 openin_imp_subset openin_subtopology_self topspace_euclidean_subtopology
+ image_subset_iff_funcset)
lemma homotopy_eqv_inj_linear_image:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -3963,7 +3968,8 @@
shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}" (is "?lhs = ?rhs")
proof
assume ?lhs then show ?rhs
- by (metis continuous_map_subtopology_eu empty_iff equalityI homotopy_equivalent_space_def image_subset_iff subsetI)
+ by (meson continuous_map_subtopology_eu equals0D equals0I funcset_mem
+ homotopy_equivalent_space_def)
qed (use homeomorphic_imp_homotopy_eqv in force)
lemma homotopy_eqv_empty2 [simp]:
@@ -5281,8 +5287,8 @@
assume c: "homotopic_with_canon (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)"
then have contf: "continuous_on (sphere a r) f"
by (metis homotopic_with_imp_continuous)
- moreover have fim: "f ` sphere a r \<subseteq> S"
- by (meson continuous_map_subtopology_eu c homotopic_with_imp_continuous_maps)
+ moreover have fim: "f \<in> sphere a r \<rightarrow> S"
+ using homotopic_with_imp_subset1 that by blast
show ?P
using contf fim by (auto simp: sphere_def dist_norm norm_minus_commute)
qed
@@ -5373,7 +5379,7 @@
by (intro continuous_intros)
qed (auto simp: dist_norm norm_minus_commute mult_left_le_one_le)
moreover
- have "?h ` ({0..1} \<times> sphere a r) \<subseteq> S"
+ have "?h \<in> ({0..1} \<times> sphere a r) \<rightarrow> S"
by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gim [THEN subsetD])
moreover
have "\<forall>x\<in>sphere a r. ?h (0, x) = g a" "\<forall>x\<in>sphere a r. ?h (1, x) = f x"--- a/src/HOL/Analysis/Retracts.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Analysis/Retracts.thy Sun Mar 23 22:33:19 2025 +0000
@@ -1815,7 +1815,7 @@
apply (intro continuous_on_compose continuous_intros)
apply (force intro: inV continuous_on_subset [OF contk] continuous_on_subset [OF conta])+
done
- show "(k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) ` ({0..1} \<times> T) \<subseteq> U"
+ show "(k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) \<in> ({0..1} \<times> T) \<rightarrow> U"
using inV kim by auto
show "\<forall>x\<in>T. (k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) (0, x) = f x"
by (simp add: B_def h'_def keq)
@@ -2211,7 +2211,7 @@
proof (simp add: homotopic_with, intro exI conjI)
show "continuous_on ({0..1} \<times> T') k"
using TW continuous_on_subset contk by auto
- show "k ` ({0..1} \<times> T') \<subseteq> U"
+ show "k \<in> ({0..1} \<times> T') \<rightarrow> U"
using TW kim by fastforce
have "T' \<subseteq> S"
by (meson opeT' subsetD openin_imp_subset)
@@ -2246,7 +2246,7 @@
and hom: "\<And>n. homotopic_with_canon (\<lambda>x. True) (V n) T f g"
using assms by auto
then obtain h where conth: "\<And>n. continuous_on ({0..1::real} \<times> V n) (h n)"
- and him: "\<And>n. h n ` ({0..1} \<times> V n) \<subseteq> T"
+ and him: "\<And>n. h n \<in> ({0..1} \<times> V n) \<rightarrow> T"
and h0: "\<And>n. \<And>x. x \<in> V n \<Longrightarrow> h n (0, x) = f x"
and h1: "\<And>n. \<And>x. x \<in> V n \<Longrightarrow> h n (1, x) = g x"
by (simp add: homotopic_with) metis
@@ -2277,7 +2277,7 @@
proof (simp add: homotopic_with eqU [symmetric], intro exI conjI ballI)
show "continuous_on ({0..1} \<times> \<Union>\<V>) \<zeta>"
using V eqU by (blast intro!: continuous_on_subset [OF cont])
- show "\<zeta>` ({0..1} \<times> \<Union>\<V>) \<subseteq> T"
+ show "\<zeta> \<in> ({0..1} \<times> \<Union>\<V>) \<rightarrow> T"
proof clarsimp
fix t :: real and y :: "'a" and X :: "'a set"
assume "y \<in> X" "X \<in> \<V>" and t: "0 \<le> t" "t \<le> 1"--- a/src/HOL/Analysis/Urysohn.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Analysis/Urysohn.thy Sun Mar 23 22:33:19 2025 +0000
@@ -45,7 +45,7 @@
then show ?thesis
by (auto simp: f_def cInf_lower)
qed
- ultimately have fim: "f ` topspace X \<subseteq> {0..1}"
+ ultimately have fim: "f \<in> topspace X \<rightarrow> {0..1}"
by (auto simp: f_def)
have 0: "0 \<in> dyadics \<inter> {0..1::real}" and 1: "1 \<in> dyadics \<inter> {0..1::real}"
by (force simp: dyadics_def)+
@@ -161,17 +161,17 @@
qed
qed
then have contf: "continuous_map X (top_of_set {0..1}) f"
- by (force simp: Met_TC.continuous_map_to_metric dist_real_def continuous_map_in_subtopology fim simp flip: mtopology_is_euclidean)
+ by (auto simp: Met_TC.continuous_map_to_metric dist_real_def continuous_map_in_subtopology fim abs_minus_commute simp flip: mtopology_is_euclidean)
define g where "g \<equiv> \<lambda>x. a + (b - a) * f x"
show thesis
proof
have "continuous_map X euclideanreal g"
using contf \<open>a \<le> b\<close> unfolding g_def by (auto simp: continuous_intros continuous_map_in_subtopology)
- moreover have "g ` (topspace X) \<subseteq> {a..b}"
- using mult_left_le [of "f _" "b-a"] contf \<open>a \<le> b\<close>
- by (simp add: g_def add.commute continuous_map_in_subtopology image_subset_iff le_diff_eq)
+ moreover have "g \<in> (topspace X) \<rightarrow> {a..b}"
+ using mult_left_le [of "f _" "b-a"] contf \<open>a \<le> b\<close>
+ by (simp add: g_def Pi_iff add.commute continuous_map_in_subtopology image_subset_iff le_diff_eq)
ultimately show "continuous_map X (top_of_set {a..b}) g"
- by (meson continuous_map_in_subtopology)
+ using continuous_map_in_subtopology by blast
show "g ` S \<subseteq> {a}" "g ` T \<subseteq> {b}"
using fimS fimT by (auto simp: g_def)
qed
@@ -576,8 +576,8 @@
where conth: "continuous_map X (top_of_set {0..1}) h"
and him: "h ` W \<subseteq> {0}" "h ` S \<subseteq> {1}"
by (metis XS normal_space_iff_Urysohn)
- then have him01: "h ` topspace X \<subseteq> {0..1}"
- by (meson continuous_map_in_subtopology)
+ then have him01: "h \<in> topspace X \<rightarrow> {0..1}"
+ by (metis continuous_map_in_subtopology)
obtain z where "z \<in> T"
using \<open>T \<noteq> {}\<close> by blast
define g' where "g' \<equiv> \<lambda>x. z + h x * (g x - z)"
@@ -1066,7 +1066,7 @@
proof -
have *: "\<exists>U V. openin X U \<and> openin X V \<and> a \<in> U \<and> C \<subseteq> V \<and> disjnt U V"
if contf: "continuous_map X euclideanreal f" and a: "a \<in> topspace X - C" and "closedin X C"
- and fim: "f ` topspace X \<subseteq> {0..1}" and f0: "f a = 0" and f1: "f ` C \<subseteq> {1}"
+ and fim: "f \<in> topspace X \<rightarrow> {0..1}" and f0: "f a = 0" and f1: "f ` C \<subseteq> {1}"
for C a f
proof (intro exI conjI)
show "openin X {x \<in> topspace X. f x \<in> {..<1 / 2}}" "openin X {x \<in> topspace X. f x \<in> {1 / 2<..}}"
@@ -1078,9 +1078,9 @@
using \<open>closedin X C\<close> f1 closedin_subset by auto
qed (auto simp: disjnt_iff)
show ?thesis
- using assms
+ using assms *
unfolding completely_regular_space_def regular_space_def continuous_map_in_subtopology
- by (meson "*")
+ by metis
qed
@@ -4028,11 +4028,11 @@
have "closedin X {x}"
by (simp add: \<open>Hausdorff_space X\<close> closedin_Hausdorff_singleton \<open>x \<in> topspace X\<close>)
then obtain f where contf: "continuous_map X euclideanreal f"
- and f01: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> {0..1}" and fxy: "f y = 0" "f x = 1"
- using \<open>completely_regular_space X\<close> xy unfolding completely_regular_space_def
- by (smt (verit, ccfv_threshold) Diff_iff continuous_map_in_subtopology image_subset_iff singleton_iff)
+ and f01: "f \<in> topspace X \<rightarrow> {0..1}" and fxy: "f y = 0" "f x = 1"
+ using \<open>completely_regular_space X\<close> xy unfolding completely_regular_space_def Pi_iff continuous_map_in_subtopology image_subset_iff
+ by (metis Diff_iff empty_iff insert_iff)
then have "bounded (f ` topspace X)"
- by (meson bounded_closed_interval bounded_subset image_subset_iff)
+ by (metis bounded_closed_interval bounded_subset image_subset_iff_funcset)
with contf f01 have "restrict f (topspace X) \<in> K"
by (auto simp: K_def)
with fxy xy show ?thesis
@@ -4047,11 +4047,13 @@
fix x U
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}"
+ and gim: "g \<in> (topspace X - U) \<rightarrow> {1::real}"
using \<open>completely_regular_space X\<close> unfolding completely_regular_space_def
- by (metis Diff_iff openin_closedin_eq)
+ using Diff_iff openin_closedin_eq
+ by (metis image_subset_iff_funcset)
then have "bounded (g ` topspace X)"
- by (meson bounded_closed_interval bounded_subset continuous_map_in_subtopology)
+ by (meson bounded_closed_interval bounded_subset continuous_map_in_subtopology
+ image_subset_iff_funcset)
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"
@@ -4067,7 +4069,7 @@
have "e y (restrict g (topspace X)) \<in> {0..<1}"
using ey by (smt (verit, ccfv_SIG) PiE_mem g_in_K)
with gim g_in_K y \<open>y \<notin> U\<close> show ?thesis
- by (fastforce simp: e_def)
+ by (fastforce simp: e_def Pi_iff)
qed
ultimately
show "\<exists>W. openin (product_topology (\<lambda>f. top_of_set {0..1}) K) W \<and> e x \<in> W \<and> e' ` (e ` topspace X \<inter> W - {e x}) \<subseteq> U"
@@ -4120,7 +4122,7 @@
and g1: "\<And>t. t \<in> T \<Longrightarrow> g t ` S \<subseteq> {1}"
by metis
then have g01: "\<And>t. t \<in> T \<Longrightarrow> g t ` topspace X \<subseteq> {0..1}"
- by (meson continuous_map_in_subtopology)
+ by (meson continuous_map_in_subtopology image_subset_iff_funcset)
define G where "G \<equiv> \<lambda>t. {x \<in> topspace X. g t x \<in> {..<1/2}}"
have "Ball (G`T) (openin X)"
using contg unfolding G_def continuous_map_in_subtopology
@@ -4171,11 +4173,12 @@
define g where "g \<equiv> \<lambda>x. a + (b - a) * f x"
show thesis
proof
- have "\<forall>x\<in>topspace X. a + (b - a) * f x \<le> b"
- using contf \<open>a \<le> b\<close> apply (simp add: continuous_map_in_subtopology image_subset_iff)
- by (smt (verit, best) mult_right_le_one_le)
+ have "a + (b - a) * f i \<le> b" if "i \<in> topspace X" for i
+ using that contf \<open>a \<le> b\<close> affine_ineq [of "f i" a b]
+ unfolding continuous_map_in_subtopology continuous_map_upper_lower_semicontinuous_le_gen Pi_iff
+ by (simp add: algebra_simps)
then show "continuous_map X (top_of_set {a..b}) g"
- using contf \<open>a \<le> b\<close> unfolding g_def continuous_map_in_subtopology image_subset_iff
+ using contf \<open>a \<le> b\<close> unfolding g_def continuous_map_in_subtopology Pi_iff
by (intro conjI continuous_intros; simp)
show "g ` T \<subseteq> {a}" "g ` S \<subseteq> {b}"
using f0 f1 by (auto simp: g_def)
@@ -4193,7 +4196,7 @@
show thesis
proof
show "continuous_map X (top_of_set {a..b}) (uminus \<circ> f)"
- using contf by (auto simp: continuous_map_in_subtopology o_def)
+ using contf by (auto simp: continuous_map_in_subtopology o_def Pi_iff)
show "(uminus o f) ` T \<subseteq> {a}" "(uminus o f) ` S \<subseteq> {b}"
using fim by fastforce+
qed
@@ -4256,7 +4259,7 @@
proof
show "continuous_map (subtopology cube (e ` S)) X e'"
by (meson \<open>compactin X S\<close> compactin_subset_topspace conte' continuous_map_from_subtopology_mono image_mono)
- show "e' ` topspace (subtopology cube (e ` S)) \<subseteq> S"
+ show "e' \<in> topspace (subtopology cube (e ` S)) \<rightarrow> S"
using \<open>compactin X S\<close> compactin_subset_topspace e'e by fastforce
qed
qed (simp add: contf)--- a/src/HOL/Homology/Brouwer_Degree.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Homology/Brouwer_Degree.thy Sun Mar 23 22:33:19 2025 +0000
@@ -96,7 +96,7 @@
"hom_boundary p X S
\<in> hom (relative_homology_group p X S) (reduced_homology_group (p-1) (subtopology X S))"
proof -
- have *: "continuous_map X (discrete_topology {()}) (\<lambda>x. ())" "(\<lambda>x. ()) ` S \<subseteq> {()}"
+ have *: "continuous_map X (discrete_topology {()}) (\<lambda>x. ())" "(\<lambda>x. ()) \<in> S \<rightarrow> {()}"
by auto
interpret group_hom "relative_homology_group p (discrete_topology {()}) {()}"
"homology_group (p-1) (discrete_topology {()})"
@@ -435,33 +435,34 @@
lemma deformation_retraction_relative_homology_group_isomorphisms:
- "\<lbrakk>retraction_maps X Y r s; r ` U \<subseteq> V; s ` V \<subseteq> U; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X (s \<circ> r) id\<rbrakk>
+ "\<lbrakk>retraction_maps X Y r s; r \<in> U \<rightarrow> V; s \<in> V \<rightarrow> U; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X (s \<circ> r) id\<rbrakk>
\<Longrightarrow> group_isomorphisms (relative_homology_group p X U) (relative_homology_group p Y V)
(hom_induced p X U Y V r) (hom_induced p Y V X U s)"
apply (simp add: retraction_maps_def)
apply (rule homotopy_equivalence_relative_homology_group_isomorphisms)
- apply (auto simp: image_subset_iff continuous_map_compose homotopic_with_equal)
+ apply (auto simp: image_subset_iff_funcset Pi_iff continuous_map_compose homotopic_with_equal)
done
lemma deformation_retract_relative_homology_group_isomorphisms:
- "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r ` U \<subseteq> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
+ "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r \<in> U \<rightarrow> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
\<Longrightarrow> group_isomorphisms (relative_homology_group p X U) (relative_homology_group p Y V)
(hom_induced p X U Y V r) (hom_induced p Y V X U id)"
- by (simp add: deformation_retraction_relative_homology_group_isomorphisms)
+ by (simp add: deformation_retraction_relative_homology_group_isomorphisms
+ in_mono)
lemma deformation_retract_relative_homology_group_isomorphism:
- "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r ` U \<subseteq> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
+ "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r \<in> U \<rightarrow> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
\<Longrightarrow> (hom_induced p X U Y V r) \<in> iso (relative_homology_group p X U) (relative_homology_group p Y V)"
by (metis deformation_retract_relative_homology_group_isomorphisms group_isomorphisms_imp_iso)
lemma deformation_retract_relative_homology_group_isomorphism_id:
- "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r ` U \<subseteq> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
+ "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r \<in> U \<rightarrow> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
\<Longrightarrow> (hom_induced p Y V X U id) \<in> iso (relative_homology_group p Y V) (relative_homology_group p X U)"
by (metis deformation_retract_relative_homology_group_isomorphisms group_isomorphisms_imp_iso group_isomorphisms_sym)
lemma deformation_retraction_imp_isomorphic_relative_homology_groups:
- "\<lbrakk>retraction_maps X Y r s; r ` U \<subseteq> V; s ` V \<subseteq> U; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X (s \<circ> r) id\<rbrakk>
+ "\<lbrakk>retraction_maps X Y r s; r \<in> U \<rightarrow> V; s ` V \<subseteq> U; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X (s \<circ> r) id\<rbrakk>
\<Longrightarrow> relative_homology_group p X U \<cong> relative_homology_group p Y V"
by (blast intro: is_isoI group_isomorphisms_imp_iso deformation_retraction_relative_homology_group_isomorphisms)
@@ -471,7 +472,7 @@
by (simp add: deformation_retraction_imp_homotopy_equivalent_space homotopy_equivalent_space_imp_isomorphic_homology_groups)
lemma deformation_retract_imp_isomorphic_relative_homology_groups:
- "\<lbrakk>retraction_maps X X' r id; V \<subseteq> U; r ` U \<subseteq> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
+ "\<lbrakk>retraction_maps X X' r id; V \<subseteq> U; r \<in> U \<rightarrow> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
\<Longrightarrow> relative_homology_group p X U \<cong> relative_homology_group p X' V"
by (simp add: deformation_retraction_imp_isomorphic_relative_homology_groups)
@@ -482,7 +483,7 @@
lemma epi_hom_induced_inclusion:
- assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+ assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
shows "(hom_induced p (subtopology X S) {} X {} id)
\<in> epi (homology_group p (subtopology X S)) (homology_group p X)"
proof (rule epi_right_invertible)
@@ -493,14 +494,20 @@
\<in> carrier (homology_group p X) \<rightarrow> carrier (homology_group p (subtopology X S))"
by (simp add: hom_induced_carrier)
fix x
- assume "x \<in> carrier (homology_group p X)"
- then show "hom_induced p (subtopology X S) {} X {} id (hom_induced p X {} (subtopology X S) {} f x) = x"
- by (metis assms continuous_map_id_subt continuous_map_in_subtopology hom_induced_compose' hom_induced_id homology_homotopy_empty homotopic_with_imp_continuous_maps image_empty order_refl)
+ assume x: "x \<in> carrier (homology_group p X)"
+ show "hom_induced p (subtopology X S) {} X {} id (hom_induced p X {} (subtopology X S) {} f x) = x"
+ proof (subst hom_induced_compose')
+ show "continuous_map X (subtopology X S) f"
+ by (meson assms continuous_map_into_subtopology
+ homotopic_with_imp_continuous_maps)
+ show "hom_induced p X {} X {} (id \<circ> f) x = x"
+ by (metis assms(1) hom_induced_id homology_homotopy_empty id_comp x)
+ qed (use assms in auto)
qed
lemma trivial_homomorphism_hom_induced_relativization:
- assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+ assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
shows "trivial_homomorphism (homology_group p X) (relative_homology_group p X S)
(hom_induced p X {} X S id)"
proof -
@@ -514,7 +521,7 @@
lemma mon_hom_boundary_inclusion:
- assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+ assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
shows "(hom_boundary p X S) \<in> mon
(relative_homology_group p X S) (homology_group (p - 1) (subtopology X S))"
proof -
@@ -528,7 +535,7 @@
qed
lemma short_exact_sequence_hom_induced_relativization:
- assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+ assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
shows "short_exact_sequence (homology_group (p-1) X) (homology_group (p-1) (subtopology X S)) (relative_homology_group p X S)
(hom_induced (p-1) (subtopology X S) {} X {} id) (hom_boundary p X S)"
unfolding short_exact_sequence_iff
@@ -537,7 +544,7 @@
lemma group_isomorphisms_homology_group_prod_deformation:
fixes p::int
- assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+ assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
obtains H K where
"subgroup H (homology_group p (subtopology X S))"
"subgroup K (homology_group p (subtopology X S))"
@@ -561,15 +568,19 @@
have x: "short_exact_sequence (?pX) ?pXS ?rhs ?hi ?hb"
using short_exact_sequence_hom_induced_relativization [OF assms, of "p + 1"] by simp
have contf: "continuous_map X (subtopology X S) f"
- by (meson assms continuous_map_in_subtopology homotopic_with_imp_continuous_maps)
+ by (metis assms continuous_map_into_subtopology homotopic_with_imp_continuous_maps)
obtain H K where HK: "H \<lhd> ?pXS" "subgroup K ?pXS" "H \<inter> K \<subseteq> {one ?pXS}" "set_mult ?pXS H K = carrier ?pXS"
and iso: "?hb \<in> iso ?rhs (subgroup_generated ?pXS H)" "?hi \<in> iso (subgroup_generated ?pXS K) ?pX"
- apply (rule splitting_lemma_right [OF x, where g' = "hom_induced p X {} (subtopology X S) {} f"])
- apply (simp add: hom_induced_empty_hom)
- apply (simp add: contf hom_induced_compose')
- apply (metis (full_types) assms(1) hom_induced_id homology_homotopy_empty)
- apply blast
- done
+ proof (rule splitting_lemma_right [OF x, where g' = "hom_induced p X {} (subtopology X S) {} f"])
+ show "hom_induced p X {} (subtopology X S) {} f \<in> hom (homology_group p X) (homology_group p (subtopology X S))"
+ using hom_induced_empty_hom by blast
+ next
+ fix z
+ assume "z \<in> carrier (homology_group p X)"
+ then show "hom_induced p (subtopology X S) {} X {} id (hom_induced p X {} (subtopology X S) {} f z) = z"
+ using assms(1) contf hom_induced_id homology_homotopy_empty
+ by (fastforce simp add: hom_induced_compose')
+ qed blast
show ?thesis
proof
show "subgroup H ?pXS"
@@ -587,7 +598,7 @@
qed
lemma iso_homology_group_prod_deformation:
- assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+ assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
shows "homology_group p (subtopology X S)
\<cong> DirProd (homology_group p X) (relative_homology_group(p + 1) X S)"
(is "?G \<cong> DirProd ?H ?R")
@@ -613,7 +624,7 @@
assumes "contractible_space X" "S \<subseteq> topspace X" "S \<noteq> {}"
shows "homology_group 0 (subtopology X S) \<cong> DirProd integer_group (relative_homology_group(1) X S)"
proof -
- obtain f where "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+ obtain f where "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
using assms contractible_space_alt by fastforce
then have "homology_group 0 (subtopology X S) \<cong> homology_group 0 X \<times>\<times> relative_homology_group 1 X S"
using iso_homology_group_prod_deformation [of X _ S 0] by auto
@@ -911,7 +922,8 @@
qed
ultimately
have cmh: "continuous_map (prod_topology ?T01 ?X12) (nsphere n) h"
- by (subst (2) nsphere) (simp add: continuous_map_in_subtopology continuous_map_componentwise_UNIV)
+ proof (subst (2) nsphere)
+ qed (fastforce simp add: continuous_map_in_subtopology continuous_map_componentwise_UNIV)
have "hom_induced p (subtopology (nsphere n) {x. 0 \<le> x k})
(topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {x. x k = 0}) ?X12
(topspace ?X12 \<inter> {x. - 1/2 \<le> x k \<and> x k \<le> 0}) id
@@ -928,13 +940,13 @@
apply (auto simp: h_def Let_def)
done
show "continuous_map (subtopology (nsphere n) {x. 0 \<le> x k}) ?X12 id"
- by (simp add: continuous_map_in_subtopology) (auto simp: nsphere)
+ by (simp add: continuous_map_in_subtopology)
qed (simp add: nsphere h)
next
have h0: "\<And>xa. \<lbrakk>xa \<in> topspace (nsphere n); - (1/2) \<le> xa k; xa k \<le> 0\<rbrakk> \<Longrightarrow> h (0, xa) k = 0"
by (simp add: h_def Let_def)
- show "(h \<circ> (\<lambda>x. (0,x))) ` (topspace ?X12 \<inter> {x. - 1 / 2 \<le> x k \<and> x k \<le> 0})
- \<subseteq> topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {x. x k = 0}"
+ show "(h \<circ> (\<lambda>x. (0,x))) \<in> (topspace ?X12 \<inter> {x. - 1 / 2 \<le> x k \<and> x k \<le> 0})
+ \<rightarrow> topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {x. x k = 0}"
apply (auto simp: h0)
apply (rule subsetD [OF continuous_map_image_subset_topspace [OF cmh]])
apply (force simp: nsphere)
@@ -981,9 +993,8 @@
by (simp add: nsphere if_distrib [of "\<lambda>x. x ^ 2"] cong: if_cong)
show ?thesis
unfolding n
- apply (rule iso_relative_homology_of_contractible [where p = "1 + p", simplified])
- using contractible_space_upper_hemisphere ne apply blast+
- done
+ using iso_relative_homology_of_contractible [where p = "1 + p", simplified]
+ by (metis contractible_space_upper_hemisphere dual_order.refl empty_iff ne)
qed
corollary iso_reduced_homology_group_upper_hemisphere:
@@ -1090,10 +1101,8 @@
"\<lbrakk>\<exists>f \<in> iso G1 G2. \<forall>x \<in> carrier G1. r2(f x) = f(r1 x); \<exists>f \<in> iso G2 G3. \<forall>x \<in> carrier G2. r3(f x) = f(r2 x)\<rbrakk>
\<Longrightarrow> \<exists>f \<in> iso G1 G3. \<forall>x \<in> carrier G1. r3(f x) = f(r1 x)"
apply clarify
- apply (rename_tac g f)
- apply (rule_tac x="f \<circ> g" in bexI)
- apply (metis iso_iff comp_apply hom_in_carrier)
- using iso_set_trans by blast
+ by (smt (verit, ccfv_threshold) Group.iso_iff hom_in_carrier iso_set_trans
+ o_apply)
lemma reduced_homology_group_nsphere_step:
"\<exists>f \<in> iso(reduced_homology_group p (nsphere n))
@@ -1106,7 +1115,9 @@
define r where "r \<equiv> \<lambda>x::nat\<Rightarrow>real. \<lambda>i. if i = 0 then -x i else x i"
have cmr: "continuous_map (nsphere n) (nsphere n) r" for n
unfolding r_def by (rule continuous_map_nsphere_reflection)
- have rsub: "r ` {x. 0 \<le> x (Suc n)} \<subseteq> {x. 0 \<le> x (Suc n)}" "r ` {x. x (Suc n) \<le> 0} \<subseteq> {x. x (Suc n) \<le> 0}" "r ` {x. x (Suc n) = 0} \<subseteq> {x. x (Suc n) = 0}"
+ have rsub: "r \<in> {x. 0 \<le> x (Suc n)} \<rightarrow> {x. 0 \<le> x (Suc n)}"
+ "r \<in> {x. x (Suc n) \<le> 0} \<rightarrow> {x. x (Suc n) \<le> 0}"
+ "r \<in> {x. x (Suc n) = 0} \<rightarrow> {x. x (Suc n) = 0}"
by (force simp: r_def)+
let ?sub = "subtopology (nsphere (Suc n)) {x. x (Suc n) \<ge> 0}"
let ?G2 = "relative_homology_group (1 + p) ?sub {x. x (Suc n) = 0}"
@@ -1126,12 +1137,13 @@
fix c
assume "c \<in> carrier ?G2"
have cmrs: "continuous_map ?sub ?sub r"
- by (metis (mono_tags, lifting) IntE cmr continuous_map_from_subtopology continuous_map_in_subtopology image_subset_iff rsub(1) topspace_subtopology)
+ by (metis (no_types, lifting) IntE Pi_iff cmr continuous_map_from_subtopology
+ continuous_map_into_subtopology rsub(1) topspace_subtopology)
have "hom_induced p (nsphere n) {} (nsphere n) {} r \<circ> hom_boundary (1 + p) ?sub {x. x (Suc n) = 0}
= hom_boundary (1 + p) ?sub {x. x (Suc n) = 0} \<circ>
hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r"
using naturality_hom_induced [OF cmrs rsub(3), symmetric, of "1+p", simplified]
- by (simp add: subtopology_subtopology subtopology_nsphere_equator flip: Collect_conj_eq cong: rev_conj_cong)
+ by (simp add: Pi_iff subtopology_subtopology subtopology_nsphere_equator flip: Collect_conj_eq cong: rev_conj_cong)
then show "?j p n (?f c) = ?f (hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r c)"
by (metis comp_def)
next
@@ -1199,12 +1211,11 @@
then show ?thesis
by (simp add: nsphere)
qed
- have *: "reduced_homology_group p (subtopology (powertop_real UNIV) {?a, ?b}) \<cong>
+ have "t1_space (powertop_real UNIV)"
+ using t1_space_euclidean t1_space_product_topology by blast
+ then have *: "reduced_homology_group p (subtopology (powertop_real UNIV) {?a, ?b}) \<cong>
homology_group p (subtopology (powertop_real UNIV) {?a})"
- apply (rule reduced_homology_group_pair)
- apply (simp_all add: fun_eq_iff)
- apply (simp add: open_fun_def separation_t1 t1_space_def)
- done
+ by (intro reduced_homology_group_pair) (auto simp: fun_eq_iff)
have "reduced_homology_group 0 (nsphere 0) \<cong> integer_group" if "p=0"
proof -
have "reduced_homology_group 0 (nsphere 0) \<cong> homology_group 0 (top_of_set {?a})" if "p=0"
@@ -1352,9 +1363,9 @@
and aeq: "subgroup_generated ?G {a} = ?G"
using cyclic_reduced_homology_group_nsphere [of p p] by (auto simp: cyclic_group_def)
show ?thesis
- using hi [OF a]
- apply (simp add: Brouwer_degree2 a)
- by (metis Brouwer_degree2_iff a aeq f group.trivial_group_subgroup_generated group_reduced_homology_group subsetI trivial_reduced_homology_group_nsphere)
+ using hi [OF a] unfolding Brouwer_degree2 a
+ by (metis Brouwer_degree2_iff a aeq f group.trivial_group_subgroup_generated
+ group_reduced_homology_group subsetI trivial_reduced_homology_group_nsphere)
qed
lemma Brouwer_degree2_unique_generator:
@@ -1487,7 +1498,7 @@
then have he: "hom_induced p (nsphere p) {} (nsphere p) {} (\<lambda>x. a)
= hom_induced p (subtopology (nsphere p) {a}) {} (nsphere p) {} id \<circ>
hom_induced p (nsphere p) {} (subtopology (nsphere p) {a}) {} (\<lambda>x. a)"
- by (metis continuous_map_id_subt hom_induced_compose id_comp image_empty order_refl)
+ by (metis continuous_map_id_subt fun.map_id hom_induced_compose_empty)
have 1: "hom_induced p (nsphere p) {} (subtopology (nsphere p) {a}) {} (\<lambda>x. a) c =
\<one>\<^bsub>reduced_homology_group (int p) (subtopology (nsphere p) {a})\<^esub>"
using c trivial_reduced_homology_group_contractible_space [of "subtopology (nsphere p) {a}" p]
@@ -1586,11 +1597,12 @@
obtain d d' where d: "d \<in> carrier ?P" and d': "d' \<in> carrier ?N" and eqc: "?f(d,d') = c"
using c by (force simp flip: fim)
let ?h = "\<lambda>xx. hom_induced 0 (subtopology (nsphere 0) {xx}) {} (discrete_topology {()}) {} (\<lambda>x. ())"
- have "retraction_map (subtopology (nsphere 0) {pp}) (subtopology (nsphere 0) {nn}) r"
- apply (simp add: retraction_map_def retraction_maps_def continuous_map_in_subtopology continuous_map_from_subtopology cmr image_subset_iff)
- apply (rule_tac x=r in exI)
- apply (force simp: retraction_map_def retraction_maps_def continuous_map_in_subtopology continuous_map_from_subtopology cmr)
- done
+ have "continuous_map (subtopology (nsphere 0) {nn}) (nsphere 0) r"
+ using cmr continuous_map_from_subtopology by blast
+ then have "retraction_map (subtopology (nsphere 0) {pp}) (subtopology (nsphere 0) {nn}) r"
+ apply (simp add: retraction_map_def retraction_maps_def continuous_map_in_subtopology)
+ using \<open>r nn = pp\<close> \<open>r pp = nn\<close> cmr continuous_map_from_subtopology
+ by blast
then have "carrier ?N = (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r) ` carrier ?P"
by (rule surj_hom_induced_retraction_map)
then obtain e where e: "e \<in> carrier ?P" and eqd': "hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r e = d'"--- a/src/HOL/Homology/Homology_Groups.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Homology/Homology_Groups.thy Sun Mar 23 22:33:19 2025 +0000
@@ -379,19 +379,19 @@
by (metis hom_boundary)+
lemma hom_chain_map:
- "\<lbrakk>continuous_map X Y f; f ` S \<subseteq> T\<rbrakk>
+ "\<lbrakk>continuous_map X Y f; f \<in> S \<rightarrow> T\<rbrakk>
\<Longrightarrow> (chain_map p f) \<in> hom (relcycle_group p X S) (relcycle_group p Y T)"
- by (force simp: chain_map_add singular_relcycle_chain_map hom_def)
+ by (simp add: chain_map_add hom_def singular_relcycle_chain_map)
lemma hom_induced1:
"\<exists>hom_relmap.
(\<forall>p X S Y T f.
- continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T
+ continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T
\<longrightarrow> (hom_relmap p X S Y T f) \<in> hom (relative_homology_group (int p) X S)
(relative_homology_group (int p) Y T)) \<and>
(\<forall>p X S Y T f c.
- continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
+ continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
singular_relcycle p X S c
\<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c))"
@@ -399,7 +399,7 @@
have "\<exists>y. (y \<in> hom (relative_homology_group (int p) X S) (relative_homology_group (int p) Y T)) \<and>
(\<forall>c. singular_relcycle p X S c \<longrightarrow>
y (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c))"
- if contf: "continuous_map X Y f" and fim: "f ` (topspace X \<inter> S) \<subseteq> T"
+ if contf: "continuous_map X Y f" and fim: "f \<in> (topspace X \<inter> S) \<rightarrow> T"
for p X S Y T and f :: "'a \<Rightarrow> 'b"
proof -
let ?f = "(#>\<^bsub>relcycle_group p Y T\<^esub>) (singular_relboundary_set p Y T) \<circ> chain_map p f"
@@ -441,12 +441,12 @@
"\<exists>hom_relmap.
(\<forall>p X S Y T f.
continuous_map X Y f \<and>
- f ` (topspace X \<inter> S) \<subseteq> T
+ f \<in> (topspace X \<inter> S) \<rightarrow> T
\<longrightarrow> (hom_relmap p X S Y T f) \<in> hom (relative_homology_group p X S)
(relative_homology_group p Y T)) \<and>
(\<forall>p X S Y T f c.
continuous_map X Y f \<and>
- f ` (topspace X \<inter> S) \<subseteq> T \<and>
+ f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
singular_relcycle p X S c
\<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)) \<and>
@@ -464,13 +464,13 @@
lemma hom_induced3:
"\<exists>hom_relmap.
((\<forall>p X S Y T f c.
- ~(continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
+ ~(continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
c \<in> carrier(relative_homology_group p X S))
\<longrightarrow> hom_relmap p X S Y T f c = one(relative_homology_group p Y T)) \<and>
(\<forall>p X S Y T f.
hom_relmap p X S Y T f \<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)) \<and>
(\<forall>p X S Y T f c.
- continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and> singular_relcycle p X S c
+ continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and> singular_relcycle p X S c
\<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)) \<and>
(\<forall>p X S Y T.
@@ -486,24 +486,24 @@
moreover have "\<exists>x. ?P x \<and> ?Q x"
proof -
obtain hom_relmap:: "[int,'a topology,'a set,'b topology,'b set,'a \<Rightarrow> 'b,('a chain) set] \<Rightarrow> ('b chain) set"
- where 1: "\<And>p X S Y T f. \<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T\<rbrakk> \<Longrightarrow>
+ where 1: "\<And>p X S Y T f. \<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T\<rbrakk> \<Longrightarrow>
hom_relmap p X S Y T f
\<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)"
and 2: "\<And>p X S Y T f c.
- \<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T; singular_relcycle p X S c\<rbrakk>
+ \<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T; singular_relcycle p X S c\<rbrakk>
\<Longrightarrow>
hom_relmap (int p) X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)"
and 3: "(\<forall>p. p < 0 \<longrightarrow> hom_relmap p = (\<lambda>X S Y T f c. undefined))"
using hom_induced2 [where ?'a='a and ?'b='b]
- by (metis (mono_tags, lifting))
- have 4: "\<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T; c \<in> carrier (relative_homology_group p X S)\<rbrakk> \<Longrightarrow>
+ by (fastforce simp: Pi_iff)
+ have 4: "\<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T; c \<in> carrier (relative_homology_group p X S)\<rbrakk> \<Longrightarrow>
hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
\<in> carrier (relative_homology_group p Y T)"
for p X S Y f T c
using hom_carrier [OF 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]]
continuous_map_image_subset_topspace by fastforce
- have inhom: "(\<lambda>c. if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
+ have inhom: "(\<lambda>c. if continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
c \<in> carrier (relative_homology_group p X S)
then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
else \<one>\<^bsub>relative_homology_group p Y T\<^esub>)
@@ -522,16 +522,16 @@
show ?thesis
proof (cases "continuous_map X Y f")
case True
- then have "f ` (topspace X \<inter> S) \<subseteq> topspace Y"
+ then have "f \<in> (topspace X \<inter> S) \<rightarrow> topspace Y"
using continuous_map_image_subset_topspace by blast
then show ?thesis
using True False that
using 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]
- by (simp add: 4 continuous_map_image_subset_topspace hom_mult not_less group.is_monoid monoid.m_closed Int_left_absorb)
+ by (simp add: 4 Pi_iff continuous_map_funspace hom_mult not_less group.is_monoid monoid.m_closed Int_left_absorb)
qed (simp add: group.is_monoid)
qed
qed
- have hrel: "\<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T; singular_relcycle p X S c\<rbrakk>
+ have hrel: "\<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T; singular_relcycle p X S c\<rbrakk>
\<Longrightarrow> hom_relmap (int p) X (topspace X \<inter> S) Y (topspace Y \<inter> T)
f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
for p X S Y T f c
@@ -539,13 +539,14 @@
continuous_map_image_subset_topspace by fastforce
show ?thesis
apply (rule_tac x="\<lambda>p X S Y T f c.
- if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
+ if continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
c \<in> carrier(relative_homology_group p X S)
then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
else one(relative_homology_group p Y T)" in exI)
apply (simp add: Int_left_absorb subtopology_restrict carrier_relative_homology_group
- group.is_monoid group.restrict_hom_iff 4 inhom hrel cong: if_cong)
- apply (force simp: continuous_map_def intro!: ext)
+ group.is_monoid group.restrict_hom_iff 4 inhom hrel split: if_splits)
+ apply (intro ext strip)
+ apply (auto simp: continuous_map_def)
done
qed
ultimately show ?thesis
@@ -558,7 +559,7 @@
hom_induced:
"((\<forall>p X S Y T f c.
~(continuous_map X Y f \<and>
- f ` (topspace X \<inter> S) \<subseteq> T \<and>
+ f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
c \<in> carrier(relative_homology_group p X S))
\<longrightarrow> hom_induced p X (S::'a set) Y (T::'b set) f c =
one(relative_homology_group p Y T)) \<and>
@@ -567,7 +568,7 @@
(relative_homology_group p Y T)) \<and>
(\<forall>p X S Y T f c.
continuous_map X Y f \<and>
- f ` (topspace X \<inter> S) \<subseteq> T \<and>
+ f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
singular_relcycle p X S c
\<longrightarrow> hom_induced p X (S::'a set) Y (T::'b set) f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)) \<and>
@@ -581,7 +582,7 @@
by (fact hom_induced3)
lemma hom_induced_default:
- "~(continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and> c \<in> carrier(relative_homology_group p X S))
+ "~(continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and> c \<in> carrier(relative_homology_group p X S))
\<Longrightarrow> hom_induced p X S Y T f c = one(relative_homology_group p Y T)"
and hom_induced_hom:
"hom_induced p X S Y T f \<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)"
@@ -593,15 +594,15 @@
by (metis hom_induced)+
lemma hom_induced_chain_map_gen:
- "\<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T; singular_relcycle p X S c\<rbrakk>
+ "\<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T; singular_relcycle p X S c\<rbrakk>
\<Longrightarrow> hom_induced p X S Y T f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
by (metis hom_induced)
lemma hom_induced_chain_map:
- "\<lbrakk>continuous_map X Y f; f ` S \<subseteq> T; singular_relcycle p X S c\<rbrakk>
+ "\<lbrakk>continuous_map X Y f; f \<in> S \<rightarrow> T; singular_relcycle p X S c\<rbrakk>
\<Longrightarrow> hom_induced p X S Y T f (homologous_rel_set p X S c)
= homologous_rel_set p Y T (chain_map p f c)"
- by (meson Int_lower2 hom_induced image_subsetI image_subset_iff subset_iff)
+ by (simp add: Pi_iff hom_induced_chain_map_gen)
lemma hom_induced_eq:
@@ -619,10 +620,11 @@
case 2
have "hom_induced n X S Y T f C = hom_induced n X S Y T g C" for C
proof -
- have "continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and> C \<in> carrier (relative_homology_group n X S)
- \<longleftrightarrow> continuous_map X Y g \<and> g ` (topspace X \<inter> S) \<subseteq> T \<and> C \<in> carrier (relative_homology_group n X S)"
+ have "continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and> C \<in> carrier (relative_homology_group n X S)
+ \<longleftrightarrow> continuous_map X Y g \<and> g \<in> (topspace X \<inter> S) \<rightarrow> T \<and> C \<in> carrier (relative_homology_group n X S)"
(is "?P = ?Q")
- by (metis IntD1 assms continuous_map_eq image_cong)
+ using assms Pi_iff continuous_map_eq [of X Y]
+ by (smt (verit, ccfv_SIG) Int_iff)
then consider "\<not> ?P \<and> \<not> ?Q" | "?P \<and> ?Q"
by blast
then show ?thesis
@@ -633,18 +635,18 @@
next
case 2
have "homologous_rel_set n Y T (chain_map n f c) = homologous_rel_set n Y T (chain_map n g c)"
- if "continuous_map X Y f" "f ` (topspace X \<inter> S) \<subseteq> T"
- "continuous_map X Y g" "g ` (topspace X \<inter> S) \<subseteq> T"
+ if "continuous_map X Y f" "f \<in> (topspace X \<inter> S) \<rightarrow> T"
+ "continuous_map X Y g" "g \<in> (topspace X \<inter> S) \<rightarrow> T"
"C = homologous_rel_set n X S c" "singular_relcycle n X S c"
for c
proof -
have "chain_map n f c = chain_map n g c"
- using assms chain_map_eq singular_relcycle that by blast
+ using assms chain_map_eq singular_relcycle that by metis
then show ?thesis
by simp
qed
with 2 show ?thesis
- by (auto simp: relative_homology_group_def carrier_FactGroup
+ by (force simp: relative_homology_group_def carrier_FactGroup
right_coset_singular_relboundary hom_induced_chain_map_gen)
qed
qed
@@ -705,7 +707,7 @@
by (rule hom_induced_id_gen) auto
lemma hom_induced_compose:
- assumes "continuous_map X Y f" "f ` S \<subseteq> T" "continuous_map Y Z g" "g ` T \<subseteq> U"
+ assumes "continuous_map X Y f" "f \<in> S \<rightarrow> T" "continuous_map Y Z g" "g \<in> T \<rightarrow> U"
shows "hom_induced p X S Z U (g \<circ> f) = hom_induced p Y T Z U g \<circ> hom_induced p X S Y T f"
proof -
consider (neg) "p < 0" | (int) n where "p = int n"
@@ -715,7 +717,7 @@
case int
have gf: "continuous_map X Z (g \<circ> f)"
using assms continuous_map_compose by fastforce
- have gfim: "(g \<circ> f) ` S \<subseteq> U"
+ have gfim: "(g \<circ> f) \<in> S \<rightarrow> U"
unfolding o_def using assms by blast
have sr: "\<And>a. singular_relcycle n X S a \<Longrightarrow> singular_relcycle n Y T (chain_map n f a)"
by (simp add: assms singular_relcycle_chain_map)
@@ -727,7 +729,8 @@
case True
with gfim show ?thesis
unfolding int
- by (auto simp: carrier_relative_homology_group gf gfim assms sr chain_map_compose hom_induced_chain_map)
+ by (auto simp: carrier_relative_homology_group gf gfim assms
+ sr chain_map_compose hom_induced_chain_map)
next
case False
then show ?thesis
@@ -738,12 +741,12 @@
qed
lemma hom_induced_compose':
- assumes "continuous_map X Y f" "f ` S \<subseteq> T" "continuous_map Y Z g" "g ` T \<subseteq> U"
+ assumes "continuous_map X Y f" "f \<in> S \<rightarrow> T" "continuous_map Y Z g" "g \<in> T \<rightarrow> U"
shows "hom_induced p Y T Z U g (hom_induced p X S Y T f x) = hom_induced p X S Z U (g \<circ> f) x"
using hom_induced_compose [OF assms] by simp
lemma naturality_hom_induced:
- assumes "continuous_map X Y f" "f ` S \<subseteq> T"
+ assumes "continuous_map X Y f" "f \<in> S \<rightarrow> T"
shows "hom_boundary q Y T \<circ> hom_induced q X S Y T f
= hom_induced (q - 1) (subtopology X S) {} (subtopology Y T) {} f \<circ> hom_boundary q X S"
proof (cases "q \<le> 0")
@@ -767,7 +770,7 @@
using p1 by auto
have cbm: "(chain_boundary p (chain_map p f a))
= (chain_map (p - Suc 0) f (chain_boundary p a))"
- using a chain_boundary_chain_map singular_relcycle by blast
+ using a chain_boundary_chain_map singular_relcycle by metis
have contf: "continuous_map (subtopology X S) (subtopology Y T) f"
using assms
by (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology)
@@ -838,8 +841,9 @@
\<Longrightarrow> f ` A = f ` B" for f A B
by blast
have "?lhs = homologous_rel_set (Suc n) X S ` singular_relcycle_set (Suc n) X {}"
- using hom_induced_chain_map chain_map_ident [of _ X] singular_relcycle
- by (smt (verit) bot.extremum comp_apply continuous_map_id image_cong image_empty mem_Collect_eq)
+ using hom_induced_chain_map chain_map_ident [of _ X] singular_relcycle
+ by (smt (verit, best) comp_apply continuous_map_id empty_iff funcsetI
+ image_cong mem_Collect_eq)
also have "\<dots> = homologous_rel_set (Suc n) X S `
(singular_relcycle_set (Suc n) X S \<inter>
{c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)})"
@@ -849,7 +853,9 @@
then show "\<exists>y. y \<in> singular_relcycle_set (Suc n) X S \<inter>
{c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)} \<and>
homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S y"
- using singular_cycle singular_relcycle by (fastforce simp: singular_boundary)
+ using singular_cycle singular_relcycle
+ by (metis Int_Collect mem_Collect_eq singular_chain_0
+ singular_relboundary_0)
next
fix c
assume c: "c \<in> singular_relcycle_set (Suc n) X S \<inter>
@@ -956,15 +962,21 @@
have 2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> B \<and> f x = f y; \<And>x. x \<in> B \<Longrightarrow> \<exists>y. y \<in> A \<and> f x = f y\<rbrakk>
\<Longrightarrow> f ` A = f ` B" for f A B
by blast
- have "?lhs = homologous_rel_set n X {} ` (singular_relcycle_set n (subtopology X S) {})"
- by (smt (verit) chain_map_ident continuous_map_id_subt empty_subsetI hom_induced_chain_map image_cong image_empty image_image mem_Collect_eq singular_relcycle)
+ have "\<And>f. singular_chain n (subtopology X S) f \<and>
+ singular_chain (n - Suc 0) trivial_topology (chain_boundary n f) \<Longrightarrow>
+ hom_induced (int n) (subtopology X S) {} X {} id (homologous_rel_set n (subtopology X S) {} f) =
+ homologous_rel_set n X {} f"
+ by (auto simp: chain_map_ident hom_induced_chain_map singular_relcycle)
+ then have "?lhs = homologous_rel_set n X {} ` (singular_relcycle_set n (subtopology X S) {})"
+ by (simp add: singular_relcycle image_comp)
also have "\<dots> = homologous_rel_set n X {} ` (singular_relcycle_set n X {} \<inter> singular_relboundary_set n X S)"
proof (rule 2)
fix c
assume "c \<in> singular_relcycle_set n (subtopology X S) {}"
then show "\<exists>y. y \<in> singular_relcycle_set n X {} \<inter> singular_relboundary_set n X S \<and>
homologous_rel_set n X {} c = homologous_rel_set n X {} y"
- using singular_chain_imp_relboundary singular_cycle singular_relboundary_imp_chain singular_relcycle by fastforce
+ using singular_chain_imp_relboundary singular_relboundary_imp_chain
+ by (fastforce simp: singular_cycle)
next
fix c
assume "c \<in> singular_relcycle_set n X {} \<inter> singular_relboundary_set n X S"
@@ -1031,7 +1043,7 @@
proposition homology_homotopy_axiom:
- assumes "homotopic_with (\<lambda>h. h ` S \<subseteq> T) X Y f g"
+ assumes "homotopic_with (\<lambda>h. h \<in> S \<rightarrow> T) X Y f g"
shows "hom_induced p X S Y T f = hom_induced p X S Y T g"
proof (cases "p < 0")
case True
@@ -1043,7 +1055,7 @@
by (metis int_nat_eq not_le)
have cont: "continuous_map X Y f" "continuous_map X Y g"
using assms homotopic_with_imp_continuous_maps by blast+
- have im: "f ` (topspace X \<inter> S) \<subseteq> T" "g ` (topspace X \<inter> S) \<subseteq> T"
+ have im: "f \<in> (topspace X \<inter> S) \<rightarrow> T" "g \<in> (topspace X \<inter> S) \<rightarrow> T"
using homotopic_with_imp_property assms by blast+
show ?thesis
proof
@@ -1073,7 +1085,7 @@
then obtain n where peq: "p = int n"
by (metis int_nat_eq not_le)
have cont: "continuous_map (subtopology X (S - U)) (subtopology X S) id"
- by (simp add: closure_of_subtopology_mono continuous_map_eq_image_closure_subset)
+ by (meson Diff_subset continuous_map_from_subtopology_mono continuous_map_id)
have TU: "topspace X \<inter> (S - U) \<inter> (T - U) \<subseteq> T"
by auto
show ?thesis
@@ -1090,9 +1102,9 @@
(homologous_rel_set n (subtopology X (S - U)) (T - U) c)
= hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id
(homologous_rel_set n (subtopology X (S - U)) (T - U) d)"
- then have scc: "singular_chain n (subtopology X (S - U)) c"
+ then obtain scc: "singular_chain n (subtopology X (S - U)) c"
and scd: "singular_chain n (subtopology X (S - U)) d"
- using singular_relcycle by blast+
+ using singular_relcycle by metis
have "singular_relboundary n (subtopology X (S - U)) (T - U) c"
if srb: "singular_relboundary n (subtopology X S) T c"
and src: "singular_relcycle n (subtopology X (S - U)) (T - U) c" for c
@@ -1167,7 +1179,8 @@
"homologous_rel n (subtopology X S) T a c'"
using a by (blast intro: excised_relcycle_exists [OF assms])
then have scc': "singular_chain n (subtopology X S) c'"
- using homologous_rel_singular_chain singular_relcycle that by blast
+ using homologous_rel_singular_chain that
+ by (force simp: singular_relcycle)
then show ?thesis
using scc' chain_map_ident [of _ "subtopology X S"] c' homologous_rel_set_eq
by fastforce
@@ -1182,7 +1195,7 @@
homologous_rel_set n (subtopology X (S - U)) (T - U) `
singular_relcycle_set n (subtopology X (S - U)) (T - U)
= homologous_rel_set n (subtopology X S) T ` singular_relcycle_set n (subtopology X S) T"
- by (simp add: image_comp o_def hom_induced_chain_map_gen cont TU topspace_subtopology
+ by (simp add: image_comp o_def hom_induced_chain_map_gen cont TU
cong: image_cong_simp)
qed
qed
@@ -1776,10 +1789,10 @@
by (simp add: homology_homotopy_axiom)
lemma homotopy_equivalence_relative_homology_group_isomorphisms:
- assumes contf: "continuous_map X Y f" and fim: "f ` S \<subseteq> T"
- and contg: "continuous_map Y X g" and gim: "g ` T \<subseteq> S"
- and gf: "homotopic_with (\<lambda>h. h ` S \<subseteq> S) X X (g \<circ> f) id"
- and fg: "homotopic_with (\<lambda>k. k ` T \<subseteq> T) Y Y (f \<circ> g) id"
+ assumes contf: "continuous_map X Y f" and fim: "f \<in> S \<rightarrow> T"
+ and contg: "continuous_map Y X g" and gim: "g \<in> T \<rightarrow> S"
+ and gf: "homotopic_with (\<lambda>h. h \<in> S \<rightarrow> S) X X (g \<circ> f) id"
+ and fg: "homotopic_with (\<lambda>k. k \<in> T \<rightarrow> T) Y Y (f \<circ> g) id"
shows "group_isomorphisms (relative_homology_group p X S) (relative_homology_group p Y T)
(hom_induced p X S Y T f) (hom_induced p Y T X S g)"
unfolding group_isomorphisms_def
@@ -1799,10 +1812,10 @@
lemma homotopy_equivalence_relative_homology_group_isomorphism:
- assumes "continuous_map X Y f" and fim: "f ` S \<subseteq> T"
- and "continuous_map Y X g" and gim: "g ` T \<subseteq> S"
- and "homotopic_with (\<lambda>h. h ` S \<subseteq> S) X X (g \<circ> f) id"
- and "homotopic_with (\<lambda>k. k ` T \<subseteq> T) Y Y (f \<circ> g) id"
+ assumes "continuous_map X Y f" and fim: "f \<in> S \<rightarrow> T"
+ and "continuous_map Y X g" and gim: "g \<in> T \<rightarrow> S"
+ and "homotopic_with (\<lambda>h. h \<in> S \<rightarrow> S) X X (g \<circ> f) id"
+ and "homotopic_with (\<lambda>k. k \<in> T \<rightarrow> T) Y Y (f \<circ> g) id"
shows "(hom_induced p X S Y T f) \<in> iso (relative_homology_group p X S) (relative_homology_group p Y T)"
using homotopy_equivalence_relative_homology_group_isomorphisms [OF assms] group_isomorphisms_imp_iso
by metis
@@ -1816,10 +1829,10 @@
using assms by (intro homotopy_equivalence_relative_homology_group_isomorphism) auto
lemma homotopy_equivalent_space_imp_isomorphic_relative_homology_groups:
- assumes "continuous_map X Y f" and fim: "f ` S \<subseteq> T"
- and "continuous_map Y X g" and gim: "g ` T \<subseteq> S"
- and "homotopic_with (\<lambda>h. h ` S \<subseteq> S) X X (g \<circ> f) id"
- and "homotopic_with (\<lambda>k. k ` T \<subseteq> T) Y Y (f \<circ> g) id"
+ assumes "continuous_map X Y f" and fim: "f \<in> S \<rightarrow> T"
+ and "continuous_map Y X g" and gim: "g \<in> T \<rightarrow> S"
+ and "homotopic_with (\<lambda>h. h \<in> S \<rightarrow> S) X X (g \<circ> f) id"
+ and "homotopic_with (\<lambda>k. k \<in> T \<rightarrow> T) Y Y (f \<circ> g) id"
shows "relative_homology_group p X S \<cong> relative_homology_group p Y T"
using homotopy_equivalence_relative_homology_group_isomorphism [OF assms]
unfolding is_iso_def by blast
@@ -1871,7 +1884,7 @@
by (simp add: trivial_relative_homology_group_empty)
lemma homeomorphic_maps_relative_homology_group_isomorphisms:
- assumes "homeomorphic_maps X Y f g" and im: "f ` S \<subseteq> T" "g ` T \<subseteq> S"
+ assumes "homeomorphic_maps X Y f g" and im: "f \<in> S \<rightarrow> T" "g \<in> T \<rightarrow> S"
shows "group_isomorphisms (relative_homology_group p X S) (relative_homology_group p Y T)
(hom_induced p X S Y T f) (hom_induced p Y T X S g)"
proof -
@@ -1884,10 +1897,10 @@
(hom_induced p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f)
(hom_induced p Y (topspace Y \<inter> T) X (topspace X \<inter> S) g)"
proof (rule homotopy_equivalence_relative_homology_group_isomorphisms)
- show "homotopic_with (\<lambda>h. h ` (topspace X \<inter> S) \<subseteq> topspace X \<inter> S) X X (g \<circ> f) id"
+ show "homotopic_with (\<lambda>h. h \<in> (topspace X \<inter> S) \<rightarrow> topspace X \<inter> S) X X (g \<circ> f) id"
using fg im by (auto intro: homotopic_with_equal continuous_map_compose)
next
- show "homotopic_with (\<lambda>k. k ` (topspace Y \<inter> T) \<subseteq> topspace Y \<inter> T) Y Y (f \<circ> g) id"
+ show "homotopic_with (\<lambda>k. k \<in> (topspace Y \<inter> T) \<rightarrow> topspace Y \<inter> T) Y Y (f \<circ> g) id"
using fg im by (auto intro: homotopic_with_equal continuous_map_compose)
qed (use im fg in \<open>auto simp: continuous_map_def\<close>)
then show ?thesis
@@ -2197,21 +2210,23 @@
by (simp add: ext hom_boundary_carrier hom_induced_id hom_relboundary_def)
lemma naturality_hom_induced_relboundary:
- assumes "continuous_map X Y f" "f ` S \<subseteq> U" "f ` T \<subseteq> V"
+ assumes "continuous_map X Y f" "f \<in> S \<rightarrow> U" "f \<in> T \<rightarrow> V"
shows "hom_relboundary p Y U V \<circ>
hom_induced p X S Y (U) f =
hom_induced (p-1) (subtopology X S) T (subtopology Y U) V f \<circ>
hom_relboundary p X S T"
proof -
have [simp]: "continuous_map (subtopology X S) (subtopology Y U) f"
- using assms continuous_map_from_subtopology continuous_map_in_subtopology topspace_subtopology by fastforce
+ using assms continuous_map_from_subtopology continuous_map_in_subtopology topspace_subtopology
+ by (fastforce simp: Pi_iff)
have "hom_induced (p-1) (subtopology Y U) {} (subtopology Y U) V id \<circ>
hom_induced (p-1) (subtopology X S) {} (subtopology Y U) {} f
= hom_induced (p-1) (subtopology X S) T (subtopology Y U) V f \<circ>
hom_induced (p-1) (subtopology X S) {} (subtopology X S) T id"
using assms by (simp flip: hom_induced_compose)
with assms show ?thesis
- by (metis (no_types, lifting) fun.map_comp hom_relboundary_def naturality_hom_induced)
+ unfolding hom_relboundary_def
+ by (metis (no_types, lifting) ext fun.map_comp naturality_hom_induced)
qed
proposition homology_exactness_triple_1:
@@ -2222,7 +2237,7 @@
[hom_relboundary p X S T, hom_induced p X T X S id])"
(is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])")
proof -
- have iTS: "id ` T \<subseteq> S" and [simp]: "S \<inter> T = T"
+ have iTS: "id \<in> T \<rightarrow> S" and [simp]: "S \<inter> T = T"
using assms by auto
have "?h2 B \<in> kernel ?G2 ?G1 ?h1" for B
proof -
@@ -2291,7 +2306,7 @@
interpret comm_group "?G2"
by (rule abelian_relative_homology_group)
have "hom_induced p X T X S id (hom_induced p X {} X T id W) = hom_induced p X {} X S id W"
- by (simp add: assms hom_induced_compose')
+ using assms iTS by (simp add: hom_induced_compose')
then have "B = (?h2 \<circ> hom_induced p X {} X T id) W \<otimes>\<^bsub>?G2\<^esub> ?h2 D"
by (simp add: Bcarr Weq hb.G.m_assoc hom_induced_carrier)
then show "B = ?h2 ?W"
@@ -2314,14 +2329,14 @@
(is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])")
proof -
let ?H2 = "homology_group (p-1) (subtopology X S)"
- have iTS: "id ` T \<subseteq> S" and [simp]: "S \<inter> T = T"
+ have iTS: "id \<in> T \<rightarrow> S" and [simp]: "S \<inter> T = T"
using assms by auto
have "?h2 C \<in> kernel ?G2 ?G1 ?h1" for C
proof -
have "?h1 (?h2 C)
= (hom_induced (p-1) X {} X T id \<circ> hom_induced (p-1) (subtopology X S) {} X {} id \<circ> hom_boundary p X S) C"
unfolding hom_relboundary_def
- by (metis (no_types, lifting) comp_apply continuous_map_id continuous_map_id_subt empty_subsetI hom_induced_compose id_apply image_empty image_id order_refl)
+ by (metis Pi_empty comp_eq_dest_lhs continuous_map_id continuous_map_id_subt funcsetI hom_induced_compose' id_apply)
also have "\<dots> = \<one>\<^bsub>?G1\<^esub>"
proof -
have *: "hom_boundary p X S C \<in> carrier ?H2"
@@ -2349,7 +2364,8 @@
using that by (simp add: kernel_def)
moreover
have "hom_boundary (p-1) X T \<circ> hom_induced (p-1) (subtopology X S) T X T id = hom_boundary (p-1) (subtopology X S) T"
- by (metis Int_lower2 \<open>S \<inter> T = T\<close> continuous_map_id_subt hom_relboundary_def hom_relboundary_empty id_apply image_id naturality_hom_induced subtopology_subtopology)
+ by (metis funcsetI \<open>S \<inter> T = T\<close> continuous_map_id_subt hom_relboundary_def
+ hom_relboundary_empty id_apply naturality_hom_induced subtopology_subtopology)
then have "hom_boundary (p-1) (subtopology X S) T x = \<one>\<^bsub>homology_group (p - 2) (subtopology (subtopology X S) T)\<^esub>"
using naturality_hom_induced [of "subtopology X S" X id T T "p-1"] that
hom_one [OF hom_boundary_hom group_relative_homology_group group_relative_homology_group, of "p-1" X T]
@@ -2416,14 +2432,14 @@
[hom_induced p X T X S id, hom_induced p (subtopology X S) T X T id])"
(is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])")
proof -
- have iTS: "id ` T \<subseteq> S" and [simp]: "S \<inter> T = T"
+ have iTS: "id \<in> T \<rightarrow> S" and [simp]: "S \<inter> T = T"
using assms by auto
have 1: "?h2 x \<in> kernel ?G2 ?G1 ?h1" for x
proof -
have "?h1 (?h2 x)
= (hom_induced p (subtopology X S) S X S id \<circ>
hom_induced p (subtopology X S) T (subtopology X S) S id) x"
- by (metis comp_eq_dest_lhs continuous_map_id continuous_map_id_subt hom_induced_compose iTS id_apply image_subsetI)
+ by (simp add: hom_induced_compose' iTS)
also have "\<dots> = \<one>\<^bsub>relative_homology_group p X S\<^esub>"
proof -
have "trivial_group (relative_homology_group p (subtopology X S) S)"
@@ -2451,7 +2467,8 @@
have "hom_boundary p X S (hom_induced p X T X S id x)
= hom_induced (p-1) (subtopology X T) {} (subtopology X S) {} id
(hom_boundary p X T x)"
- using naturality_hom_induced [of X X id T S p] by (simp add: assms o_def) meson
+ using naturality_hom_induced [of X X id T S p] iTS
+ by (simp add: assms o_def) meson
with bcarr have "hom_boundary p X T x \<in> hom_boundary p (subtopology X S) T ` carrier ?G3"
using homology_exactness_axiom_2 [of p "subtopology X S" T] x
apply (simp add: kernel_def set_eq_iff subtopology_subtopology)
@@ -2467,8 +2484,9 @@
have yyy: "hom_boundary p X T y = \<one>\<^bsub>homology_group (p-1) (subtopology X T)\<^esub>"
apply (simp add: y_def bcarr xcarr hom_induced_carrier hom_boundary_carrier hb.inv_solve_right')
using naturality_hom_induced [of concl: p X T "subtopology X S" T id]
- by (smt (verit, best) \<open>S \<inter> T = T\<close> bcarr comp_eq_dest continuous_map_id_subt hom_induced_id id_apply
- image_subset_iff subtopology_subtopology ueq)
+ by (metis \<open>S \<inter> T = T\<close> comp_eq_dest_lhs continuous_map_id_subt
+ hom_relboundary_def hom_relboundary_empty id_apply image_id
+ image_subset_iff_funcset subsetI subtopology_subtopology ueq)
then have "y \<in> hom_induced p X {} X T id ` carrier (homology_group p X)"
using homology_exactness_axiom_1 [of p X T] x ycarr by (auto simp: kernel_def)
then obtain z where zcarr: "z \<in> carrier (homology_group p X)"
@@ -2478,7 +2496,7 @@
by (meson group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced)
have "hom_induced p X {} X S id z = (hom_induced p X T X S id \<circ> hom_induced p X {} X T id) z"
- by (simp add: assms flip: hom_induced_compose)
+ using iTS by (simp add: assms flip: hom_induced_compose)
also have "\<dots> = \<one>\<^bsub>relative_homology_group p X S\<^esub>"
using x 1 by (simp add: kernel_def zeq y_def)
finally have "hom_induced p X {} X S id z = \<one>\<^bsub>relative_homology_group p X S\<^esub>" .--- a/src/HOL/Homology/Invariance_of_Domain.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Homology/Invariance_of_Domain.thy Sun Mar 23 22:33:19 2025 +0000
@@ -9,8 +9,8 @@
theorem Borsuk_odd_mapping_degree_step:
assumes cmf: "continuous_map (nsphere n) (nsphere n) f"
- and f: "\<And>x. x \<in> topspace(nsphere n) \<Longrightarrow> (f \<circ> (\<lambda>x i. -x i)) x = ((\<lambda>x i. -x i) \<circ> f) x"
- and fim: "f ` (topspace(nsphere(n - Suc 0))) \<subseteq> topspace(nsphere(n - Suc 0))"
+ and f: "\<And>u. u \<in> topspace(nsphere n) \<Longrightarrow> (f \<circ> (\<lambda>x i. -x i)) u = ((\<lambda>x i. -x i) \<circ> f) u"
+ and fim: "f \<in> (topspace(nsphere(n - Suc 0))) \<rightarrow> topspace(nsphere(n - Suc 0))"
shows "even (Brouwer_degree2 n f - Brouwer_degree2 (n - Suc 0) f)"
proof (cases "n = 0")
case False
@@ -24,6 +24,8 @@
by (force simp: neg_def)
have equator_upper: "equator n \<subseteq> upper n"
by (force simp: equator_def upper_def)
+ then have [simp]: "id \<in> equator n \<rightarrow> upper n"
+ by force
have upper_usphere: "subtopology (nsphere n) (upper n) = usphere n"
by (simp add: usphere_def)
let ?rhgn = "relative_homology_group n (nsphere n)"
@@ -41,12 +43,13 @@
have subt_eq: "subtopology (nsphere n) {x. x n = 0} = nsphere (n - Suc 0)"
by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator)
then have equ: "subtopology (nsphere n) (equator n) = nsphere(n - Suc 0)"
- "subtopology (lsphere n) (equator n) = nsphere(n - Suc 0)"
- "subtopology (usphere n) (equator n) = nsphere(n - Suc 0)"
- using False by (auto simp: lsphere_def usphere_def equator_def lower_def upper_def subtopology_subtopology simp flip: Collect_conj_eq cong: rev_conj_cong)
+ "subtopology (lsphere n) (equator n) = nsphere(n - Suc 0)"
+ "subtopology (usphere n) (equator n) = nsphere(n - Suc 0)"
+ using False by (auto simp: lsphere_def usphere_def equator_def lower_def upper_def
+ subtopology_subtopology simp flip: Collect_conj_eq cong: rev_conj_cong)
have cmr: "continuous_map (nsphere(n - Suc 0)) (nsphere(n - Suc 0)) f"
- by (metis (no_types, lifting) IntE cmf fim continuous_map_from_subtopology continuous_map_in_subtopology equ(1) image_subset_iff topspace_subtopology)
-
+ by (metis cmf continuous_map_from_subtopology continuous_map_in_subtopology equ(1)
+ fim subtopology_restrict topspace_subtopology)
have "f x n = 0" if "x \<in> topspace (nsphere n)" "x n = 0" for x
proof -
have "x \<in> topspace (nsphere (n - Suc 0))"
@@ -56,7 +59,7 @@
ultimately show ?thesis
using fim by auto
qed
- then have fimeq: "f ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
+ then have fimeq: "f \<in> (topspace (nsphere n) \<inter> equator n) \<rightarrow> topspace (nsphere n) \<inter> equator n"
using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff)
have "\<And>k. continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. - x k)"
by (metis UNIV_I continuous_map_product_projection continuous_map_minus)
@@ -182,13 +185,13 @@
show "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id
\<in> Group.iso (relative_homology_group n (lsphere n) (equator n))
(?rhgn (upper n))"
- apply (simp add: lsphere_def usphere_def equator_def lower_def upper_def)
+ unfolding lsphere_def usphere_def equator_def lower_def upper_def
using iso_relative_homology_group_lower_hemisphere by blast
show "hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id
\<in> Group.iso (relative_homology_group n (usphere n) (equator n))
(?rhgn (lower n))"
- apply (simp_all add: lsphere_def usphere_def equator_def lower_def upper_def)
- using iso_relative_homology_group_upper_hemisphere by blast+
+ unfolding lsphere_def usphere_def equator_def lower_def upper_def
+ using iso_relative_homology_group_upper_hemisphere by blast
show "exact_seq
([?rhgn (lower n),
?rhgn (equator n),
@@ -383,7 +386,7 @@
by (simp add: ueq poweq hom_induced_compose' cmf flip: GH_hi.hom_int_pow Brouwer_degree2)
also have "\<dots> = hom_induced n (nsphere n) (topspace(nsphere n) \<inter> equator n) (nsphere n) (equator n) f
(hom_induced n (nsphere n) {} (nsphere n) (topspace(nsphere n) \<inter> equator n) id v)"
- using fimeq by (simp add: hom_induced_compose' cmf)
+ using fimeq by (simp add: hom_induced_compose' cmf Pi_iff)
also have "\<dots> = ?hi_ee f u"
by (metis hom_induced inf.left_idem ueq)
finally show ?thesis .
@@ -467,12 +470,13 @@
let ?TE = "topspace (nsphere n) \<inter> equator n"
have fneg: "(f \<circ> neg) x = (neg \<circ> f) x" if "x \<in> topspace (nsphere n)" for x
using f [OF that] by (force simp: neg_def)
- have neg_im: "neg ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
- by (metis cm_neg continuous_map_image_subset_topspace equ(1) topspace_subtopology)
+ have neg_im: "neg \<in> (topspace (nsphere n) \<inter> equator n) \<rightarrow> topspace (nsphere n) \<inter> equator n"
+ using cm_neg continuous_map_image_subset_topspace equator_def
+ by fastforce
have 1: "hom_induced n (nsphere n) ?TE (nsphere n) ?TE f \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg
= hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE f"
- using neg_im fimeq cm_neg cmf
- apply (simp add: flip: hom_induced_compose del: hom_induced_restrict)
+ using neg_im fimeq cm_neg cmf fneg
+ apply (simp flip: hom_induced_compose del: hom_induced_restrict)
using fneg by (auto intro: hom_induced_eq)
have "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \<otimes>\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
= un [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * a * Brouwer_degree2 (n - 1) neg)
@@ -577,18 +581,25 @@
if "squashable t U" "squashable t V" for U V t
unfolding homotopic_with_def
proof (intro exI conjI allI ballI)
- let ?h = "\<lambda>(z,x). ret ((1 - z) * t + z * x n) x"
- show "(\<lambda>x. ?h (u, x)) ` V \<subseteq> V" if "u \<in> {0..1}" for u
- using that
+ define h where "h \<equiv> \<lambda>(z,x). ret ((1 - z) * t + z * x n) x"
+ show "(\<lambda>x. h (u, x)) ` V \<subseteq> V" if "u \<in> {0..1}" for u
+ using that unfolding h_def
by clarsimp (metis squashableD [OF \<open>squashable t V\<close>] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
- have 1: "?h ` ({0..1} \<times> ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U)) \<subseteq> U"
- by clarsimp (metis squashableD [OF \<open>squashable t U\<close>] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
- show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U))
- (subtopology (Euclidean_space (Suc n)) U) ?h"
- apply (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology 1)
- apply (auto simp: case_prod_unfold ret_def continuous_map_componentwise_UNIV)
+ have "\<And>x y i. \<lbrakk>\<forall>k\<ge>Suc n. y k = 0; Suc n \<le> i\<rbrakk> \<Longrightarrow> ret ((1 - x) * t + x * y n) y i = 0"
+ by (simp add: ret_def)
+ then have "h \<in> {0..1} \<times> ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U) \<rightarrow> {x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U"
+ using squashableD [OF \<open>squashable t U\<close>] segment_bound_lemma
+ apply (clarsimp simp: h_def Pi_iff)
+ by (metis convex_bound_le eq_diff_eq ge_iff_diff_ge_0 linorder_le_cases)
+ moreover
+ have "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV)
+ ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U))) (powertop_real UNIV) h"
+ apply (auto simp: h_def case_prod_unfold ret_def continuous_map_componentwise_UNIV)
apply (intro continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd continuous_intros)
by (auto simp: cm_snd)
+ ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U))
+ (subtopology (Euclidean_space (Suc n)) U) h"
+ by (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology)
qed (auto simp: ret_def)
have cs_hi: "contractible_space(subtopology (Euclidean_space(Suc n)) hi)"
proof -
@@ -624,7 +635,7 @@
then have "ret 0 x \<in> topspace (Euclidean_space n)"
if "x \<in> topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x
using that by (metis continuous_map_image_subset_topspace image_subset_iff retraction_maps_def)
- then show "(ret 0) ` (lo \<inter> hi) \<subseteq> topspace (Euclidean_space n) - S"
+ then show "(ret 0) \<in> (lo \<inter> hi) \<rightarrow> topspace (Euclidean_space n) - S"
by (auto simp: local.cong ret_def hi_def lo_def)
show "homotopic_with (\<lambda>h. h ` (lo \<inter> hi) \<subseteq> lo \<inter> hi) (Euclidean_space (Suc n)) (Euclidean_space (Suc n)) (ret 0) id"
using hw_sub [OF squashable squashable_0_lohi] by simp
@@ -1836,11 +1847,13 @@
proof -
have *: "Euclidean_space n = subtopology (Euclidean_space m) (topspace(Euclidean_space n))"
by (metis Euclidean_space_def \<open>n \<le> m\<close> inf.absorb_iff2 subset_Euclidean_space subtopology_subtopology topspace_Euclidean_space)
+ then have "openin (Euclidean_space m) (f ` U)"
+ by (metis "*" U assms(4) cmf continuous_map_in_subtopology invariance_of_domain_Euclidean_space)
moreover have "U \<subseteq> topspace (subtopology (Euclidean_space m) U)"
by (metis U inf.absorb_iff2 openin_subset openin_subtopology openin_topspace)
ultimately show ?thesis
- by (metis (no_types) U \<open>inj_on f U\<close> cmf continuous_map_in_subtopology inf.absorb_iff2
- inf.orderE invariance_of_domain_Euclidean_space openin_imp_subset openin_subtopology openin_topspace)
+ by (metis "*" cmf continuous_map_image_subset_topspace dual_order.antisym
+ openin_imp_subset openin_topspace subset_openin_subtopology)
qed
corollary invariance_of_domain_Euclidean_space_embedding_map_gen:
@@ -2067,7 +2080,7 @@
lemma homeomorphic_maps_iff_homeomorphism [simp]:
"homeomorphic_maps (top_of_set S) (top_of_set T) f g \<longleftrightarrow> homeomorphism S T f g"
- unfolding homeomorphic_maps_def homeomorphism_def by force
+ by (force simp: Pi_iff homeomorphic_maps_def homeomorphism_def)
lemma homeomorphic_space_iff_homeomorphic [simp]:
"(top_of_set S) homeomorphic_space (top_of_set T) \<longleftrightarrow> S homeomorphic T"
@@ -2159,7 +2172,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes ope: "openin (top_of_set U) S"
and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
- and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> V"
and injf: "inj_on f S"
shows "openin (top_of_set V) (f ` S)"
proof -
@@ -2189,26 +2202,25 @@
have "continuous_on ({x. \<forall>i\<ge>dim U. x i = 0} \<inter> \<phi> ` S) \<phi>'"
if "continuous_on {x. \<forall>i\<ge>dim U. x i = 0} \<phi>'"
using that by (force elim: continuous_on_subset)
- moreover have "\<phi>' ` ({x. \<forall>i\<ge>dim U. x i = 0} \<inter> \<phi> ` S) \<subseteq> S"
+ moreover have "\<phi>' \<in> ({x. \<forall>i\<ge>dim U. x i = 0} \<inter> \<phi> ` S) \<rightarrow> S"
if "\<forall>x\<in>U. \<phi>' (\<phi> x) = x"
using that \<open>S \<subseteq> U\<close> by fastforce
ultimately show "continuous_map (subtopology (Euclidean_space (dim U)) (\<phi> ` S)) (top_of_set S) \<phi>'"
using hom unfolding homeomorphic_maps_def
- by (simp add: Euclidean_space_def subtopology_subtopology euclidean_product_topology)
+ by (simp add: Euclidean_space_def subtopology_subtopology euclidean_product_topology)
show "continuous_map (top_of_set S) (top_of_set V) f"
by (simp add: contf fim)
show "continuous_map (top_of_set V) (Euclidean_space (dim V)) \<psi>"
by (simp add: \<psi> homeomorphic_imp_continuous_map)
qed
show "inj_on (\<psi> \<circ> f \<circ> \<phi>') (\<phi> ` S)"
- using injf hom
- unfolding inj_on_def homeomorphic_maps_map
- by simp (metis \<open>S \<subseteq> U\<close> \<psi>'\<psi> fim imageI subsetD)
+ using injf hom \<open>S \<subseteq> U\<close> \<psi>'\<psi> fim
+ by (simp add: inj_on_def homeomorphic_maps_map Pi_iff) (metis subsetD)
qed
ultimately have "openin (Euclidean_space (dim V)) (\<psi> ` f ` S)"
by (simp add: image_comp)
- then show ?thesis
- by (simp add: fim homeomorphic_map_openness_eq [OF \<psi>])
+ with fim show ?thesis
+ by (auto simp: homeomorphic_map_openness_eq [OF \<psi>])
qed
lemma invariance_of_domain:
@@ -2279,7 +2291,7 @@
by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
- show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
+ show "((+) (- b) \<circ> f \<circ> (+) a) \<in> (+) (- a) ` S \<rightarrow> (+) (- b) ` V"
using fim by auto
show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
by (auto simp: inj_on_def) (meson inj_onD injf)--- a/src/HOL/Homology/Simplices.thy Sun Mar 23 17:07:55 2025 +0100
+++ b/src/HOL/Homology/Simplices.thy Sun Mar 23 22:33:19 2025 +0000
@@ -87,7 +87,7 @@
unfolding g_def continuous_map_componentwise
by (force intro: continuous_intros)
moreover
- have "g x y ` {0..1} \<subseteq> standard_simplex p" "g x y 0 = x" "g x y 1 = y"
+ have "g x y \<in> {0..1} \<rightarrow> standard_simplex p" "g x y 0 = x" "g x y 1 = y"
if "x \<in> standard_simplex p" "y \<in> standard_simplex p" for x y
using that by (auto simp: convex_standard_simplex g_def)
ultimately
@@ -183,7 +183,7 @@
shows "singular_simplex (p - Suc 0) X (singular_face p k f)"
proof -
let ?PT = "(powertop_real UNIV)"
- have 0: "simplical_face k ` standard_simplex (p - Suc 0) \<subseteq> standard_simplex p"
+ have 0: "simplical_face k \<in> standard_simplex (p - Suc 0) \<rightarrow> standard_simplex p"
using assms simplical_face_in_standard_simplex by auto
have 1: "continuous_map (subtopology ?PT (standard_simplex (p - Suc 0)))
(subtopology ?PT (standard_simplex p))
@@ -341,8 +341,8 @@
subsection\<open>Relative cycles $Z_pX (S)$ where $X$ is a topology and $S$ a subset \<close>
definition singular_relcycle :: "nat \<Rightarrow> 'a topology \<Rightarrow> 'a set \<Rightarrow> ('a chain) \<Rightarrow> bool"
- where "singular_relcycle p X S \<equiv>
- \<lambda>c. singular_chain p X c \<and> (chain_boundary p c, 0) \<in> mod_subset (p-1) (subtopology X S)"
+ where "singular_relcycle \<equiv>
+ \<lambda>p X S c. singular_chain p X c \<and> (chain_boundary p c, 0) \<in> mod_subset (p-1) (subtopology X S)"
abbreviation singular_relcycle_set
where "singular_relcycle_set p X S \<equiv> Collect (singular_relcycle p X S)"
@@ -357,8 +357,8 @@
qed
lemma singular_relcycle:
- "singular_relcycle p X S c \<longleftrightarrow>
- singular_chain p X c \<and> singular_chain (p-1) (subtopology X S) (chain_boundary p c)"
+ "singular_relcycle \<equiv>
+ \<lambda>p X S c. singular_chain p X c \<and> singular_chain (p-1) (subtopology X S) (chain_boundary p c)"
by (simp add: singular_relcycle_def mod_subset_def)
lemma singular_relcycle_0 [simp]: "singular_relcycle p X S 0"
@@ -777,7 +777,7 @@
\<Longrightarrow> chain_map p f c = c"
unfolding singular_chain_def
by (erule frag_induction) (auto simp: chain_map_diff simplex_map_id_gen)
-
+
lemma chain_map_ident:
"singular_chain p X c \<Longrightarrow> chain_map p id c = c"
by (simp add: chain_map_id_gen)
@@ -831,19 +831,20 @@
qed auto
lemma singular_relcycle_chain_map:
- assumes "singular_relcycle p X S c" "continuous_map X X' g" "g ` S \<subseteq> T"
+ assumes "singular_relcycle p X S c" "continuous_map X X' g" "g \<in> S \<rightarrow> T"
shows "singular_relcycle p X' T (chain_map p g c)"
proof -
have "continuous_map (subtopology X S) (subtopology X' T) g"
using assms
- using continuous_map_from_subtopology continuous_map_in_subtopology topspace_subtopology by fastforce
+ by (metis Pi_anti_mono continuous_map_from_subtopology continuous_map_in_subtopology
+ openin_imp_subset openin_topspace subsetD)
then show ?thesis
using chain_boundary_chain_map [of p X c g]
by (metis One_nat_def assms(1) assms(2) singular_chain_chain_map singular_relcycle)
qed
lemma singular_relboundary_chain_map:
- assumes "singular_relboundary p X S c" "continuous_map X X' g" "g ` S \<subseteq> T"
+ assumes "singular_relboundary p X S c" "continuous_map X X' g" "g \<in> S \<rightarrow> T"
shows "singular_relboundary p X' T (chain_map p g c)"
proof -
obtain d e where d: "singular_chain (Suc p) X d"
@@ -853,10 +854,11 @@
using assms(2) d singular_chain_chain_map by blast
moreover have "singular_chain p (subtopology X' T) (chain_map p g e)"
proof -
- have "\<forall>t. g ` topspace (subtopology t S) \<subseteq> T"
- by (metis assms(3) closure_of_subset_subtopology closure_of_topspace dual_order.trans image_mono)
+ have "\<And>Y. g \<in> topspace (subtopology Y S) \<rightarrow> T"
+ using assms(3) by auto
then show ?thesis
- by (meson assms(2) continuous_map_from_subtopology continuous_map_in_subtopology e singular_chain_chain_map)
+ by (metis assms(2) continuous_map_from_subtopology continuous_map_into_subtopology e
+ singular_chain_chain_map)
qed
moreover have "chain_boundary (Suc p) (chain_map (Suc p) g d) + chain_map p g e =
chain_map p g (chain_boundary (Suc p) d + e)"
@@ -1705,7 +1707,7 @@
proof
assume ?lhs
then show ?rhs
- by (simp add: simplicial_simplex_def singular_simplex_def continuous_map_in_subtopology set_mp)
+ by (simp add: simplicial_simplex)
next
assume R: ?rhs
then have cm: "continuous_map
@@ -1777,7 +1779,7 @@
have "(\<lambda>i. \<Sum>j\<le>p. m j i * x j) \<in> standard_simplex q"
if "x \<in> standard_simplex p" for x
using that m unfolding oriented_simplex_def singular_simplex_def
- by (auto simp: continuous_map_in_subtopology image_subset_iff)
+ by (auto simp: continuous_map_in_subtopology Pi_iff)
then show ?thesis
unfolding oriented_simplex_def simplex_map_def
apply (rule_tac x="\<lambda>j k. (\<Sum>i\<le>q. l i k * m j i)" in exI)
@@ -1785,7 +1787,7 @@
done
qed
then show ?case
- using f one
+ using f one
apply (simp add: simplicial_simplex_def)
using singular_simplex_def singular_simplex_simplex_map by blast
next
@@ -2492,7 +2494,7 @@
and X: "topspace X \<subseteq> \<Union>\<C>"
and p: "singular_chain p X c"
obtains n where "\<And>m f. \<lbrakk>n \<le> m; f \<in> Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\<rbrakk>
- \<Longrightarrow> \<exists>V \<in> \<C>. f ` (standard_simplex p) \<subseteq> V"
+ \<Longrightarrow> \<exists>V \<in> \<C>. f \<in> (standard_simplex p) \<rightarrow> V"
proof (cases "c = 0")
case False
then show ?thesis
@@ -2511,7 +2513,7 @@
case False
have "\<exists>e. 0 < e \<and>
(\<forall>K. K \<subseteq> standard_simplex p \<longrightarrow> (\<forall>x y i. x \<in> K \<and> y \<in> K \<and> i \<le> p \<longrightarrow> \<bar>x i - y i\<bar> \<le> e)
- \<longrightarrow> (\<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V))"
+ \<longrightarrow> (\<exists>V. V \<in> \<C> \<and> f \<in> K \<rightarrow> V))"
if f: "f \<in> Poly_Mapping.keys c" for f
proof -
have ssf: "singular_simplex p X f"
@@ -2551,19 +2553,19 @@
and Kd: "\<forall>x y i. x \<in> K \<and> y \<in> K \<and> i \<le> p \<longrightarrow> \<bar>x i - y i\<bar> \<le> d"
then have "\<exists>U. U \<in> g ` \<C> \<and> K \<subseteq> U"
using d [OF K] by auto
- then show "\<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
+ then show "\<exists>V. V \<in> \<C> \<and> f \<in> K \<rightarrow> V"
using K geq by fastforce
qed (rule \<open>d > 0\<close>)
qed
then obtain \<psi> where epos: "\<forall>f \<in> Poly_Mapping.keys c. 0 < \<psi> f"
and e: "\<And>f K. \<lbrakk>f \<in> Poly_Mapping.keys c; K \<subseteq> standard_simplex p;
\<And>x y i. x \<in> K \<and> y \<in> K \<and> i \<le> p \<Longrightarrow> \<bar>x i - y i\<bar> \<le> \<psi> f\<rbrakk>
- \<Longrightarrow> \<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
+ \<Longrightarrow> \<exists>V. V \<in> \<C> \<and> f \<in> K \<rightarrow> V"
by metis
obtain d where "0 < d"
and d: "\<And>f K. \<lbrakk>f \<in> Poly_Mapping.keys c; K \<subseteq> standard_simplex p;
\<And>x y i. \<lbrakk>x \<in> K; y \<in> K; i \<le> p\<rbrakk> \<Longrightarrow> \<bar>x i - y i\<bar> \<le> d\<rbrakk>
- \<Longrightarrow> \<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
+ \<Longrightarrow> \<exists>V. V \<in> \<C> \<and> f \<in> K \<rightarrow> V"
proof
show "Inf (\<psi> ` Poly_Mapping.keys c) > 0"
by (simp add: finite_less_Inf_iff \<open>c \<noteq> 0\<close> epos)
@@ -2572,7 +2574,7 @@
and le: "\<And>x y i. \<lbrakk>x \<in> K; y \<in> K; i \<le> p\<rbrakk> \<Longrightarrow> \<bar>x i - y i\<bar> \<le> Inf (\<psi> ` Poly_Mapping.keys c)"
then have lef: "Inf (\<psi> ` Poly_Mapping.keys c) \<le> \<psi> f"
by (auto intro: cInf_le_finite)
- show "\<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
+ show "\<exists>V. V \<in> \<C> \<and> f \<in> K \<rightarrow> V"
using le lef by (blast intro: dual_order.trans e [OF fK])
qed
let ?d = "\<lambda>m. (simplicial_subdivision p ^^ m) (frag_of (restrict id (standard_simplex p)))"
@@ -2626,9 +2628,9 @@
then have "\<bar>x i - y i\<bar> \<le> d"
if "x \<in> g ` (standard_simplex p)" "y \<in> g ` (standard_simplex p)" "i \<le> p" for i x y
using that by blast
- ultimately show "\<exists>V\<in>\<C>. h ` standard_simplex p \<subseteq> V"
+ ultimately show "\<exists>V\<in>\<C>. h \<in> standard_simplex p \<rightarrow> V"
using \<open>f \<in> Poly_Mapping.keys c\<close> d [of f "g ` standard_simplex p"]
- by (simp add: Bex_def heq image_image)
+ using heq image_subset_iff_funcset by fastforce
qed
qed
qed
@@ -2640,13 +2642,13 @@
and X: "topspace X \<subseteq> \<Union>\<C>"
and p: "singular_relcycle p X S c"
obtains c' where "singular_relcycle p X S c'" "homologous_rel p X S c c'"
- "\<And>f. f \<in> Poly_Mapping.keys c' \<Longrightarrow> \<exists>V \<in> \<C>. f ` (standard_simplex p) \<subseteq> V"
+ "\<And>f. f \<in> Poly_Mapping.keys c' \<Longrightarrow> \<exists>V \<in> \<C>. f \<in> (standard_simplex p) \<rightarrow> V"
proof -
have "singular_chain p X c"
"(chain_boundary p c, 0) \<in> (mod_subset (p - Suc 0) (subtopology X S))"
using p unfolding singular_relcycle_def by auto
then obtain n where n: "\<And>m f. \<lbrakk>n \<le> m; f \<in> Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\<rbrakk>
- \<Longrightarrow> \<exists>V \<in> \<C>. f ` (standard_simplex p) \<subseteq> V"
+ \<Longrightarrow> \<exists>V \<in> \<C>. f \<in> (standard_simplex p) \<rightarrow> V"
by (blast intro: sufficient_iterated_singular_subdivision_exists [OF \<C> X])
let ?c' = "(singular_subdivision p ^^ n) c"
show ?thesis
@@ -2665,7 +2667,7 @@
next
fix f :: "(nat \<Rightarrow> real) \<Rightarrow> 'a"
assume "f \<in> Poly_Mapping.keys ?c'"
- then show "\<exists>V\<in>\<C>. f ` standard_simplex p \<subseteq> V"
+ then show "\<exists>V\<in>\<C>. f \<in> (standard_simplex p) \<rightarrow> V"
by (rule n [OF order_refl])
qed
qed
@@ -2685,7 +2687,7 @@
for p X c S and T U :: "'a set"
proof -
obtain n where n: "\<And>m f. \<lbrakk>n \<le> m; f \<in> Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\<rbrakk>
- \<Longrightarrow> \<exists>V \<in> {S \<inter> X interior_of T, S - X closure_of U}. f ` standard_simplex p \<subseteq> V"
+ \<Longrightarrow> \<exists>V \<in> {S \<inter> X interior_of T, S - X closure_of U}. f \<in> (standard_simplex p) \<rightarrow> V"
apply (rule sufficient_iterated_singular_subdivision_exists
[of "{S \<inter> X interior_of T, S - X closure_of U}"])
using X S c
@@ -2791,7 +2793,7 @@
subsection\<open>Homotopy invariance\<close>
theorem homotopic_imp_homologous_rel_chain_maps:
- assumes hom: "homotopic_with (\<lambda>h. h ` T \<subseteq> V) S U f g" and c: "singular_relcycle p S T c"
+ assumes hom: "homotopic_with (\<lambda>h. h \<in> T \<rightarrow> V) S U f g" and c: "singular_relcycle p S T c"
shows "homologous_rel p U V (chain_map p f c) (chain_map p g c)"
proof -
note sum.atMost_Suc [simp del]