--- a/src/HOL/Analysis/Abstract_Topology.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Tue Mar 26 17:01:55 2019 +0000
@@ -1609,6 +1609,8 @@
qed
qed (auto simp: continuous_map_on_empty)
+declare continuous_map_const [THEN iffD2, continuous_intros]
+
lemma continuous_map_compose:
assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
shows "continuous_map X X'' (g \<circ> f)"
@@ -3773,6 +3775,13 @@
shows "closedin (top_of_set S) (S \<inter> f -` T)"
using assms continuous_on_closed by blast
+lemma continuous_map_subtopology_eu [simp]:
+ "continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
+ apply safe
+ apply (metis continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
+ apply (simp add: continuous_map_closedin_preimage_eq image_subset_iff)
+ by (metis (no_types, hide_lams) continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
+
subsection%unimportant \<open>Half-global and completely global cases\<close>
lemma continuous_openin_preimage_gen:
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Mar 26 17:01:55 2019 +0000
@@ -49,10 +49,10 @@
assumes ts: "T retract_of S"
and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
continuous_on U g; g ` U \<subseteq> S\<rbrakk>
- \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
+ \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g"
and "continuous_on U f" "f ` U \<subseteq> T"
and "continuous_on U g" "g ` U \<subseteq> T"
- shows "homotopic_with (\<lambda>x. True) U T f g"
+ shows "homotopic_with_canon (\<lambda>x. True) U T f g"
proof -
obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
using ts by (auto simp: retract_of_def retraction)
@@ -69,9 +69,9 @@
lemma retract_of_homotopically_trivial_null:
assumes ts: "T retract_of S"
and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
- \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
+ \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c)"
and "continuous_on U f" "f ` U \<subseteq> T"
- obtains c where "homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)"
proof -
obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
using ts by (auto simp: retract_of_def retraction)
@@ -98,8 +98,8 @@
by (metis locally_compact_closedin closedin_retract)
lemma homotopic_into_retract:
- "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with (\<lambda>x. True) S U f g\<rbrakk>
- \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
+ "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> 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, clarify)
apply (rule_tac x="r \<circ> h" in exI)
@@ -122,24 +122,24 @@
lemma deformation_retract_imp_homotopy_eqv:
fixes S :: "'a::euclidean_space set"
- assumes "homotopic_with (\<lambda>x. True) S S id r" and r: "retraction S T r"
+ assumes "homotopic_with_canon (\<lambda>x. True) S S id r" and r: "retraction S T r"
shows "S homotopy_eqv T"
proof -
- have "homotopic_with (\<lambda>x. True) S S (id \<circ> r) id"
+ have "homotopic_with_canon (\<lambda>x. True) S S (id \<circ> r) id"
by (simp add: assms(1) homotopic_with_symD)
- moreover have "homotopic_with (\<lambda>x. True) T T (r \<circ> id) id"
+ moreover have "homotopic_with_canon (\<lambda>x. True) T T (r \<circ> id) id"
using r unfolding retraction_def
- by (metis (no_types, lifting) comp_id continuous_on_id' homotopic_with_equal homotopic_with_symD id_def image_id order_refl)
+ by (metis eq_id_iff homotopic_with_id2 topspace_euclidean_subtopology)
ultimately
show ?thesis
- unfolding homotopy_eqv_def
- by (metis continuous_on_id' id_def image_id r retraction_def)
+ unfolding homotopy_equivalent_space_def
+ by (metis (no_types, lifting) continuous_map_subtopology_eu continuous_on_id' id_def image_id r retraction_def)
qed
lemma deformation_retract:
fixes S :: "'a::euclidean_space set"
- shows "(\<exists>r. homotopic_with (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow>
- T retract_of S \<and> (\<exists>f. homotopic_with (\<lambda>x. True) S S id f \<and> f ` S \<subseteq> T)"
+ shows "(\<exists>r. homotopic_with_canon (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow>
+ T retract_of S \<and> (\<exists>f. homotopic_with_canon (\<lambda>x. True) S S id f \<and> f ` S \<subseteq> T)"
(is "?lhs = ?rhs")
proof
assume ?lhs
@@ -160,11 +160,11 @@
lemma deformation_retract_of_contractible_sing:
fixes S :: "'a::euclidean_space set"
assumes "contractible S" "a \<in> S"
- obtains r where "homotopic_with (\<lambda>x. True) S S id r" "retraction S {a} r"
+ obtains r where "homotopic_with_canon (\<lambda>x. True) S S id r" "retraction S {a} r"
proof -
have "{a} retract_of S"
by (simp add: \<open>a \<in> S\<close>)
- moreover have "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
+ moreover have "homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
using assms
by (auto simp: contractible_def homotopic_into_contractible image_subset_iff)
moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
@@ -3392,7 +3392,7 @@
and arelS: "a \<in> rel_interior S"
and relS: "rel_frontier S \<subseteq> T"
and affS: "T \<subseteq> affine hull S"
- obtains r where "homotopic_with (\<lambda>x. True) (T - {a}) (T - {a}) id r"
+ obtains r where "homotopic_with_canon (\<lambda>x. True) (T - {a}) (T - {a}) id r"
"retraction (T - {a}) (rel_frontier S) r"
proof -
have "\<exists>d. 0 < d \<and> (a + d *\<^sub>R l) \<in> rel_frontier S \<and>
@@ -3466,7 +3466,7 @@
by (blast intro: continuous_on_subset)
show ?thesis
proof
- show "homotopic_with (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+ show "homotopic_with_canon (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
proof (rule homotopic_with_linear)
show "continuous_on (T - {a}) id"
by (intro continuous_intros continuous_on_compose)
@@ -3560,8 +3560,7 @@
apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S T])
using assms
apply auto
- apply (subst homotopy_eqv_sym)
- using deformation_retract_imp_homotopy_eqv by blast
+ using deformation_retract_imp_homotopy_eqv homotopy_equivalent_space_sym by blast
lemma homotopy_eqv_rel_frontier_punctured_affine_hull:
fixes S :: "'a::euclidean_space set"
@@ -3600,7 +3599,7 @@
lemma Borsuk_maps_homotopic_in_path_component:
assumes "path_component (- s) a b"
- shows "homotopic_with (\<lambda>x. True) s (sphere 0 1)
+ shows "homotopic_with_canon (\<lambda>x. True) s (sphere 0 1)
(\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a))
(\<lambda>x. inverse(norm(x - b)) *\<^sub>R (x - b))"
proof -
@@ -4128,8 +4127,8 @@
and anr: "(ANR S \<and> ANR T) \<or> ANR U"
and contf: "continuous_on T f"
and "f ` T \<subseteq> U"
- and "homotopic_with (\<lambda>x. True) S U f g"
- obtains g' where "homotopic_with (\<lambda>x. True) T U f g'"
+ and "homotopic_with_canon (\<lambda>x. True) S U f g"
+ obtains g' where "homotopic_with_canon (\<lambda>x. True) T U f g'"
"continuous_on T g'" "image g' T \<subseteq> U"
"\<And>x. x \<in> S \<Longrightarrow> g' x = g x"
proof -
@@ -4141,9 +4140,9 @@
define h' where "h' \<equiv> \<lambda>z. if snd z \<in> S then h z else (f \<circ> snd) z"
define B where "B \<equiv> {0::real} \<times> T \<union> {0..1} \<times> S"
have clo0T: "closedin (top_of_set ({0..1} \<times> T)) ({0::real} \<times> T)"
- by (simp add: closedin_subtopology_refl closedin_Times)
+ by (simp add: Abstract_Topology.closedin_Times)
moreover have cloT1S: "closedin (top_of_set ({0..1} \<times> T)) ({0..1} \<times> S)"
- by (simp add: closedin_subtopology_refl closedin_Times assms)
+ by (simp add: Abstract_Topology.closedin_Times assms)
ultimately have clo0TB:"closedin (top_of_set ({0..1} \<times> T)) B"
by (auto simp: B_def)
have cloBS: "closedin (top_of_set B) ({0..1} \<times> S)"
@@ -4225,7 +4224,7 @@
qed
show ?thesis
proof
- show hom: "homotopic_with (\<lambda>x. True) T U f (\<lambda>x. k (a x, x))"
+ show hom: "homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. k (a x, x))"
proof (simp add: homotopic_with, intro exI conjI)
show "continuous_on ({0..1} \<times> T) (k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z)))"
apply (intro continuous_on_compose continuous_intros)
@@ -4241,7 +4240,7 @@
by auto
qed
show "continuous_on T (\<lambda>x. k (a x, x))"
- using hom homotopic_with_imp_continuous by blast
+ using homotopic_with_imp_continuous_maps [OF hom] by auto
show "(\<lambda>x. k (a x, x)) ` T \<subseteq> U"
proof clarify
fix t
@@ -4262,12 +4261,12 @@
and "ANR T"
and fim: "f ` S \<subseteq> T"
and "S \<noteq> {}"
- shows "(\<exists>c. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)) \<longleftrightarrow>
+ shows "(\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)) \<longleftrightarrow>
(\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> T \<and> (\<forall>x \<in> S. g x = f x))"
(is "?lhs = ?rhs")
proof
assume ?lhs
- then obtain c where c: "homotopic_with (\<lambda>x. True) S T (\<lambda>x. c) f"
+ then obtain c where c: "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. c) f"
by (blast intro: homotopic_with_symD)
have "closedin (top_of_set UNIV) S"
using \<open>closed S\<close> closed_closedin by fastforce
@@ -4281,14 +4280,12 @@
assume ?rhs
then obtain g where "continuous_on UNIV g" "range g \<subseteq> T" "\<And>x. x\<in>S \<Longrightarrow> g x = f x"
by blast
- then obtain c where "homotopic_with (\<lambda>h. True) UNIV T g (\<lambda>x. c)"
+ then obtain c where "homotopic_with_canon (\<lambda>h. True) UNIV T g (\<lambda>x. c)"
using nullhomotopic_from_contractible [of UNIV g T] contractible_UNIV by blast
+ then have "homotopic_with_canon (\<lambda>x. True) S T g (\<lambda>x. c)"
+ by (simp add: homotopic_from_subtopology)
then show ?lhs
- apply (rule_tac x=c in exI)
- apply (rule homotopic_with_eq [of _ _ _ g "\<lambda>x. c"])
- apply (rule homotopic_with_subset_left)
- apply (auto simp: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
- done
+ by (force elim: homotopic_with_eq [of _ _ _ g "\<lambda>x. c"] simp: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
qed
corollary%unimportant nullhomotopic_into_rel_frontier_extension:
@@ -4298,7 +4295,7 @@
and "convex T" "bounded T"
and fim: "f ` S \<subseteq> rel_frontier T"
and "S \<noteq> {}"
- shows "(\<exists>c. homotopic_with (\<lambda>x. True) S (rel_frontier T) f (\<lambda>x. c)) \<longleftrightarrow>
+ shows "(\<exists>c. homotopic_with_canon (\<lambda>x. True) S (rel_frontier T) f (\<lambda>x. c)) \<longleftrightarrow>
(\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> rel_frontier T \<and> (\<forall>x \<in> S. g x = f x))"
by (simp add: nullhomotopic_into_ANR_extension assms ANR_rel_frontier_convex)
@@ -4306,7 +4303,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes "closed S" and contf: "continuous_on S f"
and "S \<noteq> {}" and fim: "f ` S \<subseteq> sphere a r"
- shows "((\<exists>c. homotopic_with (\<lambda>x. True) S (sphere a r) f (\<lambda>x. c)) \<longleftrightarrow>
+ shows "((\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere a r) f (\<lambda>x. c)) \<longleftrightarrow>
(\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> sphere a r \<and> (\<forall>x \<in> S. g x = f x)))"
(is "?lhs = ?rhs")
proof (cases "r = 0")
@@ -4328,7 +4325,7 @@
fixes a :: "'a :: euclidean_space"
assumes "compact S" and "a \<notin> S"
shows "bounded (connected_component_set (- S) a) \<longleftrightarrow>
- \<not>(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1)
+ \<not>(\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
(\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\<lambda>x. c))"
(is "?lhs = ?rhs")
proof (cases "S = {}")
@@ -4368,13 +4365,13 @@
using bounded_iff linear by blast
then have bnot: "b \<notin> ball 0 r"
by simp
- have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. (x - a) /\<^sub>R norm (x - a))
+ have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. (x - a) /\<^sub>R norm (x - a))
(\<lambda>x. (x - b) /\<^sub>R norm (x - b))"
apply (rule Borsuk_maps_homotopic_in_path_component)
using \<open>closed S\<close> b open_Compl open_path_connected_component apply fastforce
done
moreover
- obtain c where "homotopic_with (\<lambda>x. True) (ball 0 r) (sphere 0 1)
+ obtain c where "homotopic_with_canon (\<lambda>x. True) (ball 0 r) (sphere 0 1)
(\<lambda>x. inverse (norm (x - b)) *\<^sub>R (x - b)) (\<lambda>x. c)"
proof (rule nullhomotopic_from_contractible)
show "contractible (ball (0::'a) r)"
@@ -4384,8 +4381,7 @@
show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) ` ball 0 r \<subseteq> sphere 0 1"
using bnot Borsuk_map_into_sphere by blast
qed blast
- ultimately have "homotopic_with (\<lambda>x. True) S (sphere 0 1)
- (\<lambda>x. (x - a) /\<^sub>R norm (x - a)) (\<lambda>x. c)"
+ ultimately have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. (x - a) /\<^sub>R norm (x - a)) (\<lambda>x. c)"
by (meson homotopic_with_subset_left homotopic_with_trans r)
then show "\<not> ?rhs"
by blast
@@ -4397,7 +4393,7 @@
fixes a :: "'a :: euclidean_space"
assumes "compact S" and "a \<notin> S"and "b \<notin> S"
and boc: "bounded (connected_component_set (- S) a)"
- and hom: "homotopic_with (\<lambda>x. True) S (sphere 0 1)
+ and hom: "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
(\<lambda>x. (x - a) /\<^sub>R norm (x - a))
(\<lambda>x. (x - b) /\<^sub>R norm (x - b))"
shows "connected_component (- S) a b"
@@ -4418,7 +4414,7 @@
by (simp add: \<open>b \<notin> S\<close> notcc continuous_on_Borsuk_map)
show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) ` ?T \<subseteq> sphere 0 1"
by (simp add: \<open>b \<notin> S\<close> notcc Borsuk_map_into_sphere)
- show "homotopic_with (\<lambda>x. True) S (sphere 0 1)
+ show "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) (\<lambda>x. (x - a) /\<^sub>R norm (x - a))"
by (simp add: hom homotopic_with_symD)
qed (auto simp: ANR_sphere intro: that)
@@ -4429,7 +4425,7 @@
lemma Borsuk_maps_homotopic_in_connected_component_eq:
fixes a :: "'a :: euclidean_space"
assumes S: "compact S" "a \<notin> S" "b \<notin> S" and 2: "2 \<le> DIM('a)"
- shows "(homotopic_with (\<lambda>x. True) S (sphere 0 1)
+ shows "(homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
(\<lambda>x. (x - a) /\<^sub>R norm (x - a))
(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) \<longleftrightarrow>
connected_component (- S) a b)"
@@ -4587,9 +4583,9 @@
assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> U"
and contg: "continuous_on S g" and gim: "g ` S \<subseteq> U"
and clo: "closedin (top_of_set S) T"
- and "ANR U" and hom: "homotopic_with (\<lambda>x. True) T U f g"
+ and "ANR U" and hom: "homotopic_with_canon (\<lambda>x. True) T U f g"
obtains V where "T \<subseteq> V" "openin (top_of_set S) V"
- "homotopic_with (\<lambda>x. True) V U f g"
+ "homotopic_with_canon (\<lambda>x. True) V U f g"
proof -
have "T \<subseteq> S"
using clo closedin_imp_subset by blast
@@ -4631,7 +4627,7 @@
obtain T' where opeT': "openin (top_of_set S) T'"
and "T \<subseteq> T'" and TW: "{0..1} \<times> T' \<subseteq> W"
using tube_lemma_gen [of "{0..1::real}" T S W] W \<open>T \<subseteq> S\<close> opeW by auto
- moreover have "homotopic_with (\<lambda>x. True) T' U f g"
+ moreover have "homotopic_with_canon (\<lambda>x. True) T' U f g"
proof (simp add: homotopic_with, intro exI conjI)
show "continuous_on ({0..1} \<times> T') k"
using TW continuous_on_subset contk by auto
@@ -4651,8 +4647,8 @@
fixes \<F> :: "'a::euclidean_space set set"
assumes "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (top_of_set (\<Union>\<F>)) S"
and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (top_of_set (\<Union>\<F>)) S"
- and "\<And>S. S \<in> \<F> \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
- shows "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f g"
+ and "\<And>S. S \<in> \<F> \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g"
+ shows "homotopic_with_canon (\<lambda>x. True) (\<Union>\<F>) T f g"
proof -
obtain \<V> where "\<V> \<subseteq> \<F>" "countable \<V>" and eqU: "\<Union>\<V> = \<Union>\<F>"
using Lindelof_openin assms by blast
@@ -4660,14 +4656,14 @@
proof (cases "\<V> = {}")
case True
then show ?thesis
- by (metis Union_empty eqU homotopic_on_empty)
+ by (metis Union_empty eqU homotopic_with_canon_on_empty)
next
case False
then obtain V :: "nat \<Rightarrow> 'a set" where V: "range V = \<V>"
using range_from_nat_into \<open>countable \<V>\<close> by metis
with \<open>\<V> \<subseteq> \<F>\<close> have clo: "\<And>n. closedin (top_of_set (\<Union>\<F>)) (V n)"
and ope: "\<And>n. openin (top_of_set (\<Union>\<F>)) (V n)"
- and hom: "\<And>n. homotopic_with (\<lambda>x. True) (V n) T f g"
+ 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"
@@ -4723,9 +4719,9 @@
lemma homotopic_on_components_eq:
fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set"
assumes S: "locally connected S \<or> compact S" and "ANR T"
- shows "homotopic_with (\<lambda>x. True) S T f g \<longleftrightarrow>
+ shows "homotopic_with_canon (\<lambda>x. True) S T f g \<longleftrightarrow>
(continuous_on S f \<and> f ` S \<subseteq> T \<and> continuous_on S g \<and> g ` S \<subseteq> T) \<and>
- (\<forall>C \<in> components S. homotopic_with (\<lambda>x. True) C T f g)"
+ (\<forall>C \<in> components S. homotopic_with_canon (\<lambda>x. True) C T f g)"
(is "?lhs \<longleftrightarrow> ?C \<and> ?rhs")
proof -
have "continuous_on S f" "f ` S \<subseteq> T" "continuous_on S g" "g ` S \<subseteq> T" if ?lhs
@@ -4740,7 +4736,7 @@
assume R: ?rhs
have "\<exists>U. C \<subseteq> U \<and> closedin (top_of_set S) U \<and>
openin (top_of_set S) U \<and>
- homotopic_with (\<lambda>x. True) U T f g" if C: "C \<in> components S" for C
+ homotopic_with_canon (\<lambda>x. True) U T f g" if C: "C \<in> components S" for C
proof -
have "C \<subseteq> S"
by (simp add: in_components_subset that)
@@ -4754,15 +4750,15 @@
by (simp add: closedin_component that)
show "openin (top_of_set S) C"
by (simp add: \<open>locally connected S\<close> openin_components_locally_connected that)
- show "homotopic_with (\<lambda>x. True) C T f g"
+ show "homotopic_with_canon (\<lambda>x. True) C T f g"
by (simp add: R that)
qed auto
next
assume "compact S"
- have hom: "homotopic_with (\<lambda>x. True) C T f g"
+ have hom: "homotopic_with_canon (\<lambda>x. True) C T f g"
using R that by blast
obtain U where "C \<subseteq> U" and opeU: "openin (top_of_set S) U"
- and hom: "homotopic_with (\<lambda>x. True) U T f g"
+ and hom: "homotopic_with_canon (\<lambda>x. True) U T f g"
using homotopic_neighbourhood_extension [OF contf fim contg gim _ \<open>ANR T\<close> hom]
\<open>C \<in> components S\<close> closedin_component by blast
then obtain V where "open V" and V: "U = S \<inter> V"
@@ -4775,7 +4771,7 @@
proof (intro exI conjI)
show "closedin (top_of_set S) K"
by (meson \<open>compact K\<close> \<open>compact S\<close> closedin_compact_eq opeK openin_imp_subset)
- show "homotopic_with (\<lambda>x. True) K T f g"
+ show "homotopic_with_canon (\<lambda>x. True) K T f g"
using V \<open>K \<subseteq> V\<close> hom homotopic_with_subset_left opeK openin_imp_subset by fastforce
qed (use opeK \<open>C \<subseteq> K\<close> in auto)
qed
@@ -4783,7 +4779,7 @@
then obtain \<phi> where \<phi>: "\<And>C. C \<in> components S \<Longrightarrow> C \<subseteq> \<phi> C"
and clo\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> closedin (top_of_set S) (\<phi> C)"
and ope\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> openin (top_of_set S) (\<phi> C)"
- and hom\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> homotopic_with (\<lambda>x. True) (\<phi> C) T f g"
+ and hom\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) (\<phi> C) T f g"
by metis
have Seq: "S = \<Union> (\<phi> ` components S)"
proof
@@ -4806,11 +4802,11 @@
assumes S: "locally connected S \<or> compact S" and "ANR T"
shows
"(\<forall>f g. continuous_on S f \<longrightarrow> f ` S \<subseteq> T \<longrightarrow> continuous_on S g \<longrightarrow> g ` S \<subseteq> T \<longrightarrow>
- homotopic_with (\<lambda>x. True) S T f g)
+ homotopic_with_canon (\<lambda>x. True) S T f g)
\<longleftrightarrow>
(\<forall>C\<in>components S.
\<forall>f g. continuous_on C f \<longrightarrow> f ` C \<subseteq> T \<longrightarrow> continuous_on C g \<longrightarrow> g ` C \<subseteq> T \<longrightarrow>
- homotopic_with (\<lambda>x. True) C T f g)"
+ homotopic_with_canon (\<lambda>x. True) C T f g)"
(is "?lhs = ?rhs")
proof
assume L[rule_format]: ?lhs
@@ -4823,9 +4819,9 @@
using extension_from_component [OF S \<open>ANR T\<close> C contf fim] by metis
obtain g' where contg': "continuous_on S g'" and g'im: "g' ` S \<subseteq> T" and g'g: "\<And>x. x \<in> C \<Longrightarrow> g' x = g x"
using extension_from_component [OF S \<open>ANR T\<close> C contg gim] by metis
- have "homotopic_with (\<lambda>x. True) C T f' g'"
+ have "homotopic_with_canon (\<lambda>x. True) C T f' g'"
using L [OF contf' f'im contg' g'im] homotopic_with_subset_left C in_components_subset by fastforce
- then show "homotopic_with (\<lambda>x. True) C T f g"
+ then show "homotopic_with_canon (\<lambda>x. True) C T f g"
using f'f g'g homotopic_with_eq by force
qed
next
@@ -4835,10 +4831,10 @@
fix f g
assume contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
and contg: "continuous_on S g" and gim: "g ` S \<subseteq> T"
- moreover have "homotopic_with (\<lambda>x. True) C T f g" if "C \<in> components S" for C
+ moreover have "homotopic_with_canon (\<lambda>x. True) C T f g" if "C \<in> components S" for C
using R [OF that]
by (meson contf contg continuous_on_subset fim gim image_mono in_components_subset order.trans that)
- ultimately show "homotopic_with (\<lambda>x. True) S T f g"
+ ultimately show "homotopic_with_canon (\<lambda>x. True) S T f g"
by (subst homotopic_on_components_eq [OF S \<open>ANR T\<close>]) auto
qed
qed
--- a/src/HOL/Analysis/Complex_Transcendental.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Mar 26 17:01:55 2019 +0000
@@ -4036,11 +4036,11 @@
subsection\<open>Formulation of loop homotopy in terms of maps out of type complex\<close>
lemma homotopic_circlemaps_imp_homotopic_loops:
- assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+ assumes "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))
(g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
proof -
- have "homotopic_with (\<lambda>f. True) {z. cmod z = 1} S f g"
+ have "homotopic_with_canon (\<lambda>f. True) {z. cmod z = 1} S f g"
using assms by (auto simp: sphere_def)
moreover have "continuous_on {0..1} (exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
by (intro continuous_intros)
@@ -4056,7 +4056,7 @@
lemma homotopic_loops_imp_homotopic_circlemaps:
assumes "homotopic_loops S p q"
- shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S
+ shows "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S
(p \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))
(q \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))"
proof -
@@ -4117,7 +4117,7 @@
assumes S: "simply_connected S"
and contf: "continuous_on (sphere 0 1) f" and fim: "f ` (sphere 0 1) \<subseteq> S"
and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
- shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+ shows "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
proof -
have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * \<i>)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * \<i>))"
apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
@@ -4135,8 +4135,8 @@
and hom: "\<And>f g::complex \<Rightarrow> 'a.
\<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
- \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
- shows "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
+ \<Longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
+ shows "\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
apply (rule_tac x="h 1" in exI)
apply (rule hom)
using assms
@@ -4147,7 +4147,7 @@
assumes "\<And>f g::complex \<Rightarrow> 'a.
\<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
- \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+ \<Longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
shows "path_connected S"
proof (clarsimp simp add: path_connected_eq_homotopic_points)
fix a b
@@ -4162,14 +4162,14 @@
assumes "path_connected S"
and hom: "\<And>f::complex \<Rightarrow> 'a.
\<lbrakk>continuous_on (sphere 0 1) f; f `(sphere 0 1) \<subseteq> S\<rbrakk>
- \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)"
+ \<Longrightarrow> \<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)"
shows "simply_connected S"
proof (clarsimp simp add: simply_connected_eq_contractible_loop_some assms)
fix p
assume p: "path p" "path_image p \<subseteq> S" "pathfinish p = pathstart p"
then have "homotopic_loops S p p"
by (simp add: homotopic_loops_refl)
- then obtain a where homp: "homotopic_with (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg2pi z / (2 * pi))) (\<lambda>x. a)"
+ then obtain a where homp: "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg2pi z / (2 * pi))) (\<lambda>x. a)"
by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom)
show "\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)"
proof (intro exI conjI)
@@ -4198,7 +4198,7 @@
(\<forall>f g::complex \<Rightarrow> 'a.
continuous_on (sphere 0 1) f \<and> f ` (sphere 0 1) \<subseteq> S \<and>
continuous_on (sphere 0 1) g \<and> g ` (sphere 0 1) \<subseteq> S
- \<longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g)"
+ \<longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g)"
apply (rule iffI)
apply (blast elim: dest: simply_connected_eq_homotopic_circlemaps1)
by (simp add: simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3)
@@ -4209,7 +4209,7 @@
path_connected S \<and>
(\<forall>f::complex \<Rightarrow> 'a.
continuous_on (sphere 0 1) f \<and> f `(sphere 0 1) \<subseteq> S
- \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)))"
+ \<longrightarrow> (\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)))"
apply (rule iffI)
apply (simp add: simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b)
using simply_connected_eq_homotopic_circlemaps3 by blast
@@ -4229,7 +4229,7 @@
proof -
have "homotopic_loops (path_image \<gamma>) \<gamma> \<gamma>"
by (simp add: assms homotopic_loops_refl simple_path_imp_path)
- then have hom: "homotopic_with (\<lambda>h. True) (sphere 0 1) (path_image \<gamma>)
+ then have hom: "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) (path_image \<gamma>)
(\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi)))"
by (rule homotopic_loops_imp_homotopic_circlemaps)
have "\<exists>g. homeomorphism (sphere 0 1) (path_image \<gamma>) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) g"
--- a/src/HOL/Analysis/Further_Topology.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Tue Mar 26 17:01:55 2019 +0000
@@ -164,7 +164,7 @@
and "S \<subseteq> T"
and contf: "continuous_on (sphere 0 1 \<inter> S) f"
and fim: "f ` (sphere 0 1 \<inter> S) \<subseteq> sphere 0 1 \<inter> T"
- shows "\<exists>c. homotopic_with (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)"
+ shows "\<exists>c. homotopic_with_canon (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)"
proof -
have [simp]: "\<And>x. \<lbrakk>norm x = 1; x \<in> S\<rbrakk> \<Longrightarrow> norm (f x) = 1"
using fim by (simp add: image_subset_iff)
@@ -194,7 +194,7 @@
apply (intro derivative_intros diffg differentiable_on_compose [OF diffg])
using gnz apply auto
done
- have homfg: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) f g"
+ have homfg: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) f g"
proof (rule homotopic_with_linear [OF contf])
show "continuous_on (sphere 0 1 \<inter> S) g"
using pfg by (simp add: differentiable_imp_continuous_on diffg)
@@ -224,7 +224,7 @@
by (auto simp: between_mem_segment midpoint_def)
have conth: "continuous_on (sphere 0 1 \<inter> S) h"
using differentiable_imp_continuous_on diffh by blast
- have hom_hd: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) h (\<lambda>x. -d)"
+ have hom_hd: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) h (\<lambda>x. -d)"
apply (rule homotopic_with_linear [OF conth continuous_on_const])
apply (simp add: subset_Diff_insert non0hd)
apply (simp add: segment_convex_hull)
@@ -236,7 +236,7 @@
by (intro continuous_intros) auto
have sub0T: "(\<lambda>y. y /\<^sub>R norm y) ` (T - {0}) \<subseteq> sphere 0 1 \<inter> T"
by (fastforce simp: assms(2) subspace_mul)
- obtain c where homhc: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) h (\<lambda>x. c)"
+ obtain c where homhc: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) h (\<lambda>x. c)"
apply (rule_tac c="-d" in that)
apply (rule homotopic_with_eq)
apply (rule homotopic_compose_continuous_left [OF hom_hd conT0 sub0T])
@@ -306,7 +306,7 @@
and affST: "aff_dim S < aff_dim T"
and contf: "continuous_on (rel_frontier S) f"
and fim: "f ` (rel_frontier S) \<subseteq> rel_frontier T"
- obtains c where "homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
proof (cases "S = {}")
case True
then show ?thesis
@@ -328,7 +328,7 @@
using \<open>T \<noteq> {}\<close> by blast
with homeomorphic_imp_homotopy_eqv
have relT: "sphere 0 1 \<inter> T' homotopy_eqv rel_frontier T"
- using homotopy_eqv_sym by blast
+ using homotopy_equivalent_space_sym by blast
have "aff_dim S \<le> int (dim T')"
using affT' \<open>subspace T'\<close> affST aff_dim_subspace by force
with spheremap_lemma3 [OF \<open>bounded S\<close> \<open>convex S\<close> \<open>subspace T'\<close>] \<open>S \<noteq> {}\<close>
@@ -338,10 +338,10 @@
by metis
with homeomorphic_imp_homotopy_eqv
have relS: "sphere 0 1 \<inter> S' homotopy_eqv rel_frontier S"
- using homotopy_eqv_sym by blast
+ using homotopy_equivalent_space_sym by blast
have dimST': "dim S' < dim T'"
by (metis \<open>S' \<subseteq> T'\<close> \<open>subspace S'\<close> \<open>subspace T'\<close> affS' affST affT' less_irrefl not_le subspace_dim_equal)
- have "\<exists>c. homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
+ have "\<exists>c. homotopic_with_canon (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
apply (rule homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim])
apply (rule homotopy_eqv_cohomotopic_triviality_null[OF relS, THEN iffD1, rule_format])
apply (metis dimST' \<open>subspace S'\<close> \<open>subspace T'\<close> \<open>S' \<subseteq> T'\<close> spheremap_lemma2, blast)
@@ -354,7 +354,7 @@
fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space"
assumes
"DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \<subseteq> (sphere b s)"
- obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
proof (cases "s \<le> 0")
case True then show ?thesis
by (meson nullhomotopic_into_contractible f contractible_sphere that)
@@ -522,13 +522,13 @@
using Suc.prems affD by linarith
have contDh: "continuous_on (rel_frontier D) h"
using \<open>C \<in> \<F>\<close> relf_sub by (blast intro: continuous_on_subset [OF conth])
- then have *: "(\<exists>c. homotopic_with (\<lambda>x. True) (rel_frontier D) (rel_frontier T) h (\<lambda>x. c)) =
+ then have *: "(\<exists>c. homotopic_with_canon (\<lambda>x. True) (rel_frontier D) (rel_frontier T) h (\<lambda>x. c)) =
(\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> rel_frontier T \<and>
(\<forall>x\<in>rel_frontier D. g x = h x))"
apply (rule nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier])
apply (simp_all add: assms rel_frontier_eq_empty him_relf)
done
- have "(\<exists>c. homotopic_with (\<lambda>x. True) (rel_frontier D)
+ have "(\<exists>c. homotopic_with_canon (\<lambda>x. True) (rel_frontier D)
(rel_frontier T) h (\<lambda>x. c))"
by (metis inessential_spheremap_lowdim_gen
[OF \<open>convex D\<close> \<open>bounded D\<close> \<open>convex T\<close> \<open>bounded T\<close> affD_lessT contDh him_relf])
@@ -1706,7 +1706,7 @@
assumes "compact S"
shows "(\<forall>c \<in> components(- S). \<not>bounded c) \<longleftrightarrow>
(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
- \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
+ \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
(is "?lhs = ?rhs")
proof
assume L [rule_format]: ?lhs
@@ -1717,9 +1717,10 @@
obtain g where contg: "continuous_on UNIV g" and gim: "range g \<subseteq> sphere 0 1"
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
by (rule extend_map_UNIV_to_sphere_no_bounded_component [OF _ _ \<open>compact S\<close> contf fim L]) auto
- then show "\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)"
- using nullhomotopic_from_contractible [OF contg gim]
- by (metis assms compact_imp_closed contf empty_iff fim homotopic_with_equal nullhomotopic_into_sphere_extension)
+ then obtain c where c: "homotopic_with_canon (\<lambda>h. True) UNIV (sphere 0 1) g (\<lambda>x. c)"
+ using contractible_UNIV nullhomotopic_from_contractible by blast
+ then show "\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)"
+ by (metis assms compact_imp_closed contf contg contractible_empty fim gf gim nullhomotopic_from_contractible nullhomotopic_into_sphere_extension)
qed
next
assume R [rule_format]: ?rhs
@@ -1744,7 +1745,7 @@
assumes "compact S" and 2: "2 \<le> DIM('a)"
shows "connected(- S) \<longleftrightarrow>
(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
- \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
+ \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
@@ -2814,12 +2815,12 @@
by simp
have "convex (cball (0::complex) 1)"
by (rule convex_cball)
- then obtain c where "homotopic_with (\<lambda>z. True) (sphere (0::complex) 1) (rel_frontier S) f (\<lambda>x. c)"
+ then obtain c where "homotopic_with_canon (\<lambda>z. True) (sphere (0::complex) 1) (rel_frontier S) f (\<lambda>x. c)"
apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball \<open>convex S\<close> \<open>bounded S\<close>, where f=f])
using f 3
apply (auto simp: aff_dim_cball)
done
- then show "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) (rel_frontier S) f (\<lambda>x. a)"
+ then show "\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) (rel_frontier S) f (\<lambda>x. a)"
by blast
qed
qed
@@ -3018,7 +3019,7 @@
by (metis DIM_complex False homeomorphic_spheres_gen not_less zero_less_one)
then have "simply_connected(sphere (0::complex) 1)"
using L homeomorphic_simply_connected_eq by blast
- then obtain a::complex where "homotopic_with (\<lambda>h. True) (sphere 0 1) (sphere 0 1) id (\<lambda>x. a)"
+ then obtain a::complex where "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) (sphere 0 1) id (\<lambda>x. a)"
apply (simp add: simply_connected_eq_contractible_circlemap)
by (metis continuous_on_id' id_apply image_id subset_refl)
then show False
@@ -3496,7 +3497,7 @@
lemma inessential_eq_continuous_logarithm:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
+ shows "(\<exists>a. homotopic_with_canon (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
(\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x)))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
@@ -3506,24 +3507,24 @@
assume ?rhs
then obtain g where contg: "continuous_on S g" and f: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
by metis
- obtain a where "homotopic_with (\<lambda>h. True) S (- {of_real 0}) (exp \<circ> g) (\<lambda>x. a)"
+ obtain a where "homotopic_with_canon (\<lambda>h. True) S (- {of_real 0}) (exp \<circ> g) (\<lambda>x. a)"
proof (rule nullhomotopic_through_contractible [OF contg subset_UNIV _ _ contractible_UNIV])
show "continuous_on (UNIV::complex set) exp"
by (intro continuous_intros)
show "range exp \<subseteq> - {0}"
by auto
qed force
- thus ?lhs
- apply (rule_tac x=a in exI)
- by (simp add: f homotopic_with_eq)
+ then have "homotopic_with_canon (\<lambda>h. True) S (- {0}) f (\<lambda>t. a)"
+ using f homotopic_with_eq by fastforce
+ then show ?lhs ..
qed
corollary inessential_imp_continuous_logarithm_circle:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- assumes "homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)"
+ assumes "homotopic_with_canon (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)"
obtains g where "continuous_on S g" and "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
proof -
- have "homotopic_with (\<lambda>h. True) S (- {0}) f (\<lambda>t. a)"
+ have "homotopic_with_canon (\<lambda>h. True) S (- {0}) f (\<lambda>t. a)"
using assms homotopic_with_subset_right by fastforce
then show ?thesis
by (metis inessential_eq_continuous_logarithm that)
@@ -3532,7 +3533,7 @@
lemma inessential_eq_continuous_logarithm_circle:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)) \<longleftrightarrow>
+ shows "(\<exists>a. homotopic_with_canon (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)) \<longleftrightarrow>
(\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x))))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
@@ -3552,7 +3553,7 @@
assume ?rhs
then obtain g where contg: "continuous_on S g" and g: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(\<i>* of_real(g x))"
by metis
- obtain a where "homotopic_with (\<lambda>h. True) S (sphere 0 1) ((exp \<circ> (\<lambda>z. \<i>*z)) \<circ> (of_real \<circ> g)) (\<lambda>x. a)"
+ obtain a where "homotopic_with_canon (\<lambda>h. True) S (sphere 0 1) ((exp \<circ> (\<lambda>z. \<i>*z)) \<circ> (of_real \<circ> g)) (\<lambda>x. a)"
proof (rule nullhomotopic_through_contractible)
show "continuous_on S (complex_of_real \<circ> g)"
by (intro conjI contg continuous_intros)
@@ -3565,16 +3566,16 @@
qed (auto simp: convex_Reals convex_imp_contractible)
moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> (*)\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
by (simp add: g)
- ultimately show ?lhs
- apply (rule_tac x=a in exI)
- by (simp add: homotopic_with_eq)
+ ultimately have "homotopic_with_canon (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)"
+ using homotopic_with_eq by force
+ then show ?lhs ..
qed
proposition homotopic_with_sphere_times:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- assumes hom: "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g" and conth: "continuous_on S h"
+ assumes hom: "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f g" and conth: "continuous_on S h"
and hin: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> sphere 0 1"
- shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x * h x) (\<lambda>x. g x * h x)"
+ shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x * h x) (\<lambda>x. g x * h x)"
proof -
obtain k where contk: "continuous_on ({0..1::real} \<times> S) k"
and kim: "k ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
@@ -3592,29 +3593,29 @@
proposition homotopic_circlemaps_divide:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
+ shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
- (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c))"
+ (\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c))"
proof -
- have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
- if "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)" for c
+ have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
+ if "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)" for c
proof -
have "S = {} \<or> path_component (sphere 0 1) 1 c"
using homotopic_with_imp_subset2 [OF that] path_connected_sphere [of "0::complex" 1]
by (auto simp: path_connected_component)
- then have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. 1) (\<lambda>x. c)"
- by (metis homotopic_constant_maps)
+ then have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. 1) (\<lambda>x. c)"
+ by (simp add: homotopic_constant_maps)
then show ?thesis
using homotopic_with_symD homotopic_with_trans that by blast
qed
- then have *: "(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)) \<longleftrightarrow>
- homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
+ then have *: "(\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)) \<longleftrightarrow>
+ homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
by auto
- have "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
+ have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
- homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
+ homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume L: ?lhs
@@ -3627,7 +3628,7 @@
apply (rule continuous_on_subset [of "sphere 0 1", OF continuous_on_inverse])
apply (auto simp: continuous_on_id)
done
- have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
+ have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
using homotopic_with_sphere_times [OF L cont]
apply (rule homotopic_with_eq)
apply (auto simp: division_ring_class.divide_inverse norm_inverse)
@@ -3852,7 +3853,7 @@
assumes "continuous_on S f" "contractible S" "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
obtains g where "continuous_on S g" "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
proof -
- obtain c where hom: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>x. c)"
+ obtain c where hom: "homotopic_with_canon (\<lambda>h. True) S (-{0}) f (\<lambda>x. c)"
using nullhomotopic_from_contractible assms
by (metis imageE subset_Compl_singleton)
then show ?thesis
@@ -3920,7 +3921,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> complex"
assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f"
and fim: "f `(sphere a r) \<subseteq> (sphere 0 1)"
- obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) f (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere 0 1) f (\<lambda>x. c)"
proof -
obtain g where contg: "continuous_on (sphere a r) g"
and feq: "\<And>x. x \<in> sphere a r \<Longrightarrow> f x = exp(g x)"
@@ -3947,7 +3948,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2"
and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \<subseteq> (sphere b s)"
- obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
proof (cases "s \<le> 0")
case True
then show ?thesis
@@ -3963,16 +3964,16 @@
and him: "h ` sphere b s \<subseteq> sphere 0 1"
and kim: "k ` sphere 0 1 \<subseteq> sphere b s"
by (simp_all add: homeomorphism_def)
- obtain c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) (h \<circ> f) (\<lambda>x. c)"
+ obtain c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere 0 1) (h \<circ> f) (\<lambda>x. c)"
proof (rule inessential_spheremap_2_aux [OF a2])
show "continuous_on (sphere a r) (h \<circ> f)"
by (meson continuous_on_compose [OF contf] conth continuous_on_subset fim)
show "(h \<circ> f) ` sphere a r \<subseteq> sphere 0 1"
using fim him by force
qed auto
- then have "homotopic_with (\<lambda>f. True) (sphere a r) (sphere b s) (k \<circ> (h \<circ> f)) (k \<circ> (\<lambda>x. c))"
+ then have "homotopic_with_canon (\<lambda>f. True) (sphere a r) (sphere b s) (k \<circ> (h \<circ> f)) (k \<circ> (\<lambda>x. c))"
by (rule homotopic_compose_continuous_left [OF _ contk kim])
- then have "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. k c)"
+ then have "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. k c)"
apply (rule homotopic_with_eq, auto)
by (metis fim hk homeomorphism_def image_subset_iff mem_sphere)
then show ?thesis
@@ -4202,7 +4203,7 @@
definition%important Borsukian where
"Borsukian S \<equiv>
\<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
- \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (- {0}) f (\<lambda>x. a))"
+ \<longrightarrow> (\<exists>a. homotopic_with_canon (\<lambda>h. True) S (- {0}) f (\<lambda>x. a))"
lemma Borsukian_retraction_gen:
assumes "Borsukian S" "continuous_on S h" "h ` S = T"
@@ -4259,7 +4260,7 @@
"Borsukian S \<longleftrightarrow>
(\<forall>f g. continuous_on S f \<and> f ` S \<subseteq> -{0} \<and>
continuous_on S g \<and> g ` S \<subseteq> -{0}
- \<longrightarrow> homotopic_with (\<lambda>h. True) S (- {0::complex}) f g)"
+ \<longrightarrow> homotopic_with_canon (\<lambda>h. True) S (- {0::complex}) f g)"
unfolding Borsukian_def homotopic_triviality
by (simp add: path_connected_punctured_universe)
@@ -4343,7 +4344,7 @@
fixes S :: "'a::real_normed_vector set"
shows "Borsukian S \<longleftrightarrow>
(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
- \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (sphere (0::complex) 1) f (\<lambda>x. a)))"
+ \<longrightarrow> (\<exists>a. homotopic_with_canon (\<lambda>h. True) S (sphere (0::complex) 1) f (\<lambda>x. a)))"
by (simp add: inessential_eq_continuous_logarithm_circle Borsukian_continuous_logarithm_circle_real)
lemma contractible_imp_Borsukian: "contractible S \<Longrightarrow> Borsukian S"
@@ -5335,12 +5336,12 @@
proposition inessential_eq_extensible:
fixes f :: "'a::euclidean_space \<Rightarrow> complex"
assumes "closed S"
- shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
+ shows "(\<exists>a. homotopic_with_canon (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
(\<exists>g. continuous_on UNIV g \<and> (\<forall>x \<in> S. g x = f x) \<and> (\<forall>x. g x \<noteq> 0))"
(is "?lhs = ?rhs")
proof
assume ?lhs
- then obtain a where a: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)" ..
+ then obtain a where a: "homotopic_with_canon (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)" ..
show ?rhs
proof (cases "S = {}")
case True
@@ -5403,8 +5404,8 @@
assumes T: "path_connected T"
and "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (top_of_set (\<Union>\<F>)) S"
and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (top_of_set (\<Union>\<F>)) S"
- and hom: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)"
- obtains a where "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
+ and hom: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. a)"
+ obtains a where "homotopic_with_canon (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
proof (cases "\<Union>\<F> = {}")
case True
with that show ?thesis
@@ -5415,16 +5416,16 @@
by blast
then obtain a where clo: "closedin (top_of_set (\<Union>\<F>)) C"
and ope: "openin (top_of_set (\<Union>\<F>)) C"
- and "homotopic_with (\<lambda>x. True) C T f (\<lambda>x. a)"
+ and "homotopic_with_canon (\<lambda>x. True) C T f (\<lambda>x. a)"
using assms by blast
with \<open>C \<noteq> {}\<close> have "f ` C \<subseteq> T" "a \<in> T"
using homotopic_with_imp_subset1 homotopic_with_imp_subset2 by blast+
- have "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
+ have "homotopic_with_canon (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
proof (rule homotopic_on_clopen_Union)
show "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (top_of_set (\<Union>\<F>)) S"
"\<And>S. S \<in> \<F> \<Longrightarrow> openin (top_of_set (\<Union>\<F>)) S"
by (simp_all add: assms)
- show "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)" if "S \<in> \<F>" for S
+ show "homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. a)" if "S \<in> \<F>" for S
proof (cases "S = {}")
case True
then show ?thesis
@@ -5433,12 +5434,13 @@
case False
then obtain b where "b \<in> S"
by blast
- obtain c where c: "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)"
+ obtain c where c: "homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)"
using \<open>S \<in> \<F>\<close> hom by blast
then have "c \<in> T"
using \<open>b \<in> S\<close> homotopic_with_imp_subset2 by blast
- then have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. c)"
- using T \<open>a \<in> T\<close> homotopic_constant_maps path_connected_component by blast
+ then have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. c)"
+ using T \<open>a \<in> T\<close> homotopic_constant_maps path_connected_component
+ by (simp add: homotopic_constant_maps path_connected_component)
then show ?thesis
using c homotopic_with_symD homotopic_with_trans by blast
qed
--- a/src/HOL/Analysis/Homeomorphism.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy Tue Mar 26 17:01:55 2019 +0000
@@ -1861,7 +1861,7 @@
show "topspace ?X \<subseteq> (\<Union>i\<in>U. {0..1} \<times> V i)"
using V by force
show "\<And>i. i \<in> U \<Longrightarrow> openin (top_of_set ({0..1} \<times> U)) ({0..1} \<times> V i)"
- by (simp add: opeV openin_Times)
+ by (simp add: Abstract_Topology.openin_Times opeV)
show "\<And>i. i \<in> U \<Longrightarrow> continuous_map
(subtopology (top_of_set ({0..1} \<times> U)) ({0..1} \<times> V i)) euclidean (fs i)"
using contfs
@@ -1949,7 +1949,7 @@
and contg: "continuous_on U g"
and gim: "g ` U \<subseteq> C"
and pgeq: "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
- and hom: "homotopic_with (\<lambda>x. True) U S f f'"
+ and hom: "homotopic_with_canon (\<lambda>x. True) U S f f'"
obtains g' where "continuous_on U g'" "image g' U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g' y) = f' y"
proof -
obtain h where conth: "continuous_on ({0..1::real} \<times> U) h"
@@ -1978,7 +1978,7 @@
corollary covering_space_lift_inessential_function:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and U :: "'c::real_normed_vector set"
assumes cov: "covering_space C p S"
- and hom: "homotopic_with (\<lambda>x. True) U S f (\<lambda>x. a)"
+ and hom: "homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. a)"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
proof (cases "U = {}")
case True
--- a/src/HOL/Analysis/Homotopy.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Homotopy.thy Tue Mar 26 17:01:55 2019 +0000
@@ -5,172 +5,299 @@
section \<open>Homotopy of Maps\<close>
theory Homotopy
- imports Path_Connected Continuum_Not_Denumerable
+ imports Path_Connected Continuum_Not_Denumerable Product_Topology
begin
-definition%important homotopic_with ::
- "[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
+definition%important homotopic_with
where
- "homotopic_with P X Y p q \<equiv>
- (\<exists>h:: real \<times> 'a \<Rightarrow> 'b.
- continuous_on ({0..1} \<times> X) h \<and>
- h ` ({0..1} \<times> X) \<subseteq> Y \<and>
- (\<forall>x. h(0, x) = p x) \<and>
- (\<forall>x. h(1, x) = q x) \<and>
- (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
+ "homotopic_with P X Y f g \<equiv>
+ (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
+ (\<forall>x. h(0, x) = f x) \<and>
+ (\<forall>x. h(1, x) = g x) \<and>
+ (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t,x))))"
text\<open>\<open>p\<close>, \<open>q\<close> are functions \<open>X \<rightarrow> Y\<close>, and the property \<open>P\<close> restricts all intermediate maps.
We often just want to require that \<open>P\<close> fixes some subset, but to include the case of a loop homotopy,
it is convenient to have a general property \<open>P\<close>.\<close>
+abbreviation homotopic_with_canon ::
+ "[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
+where
+ "homotopic_with_canon P S T p q \<equiv> homotopic_with P (top_of_set S) (top_of_set T) p q"
+
+lemma split_01: "{0..1::real} = {0..1/2} \<union> {1/2..1}"
+ by force
+
+lemma split_01_prod: "{0..1::real} \<times> X = ({0..1/2} \<times> X) \<union> ({1/2..1} \<times> X)"
+ by force
+
+lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
+ by auto
+
+lemma fst_o_paired [simp]: "fst \<circ> (\<lambda>(x,y). (f x y, g x y)) = (\<lambda>(x,y). f x y)"
+ by auto
+
+lemma snd_o_paired [simp]: "snd \<circ> (\<lambda>(x,y). (f x y, g x y)) = (\<lambda>(x,y). g x y)"
+ by auto
+
+lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h \<circ> Pair t)"
+ by (fast intro: continuous_intros elim!: continuous_on_subset)
+
+lemma continuous_map_o_Pair:
+ assumes h: "continuous_map (prod_topology X Y) Z h" and t: "t \<in> topspace X"
+ shows "continuous_map Y Z (h \<circ> Pair t)"
+ apply (intro continuous_map_compose [OF _ h] continuous_map_id [unfolded id_def] continuous_intros)
+ apply (simp add: t)
+ done
+
+subsection%unimportant\<open>Trivial properties\<close>
+
text \<open>We often want to just localize the ending function equality or whatever.\<close>
text%important \<open>%whitespace\<close>
proposition homotopic_with:
- fixes X :: "'a::topological_space set" and Y :: "'b::topological_space set"
- assumes "\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
+ assumes "\<And>h k. (\<And>x. x \<in> topspace X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
shows "homotopic_with P X Y p q \<longleftrightarrow>
- (\<exists>h :: real \<times> 'a \<Rightarrow> 'b.
- continuous_on ({0..1} \<times> X) h \<and>
- h ` ({0..1} \<times> X) \<subseteq> Y \<and>
- (\<forall>x \<in> X. h(0,x) = p x) \<and>
- (\<forall>x \<in> X. h(1,x) = q x) \<and>
+ (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
+ (\<forall>x \<in> topspace X. h(0,x) = p x) \<and>
+ (\<forall>x \<in> topspace X. h(1,x) = q x) \<and>
(\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
unfolding homotopic_with_def
apply (rule iffI, blast, clarify)
- apply (rule_tac x="\<lambda>(u,v). if v \<in> X then h(u,v) else if u = 0 then p v else q v" in exI)
+ apply (rule_tac x="\<lambda>(u,v). if v \<in> topspace X then h(u,v) else if u = 0 then p v else q v" in exI)
apply auto
- apply (force elim: continuous_on_eq)
+ using continuous_map_eq apply fastforce
apply (drule_tac x=t in bspec, force)
apply (subst assms; simp)
done
-proposition homotopic_with_eq:
- assumes h: "homotopic_with P X Y f g"
- and f': "\<And>x. x \<in> X \<Longrightarrow> f' x = f x"
- and g': "\<And>x. x \<in> X \<Longrightarrow> g' x = g x"
- and P: "(\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k))"
- shows "homotopic_with P X Y f' g'"
- using h unfolding homotopic_with_def
- apply safe
- apply (rule_tac x="\<lambda>(u,v). if v \<in> X then h(u,v) else if u = 0 then f' v else g' v" in exI)
- apply (simp add: f' g', safe)
- apply (fastforce intro: continuous_on_eq, fastforce)
- apply (subst P; fastforce)
+lemma homotopic_with_mono:
+ assumes hom: "homotopic_with P X Y f g"
+ and Q: "\<And>h. \<lbrakk>continuous_map X Y h; P h\<rbrakk> \<Longrightarrow> Q h"
+ shows "homotopic_with Q X Y f g"
+ using hom
+ apply (simp add: homotopic_with_def)
+ apply (erule ex_forward)
+ apply (force simp: o_def dest: continuous_map_o_Pair intro: Q)
done
-proposition homotopic_with_equal:
- assumes contf: "continuous_on X f" and fXY: "f ` X \<subseteq> Y"
- and gf: "\<And>x. x \<in> X \<Longrightarrow> g x = f x"
- and P: "P f" "P g"
- shows "homotopic_with P X Y f g"
+lemma homotopic_with_imp_continuous_maps:
+ assumes "homotopic_with P X Y f g"
+ shows "continuous_map X Y f \<and> continuous_map X Y g"
+proof -
+ obtain h
+ where conth: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h"
+ and h: "\<forall>x. h (0, x) = f x" "\<forall>x. h (1, x) = g x"
+ using assms by (auto simp: homotopic_with_def)
+ have *: "t \<in> {0..1} \<Longrightarrow> continuous_map X Y (h \<circ> (\<lambda>x. (t,x)))" for t
+ by (rule continuous_map_compose [OF _ conth]) (simp add: o_def continuous_map_pairwise)
+ show ?thesis
+ using h *[of 0] *[of 1] by (simp add: continuous_map_eq)
+qed
+
+lemma homotopic_with_imp_continuous:
+ assumes "homotopic_with_canon P X Y f g"
+ shows "continuous_on X f \<and> continuous_on X g"
+ by (meson assms continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
+
+lemma homotopic_with_imp_property:
+ assumes "homotopic_with P X Y f g"
+ shows "P f \<and> P g"
+proof
+ obtain h where h: "\<And>x. h(0, x) = f x" "\<And>x. h(1, x) = g x" and P: "\<And>t. t \<in> {0..1::real} \<Longrightarrow> P(\<lambda>x. h(t,x))"
+ using assms by (force simp: homotopic_with_def)
+ show "P f" "P g"
+ using P [of 0] P [of 1] by (force simp: h)+
+qed
+
+lemma homotopic_with_equal:
+ assumes "P f" "P g" and contf: "continuous_map X Y f" and fg: "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x"
+ shows "homotopic_with P X Y f g"
unfolding homotopic_with_def
- apply (rule_tac x="\<lambda>(u,v). if u = 1 then g v else f v" in exI)
- using assms
- apply (intro conjI)
- apply (rule continuous_on_eq [where f = "f \<circ> snd"])
- apply (rule continuous_intros | force)+
- apply clarify
- apply (case_tac "t=1"; force)
+proof (intro exI conjI allI ballI)
+ let ?h = "\<lambda>(t::real,x). if t = 1 then g x else f x"
+ show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y ?h"
+ proof (rule continuous_map_eq)
+ show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y (f \<circ> snd)"
+ by (simp add: contf continuous_map_of_snd)
+ qed (auto simp: fg)
+ show "P (\<lambda>x. ?h (t, x))" if "t \<in> {0..1}" for t
+ by (cases "t = 1") (simp_all add: assms)
+qed auto
+
+lemma homotopic_with_imp_subset1:
+ "homotopic_with_canon P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
+ by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
+
+lemma homotopic_with_imp_subset2:
+ "homotopic_with_canon P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
+ by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
+
+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"
+ apply (simp add: homotopic_with_def)
+ apply (fast elim!: continuous_on_subset ex_forward)
+ done
+
+lemma homotopic_with_subset_right:
+ "\<lbrakk>homotopic_with_canon P X Y f g; Y \<subseteq> Z\<rbrakk> \<Longrightarrow> homotopic_with_canon P X Z f g"
+ apply (simp add: homotopic_with_def)
+ apply (fast elim!: continuous_on_subset ex_forward)
done
-
-lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
- by auto
-
-lemma homotopic_constant_maps:
- "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow> s = {} \<or> path_component t a b"
-proof (cases "s = {} \<or> t = {}")
- case True with continuous_on_const show ?thesis
- by (auto simp: homotopic_with path_component_def)
-next
- case False
- then obtain c where "c \<in> s" by blast
+subsection\<open>Homotopy with P is an equivalence relation\<close>
+
+text \<open>(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)\<close>
+
+lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f \<longleftrightarrow> continuous_map X Y f \<and> P f"
+ by (auto simp: homotopic_with_imp_continuous_maps intro: homotopic_with_equal dest: homotopic_with_imp_property)
+
+lemma homotopic_with_symD:
+ assumes "homotopic_with P X Y f g"
+ shows "homotopic_with P X Y g f"
+proof -
+ let ?I01 = "subtopology euclideanreal {0..1}"
+ let ?j = "\<lambda>y. (1 - fst y, snd y)"
+ have 1: "continuous_map (prod_topology ?I01 X) (prod_topology euclideanreal X) ?j"
+ apply (intro continuous_intros)
+ apply (simp_all add: prod_topology_subtopology continuous_map_from_subtopology [OF continuous_map_fst])
+ done
+ have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j"
+ proof -
+ have "continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} \<times> topspace X)) ?j"
+ by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff)
+ then show ?thesis
+ by (simp add: prod_topology_subtopology(1))
+ qed
show ?thesis
- proof
- assume "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b)"
- then obtain h :: "real \<times> 'a \<Rightarrow> 'b"
- where conth: "continuous_on ({0..1} \<times> s) h"
- and h: "h ` ({0..1} \<times> s) \<subseteq> t" "(\<forall>x\<in>s. h (0, x) = a)" "(\<forall>x\<in>s. h (1, x) = b)"
- by (auto simp: homotopic_with)
- have "continuous_on {0..1} (h \<circ> (\<lambda>t. (t, c)))"
- apply (rule continuous_intros conth | simp add: image_Pair_const)+
- apply (blast intro: \<open>c \<in> s\<close> continuous_on_subset [OF conth])
- done
- with \<open>c \<in> s\<close> h show "s = {} \<or> path_component t a b"
- apply (simp_all add: homotopic_with path_component_def, auto)
- apply (drule_tac x="h \<circ> (\<lambda>t. (t, c))" in spec)
- apply (auto simp: pathstart_def pathfinish_def path_image_def path_def)
- done
- next
- assume "s = {} \<or> path_component t a b"
- with False show "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b)"
- apply (clarsimp simp: homotopic_with path_component_def pathstart_def pathfinish_def path_image_def path_def)
- apply (rule_tac x="g \<circ> fst" in exI)
- apply (rule conjI continuous_intros | force)+
+ using assms
+ apply (clarsimp simp add: homotopic_with_def)
+ apply (rename_tac h)
+ apply (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI)
+ apply (simp add: continuous_map_compose [OF *])
+ done
+qed
+
+lemma homotopic_with_sym:
+ "homotopic_with P X Y f g \<longleftrightarrow> homotopic_with P X Y g f"
+ by (metis homotopic_with_symD)
+
+proposition homotopic_with_trans:
+ assumes "homotopic_with P X Y f g" "homotopic_with P X Y g h"
+ shows "homotopic_with P X Y f h"
+proof -
+ let ?X01 = "prod_topology (subtopology euclideanreal {0..1}) X"
+ obtain k1 k2
+ where contk1: "continuous_map ?X01 Y k1" and contk2: "continuous_map ?X01 Y k2"
+ and k12: "\<forall>x. k1 (1, x) = g x" "\<forall>x. k2 (0, x) = g x"
+ "\<forall>x. k1 (0, x) = f x" "\<forall>x. k2 (1, x) = h x"
+ and P: "\<forall>t\<in>{0..1}. P (\<lambda>x. k1 (t, x))" "\<forall>t\<in>{0..1}. P (\<lambda>x. k2 (t, x))"
+ using assms by (auto simp: homotopic_with_def)
+ define k where "k \<equiv> \<lambda>y. if fst y \<le> 1/2
+ then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
+ else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y"
+ have keq: "k1 (2 * u, v) = k2 (2 * u -1, v)" if "u = 1/2" for u v
+ by (simp add: k12 that)
+ show ?thesis
+ unfolding homotopic_with_def
+ proof (intro exI conjI)
+ show "continuous_map ?X01 Y k"
+ unfolding k_def
+ proof (rule continuous_map_cases_le)
+ show fst: "continuous_map ?X01 euclideanreal fst"
+ using continuous_map_fst continuous_map_in_subtopology by blast
+ show "continuous_map ?X01 euclideanreal (\<lambda>x. 1/2)"
+ by simp
+ show "continuous_map (subtopology ?X01 {y \<in> topspace ?X01. fst y \<le> 1/2}) Y
+ (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x)))"
+ apply (rule fst continuous_map_compose [OF _ contk1] continuous_intros continuous_map_into_subtopology | simp)+
+ apply (intro continuous_intros fst continuous_map_from_subtopology)
+ apply (force simp: prod_topology_subtopology)
+ using continuous_map_snd continuous_map_from_subtopology by blast
+ show "continuous_map (subtopology ?X01 {y \<in> topspace ?X01. 1/2 \<le> fst y}) Y
+ (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x)))"
+ apply (rule fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology | simp)+
+ apply (rule continuous_intros fst continuous_map_from_subtopology | simp)+
+ apply (force simp: topspace_subtopology prod_topology_subtopology)
+ using continuous_map_snd continuous_map_from_subtopology by blast
+ show "(k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y = (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y"
+ if "y \<in> topspace ?X01" and "fst y = 1/2" for y
+ using that by (simp add: keq)
+ qed
+ show "\<forall>x. k (0, x) = f x"
+ by (simp add: k12 k_def)
+ show "\<forall>x. k (1, x) = h x"
+ by (simp add: k12 k_def)
+ show "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
+ using P
+ apply (clarsimp simp add: k_def)
+ apply (case_tac "t \<le> 1/2", auto)
done
qed
qed
-
-subsection%unimportant\<open>Trivial properties\<close>
-
-lemma homotopic_with_imp_property: "homotopic_with P X Y f g \<Longrightarrow> P f \<and> P g"
- unfolding homotopic_with_def Ball_def
+lemma homotopic_with_id2:
+ "(\<And>x. x \<in> topspace X \<Longrightarrow> g (f x) = x) \<Longrightarrow> homotopic_with (\<lambda>x. True) X X (g \<circ> f) id"
+ by (metis comp_apply continuous_map_id eq_id_iff homotopic_with_equal homotopic_with_symD)
+
+subsection\<open>Continuity lemmas\<close>
+
+lemma homotopic_with_compose_continuous_map_left:
+ "\<lbrakk>homotopic_with p X1 X2 f g; continuous_map X2 X3 h; \<And>j. p j \<Longrightarrow> q(h \<circ> j)\<rbrakk>
+ \<Longrightarrow> homotopic_with q X1 X3 (h \<circ> f) (h \<circ> g)"
+ unfolding homotopic_with_def
apply clarify
- apply (frule_tac x=0 in spec)
- apply (drule_tac x=1 in spec, auto)
+ apply (rename_tac k)
+ apply (rule_tac x="h \<circ> k" in exI)
+ apply (rule conjI continuous_map_compose | simp add: o_def)+
done
-lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h \<circ> Pair t)"
- by (fast intro: continuous_intros elim!: continuous_on_subset)
-
-lemma homotopic_with_imp_continuous:
- assumes "homotopic_with P X Y f g"
- shows "continuous_on X f \<and> continuous_on X g"
+lemma homotopic_compose_continuous_map_left:
+ "\<lbrakk>homotopic_with (\<lambda>k. True) X1 X2 f g; continuous_map X2 X3 h\<rbrakk>
+ \<Longrightarrow> homotopic_with (\<lambda>k. True) X1 X3 (h \<circ> f) (h \<circ> g)"
+ by (simp add: homotopic_with_compose_continuous_map_left)
+
+lemma homotopic_with_compose_continuous_map_right:
+ assumes hom: "homotopic_with p X2 X3 f g" and conth: "continuous_map X1 X2 h"
+ and q: "\<And>j. p j \<Longrightarrow> q(j \<circ> h)"
+ shows "homotopic_with q X1 X3 (f \<circ> h) (g \<circ> h)"
proof -
- obtain h :: "real \<times> 'a \<Rightarrow> 'b"
- where conth: "continuous_on ({0..1} \<times> X) h"
- and h: "\<forall>x. h (0, x) = f x" "\<forall>x. h (1, x) = g x"
- using assms by (auto simp: homotopic_with_def)
- have *: "t \<in> {0..1} \<Longrightarrow> continuous_on X (h \<circ> (\<lambda>x. (t,x)))" for t
- by (rule continuous_intros continuous_on_subset [OF conth] | force)+
+ obtain k
+ where contk: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) X3 k"
+ and k: "\<forall>x. k (0, x) = f x" "\<forall>x. k (1, x) = g x" and p: "\<And>t. t\<in>{0..1} \<Longrightarrow> p (\<lambda>x. k (t, x))"
+ using hom unfolding homotopic_with_def by blast
+ have hsnd: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X2 (h \<circ> snd)"
+ by (rule continuous_map_compose [OF continuous_map_snd conth])
+ let ?h = "k \<circ> (\<lambda>(t,x). (t,h x))"
show ?thesis
- using h *[of 0] *[of 1] by auto
+ unfolding homotopic_with_def
+ proof (intro exI conjI allI ballI)
+ have "continuous_map (prod_topology (top_of_set {0..1}) X1)
+ (prod_topology (top_of_set {0..1::real}) X2) (\<lambda>(t, x). (t, h x))"
+ by (metis (mono_tags, lifting) case_prod_beta' comp_def continuous_map_eq continuous_map_fst continuous_map_pairedI hsnd)
+ then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X3 ?h"
+ by (intro conjI continuous_map_compose [OF _ contk])
+ show "q (\<lambda>x. ?h (t, x))" if "t \<in> {0..1}" for t
+ using q [OF p [OF that]] by (simp add: o_def)
+ qed (auto simp: k)
qed
-proposition homotopic_with_imp_subset1:
- "homotopic_with P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
- by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
-
-proposition homotopic_with_imp_subset2:
- "homotopic_with P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
- by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
-
-proposition homotopic_with_mono:
- assumes hom: "homotopic_with P X Y f g"
- and Q: "\<And>h. \<lbrakk>continuous_on X h; image h X \<subseteq> Y \<and> P h\<rbrakk> \<Longrightarrow> Q h"
- shows "homotopic_with Q X Y f g"
- using hom
- apply (simp add: homotopic_with_def)
- apply (erule ex_forward)
- apply (force simp: intro!: Q dest: continuous_on_o_Pair)
- done
-
-proposition homotopic_with_subset_left:
- "\<lbrakk>homotopic_with P X Y f g; Z \<subseteq> X\<rbrakk> \<Longrightarrow> homotopic_with P Z Y f g"
- apply (simp add: homotopic_with_def)
- apply (fast elim!: continuous_on_subset ex_forward)
- done
-
-proposition homotopic_with_subset_right:
- "\<lbrakk>homotopic_with P X Y f g; Y \<subseteq> Z\<rbrakk> \<Longrightarrow> homotopic_with P X Z f g"
- apply (simp add: homotopic_with_def)
- apply (fast elim!: continuous_on_subset ex_forward)
- done
+lemma homotopic_compose_continuous_map_right:
+ "\<lbrakk>homotopic_with (\<lambda>k. True) X2 X3 f g; continuous_map X1 X2 h\<rbrakk>
+ \<Longrightarrow> homotopic_with (\<lambda>k. True) X1 X3 (f \<circ> h) (g \<circ> h)"
+ by (meson homotopic_with_compose_continuous_map_right)
+
+corollary homotopic_compose:
+ shows "\<lbrakk>homotopic_with (\<lambda>x. True) X Y f f'; homotopic_with (\<lambda>x. True) Y Z g g'\<rbrakk>
+ \<Longrightarrow> homotopic_with (\<lambda>x. True) X Z (g \<circ> f) (g' \<circ> f')"
+ apply (rule homotopic_with_trans [where g = "g \<circ> f'"])
+ apply (simp add: homotopic_compose_continuous_map_left homotopic_with_imp_continuous_maps)
+ by (simp add: homotopic_compose_continuous_map_right homotopic_with_imp_continuous_maps)
+
+
proposition homotopic_with_compose_continuous_right:
- "\<lbrakk>homotopic_with (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
- \<Longrightarrow> homotopic_with p W Y (f \<circ> h) (g \<circ> h)"
+ "\<lbrakk>homotopic_with_canon (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
+ \<Longrightarrow> homotopic_with_canon p W Y (f \<circ> h) (g \<circ> h)"
apply (clarsimp simp add: homotopic_with_def)
apply (rename_tac k)
apply (rule_tac x="k \<circ> (\<lambda>y. (fst y, h (snd y)))" in exI)
@@ -180,13 +307,13 @@
done
proposition homotopic_compose_continuous_right:
- "\<lbrakk>homotopic_with (\<lambda>f. True) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
- \<Longrightarrow> homotopic_with (\<lambda>f. True) W Y (f \<circ> h) (g \<circ> h)"
+ "\<lbrakk>homotopic_with_canon (\<lambda>f. True) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
+ \<Longrightarrow> homotopic_with_canon (\<lambda>f. True) W Y (f \<circ> h) (g \<circ> h)"
using homotopic_with_compose_continuous_right by fastforce
proposition homotopic_with_compose_continuous_left:
- "\<lbrakk>homotopic_with (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
- \<Longrightarrow> homotopic_with p X Z (h \<circ> f) (h \<circ> g)"
+ "\<lbrakk>homotopic_with_canon (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
+ \<Longrightarrow> homotopic_with_canon p X Z (h \<circ> f) (h \<circ> g)"
apply (clarsimp simp add: homotopic_with_def)
apply (rename_tac k)
apply (rule_tac x="h \<circ> k" in exI)
@@ -196,150 +323,171 @@
done
proposition homotopic_compose_continuous_left:
- "\<lbrakk>homotopic_with (\<lambda>_. True) X Y f g;
+ "\<lbrakk>homotopic_with_canon (\<lambda>_. True) X Y f g;
continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
- \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h \<circ> f) (h \<circ> g)"
+ \<Longrightarrow> homotopic_with_canon (\<lambda>f. True) X Z (h \<circ> f) (h \<circ> g)"
using homotopic_with_compose_continuous_left by fastforce
-proposition homotopic_with_Pair:
- assumes hom: "homotopic_with p s t f g" "homotopic_with p' s' t' f' g'"
- and q: "\<And>f g. \<lbrakk>p f; p' g\<rbrakk> \<Longrightarrow> q(\<lambda>(x,y). (f x, g y))"
- shows "homotopic_with q (s \<times> s') (t \<times> t')
- (\<lambda>(x,y). (f x, f' y)) (\<lambda>(x,y). (g x, g' y))"
- using hom
- apply (clarsimp simp add: homotopic_with_def)
- apply (rename_tac k k')
- apply (rule_tac x="\<lambda>z. ((k \<circ> (\<lambda>x. (fst x, fst (snd x)))) z, (k' \<circ> (\<lambda>x. (fst x, snd (snd x)))) z)" in exI)
- apply (rule conjI continuous_intros | erule continuous_on_subset | clarsimp)+
- apply (auto intro!: q [unfolded case_prod_unfold])
- done
-
-lemma homotopic_on_empty [simp]: "homotopic_with (\<lambda>x. True) {} t f g"
- by (metis continuous_on_def empty_iff homotopic_with_equal image_subset_iff)
-
-
-text\<open>Homotopy with P is an equivalence relation (on continuous functions mapping X into Y that satisfy P,
- though this only affects reflexivity.\<close>
-
-
-proposition homotopic_with_refl:
- "homotopic_with P X Y f f \<longleftrightarrow> continuous_on X f \<and> image f X \<subseteq> Y \<and> P f"
- apply (rule iffI)
- using homotopic_with_imp_continuous homotopic_with_imp_property homotopic_with_imp_subset2 apply blast
- apply (simp add: homotopic_with_def)
- apply (rule_tac x="f \<circ> snd" in exI)
- apply (rule conjI continuous_intros | force)+
- done
-
-lemma homotopic_with_symD:
- fixes X :: "'a::real_normed_vector set"
- assumes "homotopic_with P X Y f g"
- shows "homotopic_with P X Y g f"
- using assms
- apply (clarsimp simp add: homotopic_with_def)
- apply (rename_tac h)
- apply (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI)
- apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
+lemma homotopic_from_subtopology:
+ "homotopic_with P X X' f g \<Longrightarrow> homotopic_with P (subtopology X s) X' f g"
+ unfolding homotopic_with_def
+ apply (erule ex_forward)
+ by (simp add: continuous_map_from_subtopology prod_topology_subtopology(2))
+
+lemma homotopic_on_emptyI:
+ assumes "topspace X = {}" "P f" "P g"
+ shows "homotopic_with P X X' f g"
+ unfolding homotopic_with_def
+proof (intro exI conjI ballI)
+ show "P (\<lambda>x. (\<lambda>(t,x). if t = 0 then f x else g x) (t, x))" if "t \<in> {0..1}" for t::real
+ by (cases "t = 0", auto simp: assms)
+qed (auto simp: continuous_map_atin assms)
+
+lemma homotopic_on_empty:
+ "topspace X = {} \<Longrightarrow> (homotopic_with P X X' f g \<longleftrightarrow> P f \<and> P g)"
+ using homotopic_on_emptyI homotopic_with_imp_property by metis
+
+lemma homotopic_with_canon_on_empty [simp]: "homotopic_with_canon (\<lambda>x. True) {} t f g"
+ by (auto intro: homotopic_with_equal)
+
+lemma homotopic_constant_maps:
+ "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow>
+ topspace X = {} \<or> path_component_of X' a b" (is "?lhs = ?rhs")
+proof (cases "topspace X = {}")
+ case False
+ then obtain c where c: "c \<in> topspace X"
+ by blast
+ have "\<exists>g. continuous_map (top_of_set {0..1::real}) X' g \<and> g 0 = a \<and> g 1 = b"
+ if "x \<in> topspace X" and hom: "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. a) (\<lambda>x. b)" for x
+ proof -
+ obtain h :: "real \<times> 'a \<Rightarrow> 'b"
+ where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X' h"
+ and h: "\<And>x. h (0, x) = a" "\<And>x. h (1, x) = b"
+ using hom by (auto simp: homotopic_with_def)
+ have cont: "continuous_map (top_of_set {0..1}) X' (h \<circ> (\<lambda>t. (t, c)))"
+ apply (rule continuous_map_compose [OF _ conth])
+ apply (rule continuous_intros c | simp)+
+ done
+ then show ?thesis
+ by (force simp: h)
+ qed
+ moreover have "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. g 0) (\<lambda>x. g 1)"
+ if "x \<in> topspace X" "a = g 0" "b = g 1" "continuous_map (top_of_set {0..1}) X' g"
+ for x and g :: "real \<Rightarrow> 'b"
+ unfolding homotopic_with_def
+ by (force intro!: continuous_map_compose continuous_intros c that)
+ ultimately show ?thesis
+ using False by (auto simp: path_component_of_def pathin_def)
+qed (simp add: homotopic_on_empty)
+
+proposition homotopic_with_eq:
+ assumes h: "homotopic_with P X Y f g"
+ and f': "\<And>x. x \<in> topspace X \<Longrightarrow> f' x = f x"
+ and g': "\<And>x. x \<in> topspace X \<Longrightarrow> g' x = g x"
+ and P: "(\<And>h k. (\<And>x. x \<in> topspace X \<Longrightarrow> h x = k x) \<Longrightarrow> P h \<longleftrightarrow> P k)"
+ shows "homotopic_with P X Y f' g'"
+ using h unfolding homotopic_with_def
+ apply safe
+ apply (rule_tac x="\<lambda>(u,v). if v \<in> topspace X then h(u,v) else if u = 0 then f' v else g' v" in exI)
+ apply (simp add: f' g', safe)
+ apply (fastforce intro: continuous_map_eq)
+ apply (subst P; fastforce)
done
-proposition homotopic_with_sym:
- fixes X :: "'a::real_normed_vector set"
- shows "homotopic_with P X Y f g \<longleftrightarrow> homotopic_with P X Y g f"
- using homotopic_with_symD by blast
-
-lemma split_01: "{0..1::real} = {0..1/2} \<union> {1/2..1}"
- by force
-
-lemma split_01_prod: "{0..1::real} \<times> X = ({0..1/2} \<times> X) \<union> ({1/2..1} \<times> X)"
- by force
-
-proposition homotopic_with_trans:
- fixes X :: "'a::real_normed_vector set"
- assumes "homotopic_with P X Y f g" and "homotopic_with P X Y g h"
- shows "homotopic_with P X Y f h"
+lemma homotopic_with_prod_topology:
+ assumes "homotopic_with p X1 Y1 f f'" and "homotopic_with q X2 Y2 g g'"
+ and r: "\<And>i j. \<lbrakk>p i; q j\<rbrakk> \<Longrightarrow> r(\<lambda>(x,y). (i x, j y))"
+ shows "homotopic_with r (prod_topology X1 X2) (prod_topology Y1 Y2)
+ (\<lambda>z. (f(fst z),g(snd z))) (\<lambda>z. (f'(fst z), g'(snd z)))"
proof -
- have clo1: "closedin (top_of_set ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({0..1/2::real} \<times> X)"
- apply (simp add: closedin_closed split_01_prod [symmetric])
- apply (rule_tac x="{0..1/2} \<times> UNIV" in exI)
- apply (force simp: closed_Times)
- done
- have clo2: "closedin (top_of_set ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({1/2..1::real} \<times> X)"
- apply (simp add: closedin_closed split_01_prod [symmetric])
- apply (rule_tac x="{1/2..1} \<times> UNIV" in exI)
- apply (force simp: closed_Times)
- done
- { fix k1 k2:: "real \<times> 'a \<Rightarrow> 'b"
- assume cont: "continuous_on ({0..1} \<times> X) k1" "continuous_on ({0..1} \<times> X) k2"
- and Y: "k1 ` ({0..1} \<times> X) \<subseteq> Y" "k2 ` ({0..1} \<times> X) \<subseteq> Y"
- and geq: "\<forall>x. k1 (1, x) = g x" "\<forall>x. k2 (0, x) = g x"
- and k12: "\<forall>x. k1 (0, x) = f x" "\<forall>x. k2 (1, x) = h x"
- and P: "\<forall>t\<in>{0..1}. P (\<lambda>x. k1 (t, x))" "\<forall>t\<in>{0..1}. P (\<lambda>x. k2 (t, x))"
- define k where "k y =
- (if fst y \<le> 1 / 2
- then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
- else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y)" for y
- have keq: "k1 (2 * u, v) = k2 (2 * u - 1, v)" if "u = 1/2" for u v
- by (simp add: geq that)
- have "continuous_on ({0..1} \<times> X) k"
- using cont
- apply (simp add: split_01_prod k_def)
- apply (rule clo1 clo2 continuous_on_cases_local continuous_intros | erule continuous_on_subset | simp add: linear image_subset_iff)+
- apply (force simp: keq)
+ obtain h
+ where h: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) Y1 h"
+ and h0: "\<And>x. h (0, x) = f x"
+ and h1: "\<And>x. h (1, x) = f' x"
+ and p: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> p (\<lambda>x. h (t,x))"
+ using assms unfolding homotopic_with_def by auto
+ obtain k
+ where k: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) Y2 k"
+ and k0: "\<And>x. k (0, x) = g x"
+ and k1: "\<And>x. k (1, x) = g' x"
+ and q: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> q (\<lambda>x. k (t,x))"
+ using assms unfolding homotopic_with_def by auto
+ let ?hk = "\<lambda>(t,x,y). (h(t,x), k(t,y))"
+ show ?thesis
+ unfolding homotopic_with_def
+ proof (intro conjI allI exI)
+ show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (prod_topology X1 X2))
+ (prod_topology Y1 Y2) ?hk"
+ unfolding continuous_map_pairwise case_prod_unfold
+ by (rule conjI continuous_map_pairedI continuous_intros continuous_map_id [unfolded id_def]
+ continuous_map_fst_of [unfolded o_def] continuous_map_snd_of [unfolded o_def]
+ continuous_map_compose [OF _ h, unfolded o_def]
+ continuous_map_compose [OF _ k, unfolded o_def])+
+ next
+ fix x
+ show "?hk (0, x) = (f (fst x), g (snd x))" "?hk (1, x) = (f' (fst x), g' (snd x))"
+ by (auto simp: case_prod_beta h0 k0 h1 k1)
+ qed (auto simp: p q r)
+qed
+
+
+lemma homotopic_with_product_topology:
+ assumes ht: "\<And>i. i \<in> I \<Longrightarrow> homotopic_with (p i) (X i) (Y i) (f i) (g i)"
+ and pq: "\<And>h. (\<And>i. i \<in> I \<Longrightarrow> p i (h i)) \<Longrightarrow> q(\<lambda>x. (\<lambda>i\<in>I. h i (x i)))"
+ shows "homotopic_with q (product_topology X I) (product_topology Y I)
+ (\<lambda>z. (\<lambda>i\<in>I. (f i) (z i))) (\<lambda>z. (\<lambda>i\<in>I. (g i) (z i)))"
+proof -
+ obtain h
+ where h: "\<And>i. i \<in> I \<Longrightarrow> continuous_map (prod_topology (subtopology euclideanreal {0..1}) (X i)) (Y i) (h i)"
+ and h0: "\<And>i x. i \<in> I \<Longrightarrow> h i (0, x) = f i x"
+ and h1: "\<And>i x. i \<in> I \<Longrightarrow> h i (1, x) = g i x"
+ and p: "\<And>i t. \<lbrakk>i \<in> I; t \<in> {0..1}\<rbrakk> \<Longrightarrow> p i (\<lambda>x. h i (t,x))"
+ using ht unfolding homotopic_with_def by metis
+ show ?thesis
+ unfolding homotopic_with_def
+ proof (intro conjI allI exI)
+ let ?h = "\<lambda>(t,z). \<lambda>i\<in>I. h i (t,z i)"
+ have "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
+ (Y i) (\<lambda>x. h i (fst x, snd x i))" if "i \<in> I" for i
+ unfolding continuous_map_pairwise case_prod_unfold
+ apply (intro conjI that continuous_intros continuous_map_compose [OF _ h, unfolded o_def])
+ using continuous_map_componentwise continuous_map_snd that apply fastforce
done
- moreover have "k ` ({0..1} \<times> X) \<subseteq> Y"
- using Y by (force simp: k_def)
- moreover have "\<forall>x. k (0, x) = f x"
- by (simp add: k_def k12)
- moreover have "(\<forall>x. k (1, x) = h x)"
- by (simp add: k_def k12)
- moreover have "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
- using P
- apply (clarsimp simp add: k_def)
- apply (case_tac "t \<le> 1/2", auto)
- done
- ultimately have *: "\<exists>k :: real \<times> 'a \<Rightarrow> 'b.
- continuous_on ({0..1} \<times> X) k \<and> k ` ({0..1} \<times> X) \<subseteq> Y \<and>
- (\<forall>x. k (0, x) = f x) \<and> (\<forall>x. k (1, x) = h x) \<and> (\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x)))"
- by blast
- } note * = this
- show ?thesis
- using assms by (auto intro: * simp add: homotopic_with_def)
+ then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
+ (product_topology Y I) ?h"
+ by (auto simp: continuous_map_componentwise case_prod_beta)
+ show "?h (0, x) = (\<lambda>i\<in>I. f i (x i))" "?h (1, x) = (\<lambda>i\<in>I. g i (x i))" for x
+ by (auto simp: case_prod_beta h0 h1)
+ show "\<forall>t\<in>{0..1}. q (\<lambda>x. ?h (t, x))"
+ by (force intro: p pq)
+ qed
qed
-proposition homotopic_compose:
- fixes s :: "'a::real_normed_vector set"
- shows "\<lbrakk>homotopic_with (\<lambda>x. True) s t f f'; homotopic_with (\<lambda>x. True) t u g g'\<rbrakk>
- \<Longrightarrow> homotopic_with (\<lambda>x. True) s u (g \<circ> f) (g' \<circ> f')"
- apply (rule homotopic_with_trans [where g = "g \<circ> f'"])
- apply (metis homotopic_compose_continuous_left homotopic_with_imp_continuous homotopic_with_imp_subset1)
- by (metis homotopic_compose_continuous_right homotopic_with_imp_continuous homotopic_with_imp_subset2)
-
-
text\<open>Homotopic triviality implicitly incorporates path-connectedness.\<close>
lemma homotopic_triviality:
- fixes S :: "'a::real_normed_vector set"
shows "(\<forall>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
continuous_on S g \<and> g ` S \<subseteq> T
- \<longrightarrow> homotopic_with (\<lambda>x. True) S T f g) \<longleftrightarrow>
+ \<longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g) \<longleftrightarrow>
(S = {} \<or> path_connected T) \<and>
- (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> T \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)))"
+ (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> T \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)))"
(is "?lhs = ?rhs")
proof (cases "S = {} \<or> T = {}")
- case True then show ?thesis by auto
+ case True then show ?thesis
+ by (auto simp: homotopic_on_emptyI)
next
case False show ?thesis
proof
assume LHS [rule_format]: ?lhs
have pab: "path_component T a b" if "a \<in> T" "b \<in> T" for a b
proof -
- have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. b)"
+ have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. b)"
by (simp add: LHS continuous_on_const image_subset_iff that)
then show ?thesis
- using False homotopic_constant_maps by blast
+ using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto
qed
- moreover
- have "\<exists>c. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)" if "continuous_on S f" "f ` S \<subseteq> T" for f
- by (metis (full_types) False LHS equals0I homotopic_constant_maps homotopic_with_imp_continuous homotopic_with_imp_subset2 pab that)
+ moreover
+ have "\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)" if "continuous_on S f" "f ` S \<subseteq> T" for f
+ using False LHS continuous_on_const that by blast
ultimately show ?rhs
by (simp add: path_connected_component)
next
@@ -350,15 +498,15 @@
proof clarify
fix f g
assume "continuous_on S f" "f ` S \<subseteq> T" "continuous_on S g" "g ` S \<subseteq> T"
- obtain c d where c: "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)" and d: "homotopic_with (\<lambda>x. True) S T g (\<lambda>x. d)"
+ obtain c d where c: "homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)" and d: "homotopic_with_canon (\<lambda>x. True) S T g (\<lambda>x. d)"
using False \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> T\<close> RHS \<open>continuous_on S g\<close> \<open>g ` S \<subseteq> T\<close> by blast
then have "c \<in> T" "d \<in> T"
- using False homotopic_with_imp_subset2 by fastforce+
+ using False homotopic_with_imp_continuous_maps by fastforce+
with T have "path_component T c d"
using path_connected_component by blast
- then have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. c) (\<lambda>x. d)"
+ then have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. c) (\<lambda>x. d)"
by (simp add: homotopic_constant_maps)
- with c d show "homotopic_with (\<lambda>x. True) S T f g"
+ with c d show "homotopic_with_canon (\<lambda>x. True) S T f g"
by (meson homotopic_with_symD homotopic_with_trans)
qed
qed
@@ -371,7 +519,7 @@
definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
where
"homotopic_paths s p q \<equiv>
- homotopic_with (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
+ homotopic_with_canon (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
lemma homotopic_paths:
"homotopic_paths s p q \<longleftrightarrow>
@@ -393,14 +541,14 @@
lemma homotopic_paths_imp_path:
"homotopic_paths s p q \<Longrightarrow> path p \<and> path q"
- using homotopic_paths_def homotopic_with_imp_continuous path_def by blast
+ using homotopic_paths_def homotopic_with_imp_continuous_maps path_def continuous_map_subtopology_eu by blast
lemma homotopic_paths_imp_subset:
"homotopic_paths s p q \<Longrightarrow> path_image p \<subseteq> s \<and> path_image q \<subseteq> s"
- by (simp add: homotopic_paths_def homotopic_with_imp_subset1 homotopic_with_imp_subset2 path_image_def)
+ by (metis (mono_tags) continuous_map_subtopology_eu homotopic_paths_def homotopic_with_imp_continuous_maps 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 homotopic_with_refl path_def path_image_def)
+ by (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)
@@ -409,10 +557,16 @@
by (metis homotopic_paths_sym)
proposition homotopic_paths_trans [trans]:
- "\<lbrakk>homotopic_paths s p q; homotopic_paths s q r\<rbrakk> \<Longrightarrow> homotopic_paths s p r"
- apply (simp add: homotopic_paths_def)
- apply (rule homotopic_with_trans, assumption)
- by (metis (mono_tags, lifting) homotopic_with_imp_property homotopic_with_mono)
+ assumes "homotopic_paths s p q" "homotopic_paths s q r"
+ shows "homotopic_paths s p r"
+proof -
+ have "pathstart q = pathstart p" "pathfinish q = pathfinish p"
+ using assms by (simp_all add: homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish)
+ then have "homotopic_with_canon (\<lambda>f. pathstart f = pathstart p \<and> pathfinish f = pathfinish p) {0..1} s q r"
+ using \<open>homotopic_paths s q r\<close> homotopic_paths_def by force
+ then show ?thesis
+ using assms homotopic_paths_def homotopic_with_trans by blast
+qed
proposition homotopic_paths_eq:
"\<lbrakk>path p; path_image p \<subseteq> s; \<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t\<rbrakk> \<Longrightarrow> homotopic_paths s p q"
@@ -460,7 +614,7 @@
qed
lemma homotopic_paths_subset: "\<lbrakk>homotopic_paths s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t p q"
- using homotopic_paths_def homotopic_with_subset_right by blast
+ unfolding homotopic_paths by fast
text\<open> A slightly ad-hoc but useful lemma in constructing homotopies.\<close>
@@ -514,9 +668,7 @@
proposition homotopic_paths_continuous_image:
"\<lbrakk>homotopic_paths s f g; continuous_on s h; h ` s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t (h \<circ> f) (h \<circ> g)"
unfolding homotopic_paths_def
- apply (rule homotopic_with_compose_continuous_left [of _ _ _ s])
- apply (auto simp: pathstart_def pathfinish_def elim!: homotopic_with_mono)
- done
+ by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose)
subsection\<open>Group properties for homotopy of paths\<close>
@@ -586,7 +738,7 @@
definition%important homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool" where
"homotopic_loops s p q \<equiv>
- homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
+ homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
lemma homotopic_loops:
"homotopic_loops s p q \<longleftrightarrow>
@@ -604,17 +756,17 @@
proposition homotopic_loops_imp_path:
"homotopic_loops s p q \<Longrightarrow> path p \<and> path q"
unfolding homotopic_loops_def path_def
- using homotopic_with_imp_continuous by blast
+ using homotopic_with_imp_continuous_maps continuous_map_subtopology_eu by blast
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 (metis homotopic_with_imp_subset1 homotopic_with_imp_subset2)
+ by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
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 homotopic_with_refl path_image_def path_def)
+ by (simp add: homotopic_loops_def path_image_def path_def)
proposition homotopic_loops_sym: "homotopic_loops s p q \<Longrightarrow> homotopic_loops s q p"
by (simp add: homotopic_loops_def homotopic_with_sym)
@@ -628,7 +780,7 @@
proposition homotopic_loops_subset:
"\<lbrakk>homotopic_loops s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t p q"
- by (simp add: homotopic_loops_def homotopic_with_subset_right)
+ by (fastforce simp add: homotopic_loops)
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>
@@ -642,16 +794,14 @@
proposition homotopic_loops_continuous_image:
"\<lbrakk>homotopic_loops s f g; continuous_on s h; h ` s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t (h \<circ> f) (h \<circ> g)"
unfolding homotopic_loops_def
- apply (rule homotopic_with_compose_continuous_left)
- apply (erule homotopic_with_mono)
- by (simp add: pathfinish_def pathstart_def)
+ by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def)
subsection\<open>Relations between the two variants of homotopy\<close>
proposition homotopic_paths_imp_homotopic_loops:
"\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
- by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
+ by (auto simp: homotopic_with_def homotopic_paths_def homotopic_loops_def)
proposition homotopic_loops_imp_homotopic_paths_null:
assumes "homotopic_loops s p (linepath a a)"
@@ -828,7 +978,7 @@
assumes contf: "continuous_on s f"
and contg:"continuous_on s g"
and sub: "\<And>x. x \<in> s \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> t"
- shows "homotopic_with (\<lambda>z. True) s t f g"
+ shows "homotopic_with_canon (\<lambda>z. True) s t f g"
apply (simp add: homotopic_with_def)
apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R f(snd y) + (fst y) *\<^sub>R g(snd y))" in exI)
apply (intro conjI)
@@ -1208,7 +1358,7 @@
subsection\<open>Contractible sets\<close>
definition%important contractible where
- "contractible S \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
+ "contractible S \<equiv> \<exists>a. homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
proposition contractible_imp_simply_connected:
fixes S :: "_::real_normed_vector set"
@@ -1217,10 +1367,10 @@
case True then show ?thesis by force
next
case False
- obtain a where a: "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
+ obtain a where a: "homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
using assms by (force simp: contractible_def)
then have "a \<in> S"
- by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_mem(2))
+ by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_in_topspace topspace_euclidean_subtopology)
show ?thesis
apply (simp add: simply_connected_eq_contractible_loop_all False)
apply (rule bexI [OF _ \<open>a \<in> S\<close>])
@@ -1246,14 +1396,14 @@
assumes f: "continuous_on S f" "f ` S \<subseteq> T"
and g: "continuous_on T g" "g ` T \<subseteq> U"
and T: "contractible T"
- obtains c where "homotopic_with (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
proof -
- obtain b where b: "homotopic_with (\<lambda>x. True) T T id (\<lambda>x. b)"
+ obtain b where b: "homotopic_with_canon (\<lambda>x. True) T T id (\<lambda>x. b)"
using assms by (force simp: contractible_def)
- have "homotopic_with (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
- by (rule homotopic_compose_continuous_left [OF b g])
- then have "homotopic_with (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
- by (rule homotopic_compose_continuous_right [OF _ f])
+ have "homotopic_with_canon (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
+ by (metis Abstract_Topology.continuous_map_subtopology_eu b g homotopic_compose_continuous_map_left)
+ then have "homotopic_with_canon (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
+ by (simp add: f homotopic_with_compose_continuous_map_right)
then show ?thesis
by (simp add: comp_def that)
qed
@@ -1261,7 +1411,7 @@
lemma nullhomotopic_into_contractible:
assumes f: "continuous_on S f" "f ` S \<subseteq> T"
and T: "contractible T"
- obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
apply (rule nullhomotopic_through_contractible [OF f, of id T])
using assms
apply (auto simp: continuous_on_id)
@@ -1270,7 +1420,7 @@
lemma nullhomotopic_from_contractible:
assumes f: "continuous_on S f" "f ` S \<subseteq> T"
and S: "contractible S"
- obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
apply (rule nullhomotopic_through_contractible [OF continuous_on_id _ f S, of S])
using assms
apply (auto simp: comp_def)
@@ -1283,13 +1433,13 @@
"continuous_on S f2" "f2 ` S \<subseteq> T"
"continuous_on T g2" "g2 ` T \<subseteq> U"
"contractible T" "path_connected U"
- shows "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
+ shows "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
proof -
- obtain c1 where c1: "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
+ obtain c1 where c1: "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
apply (rule nullhomotopic_through_contractible [of S f1 T g1 U])
using assms apply auto
done
- obtain c2 where c2: "homotopic_with (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
+ obtain c2 where c2: "homotopic_with_canon (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
apply (rule nullhomotopic_through_contractible [of S f2 T g2 U])
using assms apply auto
done
@@ -1299,7 +1449,7 @@
next
case False
with c1 c2 have "c1 \<in> U" "c2 \<in> U"
- using homotopic_with_imp_subset2 all_not_in_conv image_subset_iff by blast+
+ using homotopic_with_imp_continuous_maps by fastforce+
with \<open>path_connected U\<close> show ?thesis by blast
qed
show ?thesis
@@ -1315,24 +1465,24 @@
assumes f: "continuous_on S f" "f ` S \<subseteq> T"
and g: "continuous_on S g" "g ` S \<subseteq> T"
and T: "contractible T"
- shows "homotopic_with (\<lambda>h. True) S T f g"
+ shows "homotopic_with_canon (\<lambda>h. True) S T f g"
using homotopic_through_contractible [of S f T id T g id]
-by (simp add: assms contractible_imp_path_connected continuous_on_id)
+by (simp add: assms contractible_imp_path_connected)
lemma homotopic_from_contractible:
fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
assumes f: "continuous_on S f" "f ` S \<subseteq> T"
and g: "continuous_on S g" "g ` S \<subseteq> T"
and "contractible S" "path_connected T"
- shows "homotopic_with (\<lambda>h. True) S T f g"
+ shows "homotopic_with_canon (\<lambda>h. True) S T f g"
using homotopic_through_contractible [of S id S f T id g]
-by (simp add: assms contractible_imp_path_connected continuous_on_id)
+by (simp add: assms contractible_imp_path_connected)
lemma starlike_imp_contractible_gen:
fixes S :: "'a::real_normed_vector set"
assumes S: "starlike S"
and P: "\<And>a T. \<lbrakk>a \<in> S; 0 \<le> T; T \<le> 1\<rbrakk> \<Longrightarrow> P(\<lambda>x. (1 - T) *\<^sub>R x + T *\<^sub>R a)"
- obtains a where "homotopic_with P S S (\<lambda>x. x) (\<lambda>x. a)"
+ obtains a where "homotopic_with_canon P S S (\<lambda>x. x) (\<lambda>x. a)"
proof -
obtain a where "a \<in> S" and a: "\<And>x. x \<in> S \<Longrightarrow> closed_segment a x \<subseteq> S"
using S by (auto simp: starlike_def)
@@ -1385,7 +1535,7 @@
using convex_imp_simply_connected is_interval_convex_1 is_interval_path_connected_1 simply_connected_imp_path_connected by auto
lemma contractible_empty [simp]: "contractible {}"
- by (simp add: contractible_def homotopic_with)
+ by (simp add: contractible_def homotopic_on_emptyI)
lemma contractible_convex_tweak_boundary_points:
fixes S :: "'a::euclidean_space set"
@@ -1445,27 +1595,6 @@
done
qed
-lemma homotopy_dominated_contractibility:
- fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
- assumes S: "contractible S"
- and f: "continuous_on S f" "image f S \<subseteq> T"
- and g: "continuous_on T g" "image g T \<subseteq> S"
- and hom: "homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
- shows "contractible T"
-proof -
- obtain b where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. b)"
- using nullhomotopic_from_contractible [OF f S] .
- then have homg: "homotopic_with (\<lambda>x. True) T T ((\<lambda>x. b) \<circ> g) (f \<circ> g)"
- by (rule homotopic_with_compose_continuous_right [OF homotopic_with_symD g])
- show ?thesis
- apply (simp add: contractible_def)
- apply (rule exI [where x = b])
- apply (rule homotopic_with_symD)
- apply (rule homotopic_with_trans [OF _ hom])
- using homg apply (simp add: o_def)
- done
-qed
-
subsection\<open>Local versions of topological properties in general\<close>
@@ -1541,7 +1670,7 @@
apply (simp add: open_Int)
apply (rule_tac x="V1 \<inter> V2" in exI)
apply (auto intro: P)
-done
+ done
lemma locally_Times:
fixes S :: "('a::metric_space) set" and T :: "('b::metric_space) set"
@@ -1561,7 +1690,7 @@
with \<open>U \<times> V \<subseteq> W\<close> show "\<exists>u v. openin (top_of_set (S \<times> T)) u \<and> R v \<and> (x,y) \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> W"
apply (rule_tac x="U1 \<times> V1" in exI)
apply (rule_tac x="U2 \<times> V2" in exI)
- apply (auto simp: openin_Times R)
+ apply (auto simp: openin_Times R openin_Times_eq)
done
qed
@@ -3195,10 +3324,10 @@
and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f;
continuous_on u g; g ` u \<subseteq> s; P g\<rbrakk>
- \<Longrightarrow> homotopic_with P u s f g"
+ \<Longrightarrow> homotopic_with_canon P u s f g"
and contf: "continuous_on u f" and imf: "f ` u \<subseteq> t" and Qf: "Q f"
and contg: "continuous_on u g" and img: "g ` u \<subseteq> t" and Qg: "Q g"
- shows "homotopic_with Q u t f g"
+ shows "homotopic_with_canon Q u t f g"
proof -
have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
have geq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> g)) x = g x" using idhk img by auto
@@ -3214,17 +3343,15 @@
using img imk by fastforce
moreover have "P (k \<circ> g)"
by (simp add: P Qg contg img)
- ultimately have "homotopic_with P u s (k \<circ> f) (k \<circ> g)"
+ ultimately have "homotopic_with_canon P u s (k \<circ> f) (k \<circ> g)"
by (rule hom)
- then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
+ then have "homotopic_with_canon Q u t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
using Q by (auto simp: conth imh)
then show ?thesis
apply (rule homotopic_with_eq)
- apply (metis feq)
- apply (metis geq)
- apply (metis Qeq)
- done
+ using feq geq apply fastforce+
+ using Qeq topspace_euclidean_subtopology by blast
qed
lemma homotopically_trivial_retraction_null_gen:
@@ -3232,9 +3359,9 @@
and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk>
- \<Longrightarrow> \<exists>c. homotopic_with P u s f (\<lambda>x. c)"
+ \<Longrightarrow> \<exists>c. homotopic_with_canon P u s f (\<lambda>x. c)"
and contf: "continuous_on u f" and imf:"f ` u \<subseteq> t" and Qf: "Q f"
- obtains c where "homotopic_with Q u t f (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon Q u t f (\<lambda>x. c)"
proof -
have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
have "continuous_on u (k \<circ> f)"
@@ -3243,17 +3370,17 @@
using imf imk by fastforce
moreover have "P (k \<circ> f)"
by (simp add: P Qf contf imf)
- ultimately obtain c where "homotopic_with P u s (k \<circ> f) (\<lambda>x. c)"
+ ultimately obtain c where "homotopic_with_canon P u s (k \<circ> f) (\<lambda>x. c)"
by (metis hom)
- then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
+ then have "homotopic_with_canon Q u t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
using Q by (auto simp: conth imh)
then show ?thesis
apply (rule_tac c = "h c" in that)
apply (erule homotopic_with_eq)
- apply (metis feq, simp)
- apply (metis Qeq)
- done
+ using feq apply auto[1]
+ apply simp
+ using Qeq topspace_euclidean_subtopology by blast
qed
lemma cohomotopically_trivial_retraction_gen:
@@ -3262,10 +3389,10 @@
and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f;
continuous_on s g; g ` s \<subseteq> u; P g\<rbrakk>
- \<Longrightarrow> homotopic_with P s u f g"
+ \<Longrightarrow> homotopic_with_canon P s u f g"
and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f"
and contg: "continuous_on t g" and img: "g ` t \<subseteq> u" and Qg: "Q g"
- shows "homotopic_with Q t u f g"
+ shows "homotopic_with_canon Q t u f g"
proof -
have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
have geq: "\<And>x. x \<in> t \<Longrightarrow> (g \<circ> h \<circ> k) x = g x" using idhk img by auto
@@ -3281,17 +3408,16 @@
using img imh by fastforce
moreover have "P (g \<circ> h)"
by (simp add: P Qg contg img)
- ultimately have "homotopic_with P s u (f \<circ> h) (g \<circ> h)"
+ ultimately have "homotopic_with_canon P s u (f \<circ> h) (g \<circ> h)"
by (rule hom)
- then have "homotopic_with Q t u (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
+ then have "homotopic_with_canon Q t u (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
using Q by (auto simp: contk imk)
then show ?thesis
apply (rule homotopic_with_eq)
- apply (metis feq)
- apply (metis geq)
- apply (metis Qeq)
- done
+ using feq apply auto[1]
+ using geq apply auto[1]
+ using Qeq topspace_euclidean_subtopology by blast
qed
lemma cohomotopically_trivial_retraction_null_gen:
@@ -3299,9 +3425,9 @@
and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk>
- \<Longrightarrow> \<exists>c. homotopic_with P s u f (\<lambda>x. c)"
+ \<Longrightarrow> \<exists>c. homotopic_with_canon P s u f (\<lambda>x. c)"
and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f"
- obtains c where "homotopic_with Q t u f (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon Q t u f (\<lambda>x. c)"
proof -
have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
have "continuous_on s (f \<circ> h)"
@@ -3310,17 +3436,17 @@
using imf imh by fastforce
moreover have "P (f \<circ> h)"
by (simp add: P Qf contf imf)
- ultimately obtain c where "homotopic_with P s u (f \<circ> h) (\<lambda>x. c)"
+ ultimately obtain c where "homotopic_with_canon P s u (f \<circ> h) (\<lambda>x. c)"
by (metis hom)
- then have "homotopic_with Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
+ then have "homotopic_with_canon Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
using Q by (auto simp: contk imk)
then show ?thesis
apply (rule_tac c = c in that)
apply (erule homotopic_with_eq)
- apply (metis feq, simp)
- apply (metis Qeq)
- done
+ using feq apply auto[1]
+ apply simp
+ using Qeq topspace_euclidean_subtopology by blast
qed
end
@@ -3346,59 +3472,64 @@
subsection\<open>Homotopy equivalence\<close>
-definition%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
- (infix "homotopy'_eqv" 50)
- where "S homotopy_eqv T \<equiv>
- \<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
- continuous_on T g \<and> g ` T \<subseteq> S \<and>
- homotopic_with (\<lambda>x. True) S S (g \<circ> f) id \<and>
- homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
-
-lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
- unfolding homeomorphic_def homotopy_eqv_def homeomorphism_def
- by (fastforce intro!: homotopic_with_equal continuous_on_compose)
-
-lemma homotopy_eqv_refl: "S homotopy_eqv S"
- by (rule homeomorphic_imp_homotopy_eqv homeomorphic_refl)+
-
-lemma homotopy_eqv_sym: "S homotopy_eqv T \<longleftrightarrow> T homotopy_eqv S"
- by (auto simp: homotopy_eqv_def)
+subsection\<open>Homotopy equivalence of topological spaces.\<close>
+
+definition%important homotopy_equivalent_space
+ (infix "homotopy'_equivalent'_space" 50)
+ where "X homotopy_equivalent_space Y \<equiv>
+ (\<exists>f g. continuous_map X Y f \<and>
+ continuous_map Y X g \<and>
+ homotopic_with (\<lambda>x. True) X X (g \<circ> f) id \<and>
+ homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) id)"
+
+lemma homeomorphic_imp_homotopy_equivalent_space:
+ "X homeomorphic_space Y \<Longrightarrow> X homotopy_equivalent_space Y"
+ unfolding homeomorphic_space_def homotopy_equivalent_space_def
+ apply (erule ex_forward)+
+ by (simp add: homotopic_with_equal homotopic_with_sym homeomorphic_maps_def)
+
+lemma homotopy_equivalent_space_refl:
+ "X homotopy_equivalent_space X"
+ by (simp add: homeomorphic_imp_homotopy_equivalent_space homeomorphic_space_refl)
+
+lemma homotopy_equivalent_space_sym:
+ "X homotopy_equivalent_space Y \<longleftrightarrow> Y homotopy_equivalent_space X"
+ by (meson homotopy_equivalent_space_def)
lemma homotopy_eqv_trans [trans]:
- fixes S :: "'a::real_normed_vector set" and U :: "'c::real_normed_vector set"
- assumes ST: "S homotopy_eqv T" and TU: "T homotopy_eqv U"
- shows "S homotopy_eqv U"
+ assumes 1: "X homotopy_equivalent_space Y" and 2: "Y homotopy_equivalent_space U"
+ shows "X homotopy_equivalent_space U"
proof -
- obtain f1 g1 where f1: "continuous_on S f1" "f1 ` S \<subseteq> T"
- and g1: "continuous_on T g1" "g1 ` T \<subseteq> S"
- and hom1: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> f1) id"
- "homotopic_with (\<lambda>x. True) T T (f1 \<circ> g1) id"
- using ST by (auto simp: homotopy_eqv_def)
- obtain f2 g2 where f2: "continuous_on T f2" "f2 ` T \<subseteq> U"
- and g2: "continuous_on U g2" "g2 ` U \<subseteq> T"
- and hom2: "homotopic_with (\<lambda>x. True) T T (g2 \<circ> f2) id"
+ obtain f1 g1 where f1: "continuous_map X Y f1"
+ and g1: "continuous_map Y X g1"
+ and hom1: "homotopic_with (\<lambda>x. True) X X (g1 \<circ> f1) id"
+ "homotopic_with (\<lambda>x. True) Y Y (f1 \<circ> g1) id"
+ using 1 by (auto simp: homotopy_equivalent_space_def)
+ obtain f2 g2 where f2: "continuous_map Y U f2"
+ and g2: "continuous_map U Y g2"
+ and hom2: "homotopic_with (\<lambda>x. True) Y Y (g2 \<circ> f2) id"
"homotopic_with (\<lambda>x. True) U U (f2 \<circ> g2) id"
- using TU by (auto simp: homotopy_eqv_def)
- have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
- by (rule homotopic_with_compose_continuous_right hom2 f1)+
- then have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
+ using 2 by (auto simp: homotopy_equivalent_space_def)
+ have "homotopic_with (\<lambda>f. True) X Y (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
+ using f1 hom2(1) homotopic_compose_continuous_map_right by blast
+ then have "homotopic_with (\<lambda>f. True) X Y (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
by (simp add: o_assoc)
- then have "homotopic_with (\<lambda>x. True) S S
+ then have "homotopic_with (\<lambda>x. True) X X
(g1 \<circ> (g2 \<circ> (f2 \<circ> f1))) (g1 \<circ> (id \<circ> f1))"
- by (simp add: g1 homotopic_with_compose_continuous_left)
- moreover have "homotopic_with (\<lambda>x. True) S S (g1 \<circ> id \<circ> f1) id"
+ by (simp add: g1 homotopic_compose_continuous_map_left)
+ moreover have "homotopic_with (\<lambda>x. True) X X (g1 \<circ> id \<circ> f1) id"
using hom1 by simp
- ultimately have SS: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
+ ultimately have SS: "homotopic_with (\<lambda>x. True) X X (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
apply (simp add: o_assoc)
apply (blast intro: homotopic_with_trans)
done
- have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> g1 \<circ> g2) (id \<circ> g2)"
- by (rule homotopic_with_compose_continuous_right hom1 g2)+
- then have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
+ have "homotopic_with (\<lambda>f. True) U Y (f1 \<circ> g1 \<circ> g2) (id \<circ> g2)"
+ using g2 hom1(2) homotopic_with_compose_continuous_map_right by fastforce
+ then have "homotopic_with (\<lambda>f. True) U Y (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
by (simp add: o_assoc)
then have "homotopic_with (\<lambda>x. True) U U
(f2 \<circ> (f1 \<circ> (g1 \<circ> g2))) (f2 \<circ> (id \<circ> g2))"
- by (simp add: f2 homotopic_with_compose_continuous_left)
+ by (simp add: f2 homotopic_with_compose_continuous_map_left)
moreover have "homotopic_with (\<lambda>x. True) U U (f2 \<circ> id \<circ> g2) id"
using hom2 by simp
ultimately have UU: "homotopic_with (\<lambda>x. True) U U (f2 \<circ> f1 \<circ> (g1 \<circ> g2)) id"
@@ -3406,14 +3537,382 @@
apply (blast intro: homotopic_with_trans)
done
show ?thesis
- unfolding homotopy_eqv_def
- apply (rule_tac x = "f2 \<circ> f1" in exI)
- apply (rule_tac x = "g1 \<circ> g2" in exI)
- apply (intro conjI continuous_on_compose SS UU)
- using f1 f2 g1 g2 apply (force simp: elim!: continuous_on_subset)+
- done
+ unfolding homotopy_equivalent_space_def
+ by (blast intro: f1 f2 g1 g2 continuous_map_compose SS UU)
+qed
+
+lemma deformation_retraction_imp_homotopy_equivalent_space:
+ "\<lbrakk>homotopic_with (\<lambda>x. True) X X (s \<circ> r) id; retraction_maps X Y r s\<rbrakk>
+ \<Longrightarrow> X homotopy_equivalent_space Y"
+ unfolding homotopy_equivalent_space_def retraction_maps_def
+ apply (rule_tac x=r in exI)
+ apply (rule_tac x=s in exI)
+ apply (auto simp: homotopic_with_equal continuous_map_compose)
+ done
+
+lemma deformation_retract_imp_homotopy_equivalent_space:
+ "\<lbrakk>homotopic_with (\<lambda>x. True) X X r id; retraction_maps X Y r id\<rbrakk>
+ \<Longrightarrow> X homotopy_equivalent_space Y"
+ using deformation_retraction_imp_homotopy_equivalent_space by force
+
+lemma deformation_retract_of_space:
+ "S \<subseteq> topspace X \<and>
+ (\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id) \<longleftrightarrow>
+ S retract_of_space X \<and> (\<exists>f. homotopic_with (\<lambda>x. True) X X id f \<and> f ` (topspace X) \<subseteq> S)"
+proof (cases "S \<subseteq> topspace X")
+ case True
+ moreover have "(\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id)
+ \<longleftrightarrow> (S retract_of_space X \<and> (\<exists>f. homotopic_with (\<lambda>x. True) X X id f \<and> f ` topspace X \<subseteq> S))"
+ unfolding retract_of_space_def
+ proof safe
+ fix f r
+ assume f: "homotopic_with (\<lambda>x. True) X X id f"
+ and fS: "f ` topspace X \<subseteq> S"
+ and r: "continuous_map X (subtopology X S) r"
+ and req: "\<forall>x\<in>S. r x = x"
+ show "\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id"
+ proof (intro exI conjI)
+ have "homotopic_with (\<lambda>x. True) X X f r"
+ proof (rule homotopic_with_eq)
+ show "homotopic_with (\<lambda>x. True) X X (r \<circ> f) (r \<circ> id)"
+ using homotopic_with_symD continuous_map_into_fulltopology f homotopic_compose_continuous_map_left r by blast
+ show "f x = (r \<circ> f) x" if "x \<in> topspace X" for x
+ using that fS req by auto
+ qed auto
+ then show "homotopic_with (\<lambda>x. True) X X id r"
+ by (rule homotopic_with_trans [OF f])
+ next
+ show "retraction_maps X (subtopology X S) r id"
+ by (simp add: r req retraction_maps_def topspace_subtopology)
+ qed
+ qed (use True in \<open>auto simp: retraction_maps_def topspace_subtopology_subset continuous_map_in_subtopology\<close>)
+ ultimately show ?thesis by simp
+qed (auto simp: retract_of_space_def retraction_maps_def)
+
+
+
+subsection\<open>Contractible spaces\<close>
+
+text\<open>The definition (which agrees with "contractible" on subsets of Euclidean space)
+is a little cryptic because we don't in fact assume that the constant "a" is in the space.
+This forces the convention that the empty space / set is contractible, avoiding some special cases. \<close>
+
+definition contractible_space where
+ "contractible_space X \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
+
+lemma contractible_space_top_of_set [simp]:"contractible_space (top_of_set S) \<longleftrightarrow> contractible S"
+ by (auto simp: contractible_space_def contractible_def)
+
+lemma contractible_space_empty:
+ "topspace X = {} \<Longrightarrow> contractible_space X"
+ apply (simp add: contractible_space_def homotopic_with_def)
+ apply (rule_tac x=undefined in exI)
+ apply (rule_tac x="\<lambda>(t,x). if t = 0 then x else undefined" in exI)
+ apply (auto simp: continuous_map_on_empty)
+ done
+
+lemma contractible_space_singleton:
+ "topspace X = {a} \<Longrightarrow> contractible_space X"
+ apply (simp add: contractible_space_def homotopic_with_def)
+ apply (rule_tac x=a in exI)
+ apply (rule_tac x="\<lambda>(t,x). if t = 0 then x else a" in exI)
+ apply (auto intro: continuous_map_eq [where f = "\<lambda>z. a"])
+ done
+
+lemma contractible_space_subset_singleton:
+ "topspace X \<subseteq> {a} \<Longrightarrow> contractible_space X"
+ by (meson contractible_space_empty contractible_space_singleton subset_singletonD)
+
+lemma contractible_space_subtopology_singleton:
+ "contractible_space(subtopology X {a})"
+ by (meson contractible_space_subset_singleton insert_subset path_connectedin_singleton path_connectedin_subtopology subsetI)
+
+lemma contractible_space:
+ "contractible_space X \<longleftrightarrow>
+ topspace X = {} \<or>
+ (\<exists>a \<in> topspace X. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a))"
+proof (cases "topspace X = {}")
+ case False
+ then show ?thesis
+ apply (auto simp: contractible_space_def)
+ using homotopic_with_imp_continuous_maps by fastforce
+qed (simp add: contractible_space_empty)
+
+lemma contractible_imp_path_connected_space:
+ assumes "contractible_space X" shows "path_connected_space X"
+proof (cases "topspace X = {}")
+ case False
+ have *: "path_connected_space X"
+ if "a \<in> topspace X" and conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X h"
+ and h: "\<forall>x. h (0, x) = x" "\<forall>x. h (1, x) = a"
+ for a and h :: "real \<times> 'a \<Rightarrow> 'a"
+ proof -
+ have "path_component_of X b a" if "b \<in> topspace X" for b
+ using that unfolding path_component_of_def
+ apply (rule_tac x="h \<circ> (\<lambda>x. (x,b))" in exI)
+ apply (simp add: h pathin_def)
+ apply (rule continuous_map_compose [OF _ conth])
+ apply (auto simp: continuous_map_pairwise intro!: continuous_intros continuous_map_compose continuous_map_id [unfolded id_def])
+ done
+ then show ?thesis
+ by (metis path_component_of_equiv path_connected_space_iff_path_component)
+ qed
+ show ?thesis
+ using assms False by (auto simp: contractible_space homotopic_with_def *)
+qed (simp add: path_connected_space_topspace_empty)
+
+lemma contractible_imp_connected_space:
+ "contractible_space X \<Longrightarrow> connected_space X"
+ by (simp add: contractible_imp_path_connected_space path_connected_imp_connected_space)
+
+lemma contractible_space_alt:
+ "contractible_space X \<longleftrightarrow> (\<forall>a \<in> topspace X. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a))" (is "?lhs = ?rhs")
+proof
+ assume X: ?lhs
+ then obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
+ by (auto simp: contractible_space_def)
+ show ?rhs
+ proof
+ show "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. b)" if "b \<in> topspace X" for b
+ apply (rule homotopic_with_trans [OF a])
+ using homotopic_constant_maps path_connected_space_imp_path_component_of
+ by (metis (full_types) X a continuous_map_const contractible_imp_path_connected_space homotopic_with_imp_continuous_maps that)
+ qed
+next
+ assume R: ?rhs
+ then show ?lhs
+ apply (simp add: contractible_space_def)
+ by (metis equals0I homotopic_on_emptyI)
+qed
+
+
+lemma compose_const [simp]: "f \<circ> (\<lambda>x. a) = (\<lambda>x. f a)" "(\<lambda>x. a) \<circ> g = (\<lambda>x. a)"
+ by (simp_all add: o_def)
+
+lemma nullhomotopic_through_contractible_space:
+ assumes f: "continuous_map X Y f" and g: "continuous_map Y Z g" and Y: "contractible_space Y"
+ obtains c where "homotopic_with (\<lambda>h. True) X Z (g \<circ> f) (\<lambda>x. c)"
+proof -
+ obtain b where b: "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. b)"
+ using Y by (auto simp: contractible_space_def)
+ show thesis
+ using homotopic_compose_continuous_map_right
+ [OF homotopic_compose_continuous_map_left [OF b g] f]
+ by (simp add: that)
qed
+lemma nullhomotopic_into_contractible_space:
+ assumes f: "continuous_map X Y f" and Y: "contractible_space Y"
+ obtains c where "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
+ using nullhomotopic_through_contractible_space [OF f _ Y]
+ by (metis continuous_map_id id_comp)
+
+lemma nullhomotopic_from_contractible_space:
+ assumes f: "continuous_map X Y f" and X: "contractible_space X"
+ obtains c where "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
+ using nullhomotopic_through_contractible_space [OF _ f X]
+ by (metis comp_id continuous_map_id)
+
+lemma homotopy_dominated_contractibility:
+ assumes f: "continuous_map X Y f" and g: "continuous_map Y X g"
+ and hom: "homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) id" and X: "contractible_space X"
+ shows "contractible_space Y"
+proof -
+ obtain c where c: "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
+ using nullhomotopic_from_contractible_space [OF f X] .
+ have "homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) (\<lambda>x. c)"
+ using homotopic_compose_continuous_map_right [OF c g] by fastforce
+ then have "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. c)"
+ using homotopic_with_trans [OF _ hom] homotopic_with_symD by blast
+ then show ?thesis
+ unfolding contractible_space_def ..
+qed
+
+lemma homotopy_equivalent_space_contractibility:
+ "X homotopy_equivalent_space Y \<Longrightarrow> (contractible_space X \<longleftrightarrow> contractible_space Y)"
+ unfolding homotopy_equivalent_space_def
+ by (blast intro: homotopy_dominated_contractibility)
+
+lemma homeomorphic_space_contractibility:
+ "X homeomorphic_space Y
+ \<Longrightarrow> (contractible_space X \<longleftrightarrow> contractible_space Y)"
+ by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)
+
+lemma contractible_eq_homotopy_equivalent_singleton_subtopology:
+ "contractible_space X \<longleftrightarrow>
+ topspace X = {} \<or> (\<exists>a \<in> topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is "?lhs = ?rhs")
+proof (cases "topspace X = {}")
+ case False
+ show ?thesis
+ proof
+ assume ?lhs
+ then obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
+ by (auto simp: contractible_space_def)
+ then have "a \<in> topspace X"
+ by (metis False continuous_map_const homotopic_with_imp_continuous_maps)
+ then have "X homotopy_equivalent_space subtopology X {a}"
+ unfolding homotopy_equivalent_space_def
+ apply (rule_tac x="\<lambda>x. a" in exI)
+ apply (rule_tac x=id in exI)
+ apply (auto simp: homotopic_with_sym topspace_subtopology_subset a)
+ using connectedin_absolute connectedin_sing contractible_space_alt contractible_space_subtopology_singleton by fastforce
+ with \<open>a \<in> topspace X\<close> show ?rhs
+ by blast
+ next
+ assume ?rhs
+ then show ?lhs
+ by (meson False contractible_space_subtopology_singleton homotopy_equivalent_space_contractibility)
+ qed
+qed (simp add: contractible_space_empty)
+
+lemma contractible_space_retraction_map_image:
+ assumes "retraction_map X Y f" and X: "contractible_space X"
+ shows "contractible_space Y"
+proof -
+ obtain g where f: "continuous_map X Y f" and g: "continuous_map Y X g" and fg: "\<forall>y \<in> topspace Y. f(g y) = y"
+ using assms by (auto simp: retraction_map_def retraction_maps_def)
+ obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
+ using X by (auto simp: contractible_space_def)
+ have "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. f a)"
+ proof (rule homotopic_with_eq)
+ show "homotopic_with (\<lambda>x. True) Y Y (f \<circ> id \<circ> g) (f \<circ> (\<lambda>x. a) \<circ> g)"
+ using f g a homotopic_compose_continuous_map_left homotopic_compose_continuous_map_right by metis
+ qed (use fg in auto)
+ then show ?thesis
+ unfolding contractible_space_def by blast
+qed
+
+lemma contractible_space_prod_topology:
+ "contractible_space(prod_topology X Y) \<longleftrightarrow>
+ topspace X = {} \<or> topspace Y = {} \<or> contractible_space X \<and> contractible_space Y"
+proof (cases "topspace X = {} \<or> topspace Y = {}")
+ case True
+ then have "topspace (prod_topology X Y) = {}"
+ by simp
+ then show ?thesis
+ by (auto simp: contractible_space_empty)
+next
+ case False
+ have "contractible_space(prod_topology X Y) \<longleftrightarrow> contractible_space X \<and> contractible_space Y"
+ proof safe
+ assume XY: "contractible_space (prod_topology X Y)"
+ with False have "retraction_map (prod_topology X Y) X fst"
+ by (auto simp: contractible_space False retraction_map_fst)
+ then show "contractible_space X"
+ by (rule contractible_space_retraction_map_image [OF _ XY])
+ have "retraction_map (prod_topology X Y) Y snd"
+ using False XY by (auto simp: contractible_space False retraction_map_snd)
+ then show "contractible_space Y"
+ by (rule contractible_space_retraction_map_image [OF _ XY])
+ next
+ assume "contractible_space X" and "contractible_space Y"
+ with False obtain a b
+ where "a \<in> topspace X" and a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
+ and "b \<in> topspace Y" and b: "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. b)"
+ by (auto simp: contractible_space)
+ with False show "contractible_space (prod_topology X Y)"
+ apply (simp add: contractible_space)
+ apply (rule_tac x=a in bexI)
+ apply (rule_tac x=b in bexI)
+ using homotopic_with_prod_topology [OF a b]
+ apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff)
+ apply auto
+ done
+ qed
+ with False show ?thesis
+ by auto
+qed
+
+
+
+
+lemma contractible_space_product_topology:
+ "contractible_space(product_topology X I) \<longleftrightarrow>
+ topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. contractible_space(X i))"
+proof (cases "topspace (product_topology X I) = {}")
+ case False
+ have 1: "contractible_space (X i)"
+ if XI: "contractible_space (product_topology X I)" and "i \<in> I"
+ for i
+ proof (rule contractible_space_retraction_map_image [OF _ XI])
+ show "retraction_map (product_topology X I) (X i) (\<lambda>x. x i)"
+ using False by (simp add: retraction_map_product_projection \<open>i \<in> I\<close>)
+ qed
+ have 2: "contractible_space (product_topology X I)"
+ if "x \<in> topspace (product_topology X I)" and cs: "\<forall>i\<in>I. contractible_space (X i)"
+ for x :: "'a \<Rightarrow> 'b"
+ proof -
+ obtain f where f: "\<And>i. i\<in>I \<Longrightarrow> homotopic_with (\<lambda>x. True) (X i) (X i) id (\<lambda>x. f i)"
+ using cs unfolding contractible_space_def by metis
+ have "homotopic_with (\<lambda>x. True)
+ (product_topology X I) (product_topology X I) id (\<lambda>x. restrict f I)"
+ by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto simp: topspace_product_topology)
+ then show ?thesis
+ by (auto simp: contractible_space_def)
+ qed
+ show ?thesis
+ using False 1 2 by blast
+qed (simp add: contractible_space_empty)
+
+
+lemma contractible_space_subtopology_euclideanreal [simp]:
+ "contractible_space(subtopology euclideanreal S) \<longleftrightarrow> is_interval S"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "path_connectedin (subtopology euclideanreal S) S"
+ using contractible_imp_path_connected_space path_connectedin_topspace path_connectedin_absolute
+ by (simp add: contractible_imp_path_connected)
+ then show ?rhs
+ by (simp add: is_interval_path_connected_1)
+next
+ assume ?rhs
+ then have "convex S"
+ by (simp add: is_interval_convex_1)
+ show ?lhs
+ proof (cases "S = {}")
+ case False
+ then obtain z where "z \<in> S"
+ by blast
+ show ?thesis
+ unfolding contractible_space_def homotopic_with_def
+ proof (intro exI conjI allI)
+ show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set S)) (top_of_set S)
+ (\<lambda>(t,x). (1 - t) * x + t * z)"
+ apply (auto simp: case_prod_unfold)
+ apply (intro continuous_intros)
+ using \<open>z \<in> S\<close> apply (auto intro: convexD [OF \<open>convex S\<close>, simplified])
+ done
+ qed auto
+ qed (simp add: contractible_space_empty)
+qed
+
+
+corollary contractible_space_euclideanreal: "contractible_space euclideanreal"
+proof -
+ have "contractible_space (subtopology euclideanreal UNIV)"
+ using contractible_space_subtopology_euclideanreal by blast
+ then show ?thesis
+ by simp
+qed
+
+
+abbreviation%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
+ (infix "homotopy'_eqv" 50)
+ where "S homotopy_eqv T \<equiv> top_of_set S homotopy_equivalent_space top_of_set T"
+
+
+
+
+
+lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
+ unfolding homeomorphic_def homeomorphism_def homotopy_equivalent_space_def
+ apply (erule ex_forward)+
+ apply auto
+ apply (metis homotopic_with_id2 topspace_euclidean_subtopology)
+ by (metis (full_types) homotopic_with_id2 imageE topspace_euclidean_subtopology)
+
+
lemma homotopy_eqv_inj_linear_image:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "linear f" "inj f"
@@ -3436,33 +3935,33 @@
and g: "continuous_on U g" "g ` U \<subseteq> T"
and homUS: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
continuous_on U g; g ` U \<subseteq> S\<rbrakk>
- \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
- shows "homotopic_with (\<lambda>x. True) U T f g"
+ \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g"
+ shows "homotopic_with_canon (\<lambda>x. True) U T f g"
proof -
obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
and k: "continuous_on T k" "k ` T \<subseteq> S"
- and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
- "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
- using assms by (auto simp: homotopy_eqv_def)
- have "homotopic_with (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
+ and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
+ "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
+ using assms by (auto simp: homotopy_equivalent_space_def)
+ have "homotopic_with_canon (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
apply (rule homUS)
using f g k
apply (safe intro!: continuous_on_compose h k f elim!: continuous_on_subset)
apply (force simp: o_def)+
done
- then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
+ then have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
apply (rule homotopic_with_compose_continuous_left)
apply (simp_all add: h)
done
- moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
+ moreover have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
apply (auto simp: hom f)
done
- moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
+ moreover have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
apply (auto simp: hom g)
done
- ultimately show "homotopic_with (\<lambda>x. True) U T f g"
+ ultimately show "homotopic_with_canon (\<lambda>x. True) U T f g"
apply (simp add: o_assoc)
using homotopic_with_trans homotopic_with_sym by blast
qed
@@ -3474,13 +3973,24 @@
assumes "S homotopy_eqv T"
shows "(\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> S \<and>
continuous_on U g \<and> g ` U \<subseteq> S
- \<longrightarrow> homotopic_with (\<lambda>x. True) U S f g) \<longleftrightarrow>
+ \<longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g) \<longleftrightarrow>
(\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> T \<and>
continuous_on U g \<and> g ` U \<subseteq> T
- \<longrightarrow> homotopic_with (\<lambda>x. True) U T f g)"
-apply (rule iffI)
-apply (metis assms homotopy_eqv_homotopic_triviality_imp)
-by (metis (no_types) assms homotopy_eqv_homotopic_triviality_imp homotopy_eqv_sym)
+ \<longrightarrow> homotopic_with_canon (\<lambda>x. True) U T f g)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ by (metis assms homotopy_eqv_homotopic_triviality_imp)
+next
+ assume ?rhs
+ moreover
+ have "T homotopy_eqv S"
+ using assms homotopy_equivalent_space_sym by blast
+ ultimately show ?lhs
+ by (blast intro: homotopy_eqv_homotopic_triviality_imp)
+qed
+
lemma homotopy_eqv_cohomotopic_triviality_null_imp:
fixes S :: "'a::real_normed_vector set"
@@ -3489,23 +3999,23 @@
assumes "S homotopy_eqv T"
and f: "continuous_on T f" "f ` T \<subseteq> U"
and homSU: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U\<rbrakk>
- \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c)"
- obtains c where "homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)"
+ \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) S U f (\<lambda>x. c)"
+ obtains c where "homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. c)"
proof -
obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
and k: "continuous_on T k" "k ` T \<subseteq> S"
- and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
- "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
- using assms by (auto simp: homotopy_eqv_def)
- obtain c where "homotopic_with (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
+ and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
+ "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
+ using assms by (auto simp: homotopy_equivalent_space_def)
+ obtain c where "homotopic_with_canon (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
apply (rule exE [OF homSU [of "f \<circ> h"]])
apply (intro continuous_on_compose h)
using h f apply (force elim!: continuous_on_subset)+
done
- then have "homotopic_with (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
+ then have "homotopic_with_canon (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
apply (rule homotopic_with_compose_continuous_right [where X=S])
using k by auto
- moreover have "homotopic_with (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
+ moreover have "homotopic_with_canon (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
apply (rule homotopic_with_compose_continuous_left [where Y=T])
apply (simp add: hom homotopic_with_symD)
using f apply auto
@@ -3522,12 +4032,12 @@
and U :: "'c::real_normed_vector set"
assumes "S homotopy_eqv T"
shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> U
- \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow>
+ \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow>
(\<forall>f. continuous_on T f \<and> f ` T \<subseteq> U
- \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)))"
+ \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. c)))"
apply (rule iffI)
apply (metis assms homotopy_eqv_cohomotopic_triviality_null_imp)
-by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_eqv_sym)
+by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_equivalent_space_sym)
lemma homotopy_eqv_homotopic_triviality_null_imp:
fixes S :: "'a::real_normed_vector set"
@@ -3536,23 +4046,23 @@
assumes "S homotopy_eqv T"
and f: "continuous_on U f" "f ` U \<subseteq> T"
and homSU: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
- \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
- shows "\<exists>c. homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
+ \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c)"
+ shows "\<exists>c. homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)"
proof -
obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
and k: "continuous_on T k" "k ` T \<subseteq> S"
- and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
- "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
- using assms by (auto simp: homotopy_eqv_def)
- obtain c::'a where "homotopic_with (\<lambda>x. True) U S (k \<circ> f) (\<lambda>x. c)"
+ and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
+ "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
+ using assms by (auto simp: homotopy_equivalent_space_def)
+ obtain c::'a where "homotopic_with_canon (\<lambda>x. True) U S (k \<circ> f) (\<lambda>x. c)"
apply (rule exE [OF homSU [of "k \<circ> f"]])
apply (intro continuous_on_compose h)
using k f apply (force elim!: continuous_on_subset)+
done
- then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
+ then have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
apply (rule homotopic_with_compose_continuous_left [where Y=S])
using h by auto
- moreover have "homotopic_with (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
+ moreover have "homotopic_with_canon (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
apply (rule homotopic_with_compose_continuous_right [where X=T])
apply (simp add: hom homotopic_with_symD)
using f apply auto
@@ -3567,12 +4077,12 @@
and U :: "'c::real_normed_vector set"
assumes "S homotopy_eqv T"
shows "(\<forall>f. continuous_on U f \<and> f ` U \<subseteq> S
- \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c))) \<longleftrightarrow>
+ \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c))) \<longleftrightarrow>
(\<forall>f. continuous_on U f \<and> f ` U \<subseteq> T
- \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)))"
+ \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)))"
apply (rule iffI)
apply (metis assms homotopy_eqv_homotopic_triviality_null_imp)
-by (metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_eqv_sym)
+by (metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_equivalent_space_sym)
lemma homotopy_eqv_contractible_sets:
fixes S :: "'a::real_normed_vector set"
@@ -3587,7 +4097,7 @@
with assms obtain a b where "a \<in> S" "b \<in> T"
by auto
then show ?thesis
- unfolding homotopy_eqv_def
+ unfolding homotopy_equivalent_space_def
apply (rule_tac x="\<lambda>x. b" in exI)
apply (rule_tac x="\<lambda>x. a" in exI)
apply (intro assms conjI continuous_on_id' homotopic_into_contractible)
@@ -3598,20 +4108,19 @@
lemma homotopy_eqv_empty1 [simp]:
fixes S :: "'a::real_normed_vector set"
shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}"
-apply (rule iffI)
-using homotopy_eqv_def apply fastforce
-by (simp add: homotopy_eqv_contractible_sets)
+ apply (rule iffI)
+ apply (metis Abstract_Topology.continuous_map_subtopology_eu emptyE equals0I homotopy_equivalent_space_def image_subset_iff)
+ by (simp add: homotopy_eqv_contractible_sets)
lemma homotopy_eqv_empty2 [simp]:
fixes S :: "'a::real_normed_vector set"
shows "({}::'b::real_normed_vector set) homotopy_eqv S \<longleftrightarrow> S = {}"
-by (metis homotopy_eqv_empty1 homotopy_eqv_sym)
+ using homotopy_equivalent_space_sym homotopy_eqv_empty1 by blast
lemma homotopy_eqv_contractibility:
fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
shows "S homotopy_eqv T \<Longrightarrow> (contractible S \<longleftrightarrow> contractible T)"
-unfolding homotopy_eqv_def
-by (blast intro: homotopy_dominated_contractibility)
+ by (meson contractible_space_top_of_set homotopy_equivalent_space_contractibility)
lemma homotopy_eqv_sing:
fixes S :: "'a::real_normed_vector set" and a :: "'b::real_normed_vector"
@@ -5034,11 +5543,15 @@
proposition nullhomotopic_from_sphere_extension:
fixes f :: "'M::euclidean_space \<Rightarrow> 'a::real_normed_vector"
- shows "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
+ shows "(\<exists>c. homotopic_with_canon (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
(\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
(\<forall>x \<in> sphere a r. g x = f x))"
(is "?lhs = ?rhs")
proof (cases r "0::real" rule: linorder_cases)
+ case less
+ then show ?thesis
+ by (simp add: homotopic_on_emptyI)
+next
case equal
then show ?thesis
apply (auto simp: homotopic_with)
@@ -5051,9 +5564,11 @@
have ?P if ?lhs using that
proof
fix c
- assume c: "homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)"
- then have contf: "continuous_on (sphere a r) f" and fim: "f ` sphere a r \<subseteq> S"
- by (auto simp: homotopic_with_imp_subset1 homotopic_with_imp_continuous)
+ 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)
show ?P
using contf fim by (auto simp: sphere_def dist_norm norm_minus_commute)
qed
@@ -5070,7 +5585,7 @@
moreover have ?thesis if ?P
proof
assume ?lhs
- then obtain c where "homotopic_with (\<lambda>x. True) (sphere a r) S (\<lambda>x. c) f"
+ then obtain c where "homotopic_with_canon (\<lambda>x. True) (sphere a r) S (\<lambda>x. c) f"
using homotopic_with_sym by blast
then obtain h where conth: "continuous_on ({0..1::real} \<times> sphere a r) h"
and him: "h ` ({0..1} \<times> sphere a r) \<subseteq> S"
@@ -5159,6 +5674,6 @@
qed
ultimately
show ?thesis by meson
-qed simp
+qed
end
\ No newline at end of file
--- a/src/HOL/Analysis/Jordan_Curve.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Jordan_Curve.thy Tue Mar 26 17:01:55 2019 +0000
@@ -103,7 +103,7 @@
using z by fastforce
qed (auto simp: g h algebra_simps exp_add)
qed
- ultimately have *: "homotopic_with (\<lambda>x. True) (S \<union> T) (sphere 0 1)
+ ultimately have *: "homotopic_with_canon (\<lambda>x. True) (S \<union> T) (sphere 0 1)
(\<lambda>x. (x - a) /\<^sub>R cmod (x - a)) (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle)
show ?thesis
--- a/src/HOL/Analysis/Path_Connected.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Tue Mar 26 17:01:55 2019 +0000
@@ -1976,6 +1976,13 @@
definition path_components_of :: "'a topology \<Rightarrow> 'a set set"
where "path_components_of X \<equiv> path_component_of_set X ` topspace X"
+lemma pathin_canon_iff: "pathin (top_of_set T) g \<longleftrightarrow> path g \<and> g ` {0..1} \<subseteq> T"
+ by (simp add: path_def pathin_def)
+
+lemma path_component_of_canon_iff [simp]:
+ "path_component_of (top_of_set T) a b \<longleftrightarrow> path_component T a b"
+ by (simp add: path_component_of_def pathin_canon_iff path_defs)
+
lemma path_component_in_topspace:
"path_component_of X x y \<Longrightarrow> x \<in> topspace X \<and> y \<in> topspace X"
by (auto simp: path_component_of_def pathin_def continuous_map_def)
@@ -2028,13 +2035,11 @@
qed (auto simp: g1 g2)
qed
-
lemma path_component_of_mono:
"\<lbrakk>path_component_of (subtopology X S) x y; S \<subseteq> T\<rbrakk> \<Longrightarrow> path_component_of (subtopology X T) x y"
unfolding path_component_of_def
by (metis subsetD pathin_subtopology)
-
lemma path_component_of:
"path_component_of X x y \<longleftrightarrow> (\<exists>T. path_connectedin X T \<and> x \<in> T \<and> y \<in> T)"
apply (auto simp: path_component_of_def)
--- a/src/HOL/Analysis/Product_Topology.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Product_Topology.thy Tue Mar 26 17:01:55 2019 +0000
@@ -80,13 +80,6 @@
"prod_topology (subtopology euclidean S) (subtopology euclidean T) = subtopology euclidean (S \<times> T)"
by (simp add: prod_topology_subtopology subtopology_subtopology Times_Int_Times)
-lemma continuous_map_subtopology_eu [simp]:
- "continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
- apply safe
- apply (metis continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
- apply (simp add: continuous_map_closedin_preimage_eq image_subset_iff)
- by (metis (no_types, hide_lams) continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
-
lemma openin_prod_topology_alt:
"openin (prod_topology X Y) S \<longleftrightarrow>
(\<forall>x y. (x,y) \<in> S \<longrightarrow> (\<exists>U V. openin X U \<and> openin Y V \<and> x \<in> U \<and> y \<in> V \<and> U \<times> V \<subseteq> S))"
@@ -101,7 +94,7 @@
unfolding open_map_def openin_prod_topology_alt
by (force simp: openin_subopen [of Y "snd ` _"] intro: subset_snd_imageI)
-lemma openin_Times:
+lemma openin_prod_Times_iff:
"openin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> openin X S \<and> openin Y T"
proof (cases "S = {} \<or> T = {}")
case False
@@ -121,7 +114,7 @@
by (clarsimp simp: closure_of_def openin_prod_topology_alt) (meson SigmaI subsetD)
qed
-lemma closedin_Times:
+lemma closedin_prod_Times_iff:
"closedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> closedin X S \<and> closedin Y T"
by (auto simp: closure_of_Times times_eq_iff simp flip: closure_of_eq)
@@ -130,7 +123,7 @@
show "(X interior_of S) \<times> Y interior_of T \<subseteq> S \<times> T"
by (simp add: Sigma_mono interior_of_subset)
show "openin (prod_topology X Y) ((X interior_of S) \<times> Y interior_of T)"
- by (simp add: openin_Times)
+ by (simp add: openin_prod_Times_iff)
next
show "T' \<subseteq> (X interior_of S) \<times> Y interior_of T" if "T' \<subseteq> S \<times> T" "openin (prod_topology X Y) T'" for T'
proof (clarsimp; intro conjI)
@@ -165,7 +158,7 @@
unfolding continuous_map_def using True that
apply clarify
apply (drule_tac x="U \<times> topspace Y" in spec)
- by (simp add: openin_Times mem_Times_iff cong: conj_cong)
+ by (simp add: openin_prod_Times_iff mem_Times_iff cong: conj_cong)
with True show "continuous_map Z X (fst \<circ> f)"
by (auto simp: continuous_map_def)
next
@@ -174,7 +167,7 @@
unfolding continuous_map_def using True that
apply clarify
apply (drule_tac x="topspace X \<times> V" in spec)
- by (simp add: openin_Times mem_Times_iff cong: conj_cong)
+ by (simp add: openin_prod_Times_iff mem_Times_iff cong: conj_cong)
with True show "continuous_map Z Y (snd \<circ> f)"
by (auto simp: continuous_map_def)
next
--- a/src/HOL/Analysis/T1_Spaces.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy Tue Mar 26 17:01:55 2019 +0000
@@ -209,7 +209,7 @@
by simp
have "t1_space (prod_topology X Y) \<longleftrightarrow> (t1_space X \<and> t1_space Y)"
using False
- by (force simp: t1_space_closedin_singleton closedin_Times eq simp del: insert_Times_insert)
+ by (force simp: t1_space_closedin_singleton closedin_prod_Times_iff eq simp del: insert_Times_insert)
with False show ?thesis
by simp
qed
--- a/src/HOL/Analysis/Winding_Numbers.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Winding_Numbers.thy Tue Mar 26 17:01:55 2019 +0000
@@ -1137,23 +1137,25 @@
and qeq: "pathfinish q - pathstart q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
and peq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p t = \<zeta> + exp(q t)"
using winding_number_as_continuous_log [OF assms] by blast
- have *: "homotopic_with (\<lambda>r. pathfinish r = pathstart r)
+ have *: "homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r)
{0..1} (-{\<zeta>}) ((\<lambda>w. \<zeta> + exp w) \<circ> q) ((\<lambda>w. \<zeta> + exp w) \<circ> (\<lambda>t. 0))"
proof (rule homotopic_with_compose_continuous_left)
- show "homotopic_with (\<lambda>f. pathfinish ((\<lambda>w. \<zeta> + exp w) \<circ> f) = pathstart ((\<lambda>w. \<zeta> + exp w) \<circ> f))
+ show "homotopic_with_canon (\<lambda>f. pathfinish ((\<lambda>w. \<zeta> + exp w) \<circ> f) = pathstart ((\<lambda>w. \<zeta> + exp w) \<circ> f))
{0..1} UNIV q (\<lambda>t. 0)"
proof (rule homotopic_with_mono, simp_all add: pathfinish_def pathstart_def)
have "homotopic_loops UNIV q (\<lambda>t. 0)"
- by (rule homotopic_loops_linear) (use qeq \<open>path q\<close> in \<open>auto simp: continuous_on_const path_defs\<close>)
- then show "homotopic_with (\<lambda>h. exp (h 1) = exp (h 0)) {0..1} UNIV q (\<lambda>t. 0)"
- by (simp add: homotopic_loops_def homotopic_with_mono pathfinish_def pathstart_def)
+ by (rule homotopic_loops_linear) (use qeq \<open>path q\<close> in \<open>auto simp: path_defs\<close>)
+ then have "homotopic_with (\<lambda>r. r 1 = r 0) (top_of_set {0..1}) euclidean q (\<lambda>t. 0)"
+ by (simp add: homotopic_loops_def pathfinish_def pathstart_def)
+ then show "homotopic_with (\<lambda>h. exp (h 1) = exp (h 0)) (top_of_set {0..1}) euclidean q (\<lambda>t. 0)"
+ by (rule homotopic_with_mono) simp
qed
show "continuous_on UNIV (\<lambda>w. \<zeta> + exp w)"
by (rule continuous_intros)+
show "range (\<lambda>w. \<zeta> + exp w) \<subseteq> -{\<zeta>}"
by auto
qed
- then have "homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} (-{\<zeta>}) p (\<lambda>x. \<zeta> + 1)"
+ then have "homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} (-{\<zeta>}) p (\<lambda>x. \<zeta> + 1)"
by (rule homotopic_with_eq) (auto simp: o_def peq pathfinish_def pathstart_def)
then have "homotopic_loops (-{\<zeta>}) p (\<lambda>t. \<zeta> + 1)"
by (simp add: homotopic_loops_def)
--- a/src/HOL/Complete_Lattices.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Complete_Lattices.thy Tue Mar 26 17:01:55 2019 +0000
@@ -998,6 +998,12 @@
apply (auto simp: disjnt_def)
using inj_on_eq_iff by fastforce
+lemma disjnt_Union1 [simp]: "disjnt (\<Union>\<A>) B \<longleftrightarrow> (\<forall>A \<in> \<A>. disjnt A B)"
+ by (auto simp: disjnt_def)
+
+lemma disjnt_Union2 [simp]: "disjnt B (\<Union>\<A>) \<longleftrightarrow> (\<forall>A \<in> \<A>. disjnt B A)"
+ by (auto simp: disjnt_def)
+
subsubsection \<open>Unions of families\<close>
--- a/src/HOL/Set.thy Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Set.thy Tue Mar 26 17:01:55 2019 +0000
@@ -1926,6 +1926,12 @@
lemma disjnt_subset2 : "\<lbrakk>disjnt X Y; Z \<subseteq> Y\<rbrakk> \<Longrightarrow> disjnt X Z"
by (auto simp: disjnt_def)
+lemma disjnt_Un1 [simp]: "disjnt (A \<union> B) C \<longleftrightarrow> disjnt A C \<and> disjnt B C"
+ by (auto simp: disjnt_def)
+
+lemma disjnt_Un2 [simp]: "disjnt C (A \<union> B) \<longleftrightarrow> disjnt C A \<and> disjnt C B"
+ by (auto simp: disjnt_def)
+
lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
unfolding disjnt_def pairwise_def by fast