src/HOL/Analysis/Homotopy.thy
 changeset 69986 f2d327275065 parent 69922 4a9167f377b0 child 70033 6cbc7634135c
```     1.1 --- a/src/HOL/Analysis/Homotopy.thy	Sun Mar 24 20:31:53 2019 +0100
1.2 +++ b/src/HOL/Analysis/Homotopy.thy	Tue Mar 26 17:01:36 2019 +0000
1.3 @@ -5,172 +5,299 @@
1.4  section \<open>Homotopy of Maps\<close>
1.5
1.6  theory Homotopy
1.7 -  imports Path_Connected Continuum_Not_Denumerable
1.8 +  imports Path_Connected Continuum_Not_Denumerable Product_Topology
1.9  begin
1.10
1.11 -definition%important homotopic_with ::
1.12 -  "[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
1.13 +definition%important homotopic_with
1.14  where
1.15 - "homotopic_with P X Y p q \<equiv>
1.16 -   (\<exists>h:: real \<times> 'a \<Rightarrow> 'b.
1.17 -       continuous_on ({0..1} \<times> X) h \<and>
1.18 -       h ` ({0..1} \<times> X) \<subseteq> Y \<and>
1.19 -       (\<forall>x. h(0, x) = p x) \<and>
1.20 -       (\<forall>x. h(1, x) = q x) \<and>
1.21 -       (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
1.22 + "homotopic_with P X Y f g \<equiv>
1.23 +   (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
1.24 +       (\<forall>x. h(0, x) = f x) \<and>
1.25 +       (\<forall>x. h(1, x) = g x) \<and>
1.26 +       (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t,x))))"
1.27
1.28  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.
1.29  We often just want to require that \<open>P\<close> fixes some subset, but to include the case of a loop homotopy,
1.30  it is convenient to have a general property \<open>P\<close>.\<close>
1.31
1.32 +abbreviation homotopic_with_canon ::
1.33 +  "[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
1.34 +where
1.35 + "homotopic_with_canon P S T p q \<equiv> homotopic_with P (top_of_set S) (top_of_set T) p q"
1.36 +
1.37 +lemma split_01: "{0..1::real} = {0..1/2} \<union> {1/2..1}"
1.38 +  by force
1.39 +
1.40 +lemma split_01_prod: "{0..1::real} \<times> X = ({0..1/2} \<times> X) \<union> ({1/2..1} \<times> X)"
1.41 +  by force
1.42 +
1.43 +lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
1.44 +  by auto
1.45 +
1.46 +lemma fst_o_paired [simp]: "fst \<circ> (\<lambda>(x,y). (f x y, g x y)) = (\<lambda>(x,y). f x y)"
1.47 +  by auto
1.48 +
1.49 +lemma snd_o_paired [simp]: "snd \<circ> (\<lambda>(x,y). (f x y, g x y)) = (\<lambda>(x,y). g x y)"
1.50 +  by auto
1.51 +
1.52 +lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h \<circ> Pair t)"
1.53 +  by (fast intro: continuous_intros elim!: continuous_on_subset)
1.54 +
1.55 +lemma continuous_map_o_Pair:
1.56 +  assumes h: "continuous_map (prod_topology X Y) Z h" and t: "t \<in> topspace X"
1.57 +  shows "continuous_map Y Z (h \<circ> Pair t)"
1.58 +  apply (intro continuous_map_compose [OF _ h] continuous_map_id [unfolded id_def] continuous_intros)
1.59 +  apply (simp add: t)
1.60 +  done
1.61 +
1.62 +subsection%unimportant\<open>Trivial properties\<close>
1.63 +
1.64  text \<open>We often want to just localize the ending function equality or whatever.\<close>
1.65  text%important \<open>%whitespace\<close>
1.66  proposition homotopic_with:
1.67 -  fixes X :: "'a::topological_space set" and Y :: "'b::topological_space set"
1.68 -  assumes "\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
1.69 +  assumes "\<And>h k. (\<And>x. x \<in> topspace X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
1.70    shows "homotopic_with P X Y p q \<longleftrightarrow>
1.71 -           (\<exists>h :: real \<times> 'a \<Rightarrow> 'b.
1.72 -              continuous_on ({0..1} \<times> X) h \<and>
1.73 -              h ` ({0..1} \<times> X) \<subseteq> Y \<and>
1.74 -              (\<forall>x \<in> X. h(0,x) = p x) \<and>
1.75 -              (\<forall>x \<in> X. h(1,x) = q x) \<and>
1.76 +           (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
1.77 +              (\<forall>x \<in> topspace X. h(0,x) = p x) \<and>
1.78 +              (\<forall>x \<in> topspace X. h(1,x) = q x) \<and>
1.79                (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
1.80    unfolding homotopic_with_def
1.81    apply (rule iffI, blast, clarify)
1.82 -  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)
1.83 +  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)
1.84    apply auto
1.85 -  apply (force elim: continuous_on_eq)
1.86 +  using continuous_map_eq apply fastforce
1.87    apply (drule_tac x=t in bspec, force)
1.88    apply (subst assms; simp)
1.89    done
1.90
1.91 -proposition homotopic_with_eq:
1.92 -   assumes h: "homotopic_with P X Y f g"
1.93 -       and f': "\<And>x. x \<in> X \<Longrightarrow> f' x = f x"
1.94 -       and g': "\<And>x. x \<in> X \<Longrightarrow> g' x = g x"
1.95 -       and P:  "(\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k))"
1.96 -   shows "homotopic_with P X Y f' g'"
1.97 -  using h unfolding homotopic_with_def
1.98 -  apply safe
1.99 -  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)
1.100 -  apply (simp add: f' g', safe)
1.101 -  apply (fastforce intro: continuous_on_eq, fastforce)
1.102 -  apply (subst P; fastforce)
1.103 +lemma homotopic_with_mono:
1.104 +  assumes hom: "homotopic_with P X Y f g"
1.105 +    and Q: "\<And>h. \<lbrakk>continuous_map X Y h; P h\<rbrakk> \<Longrightarrow> Q h"
1.106 +  shows "homotopic_with Q X Y f g"
1.107 +  using hom
1.108 +  apply (simp add: homotopic_with_def)
1.109 +  apply (erule ex_forward)
1.110 +  apply (force simp: o_def dest: continuous_map_o_Pair intro: Q)
1.111    done
1.112
1.113 -proposition homotopic_with_equal:
1.114 -   assumes contf: "continuous_on X f" and fXY: "f ` X \<subseteq> Y"
1.115 -       and gf: "\<And>x. x \<in> X \<Longrightarrow> g x = f x"
1.116 -       and P:  "P f" "P g"
1.117 -   shows "homotopic_with P X Y f g"
1.118 +lemma homotopic_with_imp_continuous_maps:
1.119 +    assumes "homotopic_with P X Y f g"
1.120 +    shows "continuous_map X Y f \<and> continuous_map X Y g"
1.121 +proof -
1.122 +  obtain h
1.123 +    where conth: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h"
1.124 +      and h: "\<forall>x. h (0, x) = f x" "\<forall>x. h (1, x) = g x"
1.125 +    using assms by (auto simp: homotopic_with_def)
1.126 +  have *: "t \<in> {0..1} \<Longrightarrow> continuous_map X Y (h \<circ> (\<lambda>x. (t,x)))" for t
1.127 +    by (rule continuous_map_compose [OF _ conth]) (simp add: o_def continuous_map_pairwise)
1.128 +  show ?thesis
1.129 +    using h *[of 0] *[of 1] by (simp add: continuous_map_eq)
1.130 +qed
1.131 +
1.132 +lemma homotopic_with_imp_continuous:
1.133 +    assumes "homotopic_with_canon P X Y f g"
1.134 +    shows "continuous_on X f \<and> continuous_on X g"
1.135 +  by (meson assms continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
1.136 +
1.137 +lemma homotopic_with_imp_property:
1.138 +  assumes "homotopic_with P X Y f g"
1.139 +  shows "P f \<and> P g"
1.140 +proof
1.141 +  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))"
1.142 +    using assms by (force simp: homotopic_with_def)
1.143 +  show "P f" "P g"
1.144 +    using P [of 0] P [of 1] by (force simp: h)+
1.145 +qed
1.146 +
1.147 +lemma homotopic_with_equal:
1.148 +  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"
1.149 +  shows "homotopic_with P X Y f g"
1.150    unfolding homotopic_with_def
1.151 -  apply (rule_tac x="\<lambda>(u,v). if u = 1 then g v else f v" in exI)
1.152 -  using assms
1.153 -  apply (intro conjI)
1.154 -  apply (rule continuous_on_eq [where f = "f \<circ> snd"])
1.155 -  apply (rule continuous_intros | force)+
1.156 -  apply clarify
1.157 -  apply (case_tac "t=1"; force)
1.158 +proof (intro exI conjI allI ballI)
1.159 +  let ?h = "\<lambda>(t::real,x). if t = 1 then g x else f x"
1.160 +  show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y ?h"
1.161 +  proof (rule continuous_map_eq)
1.162 +    show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y (f \<circ> snd)"
1.163 +      by (simp add: contf continuous_map_of_snd)
1.164 +  qed (auto simp: fg)
1.165 +  show "P (\<lambda>x. ?h (t, x))" if "t \<in> {0..1}" for t
1.166 +    by (cases "t = 1") (simp_all add: assms)
1.167 +qed auto
1.168 +
1.169 +lemma homotopic_with_imp_subset1:
1.170 +     "homotopic_with_canon P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
1.171 +  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
1.172 +
1.173 +lemma homotopic_with_imp_subset2:
1.174 +     "homotopic_with_canon P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
1.175 +  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
1.176 +
1.177 +lemma homotopic_with_subset_left:
1.178 +     "\<lbrakk>homotopic_with_canon P X Y f g; Z \<subseteq> X\<rbrakk> \<Longrightarrow> homotopic_with_canon P Z Y f g"
1.179 +  apply (simp add: homotopic_with_def)
1.180 +  apply (fast elim!: continuous_on_subset ex_forward)
1.181 +  done
1.182 +
1.183 +lemma homotopic_with_subset_right:
1.184 +     "\<lbrakk>homotopic_with_canon P X Y f g; Y \<subseteq> Z\<rbrakk> \<Longrightarrow> homotopic_with_canon P X Z f g"
1.185 +  apply (simp add: homotopic_with_def)
1.186 +  apply (fast elim!: continuous_on_subset ex_forward)
1.187    done
1.188
1.189 -
1.190 -lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
1.191 -  by auto
1.192 -
1.193 -lemma homotopic_constant_maps:
1.194 -   "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow> s = {} \<or> path_component t a b"
1.195 -proof (cases "s = {} \<or> t = {}")
1.196 -  case True with continuous_on_const show ?thesis
1.197 -    by (auto simp: homotopic_with path_component_def)
1.198 -next
1.199 -  case False
1.200 -  then obtain c where "c \<in> s" by blast
1.201 +subsection\<open>Homotopy with P is an equivalence relation\<close>
1.202 +
1.203 +text \<open>(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)\<close>
1.204 +
1.205 +lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f \<longleftrightarrow> continuous_map X Y f \<and> P f"
1.206 +  by (auto simp: homotopic_with_imp_continuous_maps intro: homotopic_with_equal dest: homotopic_with_imp_property)
1.207 +
1.208 +lemma homotopic_with_symD:
1.209 +    assumes "homotopic_with P X Y f g"
1.210 +      shows "homotopic_with P X Y g f"
1.211 +proof -
1.212 +  let ?I01 = "subtopology euclideanreal {0..1}"
1.213 +  let ?j = "\<lambda>y. (1 - fst y, snd y)"
1.214 +  have 1: "continuous_map (prod_topology ?I01 X) (prod_topology euclideanreal X) ?j"
1.215 +    apply (intro continuous_intros)
1.216 +    apply (simp_all add: prod_topology_subtopology continuous_map_from_subtopology [OF continuous_map_fst])
1.217 +    done
1.218 +  have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j"
1.219 +  proof -
1.220 +    have "continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} \<times> topspace X)) ?j"
1.221 +      by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff)
1.222 +    then show ?thesis
1.223 +      by (simp add: prod_topology_subtopology(1))
1.224 +  qed
1.225    show ?thesis
1.226 -  proof
1.227 -    assume "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b)"
1.228 -    then obtain h :: "real \<times> 'a \<Rightarrow> 'b"
1.229 -        where conth: "continuous_on ({0..1} \<times> s) h"
1.230 -          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)"
1.231 -      by (auto simp: homotopic_with)
1.232 -    have "continuous_on {0..1} (h \<circ> (\<lambda>t. (t, c)))"
1.233 -      apply (rule continuous_intros conth | simp add: image_Pair_const)+
1.234 -      apply (blast intro:  \<open>c \<in> s\<close> continuous_on_subset [OF conth])
1.235 -      done
1.236 -    with \<open>c \<in> s\<close> h show "s = {} \<or> path_component t a b"
1.237 -      apply (simp_all add: homotopic_with path_component_def, auto)
1.238 -      apply (drule_tac x="h \<circ> (\<lambda>t. (t, c))" in spec)
1.239 -      apply (auto simp: pathstart_def pathfinish_def path_image_def path_def)
1.240 -      done
1.241 -  next
1.242 -    assume "s = {} \<or> path_component t a b"
1.243 -    with False show "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b)"
1.244 -      apply (clarsimp simp: homotopic_with path_component_def pathstart_def pathfinish_def path_image_def path_def)
1.245 -      apply (rule_tac x="g \<circ> fst" in exI)
1.246 -      apply (rule conjI continuous_intros | force)+
1.247 +    using assms
1.248 +    apply (clarsimp simp add: homotopic_with_def)
1.249 +    apply (rename_tac h)
1.250 +    apply (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI)
1.251 +    apply (simp add: continuous_map_compose [OF *])
1.252 +    done
1.253 +qed
1.254 +
1.255 +lemma homotopic_with_sym:
1.256 +   "homotopic_with P X Y f g \<longleftrightarrow> homotopic_with P X Y g f"
1.257 +  by (metis homotopic_with_symD)
1.258 +
1.259 +proposition homotopic_with_trans:
1.260 +    assumes "homotopic_with P X Y f g"  "homotopic_with P X Y g h"
1.261 +    shows "homotopic_with P X Y f h"
1.262 +proof -
1.263 +  let ?X01 = "prod_topology (subtopology euclideanreal {0..1}) X"
1.264 +  obtain k1 k2
1.265 +    where contk1: "continuous_map ?X01 Y k1" and contk2: "continuous_map ?X01 Y k2"
1.266 +      and k12: "\<forall>x. k1 (1, x) = g x" "\<forall>x. k2 (0, x) = g x"
1.267 +      "\<forall>x. k1 (0, x) = f x" "\<forall>x. k2 (1, x) = h x"
1.268 +      and P:   "\<forall>t\<in>{0..1}. P (\<lambda>x. k1 (t, x))" "\<forall>t\<in>{0..1}. P (\<lambda>x. k2 (t, x))"
1.269 +    using assms by (auto simp: homotopic_with_def)
1.270 +  define k where "k \<equiv> \<lambda>y. if fst y \<le> 1/2
1.271 +                             then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
1.272 +                             else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y"
1.273 +  have keq: "k1 (2 * u, v) = k2 (2 * u -1, v)" if "u = 1/2"  for u v
1.274 +    by (simp add: k12 that)
1.275 +  show ?thesis
1.276 +    unfolding homotopic_with_def
1.277 +  proof (intro exI conjI)
1.278 +    show "continuous_map ?X01 Y k"
1.279 +      unfolding k_def
1.280 +    proof (rule continuous_map_cases_le)
1.281 +      show fst: "continuous_map ?X01 euclideanreal fst"
1.282 +        using continuous_map_fst continuous_map_in_subtopology by blast
1.283 +      show "continuous_map ?X01 euclideanreal (\<lambda>x. 1/2)"
1.284 +        by simp
1.285 +      show "continuous_map (subtopology ?X01 {y \<in> topspace ?X01. fst y \<le> 1/2}) Y
1.286 +               (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x)))"
1.287 +        apply (rule fst continuous_map_compose [OF _ contk1] continuous_intros continuous_map_into_subtopology | simp)+
1.288 +          apply (intro continuous_intros fst continuous_map_from_subtopology)
1.289 +         apply (force simp: prod_topology_subtopology)
1.290 +        using continuous_map_snd continuous_map_from_subtopology by blast
1.291 +      show "continuous_map (subtopology ?X01 {y \<in> topspace ?X01. 1/2 \<le> fst y}) Y
1.292 +               (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x)))"
1.293 +        apply (rule fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology | simp)+
1.294 +          apply (rule continuous_intros fst continuous_map_from_subtopology | simp)+
1.295 +         apply (force simp: topspace_subtopology prod_topology_subtopology)
1.296 +        using continuous_map_snd  continuous_map_from_subtopology by blast
1.297 +      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"
1.298 +        if "y \<in> topspace ?X01" and "fst y = 1/2" for y
1.299 +        using that by (simp add: keq)
1.300 +    qed
1.301 +    show "\<forall>x. k (0, x) = f x"
1.302 +      by (simp add: k12 k_def)
1.303 +    show "\<forall>x. k (1, x) = h x"
1.304 +      by (simp add: k12 k_def)
1.305 +    show "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
1.306 +      using P
1.307 +      apply (clarsimp simp add: k_def)
1.308 +      apply (case_tac "t \<le> 1/2", auto)
1.309        done
1.310    qed
1.311  qed
1.312
1.313 -
1.314 -subsection%unimportant\<open>Trivial properties\<close>
1.315 -
1.316 -lemma homotopic_with_imp_property: "homotopic_with P X Y f g \<Longrightarrow> P f \<and> P g"
1.317 -  unfolding homotopic_with_def Ball_def
1.318 +lemma homotopic_with_id2:
1.319 +  "(\<And>x. x \<in> topspace X \<Longrightarrow> g (f x) = x) \<Longrightarrow> homotopic_with (\<lambda>x. True) X X (g \<circ> f) id"
1.320 +  by (metis comp_apply continuous_map_id eq_id_iff homotopic_with_equal homotopic_with_symD)
1.321 +
1.322 +subsection\<open>Continuity lemmas\<close>
1.323 +
1.324 +lemma homotopic_with_compose_continuous_map_left:
1.325 +  "\<lbrakk>homotopic_with p X1 X2 f g; continuous_map X2 X3 h; \<And>j. p j \<Longrightarrow> q(h \<circ> j)\<rbrakk>
1.326 +   \<Longrightarrow> homotopic_with q X1 X3 (h \<circ> f) (h \<circ> g)"
1.327 +  unfolding homotopic_with_def
1.328    apply clarify
1.329 -  apply (frule_tac x=0 in spec)
1.330 -  apply (drule_tac x=1 in spec, auto)
1.331 +  apply (rename_tac k)
1.332 +  apply (rule_tac x="h \<circ> k" in exI)
1.333 +  apply (rule conjI continuous_map_compose | simp add: o_def)+
1.334    done
1.335
1.336 -lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h \<circ> Pair t)"
1.337 -  by (fast intro: continuous_intros elim!: continuous_on_subset)
1.338 -
1.339 -lemma homotopic_with_imp_continuous:
1.340 -    assumes "homotopic_with P X Y f g"
1.341 -    shows "continuous_on X f \<and> continuous_on X g"
1.342 +lemma homotopic_compose_continuous_map_left:
1.343 +   "\<lbrakk>homotopic_with (\<lambda>k. True) X1 X2 f g; continuous_map X2 X3 h\<rbrakk>
1.344 +        \<Longrightarrow> homotopic_with (\<lambda>k. True) X1 X3 (h \<circ> f) (h \<circ> g)"
1.345 +  by (simp add: homotopic_with_compose_continuous_map_left)
1.346 +
1.347 +lemma homotopic_with_compose_continuous_map_right:
1.348 +  assumes hom: "homotopic_with p X2 X3 f g" and conth: "continuous_map X1 X2 h"
1.349 +    and q: "\<And>j. p j \<Longrightarrow> q(j \<circ> h)"
1.350 +  shows "homotopic_with q X1 X3 (f \<circ> h) (g \<circ> h)"
1.351  proof -
1.352 -  obtain h :: "real \<times> 'a \<Rightarrow> 'b"
1.353 -    where conth: "continuous_on ({0..1} \<times> X) h"
1.354 -      and h: "\<forall>x. h (0, x) = f x" "\<forall>x. h (1, x) = g x"
1.355 -    using assms by (auto simp: homotopic_with_def)
1.356 -  have *: "t \<in> {0..1} \<Longrightarrow> continuous_on X (h \<circ> (\<lambda>x. (t,x)))" for t
1.357 -    by (rule continuous_intros continuous_on_subset [OF conth] | force)+
1.358 +  obtain k
1.359 +    where contk: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) X3 k"
1.360 +      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))"
1.361 +    using hom unfolding homotopic_with_def by blast
1.362 +  have hsnd: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X2 (h \<circ> snd)"
1.363 +    by (rule continuous_map_compose [OF continuous_map_snd conth])
1.364 +  let ?h = "k \<circ> (\<lambda>(t,x). (t,h x))"
1.365    show ?thesis
1.366 -    using h *[of 0] *[of 1] by auto
1.367 +    unfolding homotopic_with_def
1.368 +  proof (intro exI conjI allI ballI)
1.369 +    have "continuous_map (prod_topology (top_of_set {0..1}) X1)
1.370 +     (prod_topology (top_of_set {0..1::real}) X2) (\<lambda>(t, x). (t, h x))"
1.371 +      by (metis (mono_tags, lifting) case_prod_beta' comp_def continuous_map_eq continuous_map_fst continuous_map_pairedI hsnd)
1.372 +    then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X3 ?h"
1.373 +      by (intro conjI continuous_map_compose [OF _ contk])
1.374 +    show "q (\<lambda>x. ?h (t, x))" if "t \<in> {0..1}" for t
1.375 +      using q [OF p [OF that]] by (simp add: o_def)
1.376 +  qed (auto simp: k)
1.377  qed
1.378
1.379 -proposition homotopic_with_imp_subset1:
1.380 -     "homotopic_with P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
1.381 -  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
1.382 -
1.383 -proposition homotopic_with_imp_subset2:
1.384 -     "homotopic_with P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
1.385 -  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
1.386 -
1.387 -proposition homotopic_with_mono:
1.388 -    assumes hom: "homotopic_with P X Y f g"
1.389 -        and Q: "\<And>h. \<lbrakk>continuous_on X h; image h X \<subseteq> Y \<and> P h\<rbrakk> \<Longrightarrow> Q h"
1.390 -      shows "homotopic_with Q X Y f g"
1.391 -  using hom
1.392 -  apply (simp add: homotopic_with_def)
1.393 -  apply (erule ex_forward)
1.394 -  apply (force simp: intro!: Q dest: continuous_on_o_Pair)
1.395 -  done
1.396 -
1.397 -proposition homotopic_with_subset_left:
1.398 -     "\<lbrakk>homotopic_with P X Y f g; Z \<subseteq> X\<rbrakk> \<Longrightarrow> homotopic_with P Z Y f g"
1.399 -  apply (simp add: homotopic_with_def)
1.400 -  apply (fast elim!: continuous_on_subset ex_forward)
1.401 -  done
1.402 -
1.403 -proposition homotopic_with_subset_right:
1.404 -     "\<lbrakk>homotopic_with P X Y f g; Y \<subseteq> Z\<rbrakk> \<Longrightarrow> homotopic_with P X Z f g"
1.405 -  apply (simp add: homotopic_with_def)
1.406 -  apply (fast elim!: continuous_on_subset ex_forward)
1.407 -  done
1.408 +lemma homotopic_compose_continuous_map_right:
1.409 +   "\<lbrakk>homotopic_with (\<lambda>k. True) X2 X3 f g; continuous_map X1 X2 h\<rbrakk>
1.410 +        \<Longrightarrow> homotopic_with (\<lambda>k. True) X1 X3 (f \<circ> h) (g \<circ> h)"
1.411 +  by (meson homotopic_with_compose_continuous_map_right)
1.412 +
1.413 +corollary homotopic_compose:
1.414 +      shows "\<lbrakk>homotopic_with (\<lambda>x. True) X Y f f'; homotopic_with (\<lambda>x. True) Y Z g g'\<rbrakk>
1.415 +             \<Longrightarrow> homotopic_with (\<lambda>x. True) X Z (g \<circ> f) (g' \<circ> f')"
1.416 +  apply (rule homotopic_with_trans [where g = "g \<circ> f'"])
1.417 +  apply (simp add: homotopic_compose_continuous_map_left homotopic_with_imp_continuous_maps)
1.418 +  by (simp add: homotopic_compose_continuous_map_right homotopic_with_imp_continuous_maps)
1.419 +
1.420 +
1.421
1.422  proposition homotopic_with_compose_continuous_right:
1.423 -    "\<lbrakk>homotopic_with (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
1.424 -     \<Longrightarrow> homotopic_with p W Y (f \<circ> h) (g \<circ> h)"
1.425 +    "\<lbrakk>homotopic_with_canon (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
1.426 +     \<Longrightarrow> homotopic_with_canon p W Y (f \<circ> h) (g \<circ> h)"
1.427    apply (clarsimp simp add: homotopic_with_def)
1.428    apply (rename_tac k)
1.429    apply (rule_tac x="k \<circ> (\<lambda>y. (fst y, h (snd y)))" in exI)
1.430 @@ -180,13 +307,13 @@
1.431    done
1.432
1.433  proposition homotopic_compose_continuous_right:
1.434 -     "\<lbrakk>homotopic_with (\<lambda>f. True) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
1.435 -      \<Longrightarrow> homotopic_with (\<lambda>f. True) W Y (f \<circ> h) (g \<circ> h)"
1.436 +     "\<lbrakk>homotopic_with_canon (\<lambda>f. True) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
1.437 +      \<Longrightarrow> homotopic_with_canon (\<lambda>f. True) W Y (f \<circ> h) (g \<circ> h)"
1.438    using homotopic_with_compose_continuous_right by fastforce
1.439
1.440  proposition homotopic_with_compose_continuous_left:
1.441 -     "\<lbrakk>homotopic_with (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
1.442 -      \<Longrightarrow> homotopic_with p X Z (h \<circ> f) (h \<circ> g)"
1.443 +     "\<lbrakk>homotopic_with_canon (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
1.444 +      \<Longrightarrow> homotopic_with_canon p X Z (h \<circ> f) (h \<circ> g)"
1.445    apply (clarsimp simp add: homotopic_with_def)
1.446    apply (rename_tac k)
1.447    apply (rule_tac x="h \<circ> k" in exI)
1.448 @@ -196,150 +323,171 @@
1.449    done
1.450
1.451  proposition homotopic_compose_continuous_left:
1.452 -   "\<lbrakk>homotopic_with (\<lambda>_. True) X Y f g;
1.453 +   "\<lbrakk>homotopic_with_canon (\<lambda>_. True) X Y f g;
1.454       continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
1.455 -    \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h \<circ> f) (h \<circ> g)"
1.456 +    \<Longrightarrow> homotopic_with_canon (\<lambda>f. True) X Z (h \<circ> f) (h \<circ> g)"
1.457    using homotopic_with_compose_continuous_left by fastforce
1.458
1.459 -proposition homotopic_with_Pair:
1.460 -   assumes hom: "homotopic_with p s t f g" "homotopic_with p' s' t' f' g'"
1.461 -       and q: "\<And>f g. \<lbrakk>p f; p' g\<rbrakk> \<Longrightarrow> q(\<lambda>(x,y). (f x, g y))"
1.462 -     shows "homotopic_with q (s \<times> s') (t \<times> t')
1.463 -                  (\<lambda>(x,y). (f x, f' y)) (\<lambda>(x,y). (g x, g' y))"
1.464 -  using hom
1.465 -  apply (clarsimp simp add: homotopic_with_def)
1.466 -  apply (rename_tac k k')
1.467 -  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)
1.468 -  apply (rule conjI continuous_intros | erule continuous_on_subset | clarsimp)+
1.469 -  apply (auto intro!: q [unfolded case_prod_unfold])
1.470 -  done
1.471 -
1.472 -lemma homotopic_on_empty [simp]: "homotopic_with (\<lambda>x. True) {} t f g"
1.473 -  by (metis continuous_on_def empty_iff homotopic_with_equal image_subset_iff)
1.474 -
1.475 -
1.476 -text\<open>Homotopy with P is an equivalence relation (on continuous functions mapping X into Y that satisfy P,
1.477 -     though this only affects reflexivity.\<close>
1.478 -
1.479 -
1.480 -proposition homotopic_with_refl:
1.481 -   "homotopic_with P X Y f f \<longleftrightarrow> continuous_on X f \<and> image f X \<subseteq> Y \<and> P f"
1.482 -  apply (rule iffI)
1.483 -  using homotopic_with_imp_continuous homotopic_with_imp_property homotopic_with_imp_subset2 apply blast
1.484 -  apply (simp add: homotopic_with_def)
1.485 -  apply (rule_tac x="f \<circ> snd" in exI)
1.486 -  apply (rule conjI continuous_intros | force)+
1.487 -  done
1.488 -
1.489 -lemma homotopic_with_symD:
1.490 -  fixes X :: "'a::real_normed_vector set"
1.491 -    assumes "homotopic_with P X Y f g"
1.492 -      shows "homotopic_with P X Y g f"
1.493 -  using assms
1.494 -  apply (clarsimp simp add: homotopic_with_def)
1.495 -  apply (rename_tac h)
1.496 -  apply (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI)
1.497 -  apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
1.498 +lemma homotopic_from_subtopology:
1.499 +   "homotopic_with P X X' f g \<Longrightarrow> homotopic_with P (subtopology X s) X' f g"
1.500 +  unfolding homotopic_with_def
1.501 +  apply (erule ex_forward)
1.502 +  by (simp add: continuous_map_from_subtopology prod_topology_subtopology(2))
1.503 +
1.504 +lemma homotopic_on_emptyI:
1.505 +    assumes "topspace X = {}" "P f" "P g"
1.506 +    shows "homotopic_with P X X' f g"
1.507 +  unfolding homotopic_with_def
1.508 +proof (intro exI conjI ballI)
1.509 +  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
1.510 +    by (cases "t = 0", auto simp: assms)
1.511 +qed (auto simp: continuous_map_atin assms)
1.512 +
1.513 +lemma homotopic_on_empty:
1.514 +   "topspace X = {} \<Longrightarrow> (homotopic_with P X X' f g \<longleftrightarrow> P f \<and> P g)"
1.515 +  using homotopic_on_emptyI homotopic_with_imp_property by metis
1.516 +
1.517 +lemma homotopic_with_canon_on_empty [simp]: "homotopic_with_canon (\<lambda>x. True) {} t f g"
1.518 +  by (auto intro: homotopic_with_equal)
1.519 +
1.520 +lemma homotopic_constant_maps:
1.521 +   "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow>
1.522 +    topspace X = {} \<or> path_component_of X' a b" (is "?lhs = ?rhs")
1.523 +proof (cases "topspace X = {}")
1.524 +  case False
1.525 +  then obtain c where c: "c \<in> topspace X"
1.526 +    by blast
1.527 +  have "\<exists>g. continuous_map (top_of_set {0..1::real}) X' g \<and> g 0 = a \<and> g 1 = b"
1.528 +    if "x \<in> topspace X" and hom: "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. a) (\<lambda>x. b)" for x
1.529 +  proof -
1.530 +    obtain h :: "real \<times> 'a \<Rightarrow> 'b"
1.531 +      where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X' h"
1.532 +        and h: "\<And>x. h (0, x) = a" "\<And>x. h (1, x) = b"
1.533 +      using hom by (auto simp: homotopic_with_def)
1.534 +    have cont: "continuous_map (top_of_set {0..1}) X' (h \<circ> (\<lambda>t. (t, c)))"
1.535 +      apply (rule continuous_map_compose [OF _ conth])
1.536 +      apply (rule continuous_intros c | simp)+
1.537 +      done
1.538 +    then show ?thesis
1.539 +      by (force simp: h)
1.540 +  qed
1.541 +  moreover have "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. g 0) (\<lambda>x. g 1)"
1.542 +    if "x \<in> topspace X" "a = g 0" "b = g 1" "continuous_map (top_of_set {0..1}) X' g"
1.543 +    for x and g :: "real \<Rightarrow> 'b"
1.544 +    unfolding homotopic_with_def
1.545 +    by (force intro!: continuous_map_compose continuous_intros c that)
1.546 +  ultimately show ?thesis
1.547 +    using False by (auto simp: path_component_of_def pathin_def)
1.549 +
1.550 +proposition homotopic_with_eq:
1.551 +   assumes h: "homotopic_with P X Y f g"
1.552 +       and f': "\<And>x. x \<in> topspace X \<Longrightarrow> f' x = f x"
1.553 +       and g': "\<And>x. x \<in> topspace X \<Longrightarrow> g' x = g x"
1.554 +       and P:  "(\<And>h k. (\<And>x. x \<in> topspace X \<Longrightarrow> h x = k x) \<Longrightarrow> P h \<longleftrightarrow> P k)"
1.555 +   shows "homotopic_with P X Y f' g'"
1.556 +  using h unfolding homotopic_with_def
1.557 +  apply safe
1.558 +  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)
1.559 +  apply (simp add: f' g', safe)
1.560 +  apply (fastforce intro: continuous_map_eq)
1.561 +  apply (subst P; fastforce)
1.562    done
1.563
1.564 -proposition homotopic_with_sym:
1.565 -    fixes X :: "'a::real_normed_vector set"
1.566 -    shows "homotopic_with P X Y f g \<longleftrightarrow> homotopic_with P X Y g f"
1.567 -  using homotopic_with_symD by blast
1.568 -
1.569 -lemma split_01: "{0..1::real} = {0..1/2} \<union> {1/2..1}"
1.570 -  by force
1.571 -
1.572 -lemma split_01_prod: "{0..1::real} \<times> X = ({0..1/2} \<times> X) \<union> ({1/2..1} \<times> X)"
1.573 -  by force
1.574 -
1.575 -proposition homotopic_with_trans:
1.576 -    fixes X :: "'a::real_normed_vector set"
1.577 -    assumes "homotopic_with P X Y f g" and "homotopic_with P X Y g h"
1.578 -      shows "homotopic_with P X Y f h"
1.579 +lemma homotopic_with_prod_topology:
1.580 +  assumes "homotopic_with p X1 Y1 f f'" and "homotopic_with q X2 Y2 g g'"
1.581 +    and r: "\<And>i j. \<lbrakk>p i; q j\<rbrakk> \<Longrightarrow> r(\<lambda>(x,y). (i x, j y))"
1.582 +  shows "homotopic_with r (prod_topology X1 X2) (prod_topology Y1 Y2)
1.583 +                          (\<lambda>z. (f(fst z),g(snd z))) (\<lambda>z. (f'(fst z), g'(snd z)))"
1.584  proof -
1.585 -  have clo1: "closedin (top_of_set ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({0..1/2::real} \<times> X)"
1.586 -    apply (simp add: closedin_closed split_01_prod [symmetric])
1.587 -    apply (rule_tac x="{0..1/2} \<times> UNIV" in exI)
1.588 -    apply (force simp: closed_Times)
1.589 -    done
1.590 -  have clo2: "closedin (top_of_set ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({1/2..1::real} \<times> X)"
1.591 -    apply (simp add: closedin_closed split_01_prod [symmetric])
1.592 -    apply (rule_tac x="{1/2..1} \<times> UNIV" in exI)
1.593 -    apply (force simp: closed_Times)
1.594 -    done
1.595 -  { fix k1 k2:: "real \<times> 'a \<Rightarrow> 'b"
1.596 -    assume cont: "continuous_on ({0..1} \<times> X) k1" "continuous_on ({0..1} \<times> X) k2"
1.597 -       and Y: "k1 ` ({0..1} \<times> X) \<subseteq> Y" "k2 ` ({0..1} \<times> X) \<subseteq> Y"
1.598 -       and geq: "\<forall>x. k1 (1, x) = g x" "\<forall>x. k2 (0, x) = g x"
1.599 -       and k12: "\<forall>x. k1 (0, x) = f x" "\<forall>x. k2 (1, x) = h x"
1.600 -       and P:   "\<forall>t\<in>{0..1}. P (\<lambda>x. k1 (t, x))" "\<forall>t\<in>{0..1}. P (\<lambda>x. k2 (t, x))"
1.601 -    define k where "k y =
1.602 -      (if fst y \<le> 1 / 2
1.603 -       then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
1.604 -       else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y)" for y
1.605 -    have keq: "k1 (2 * u, v) = k2 (2 * u - 1, v)" if "u = 1/2"  for u v
1.606 -      by (simp add: geq that)
1.607 -    have "continuous_on ({0..1} \<times> X) k"
1.608 -      using cont
1.609 -      apply (simp add: split_01_prod k_def)
1.610 -      apply (rule clo1 clo2 continuous_on_cases_local continuous_intros | erule continuous_on_subset | simp add: linear image_subset_iff)+
1.611 -      apply (force simp: keq)
1.612 +  obtain h
1.613 +    where h: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) Y1 h"
1.614 +      and h0: "\<And>x. h (0, x) = f x"
1.615 +      and h1: "\<And>x. h (1, x) = f' x"
1.616 +      and p: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> p (\<lambda>x. h (t,x))"
1.617 +    using assms unfolding homotopic_with_def by auto
1.618 +  obtain k
1.619 +    where k: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) Y2 k"
1.620 +      and k0: "\<And>x. k (0, x) = g x"
1.621 +      and k1: "\<And>x. k (1, x) = g' x"
1.622 +      and q: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> q (\<lambda>x. k (t,x))"
1.623 +    using assms unfolding homotopic_with_def by auto
1.624 +  let ?hk = "\<lambda>(t,x,y). (h(t,x), k(t,y))"
1.625 +  show ?thesis
1.626 +    unfolding homotopic_with_def
1.627 +  proof (intro conjI allI exI)
1.628 +    show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (prod_topology X1 X2))
1.629 +                         (prod_topology Y1 Y2) ?hk"
1.630 +      unfolding continuous_map_pairwise case_prod_unfold
1.631 +      by (rule conjI continuous_map_pairedI continuous_intros continuous_map_id [unfolded id_def]
1.632 +          continuous_map_fst_of [unfolded o_def] continuous_map_snd_of [unfolded o_def]
1.633 +          continuous_map_compose [OF _ h, unfolded o_def]
1.634 +          continuous_map_compose [OF _ k, unfolded o_def])+
1.635 +  next
1.636 +    fix x
1.637 +    show "?hk (0, x) = (f (fst x), g (snd x))" "?hk (1, x) = (f' (fst x), g' (snd x))"
1.638 +      by (auto simp: case_prod_beta h0 k0 h1 k1)
1.639 +  qed (auto simp: p q r)
1.640 +qed
1.641 +
1.642 +
1.643 +lemma homotopic_with_product_topology:
1.644 +  assumes ht: "\<And>i. i \<in> I \<Longrightarrow> homotopic_with (p i) (X i) (Y i) (f i) (g i)"
1.645 +    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)))"
1.646 +  shows "homotopic_with q (product_topology X I) (product_topology Y I)
1.647 +                          (\<lambda>z. (\<lambda>i\<in>I. (f i) (z i))) (\<lambda>z. (\<lambda>i\<in>I. (g i) (z i)))"
1.648 +proof -
1.649 +  obtain h
1.650 +    where h: "\<And>i. i \<in> I \<Longrightarrow> continuous_map (prod_topology (subtopology euclideanreal {0..1}) (X i)) (Y i) (h i)"
1.651 +      and h0: "\<And>i x. i \<in> I \<Longrightarrow> h i (0, x) = f i x"
1.652 +      and h1: "\<And>i x. i \<in> I \<Longrightarrow> h i (1, x) = g i x"
1.653 +      and p: "\<And>i t. \<lbrakk>i \<in> I; t \<in> {0..1}\<rbrakk> \<Longrightarrow> p i (\<lambda>x. h i (t,x))"
1.654 +    using ht unfolding homotopic_with_def by metis
1.655 +  show ?thesis
1.656 +    unfolding homotopic_with_def
1.657 +  proof (intro conjI allI exI)
1.658 +    let ?h = "\<lambda>(t,z). \<lambda>i\<in>I. h i (t,z i)"
1.659 +    have "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
1.660 +                         (Y i) (\<lambda>x. h i (fst x, snd x i))" if "i \<in> I" for i
1.661 +      unfolding continuous_map_pairwise case_prod_unfold
1.662 +      apply (intro conjI that  continuous_intros continuous_map_compose [OF _ h, unfolded o_def])
1.663 +      using continuous_map_componentwise continuous_map_snd that apply fastforce
1.664        done
1.665 -    moreover have "k ` ({0..1} \<times> X) \<subseteq> Y"
1.666 -      using Y by (force simp: k_def)
1.667 -    moreover have "\<forall>x. k (0, x) = f x"
1.668 -      by (simp add: k_def k12)
1.669 -    moreover have "(\<forall>x. k (1, x) = h x)"
1.670 -      by (simp add: k_def k12)
1.671 -    moreover have "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
1.672 -      using P
1.673 -      apply (clarsimp simp add: k_def)
1.674 -      apply (case_tac "t \<le> 1/2", auto)
1.675 -      done
1.676 -    ultimately have *: "\<exists>k :: real \<times> 'a \<Rightarrow> 'b.
1.677 -                       continuous_on ({0..1} \<times> X) k \<and> k ` ({0..1} \<times> X) \<subseteq> Y \<and>
1.678 -                       (\<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)))"
1.679 -      by blast
1.680 -  } note * = this
1.681 -  show ?thesis
1.682 -    using assms by (auto intro: * simp add: homotopic_with_def)
1.683 +    then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
1.684 +         (product_topology Y I) ?h"
1.685 +      by (auto simp: continuous_map_componentwise case_prod_beta)
1.686 +    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
1.687 +      by (auto simp: case_prod_beta h0 h1)
1.688 +    show "\<forall>t\<in>{0..1}. q (\<lambda>x. ?h (t, x))"
1.689 +      by (force intro: p pq)
1.690 +  qed
1.691  qed
1.692
1.693 -proposition homotopic_compose:
1.694 -      fixes s :: "'a::real_normed_vector set"
1.695 -      shows "\<lbrakk>homotopic_with (\<lambda>x. True) s t f f'; homotopic_with (\<lambda>x. True) t u g g'\<rbrakk>
1.696 -             \<Longrightarrow> homotopic_with (\<lambda>x. True) s u (g \<circ> f) (g' \<circ> f')"
1.697 -  apply (rule homotopic_with_trans [where g = "g \<circ> f'"])
1.698 -  apply (metis homotopic_compose_continuous_left homotopic_with_imp_continuous homotopic_with_imp_subset1)
1.699 -  by (metis homotopic_compose_continuous_right homotopic_with_imp_continuous homotopic_with_imp_subset2)
1.700 -
1.701 -
1.702  text\<open>Homotopic triviality implicitly incorporates path-connectedness.\<close>
1.703  lemma homotopic_triviality:
1.704 -  fixes S :: "'a::real_normed_vector set"
1.705    shows  "(\<forall>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
1.706                   continuous_on S g \<and> g ` S \<subseteq> T
1.707 -                 \<longrightarrow> homotopic_with (\<lambda>x. True) S T f g) \<longleftrightarrow>
1.708 +                 \<longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g) \<longleftrightarrow>
1.709            (S = {} \<or> path_connected T) \<and>
1.710 -          (\<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)))"
1.711 +          (\<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)))"
1.712            (is "?lhs = ?rhs")
1.713  proof (cases "S = {} \<or> T = {}")
1.714 -  case True then show ?thesis by auto
1.715 +  case True then show ?thesis
1.716 +    by (auto simp: homotopic_on_emptyI)
1.717  next
1.718    case False show ?thesis
1.719    proof
1.720      assume LHS [rule_format]: ?lhs
1.721      have pab: "path_component T a b" if "a \<in> T" "b \<in> T" for a b
1.722      proof -
1.723 -      have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. b)"
1.724 +      have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. b)"
1.725          by (simp add: LHS continuous_on_const image_subset_iff that)
1.726        then show ?thesis
1.727 -        using False homotopic_constant_maps by blast
1.728 +        using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto
1.729      qed
1.730 -      moreover
1.731 -    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
1.732 -      by (metis (full_types) False LHS equals0I homotopic_constant_maps homotopic_with_imp_continuous homotopic_with_imp_subset2 pab that)
1.733 +    moreover
1.734 +    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
1.735 +      using False LHS continuous_on_const that by blast
1.736      ultimately show ?rhs
1.738    next
1.739 @@ -350,15 +498,15 @@
1.740      proof clarify
1.741        fix f g
1.742        assume "continuous_on S f" "f ` S \<subseteq> T" "continuous_on S g" "g ` S \<subseteq> T"
1.743 -      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)"
1.744 +      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)"
1.745          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
1.746        then have "c \<in> T" "d \<in> T"
1.747 -        using False homotopic_with_imp_subset2 by fastforce+
1.748 +        using False homotopic_with_imp_continuous_maps by fastforce+
1.749        with T have "path_component T c d"
1.750          using path_connected_component by blast
1.751 -      then have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. c) (\<lambda>x. d)"
1.752 +      then have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. c) (\<lambda>x. d)"
1.754 -      with c d show "homotopic_with (\<lambda>x. True) S T f g"
1.755 +      with c d show "homotopic_with_canon (\<lambda>x. True) S T f g"
1.756          by (meson homotopic_with_symD homotopic_with_trans)
1.757      qed
1.758    qed
1.759 @@ -371,7 +519,7 @@
1.760  definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
1.761    where
1.762       "homotopic_paths s p q \<equiv>
1.763 -       homotopic_with (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
1.764 +       homotopic_with_canon (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
1.765
1.766  lemma homotopic_paths:
1.767     "homotopic_paths s p q \<longleftrightarrow>
1.768 @@ -393,14 +541,14 @@
1.769
1.770  lemma homotopic_paths_imp_path:
1.771       "homotopic_paths s p q \<Longrightarrow> path p \<and> path q"
1.772 -  using homotopic_paths_def homotopic_with_imp_continuous path_def by blast
1.773 +  using homotopic_paths_def homotopic_with_imp_continuous_maps path_def continuous_map_subtopology_eu by blast
1.774
1.775  lemma homotopic_paths_imp_subset:
1.776       "homotopic_paths s p q \<Longrightarrow> path_image p \<subseteq> s \<and> path_image q \<subseteq> s"
1.777 -  by (simp add: homotopic_paths_def homotopic_with_imp_subset1 homotopic_with_imp_subset2 path_image_def)
1.778 +  by (metis (mono_tags) continuous_map_subtopology_eu homotopic_paths_def homotopic_with_imp_continuous_maps path_image_def)
1.779
1.780  proposition homotopic_paths_refl [simp]: "homotopic_paths s p p \<longleftrightarrow> path p \<and> path_image p \<subseteq> s"
1.781 -by (simp add: homotopic_paths_def homotopic_with_refl path_def path_image_def)
1.782 +  by (simp add: homotopic_paths_def path_def path_image_def)
1.783
1.784  proposition homotopic_paths_sym: "homotopic_paths s p q \<Longrightarrow> homotopic_paths s q p"
1.785    by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)
1.786 @@ -409,10 +557,16 @@
1.787    by (metis homotopic_paths_sym)
1.788
1.789  proposition homotopic_paths_trans [trans]:
1.790 -     "\<lbrakk>homotopic_paths s p q; homotopic_paths s q r\<rbrakk> \<Longrightarrow> homotopic_paths s p r"
1.791 -  apply (simp add: homotopic_paths_def)
1.792 -  apply (rule homotopic_with_trans, assumption)
1.793 -  by (metis (mono_tags, lifting) homotopic_with_imp_property homotopic_with_mono)
1.794 +  assumes "homotopic_paths s p q" "homotopic_paths s q r"
1.795 +  shows "homotopic_paths s p r"
1.796 +proof -
1.797 +  have "pathstart q = pathstart p" "pathfinish q = pathfinish p"
1.798 +    using assms by (simp_all add: homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish)
1.799 +  then have "homotopic_with_canon (\<lambda>f. pathstart f = pathstart p \<and> pathfinish f = pathfinish p) {0..1} s q r"
1.800 +    using \<open>homotopic_paths s q r\<close> homotopic_paths_def by force
1.801 +  then show ?thesis
1.802 +    using assms homotopic_paths_def homotopic_with_trans by blast
1.803 +qed
1.804
1.805  proposition homotopic_paths_eq:
1.806       "\<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"
1.807 @@ -460,7 +614,7 @@
1.808  qed
1.809
1.810  lemma homotopic_paths_subset: "\<lbrakk>homotopic_paths s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t p q"
1.811 -  using homotopic_paths_def homotopic_with_subset_right by blast
1.812 +  unfolding homotopic_paths by fast
1.813
1.814
1.815  text\<open> A slightly ad-hoc but useful lemma in constructing homotopies.\<close>
1.816 @@ -514,9 +668,7 @@
1.817  proposition homotopic_paths_continuous_image:
1.818      "\<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)"
1.819    unfolding homotopic_paths_def
1.820 -  apply (rule homotopic_with_compose_continuous_left [of _ _ _ s])
1.821 -  apply (auto simp: pathstart_def pathfinish_def elim!: homotopic_with_mono)
1.822 -  done
1.823 +  by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose)
1.824
1.825
1.826  subsection\<open>Group properties for homotopy of paths\<close>
1.827 @@ -586,7 +738,7 @@
1.828
1.829  definition%important homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
1.830   "homotopic_loops s p q \<equiv>
1.831 -     homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
1.832 +     homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
1.833
1.834  lemma homotopic_loops:
1.835     "homotopic_loops s p q \<longleftrightarrow>
1.836 @@ -604,17 +756,17 @@
1.837  proposition homotopic_loops_imp_path:
1.838       "homotopic_loops s p q \<Longrightarrow> path p \<and> path q"
1.839    unfolding homotopic_loops_def path_def
1.840 -  using homotopic_with_imp_continuous by blast
1.841 +  using homotopic_with_imp_continuous_maps continuous_map_subtopology_eu by blast
1.842
1.843  proposition homotopic_loops_imp_subset:
1.844       "homotopic_loops s p q \<Longrightarrow> path_image p \<subseteq> s \<and> path_image q \<subseteq> s"
1.845    unfolding homotopic_loops_def path_image_def
1.846 -  by (metis homotopic_with_imp_subset1 homotopic_with_imp_subset2)
1.847 +  by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
1.848
1.849  proposition homotopic_loops_refl:
1.850       "homotopic_loops s p p \<longleftrightarrow>
1.851        path p \<and> path_image p \<subseteq> s \<and> pathfinish p = pathstart p"
1.852 -  by (simp add: homotopic_loops_def homotopic_with_refl path_image_def path_def)
1.853 +  by (simp add: homotopic_loops_def path_image_def path_def)
1.854
1.855  proposition homotopic_loops_sym: "homotopic_loops s p q \<Longrightarrow> homotopic_loops s q p"
1.856    by (simp add: homotopic_loops_def homotopic_with_sym)
1.857 @@ -628,7 +780,7 @@
1.858
1.859  proposition homotopic_loops_subset:
1.860     "\<lbrakk>homotopic_loops s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t p q"
1.861 -  by (simp add: homotopic_loops_def homotopic_with_subset_right)
1.862 +  by (fastforce simp add: homotopic_loops)
1.863
1.864  proposition homotopic_loops_eq:
1.865     "\<lbrakk>path p; path_image p \<subseteq> s; pathfinish p = pathstart p; \<And>t. t \<in> {0..1} \<Longrightarrow> p(t) = q(t)\<rbrakk>
1.866 @@ -642,16 +794,14 @@
1.867  proposition homotopic_loops_continuous_image:
1.868     "\<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)"
1.869    unfolding homotopic_loops_def
1.870 -  apply (rule homotopic_with_compose_continuous_left)
1.871 -  apply (erule homotopic_with_mono)
1.872 -  by (simp add: pathfinish_def pathstart_def)
1.873 +  by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def)
1.874
1.875
1.876  subsection\<open>Relations between the two variants of homotopy\<close>
1.877
1.878  proposition homotopic_paths_imp_homotopic_loops:
1.879      "\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
1.880 -  by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
1.881 +  by (auto simp: homotopic_with_def homotopic_paths_def homotopic_loops_def)
1.882
1.883  proposition homotopic_loops_imp_homotopic_paths_null:
1.884    assumes "homotopic_loops s p (linepath a a)"
1.885 @@ -828,7 +978,7 @@
1.886    assumes contf: "continuous_on s f"
1.887        and contg:"continuous_on s g"
1.888        and sub: "\<And>x. x \<in> s \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> t"
1.889 -    shows "homotopic_with (\<lambda>z. True) s t f g"
1.890 +    shows "homotopic_with_canon (\<lambda>z. True) s t f g"
1.892    apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R f(snd y) + (fst y) *\<^sub>R g(snd y))" in exI)
1.893    apply (intro conjI)
1.894 @@ -1208,7 +1358,7 @@
1.895  subsection\<open>Contractible sets\<close>
1.896
1.897  definition%important contractible where
1.898 - "contractible S \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
1.899 + "contractible S \<equiv> \<exists>a. homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
1.900
1.901  proposition contractible_imp_simply_connected:
1.902    fixes S :: "_::real_normed_vector set"
1.903 @@ -1217,10 +1367,10 @@
1.904    case True then show ?thesis by force
1.905  next
1.906    case False
1.907 -  obtain a where a: "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
1.908 +  obtain a where a: "homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
1.909      using assms by (force simp: contractible_def)
1.910    then have "a \<in> S"
1.911 -    by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_mem(2))
1.912 +    by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_in_topspace topspace_euclidean_subtopology)
1.913    show ?thesis
1.914      apply (simp add: simply_connected_eq_contractible_loop_all False)
1.915      apply (rule bexI [OF _ \<open>a \<in> S\<close>])
1.916 @@ -1246,14 +1396,14 @@
1.917    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
1.918        and g: "continuous_on T g" "g ` T \<subseteq> U"
1.919        and T: "contractible T"
1.920 -    obtains c where "homotopic_with (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
1.921 +    obtains c where "homotopic_with_canon (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
1.922  proof -
1.923 -  obtain b where b: "homotopic_with (\<lambda>x. True) T T id (\<lambda>x. b)"
1.924 +  obtain b where b: "homotopic_with_canon (\<lambda>x. True) T T id (\<lambda>x. b)"
1.925      using assms by (force simp: contractible_def)
1.926 -  have "homotopic_with (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
1.927 -    by (rule homotopic_compose_continuous_left [OF b g])
1.928 -  then have "homotopic_with (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
1.929 -    by (rule homotopic_compose_continuous_right [OF _ f])
1.930 +  have "homotopic_with_canon (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
1.931 +    by (metis Abstract_Topology.continuous_map_subtopology_eu b g homotopic_compose_continuous_map_left)
1.932 +  then have "homotopic_with_canon (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
1.933 +    by (simp add: f homotopic_with_compose_continuous_map_right)
1.934    then show ?thesis
1.935      by (simp add: comp_def that)
1.936  qed
1.937 @@ -1261,7 +1411,7 @@
1.938  lemma nullhomotopic_into_contractible:
1.939    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
1.940        and T: "contractible T"
1.941 -    obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
1.942 +    obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
1.943  apply (rule nullhomotopic_through_contractible [OF f, of id T])
1.944  using assms
1.945  apply (auto simp: continuous_on_id)
1.946 @@ -1270,7 +1420,7 @@
1.947  lemma nullhomotopic_from_contractible:
1.948    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
1.949        and S: "contractible S"
1.950 -    obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
1.951 +    obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
1.952  apply (rule nullhomotopic_through_contractible [OF continuous_on_id _ f S, of S])
1.953  using assms
1.954  apply (auto simp: comp_def)
1.955 @@ -1283,13 +1433,13 @@
1.956            "continuous_on S f2" "f2 ` S \<subseteq> T"
1.957            "continuous_on T g2" "g2 ` T \<subseteq> U"
1.958            "contractible T" "path_connected U"
1.959 -   shows "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
1.960 +   shows "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
1.961  proof -
1.962 -  obtain c1 where c1: "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
1.963 +  obtain c1 where c1: "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
1.964      apply (rule nullhomotopic_through_contractible [of S f1 T g1 U])
1.965      using assms apply auto
1.966      done
1.967 -  obtain c2 where c2: "homotopic_with (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
1.968 +  obtain c2 where c2: "homotopic_with_canon (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
1.969      apply (rule nullhomotopic_through_contractible [of S f2 T g2 U])
1.970      using assms apply auto
1.971      done
1.972 @@ -1299,7 +1449,7 @@
1.973    next
1.974      case False
1.975      with c1 c2 have "c1 \<in> U" "c2 \<in> U"
1.976 -      using homotopic_with_imp_subset2 all_not_in_conv image_subset_iff by blast+
1.977 +      using homotopic_with_imp_continuous_maps by fastforce+
1.978      with \<open>path_connected U\<close> show ?thesis by blast
1.979    qed
1.980    show ?thesis
1.981 @@ -1315,24 +1465,24 @@
1.982    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
1.983        and g: "continuous_on S g" "g ` S \<subseteq> T"
1.984        and T: "contractible T"
1.985 -    shows "homotopic_with (\<lambda>h. True) S T f g"
1.986 +    shows "homotopic_with_canon (\<lambda>h. True) S T f g"
1.987  using homotopic_through_contractible [of S f T id T g id]
1.988 -by (simp add: assms contractible_imp_path_connected continuous_on_id)
1.989 +by (simp add: assms contractible_imp_path_connected)
1.990
1.991  lemma homotopic_from_contractible:
1.992    fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
1.993    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
1.994        and g: "continuous_on S g" "g ` S \<subseteq> T"
1.995        and "contractible S" "path_connected T"
1.996 -    shows "homotopic_with (\<lambda>h. True) S T f g"
1.997 +    shows "homotopic_with_canon (\<lambda>h. True) S T f g"
1.998  using homotopic_through_contractible [of S id S f T id g]
1.999 -by (simp add: assms contractible_imp_path_connected continuous_on_id)
1.1000 +by (simp add: assms contractible_imp_path_connected)
1.1001
1.1002  lemma starlike_imp_contractible_gen:
1.1003    fixes S :: "'a::real_normed_vector set"
1.1004    assumes S: "starlike S"
1.1005        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)"
1.1006 -    obtains a where "homotopic_with P S S (\<lambda>x. x) (\<lambda>x. a)"
1.1007 +    obtains a where "homotopic_with_canon P S S (\<lambda>x. x) (\<lambda>x. a)"
1.1008  proof -
1.1009    obtain a where "a \<in> S" and a: "\<And>x. x \<in> S \<Longrightarrow> closed_segment a x \<subseteq> S"
1.1010      using S by (auto simp: starlike_def)
1.1011 @@ -1385,7 +1535,7 @@
1.1012  using convex_imp_simply_connected is_interval_convex_1 is_interval_path_connected_1 simply_connected_imp_path_connected by auto
1.1013
1.1014  lemma contractible_empty [simp]: "contractible {}"
1.1015 -  by (simp add: contractible_def homotopic_with)
1.1016 +  by (simp add: contractible_def homotopic_on_emptyI)
1.1017
1.1018  lemma contractible_convex_tweak_boundary_points:
1.1019    fixes S :: "'a::euclidean_space set"
1.1020 @@ -1445,27 +1595,6 @@
1.1021      done
1.1022  qed
1.1023
1.1024 -lemma homotopy_dominated_contractibility:
1.1025 -  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
1.1026 -  assumes S: "contractible S"
1.1027 -      and f: "continuous_on S f" "image f S \<subseteq> T"
1.1028 -      and g: "continuous_on T g" "image g T \<subseteq> S"
1.1029 -      and hom: "homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
1.1030 -    shows "contractible T"
1.1031 -proof -
1.1032 -  obtain b where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. b)"
1.1033 -    using nullhomotopic_from_contractible [OF f S] .
1.1034 -  then have homg: "homotopic_with (\<lambda>x. True) T T ((\<lambda>x. b) \<circ> g) (f \<circ> g)"
1.1035 -    by (rule homotopic_with_compose_continuous_right [OF homotopic_with_symD g])
1.1036 -  show ?thesis
1.1037 -    apply (simp add: contractible_def)
1.1038 -    apply (rule exI [where x = b])
1.1039 -    apply (rule homotopic_with_symD)
1.1040 -    apply (rule homotopic_with_trans [OF _ hom])
1.1041 -    using homg apply (simp add: o_def)
1.1042 -    done
1.1043 -qed
1.1044 -
1.1045
1.1046  subsection\<open>Local versions of topological properties in general\<close>
1.1047
1.1048 @@ -1541,7 +1670,7 @@
1.1050  apply (rule_tac x="V1 \<inter> V2" in exI)
1.1051  apply (auto intro: P)
1.1052 -done
1.1053 +  done
1.1054
1.1055  lemma locally_Times:
1.1056    fixes S :: "('a::metric_space) set" and T :: "('b::metric_space) set"
1.1057 @@ -1561,7 +1690,7 @@
1.1058    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"
1.1059      apply (rule_tac x="U1 \<times> V1" in exI)
1.1060      apply (rule_tac x="U2 \<times> V2" in exI)
1.1061 -    apply (auto simp: openin_Times R)
1.1062 +    apply (auto simp: openin_Times R openin_Times_eq)
1.1063      done
1.1064  qed
1.1065
1.1066 @@ -3195,10 +3324,10 @@
1.1067        and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
1.1068        and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f;
1.1069                         continuous_on u g; g ` u \<subseteq> s; P g\<rbrakk>
1.1070 -                       \<Longrightarrow> homotopic_with P u s f g"
1.1071 +                       \<Longrightarrow> homotopic_with_canon P u s f g"
1.1072        and contf: "continuous_on u f" and imf: "f ` u \<subseteq> t" and Qf: "Q f"
1.1073        and contg: "continuous_on u g" and img: "g ` u \<subseteq> t" and Qg: "Q g"
1.1074 -    shows "homotopic_with Q u t f g"
1.1075 +    shows "homotopic_with_canon Q u t f g"
1.1076  proof -
1.1077    have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
1.1078    have geq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> g)) x = g x" using idhk img by auto
1.1079 @@ -3214,17 +3343,15 @@
1.1080      using img imk by fastforce
1.1081    moreover have "P (k \<circ> g)"
1.1082      by (simp add: P Qg contg img)
1.1083 -  ultimately have "homotopic_with P u s (k \<circ> f) (k \<circ> g)"
1.1084 +  ultimately have "homotopic_with_canon P u s (k \<circ> f) (k \<circ> g)"
1.1085      by (rule hom)
1.1086 -  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
1.1087 +  then have "homotopic_with_canon Q u t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
1.1088      apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
1.1089      using Q by (auto simp: conth imh)
1.1090    then show ?thesis
1.1091      apply (rule homotopic_with_eq)
1.1092 -    apply (metis feq)
1.1093 -    apply (metis geq)
1.1094 -    apply (metis Qeq)
1.1095 -    done
1.1096 +    using feq geq apply fastforce+
1.1097 +    using Qeq topspace_euclidean_subtopology by blast
1.1098  qed
1.1099
1.1100  lemma homotopically_trivial_retraction_null_gen:
1.1101 @@ -3232,9 +3359,9 @@
1.1102        and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
1.1103        and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
1.1104        and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk>
1.1105 -                     \<Longrightarrow> \<exists>c. homotopic_with P u s f (\<lambda>x. c)"
1.1106 +                     \<Longrightarrow> \<exists>c. homotopic_with_canon P u s f (\<lambda>x. c)"
1.1107        and contf: "continuous_on u f" and imf:"f ` u \<subseteq> t" and Qf: "Q f"
1.1108 -  obtains c where "homotopic_with Q u t f (\<lambda>x. c)"
1.1109 +  obtains c where "homotopic_with_canon Q u t f (\<lambda>x. c)"
1.1110  proof -
1.1111    have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
1.1112    have "continuous_on u (k \<circ> f)"
1.1113 @@ -3243,17 +3370,17 @@
1.1114      using imf imk by fastforce
1.1115    moreover have "P (k \<circ> f)"
1.1116      by (simp add: P Qf contf imf)
1.1117 -  ultimately obtain c where "homotopic_with P u s (k \<circ> f) (\<lambda>x. c)"
1.1118 +  ultimately obtain c where "homotopic_with_canon P u s (k \<circ> f) (\<lambda>x. c)"
1.1119      by (metis hom)
1.1120 -  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
1.1121 +  then have "homotopic_with_canon Q u t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
1.1122      apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
1.1123      using Q by (auto simp: conth imh)
1.1124    then show ?thesis
1.1125      apply (rule_tac c = "h c" in that)
1.1126      apply (erule homotopic_with_eq)
1.1127 -    apply (metis feq, simp)
1.1128 -    apply (metis Qeq)
1.1129 -    done
1.1130 +    using feq apply auto
1.1131 +    apply simp
1.1132 +    using Qeq topspace_euclidean_subtopology by blast
1.1133  qed
1.1134
1.1135  lemma cohomotopically_trivial_retraction_gen:
1.1136 @@ -3262,10 +3389,10 @@
1.1137        and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
1.1138        and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f;
1.1139                         continuous_on s g; g ` s \<subseteq> u; P g\<rbrakk>
1.1140 -                       \<Longrightarrow> homotopic_with P s u f g"
1.1141 +                       \<Longrightarrow> homotopic_with_canon P s u f g"
1.1142        and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f"
1.1143        and contg: "continuous_on t g" and img: "g ` t \<subseteq> u" and Qg: "Q g"
1.1144 -    shows "homotopic_with Q t u f g"
1.1145 +    shows "homotopic_with_canon Q t u f g"
1.1146  proof -
1.1147    have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
1.1148    have geq: "\<And>x. x \<in> t \<Longrightarrow> (g \<circ> h \<circ> k) x = g x" using idhk img by auto
1.1149 @@ -3281,17 +3408,16 @@
1.1150      using img imh by fastforce
1.1151    moreover have "P (g \<circ> h)"
1.1152      by (simp add: P Qg contg img)
1.1153 -  ultimately have "homotopic_with P s u (f \<circ> h) (g \<circ> h)"
1.1154 +  ultimately have "homotopic_with_canon P s u (f \<circ> h) (g \<circ> h)"
1.1155      by (rule hom)
1.1156 -  then have "homotopic_with Q t u (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
1.1157 +  then have "homotopic_with_canon Q t u (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
1.1158      apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
1.1159      using Q by (auto simp: contk imk)
1.1160    then show ?thesis
1.1161      apply (rule homotopic_with_eq)
1.1162 -    apply (metis feq)
1.1163 -    apply (metis geq)
1.1164 -    apply (metis Qeq)
1.1165 -    done
1.1166 +    using feq apply auto
1.1167 +    using geq apply auto
1.1168 +    using Qeq topspace_euclidean_subtopology by blast
1.1169  qed
1.1170
1.1171  lemma cohomotopically_trivial_retraction_null_gen:
1.1172 @@ -3299,9 +3425,9 @@
1.1173        and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
1.1174        and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
1.1175        and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk>
1.1176 -                       \<Longrightarrow> \<exists>c. homotopic_with P s u f (\<lambda>x. c)"
1.1177 +                       \<Longrightarrow> \<exists>c. homotopic_with_canon P s u f (\<lambda>x. c)"
1.1178        and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f"
1.1179 -  obtains c where "homotopic_with Q t u f (\<lambda>x. c)"
1.1180 +  obtains c where "homotopic_with_canon Q t u f (\<lambda>x. c)"
1.1181  proof -
1.1182    have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
1.1183    have "continuous_on s (f \<circ> h)"
1.1184 @@ -3310,17 +3436,17 @@
1.1185      using imf imh by fastforce
1.1186    moreover have "P (f \<circ> h)"
1.1187      by (simp add: P Qf contf imf)
1.1188 -  ultimately obtain c where "homotopic_with P s u (f \<circ> h) (\<lambda>x. c)"
1.1189 +  ultimately obtain c where "homotopic_with_canon P s u (f \<circ> h) (\<lambda>x. c)"
1.1190      by (metis hom)
1.1191 -  then have "homotopic_with Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
1.1192 +  then have "homotopic_with_canon Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
1.1193      apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
1.1194      using Q by (auto simp: contk imk)
1.1195    then show ?thesis
1.1196      apply (rule_tac c = c in that)
1.1197      apply (erule homotopic_with_eq)
1.1198 -    apply (metis feq, simp)
1.1199 -    apply (metis Qeq)
1.1200 -    done
1.1201 +    using feq apply auto
1.1202 +    apply simp
1.1203 +    using Qeq topspace_euclidean_subtopology by blast
1.1204  qed
1.1205
1.1206  end
1.1207 @@ -3346,59 +3472,64 @@
1.1208
1.1209  subsection\<open>Homotopy equivalence\<close>
1.1210
1.1211 -definition%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
1.1212 -             (infix "homotopy'_eqv" 50)
1.1213 -  where "S homotopy_eqv T \<equiv>
1.1214 -        \<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
1.1215 -              continuous_on T g \<and> g ` T \<subseteq> S \<and>
1.1216 -              homotopic_with (\<lambda>x. True) S S (g \<circ> f) id \<and>
1.1217 -              homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
1.1218 -
1.1219 -lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
1.1220 -  unfolding homeomorphic_def homotopy_eqv_def homeomorphism_def
1.1221 -  by (fastforce intro!: homotopic_with_equal continuous_on_compose)
1.1222 -
1.1223 -lemma homotopy_eqv_refl: "S homotopy_eqv S"
1.1224 -  by (rule homeomorphic_imp_homotopy_eqv homeomorphic_refl)+
1.1225 -
1.1226 -lemma homotopy_eqv_sym: "S homotopy_eqv T \<longleftrightarrow> T homotopy_eqv S"
1.1227 -  by (auto simp: homotopy_eqv_def)
1.1228 +subsection\<open>Homotopy equivalence of topological spaces.\<close>
1.1229 +
1.1230 +definition%important homotopy_equivalent_space
1.1231 +             (infix "homotopy'_equivalent'_space" 50)
1.1232 +  where "X homotopy_equivalent_space Y \<equiv>
1.1233 +        (\<exists>f g. continuous_map X Y f \<and>
1.1234 +              continuous_map Y X g \<and>
1.1235 +              homotopic_with (\<lambda>x. True) X X (g \<circ> f) id \<and>
1.1236 +              homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) id)"
1.1237 +
1.1238 +lemma homeomorphic_imp_homotopy_equivalent_space:
1.1239 +  "X homeomorphic_space Y \<Longrightarrow> X homotopy_equivalent_space Y"
1.1240 +  unfolding homeomorphic_space_def homotopy_equivalent_space_def
1.1241 +  apply (erule ex_forward)+
1.1242 +  by (simp add: homotopic_with_equal homotopic_with_sym homeomorphic_maps_def)
1.1243 +
1.1244 +lemma homotopy_equivalent_space_refl:
1.1245 +   "X homotopy_equivalent_space X"
1.1246 +  by (simp add: homeomorphic_imp_homotopy_equivalent_space homeomorphic_space_refl)
1.1247 +
1.1248 +lemma homotopy_equivalent_space_sym:
1.1249 +   "X homotopy_equivalent_space Y \<longleftrightarrow> Y homotopy_equivalent_space X"
1.1250 +  by (meson homotopy_equivalent_space_def)
1.1251
1.1252  lemma homotopy_eqv_trans [trans]:
1.1253 -    fixes S :: "'a::real_normed_vector set" and U :: "'c::real_normed_vector set"
1.1254 -  assumes ST: "S homotopy_eqv T" and TU: "T homotopy_eqv U"
1.1255 -    shows "S homotopy_eqv U"
1.1256 +  assumes 1: "X homotopy_equivalent_space Y" and 2: "Y homotopy_equivalent_space U"
1.1257 +    shows "X homotopy_equivalent_space U"
1.1258  proof -
1.1259 -  obtain f1 g1 where f1: "continuous_on S f1" "f1 ` S \<subseteq> T"
1.1260 -                 and g1: "continuous_on T g1" "g1 ` T \<subseteq> S"
1.1261 -                 and hom1: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> f1) id"
1.1262 -                           "homotopic_with (\<lambda>x. True) T T (f1 \<circ> g1) id"
1.1263 -    using ST by (auto simp: homotopy_eqv_def)
1.1264 -  obtain f2 g2 where f2: "continuous_on T f2" "f2 ` T \<subseteq> U"
1.1265 -                 and g2: "continuous_on U g2" "g2 ` U \<subseteq> T"
1.1266 -                 and hom2: "homotopic_with (\<lambda>x. True) T T (g2 \<circ> f2) id"
1.1267 +  obtain f1 g1 where f1: "continuous_map X Y f1"
1.1268 +                 and g1: "continuous_map Y X g1"
1.1269 +                 and hom1: "homotopic_with (\<lambda>x. True) X X (g1 \<circ> f1) id"
1.1270 +                           "homotopic_with (\<lambda>x. True) Y Y (f1 \<circ> g1) id"
1.1271 +    using 1 by (auto simp: homotopy_equivalent_space_def)
1.1272 +  obtain f2 g2 where f2: "continuous_map Y U f2"
1.1273 +                 and g2: "continuous_map U Y g2"
1.1274 +                 and hom2: "homotopic_with (\<lambda>x. True) Y Y (g2 \<circ> f2) id"
1.1275                             "homotopic_with (\<lambda>x. True) U U (f2 \<circ> g2) id"
1.1276 -    using TU by (auto simp: homotopy_eqv_def)
1.1277 -  have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
1.1278 -    by (rule homotopic_with_compose_continuous_right hom2 f1)+
1.1279 -  then have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
1.1280 +    using 2 by (auto simp: homotopy_equivalent_space_def)
1.1281 +  have "homotopic_with (\<lambda>f. True) X Y (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
1.1282 +    using f1 hom2(1) homotopic_compose_continuous_map_right by blast
1.1283 +  then have "homotopic_with (\<lambda>f. True) X Y (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
1.1285 -  then have "homotopic_with (\<lambda>x. True) S S
1.1286 +  then have "homotopic_with (\<lambda>x. True) X X
1.1287           (g1 \<circ> (g2 \<circ> (f2 \<circ> f1))) (g1 \<circ> (id \<circ> f1))"
1.1288 -    by (simp add: g1 homotopic_with_compose_continuous_left)
1.1289 -  moreover have "homotopic_with (\<lambda>x. True) S S (g1 \<circ> id \<circ> f1) id"
1.1290 +    by (simp add: g1 homotopic_compose_continuous_map_left)
1.1291 +  moreover have "homotopic_with (\<lambda>x. True) X X (g1 \<circ> id \<circ> f1) id"
1.1292      using hom1 by simp
1.1293 -  ultimately have SS: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
1.1294 +  ultimately have SS: "homotopic_with (\<lambda>x. True) X X (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
1.1296      apply (blast intro: homotopic_with_trans)
1.1297      done
1.1298 -  have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> g1 \<circ> g2) (id \<circ> g2)"
1.1299 -    by (rule homotopic_with_compose_continuous_right hom1 g2)+
1.1300 -  then have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
1.1301 +  have "homotopic_with (\<lambda>f. True) U Y (f1 \<circ> g1 \<circ> g2) (id \<circ> g2)"
1.1302 +    using g2 hom1(2) homotopic_with_compose_continuous_map_right by fastforce
1.1303 +  then have "homotopic_with (\<lambda>f. True) U Y (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
1.1305    then have "homotopic_with (\<lambda>x. True) U U
1.1306           (f2 \<circ> (f1 \<circ> (g1 \<circ> g2))) (f2 \<circ> (id \<circ> g2))"
1.1307 -    by (simp add: f2 homotopic_with_compose_continuous_left)
1.1308 +    by (simp add: f2 homotopic_with_compose_continuous_map_left)
1.1309    moreover have "homotopic_with (\<lambda>x. True) U U (f2 \<circ> id \<circ> g2) id"
1.1310      using hom2 by simp
1.1311    ultimately have UU: "homotopic_with (\<lambda>x. True) U U (f2 \<circ> f1 \<circ> (g1 \<circ> g2)) id"
1.1312 @@ -3406,14 +3537,382 @@
1.1313      apply (blast intro: homotopic_with_trans)
1.1314      done
1.1315    show ?thesis
1.1316 -    unfolding homotopy_eqv_def
1.1317 -    apply (rule_tac x = "f2 \<circ> f1" in exI)
1.1318 -    apply (rule_tac x = "g1 \<circ> g2" in exI)
1.1319 -    apply (intro conjI continuous_on_compose SS UU)
1.1320 -    using f1 f2 g1 g2  apply (force simp: elim!: continuous_on_subset)+
1.1321 -    done
1.1322 +    unfolding homotopy_equivalent_space_def
1.1323 +    by (blast intro: f1 f2 g1 g2 continuous_map_compose SS UU)
1.1324 +qed
1.1325 +
1.1326 +lemma deformation_retraction_imp_homotopy_equivalent_space:
1.1327 +  "\<lbrakk>homotopic_with (\<lambda>x. True) X X (s \<circ> r) id; retraction_maps X Y r s\<rbrakk>
1.1328 +    \<Longrightarrow> X homotopy_equivalent_space Y"
1.1329 +  unfolding homotopy_equivalent_space_def retraction_maps_def
1.1330 +  apply (rule_tac x=r in exI)
1.1331 +  apply (rule_tac x=s in exI)
1.1332 +  apply (auto simp: homotopic_with_equal continuous_map_compose)
1.1333 +  done
1.1334 +
1.1335 +lemma deformation_retract_imp_homotopy_equivalent_space:
1.1336 +   "\<lbrakk>homotopic_with (\<lambda>x. True) X X r id; retraction_maps X Y r id\<rbrakk>
1.1337 +    \<Longrightarrow> X homotopy_equivalent_space Y"
1.1338 +  using deformation_retraction_imp_homotopy_equivalent_space by force
1.1339 +
1.1340 +lemma deformation_retract_of_space:
1.1341 +  "S \<subseteq> topspace X \<and>
1.1342 +   (\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id) \<longleftrightarrow>
1.1343 +   S retract_of_space X \<and> (\<exists>f. homotopic_with (\<lambda>x. True) X X id f \<and> f ` (topspace X) \<subseteq> S)"
1.1344 +proof (cases "S \<subseteq> topspace X")
1.1345 +  case True
1.1346 +  moreover have "(\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id)
1.1347 +             \<longleftrightarrow> (S retract_of_space X \<and> (\<exists>f. homotopic_with (\<lambda>x. True) X X id f \<and> f ` topspace X \<subseteq> S))"
1.1348 +    unfolding retract_of_space_def
1.1349 +  proof safe
1.1350 +    fix f r
1.1351 +    assume f: "homotopic_with (\<lambda>x. True) X X id f"
1.1352 +      and fS: "f ` topspace X \<subseteq> S"
1.1353 +      and r: "continuous_map X (subtopology X S) r"
1.1354 +      and req: "\<forall>x\<in>S. r x = x"
1.1355 +    show "\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id"
1.1356 +    proof (intro exI conjI)
1.1357 +      have "homotopic_with (\<lambda>x. True) X X f r"
1.1358 +        proof (rule homotopic_with_eq)
1.1359 +          show "homotopic_with (\<lambda>x. True) X X (r \<circ> f) (r \<circ> id)"
1.1360 +            using homotopic_with_symD continuous_map_into_fulltopology f homotopic_compose_continuous_map_left r by blast
1.1361 +          show "f x = (r \<circ> f) x" if "x \<in> topspace X" for x
1.1362 +            using that fS req by auto
1.1363 +        qed auto
1.1364 +      then show "homotopic_with (\<lambda>x. True) X X id r"
1.1365 +        by (rule homotopic_with_trans [OF f])
1.1366 +    next
1.1367 +      show "retraction_maps X (subtopology X S) r id"
1.1368 +        by (simp add: r req retraction_maps_def topspace_subtopology)
1.1369 +    qed
1.1370 +  qed (use True in \<open>auto simp: retraction_maps_def topspace_subtopology_subset continuous_map_in_subtopology\<close>)
1.1371 +  ultimately show ?thesis by simp
1.1372 +qed (auto simp: retract_of_space_def retraction_maps_def)
1.1373 +
1.1374 +
1.1375 +
1.1376 +subsection\<open>Contractible spaces\<close>
1.1377 +
1.1378 +text\<open>The definition (which agrees with "contractible" on subsets of Euclidean space)
1.1379 +is a little cryptic because we don't in fact assume that the constant "a" is in the space.
1.1380 +This forces the convention that the empty space / set is contractible, avoiding some special cases. \<close>
1.1381 +
1.1382 +definition contractible_space where
1.1383 +  "contractible_space X \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
1.1384 +
1.1385 +lemma contractible_space_top_of_set [simp]:"contractible_space (top_of_set S) \<longleftrightarrow> contractible S"
1.1386 +  by (auto simp: contractible_space_def contractible_def)
1.1387 +
1.1388 +lemma contractible_space_empty:
1.1389 +   "topspace X = {} \<Longrightarrow> contractible_space X"
1.1390 +  apply (simp add: contractible_space_def homotopic_with_def)
1.1391 +  apply (rule_tac x=undefined in exI)
1.1392 +  apply (rule_tac x="\<lambda>(t,x). if t = 0 then x else undefined" in exI)
1.1393 +  apply (auto simp: continuous_map_on_empty)
1.1394 +  done
1.1395 +
1.1396 +lemma contractible_space_singleton:
1.1397 +  "topspace X = {a} \<Longrightarrow> contractible_space X"
1.1398 +  apply (simp add: contractible_space_def homotopic_with_def)
1.1399 +  apply (rule_tac x=a in exI)
1.1400 +  apply (rule_tac x="\<lambda>(t,x). if t = 0 then x else a" in exI)
1.1401 +  apply (auto intro: continuous_map_eq [where f = "\<lambda>z. a"])
1.1402 +  done
1.1403 +
1.1404 +lemma contractible_space_subset_singleton:
1.1405 +   "topspace X \<subseteq> {a} \<Longrightarrow> contractible_space X"
1.1406 +  by (meson contractible_space_empty contractible_space_singleton subset_singletonD)
1.1407 +
1.1408 +lemma contractible_space_subtopology_singleton:
1.1409 +   "contractible_space(subtopology X {a})"
1.1410 +  by (meson contractible_space_subset_singleton insert_subset path_connectedin_singleton path_connectedin_subtopology subsetI)
1.1411 +
1.1412 +lemma contractible_space:
1.1413 +   "contractible_space X \<longleftrightarrow>
1.1414 +        topspace X = {} \<or>
1.1415 +        (\<exists>a \<in> topspace X. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a))"
1.1416 +proof (cases "topspace X = {}")
1.1417 +  case False
1.1418 +  then show ?thesis
1.1419 +    apply (auto simp: contractible_space_def)
1.1420 +    using homotopic_with_imp_continuous_maps by fastforce
1.1422 +
1.1423 +lemma contractible_imp_path_connected_space:
1.1424 +  assumes "contractible_space X" shows "path_connected_space X"
1.1425 +proof (cases "topspace X = {}")
1.1426 +  case False
1.1427 +  have *: "path_connected_space X"
1.1428 +    if "a \<in> topspace X" and conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X h"
1.1429 +      and h: "\<forall>x. h (0, x) = x" "\<forall>x. h (1, x) = a"
1.1430 +    for a and h :: "real \<times> 'a \<Rightarrow> 'a"
1.1431 +  proof -
1.1432 +    have "path_component_of X b a" if "b \<in> topspace X" for b
1.1433 +      using that unfolding path_component_of_def
1.1434 +      apply (rule_tac x="h \<circ> (\<lambda>x. (x,b))" in exI)
1.1435 +      apply (simp add: h pathin_def)
1.1436 +      apply (rule continuous_map_compose [OF _ conth])
1.1437 +      apply (auto simp: continuous_map_pairwise intro!: continuous_intros continuous_map_compose continuous_map_id [unfolded id_def])
1.1438 +      done
1.1439 +  then show ?thesis
1.1440 +    by (metis path_component_of_equiv path_connected_space_iff_path_component)
1.1441 +  qed
1.1442 +  show ?thesis
1.1443 +    using assms False by (auto simp: contractible_space homotopic_with_def *)
1.1445 +
1.1446 +lemma contractible_imp_connected_space:
1.1447 +   "contractible_space X \<Longrightarrow> connected_space X"
1.1448 +  by (simp add: contractible_imp_path_connected_space path_connected_imp_connected_space)
1.1449 +
1.1450 +lemma contractible_space_alt:
1.1451 +   "contractible_space X \<longleftrightarrow> (\<forall>a \<in> topspace X. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a))" (is "?lhs = ?rhs")
1.1452 +proof
1.1453 +  assume X: ?lhs
1.1454 +  then obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
1.1455 +    by (auto simp: contractible_space_def)
1.1456 +  show ?rhs
1.1457 +  proof
1.1458 +    show "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. b)" if "b \<in> topspace X" for b
1.1459 +      apply (rule homotopic_with_trans [OF a])
1.1460 +      using homotopic_constant_maps path_connected_space_imp_path_component_of
1.1461 +      by (metis (full_types) X a continuous_map_const contractible_imp_path_connected_space homotopic_with_imp_continuous_maps that)
1.1462 +  qed
1.1463 +next
1.1464 +  assume R: ?rhs
1.1465 +  then show ?lhs
1.1466 +    apply (simp add: contractible_space_def)
1.1467 +    by (metis equals0I homotopic_on_emptyI)
1.1468 +qed
1.1469 +
1.1470 +
1.1471 +lemma compose_const [simp]: "f \<circ> (\<lambda>x. a) = (\<lambda>x. f a)" "(\<lambda>x. a) \<circ> g = (\<lambda>x. a)"
1.1472 +  by (simp_all add: o_def)
1.1473 +
1.1474 +lemma nullhomotopic_through_contractible_space:
1.1475 +  assumes f: "continuous_map X Y f" and g: "continuous_map Y Z g" and Y: "contractible_space Y"
1.1476 +  obtains c where "homotopic_with (\<lambda>h. True) X Z (g \<circ> f) (\<lambda>x. c)"
1.1477 +proof -
1.1478 +  obtain b where b: "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. b)"
1.1479 +    using Y by (auto simp: contractible_space_def)
1.1480 +  show thesis
1.1481 +    using homotopic_compose_continuous_map_right
1.1482 +           [OF homotopic_compose_continuous_map_left [OF b g] f]
1.1483 +    by (simp add: that)
1.1484  qed
1.1485
1.1486 +lemma nullhomotopic_into_contractible_space:
1.1487 +  assumes f: "continuous_map X Y f" and Y: "contractible_space Y"
1.1488 +  obtains c where "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
1.1489 +  using nullhomotopic_through_contractible_space [OF f _ Y]
1.1490 +  by (metis continuous_map_id id_comp)
1.1491 +
1.1492 +lemma nullhomotopic_from_contractible_space:
1.1493 +  assumes f: "continuous_map X Y f" and X: "contractible_space X"
1.1494 +  obtains c where "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
1.1495 +  using nullhomotopic_through_contractible_space [OF _ f X]
1.1496 +  by (metis comp_id continuous_map_id)
1.1497 +
1.1498 +lemma homotopy_dominated_contractibility:
1.1499 +  assumes f: "continuous_map X Y f" and g: "continuous_map Y X g"
1.1500 +    and hom: "homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) id" and X: "contractible_space X"
1.1501 +  shows "contractible_space Y"
1.1502 +proof -
1.1503 +  obtain c where c: "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
1.1504 +    using nullhomotopic_from_contractible_space [OF f X] .
1.1505 +  have "homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) (\<lambda>x. c)"
1.1506 +    using homotopic_compose_continuous_map_right [OF c g] by fastforce
1.1507 +  then have "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. c)"
1.1508 +    using homotopic_with_trans [OF _ hom] homotopic_with_symD by blast
1.1509 +  then show ?thesis
1.1510 +    unfolding contractible_space_def ..
1.1511 +qed
1.1512 +
1.1513 +lemma homotopy_equivalent_space_contractibility:
1.1514 +   "X homotopy_equivalent_space Y \<Longrightarrow> (contractible_space X \<longleftrightarrow> contractible_space Y)"
1.1515 +  unfolding homotopy_equivalent_space_def
1.1516 +  by (blast intro: homotopy_dominated_contractibility)
1.1517 +
1.1518 +lemma homeomorphic_space_contractibility:
1.1519 +   "X homeomorphic_space Y
1.1520 +        \<Longrightarrow> (contractible_space X \<longleftrightarrow> contractible_space Y)"
1.1521 +  by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)
1.1522 +
1.1523 +lemma contractible_eq_homotopy_equivalent_singleton_subtopology:
1.1524 +   "contractible_space X \<longleftrightarrow>
1.1525 +        topspace X = {} \<or> (\<exists>a \<in> topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is "?lhs = ?rhs")
1.1526 +proof (cases "topspace X = {}")
1.1527 +  case False
1.1528 +  show ?thesis
1.1529 +  proof
1.1530 +    assume ?lhs
1.1531 +    then obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
1.1532 +      by (auto simp: contractible_space_def)
1.1533 +    then have "a \<in> topspace X"
1.1534 +      by (metis False continuous_map_const homotopic_with_imp_continuous_maps)
1.1535 +    then have "X homotopy_equivalent_space subtopology X {a}"
1.1536 +      unfolding homotopy_equivalent_space_def
1.1537 +      apply (rule_tac x="\<lambda>x. a" in exI)
1.1538 +      apply (rule_tac x=id in exI)
1.1539 +      apply (auto simp: homotopic_with_sym topspace_subtopology_subset a)
1.1540 +      using connectedin_absolute connectedin_sing contractible_space_alt contractible_space_subtopology_singleton by fastforce
1.1541 +    with \<open>a \<in> topspace X\<close> show ?rhs
1.1542 +      by blast
1.1543 +  next
1.1544 +    assume ?rhs
1.1545 +    then show ?lhs
1.1546 +      by (meson False contractible_space_subtopology_singleton homotopy_equivalent_space_contractibility)
1.1547 +  qed
1.1549 +
1.1550 +lemma contractible_space_retraction_map_image:
1.1551 +  assumes "retraction_map X Y f" and X: "contractible_space X"
1.1552 +  shows "contractible_space Y"
1.1553 +proof -
1.1554 +  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"
1.1555 +    using assms by (auto simp: retraction_map_def retraction_maps_def)
1.1556 +  obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
1.1557 +    using X by (auto simp: contractible_space_def)
1.1558 +  have "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. f a)"
1.1559 +  proof (rule homotopic_with_eq)
1.1560 +    show "homotopic_with (\<lambda>x. True) Y Y (f \<circ> id \<circ> g) (f \<circ> (\<lambda>x. a) \<circ> g)"
1.1561 +      using f g a homotopic_compose_continuous_map_left homotopic_compose_continuous_map_right by metis
1.1562 +  qed (use fg in auto)
1.1563 +  then show ?thesis
1.1564 +    unfolding contractible_space_def by blast
1.1565 +qed
1.1566 +
1.1567 +lemma contractible_space_prod_topology:
1.1568 +   "contractible_space(prod_topology X Y) \<longleftrightarrow>
1.1569 +    topspace X = {} \<or> topspace Y = {} \<or> contractible_space X \<and> contractible_space Y"
1.1570 +proof (cases "topspace X = {} \<or> topspace Y = {}")
1.1571 +  case True
1.1572 +  then have "topspace (prod_topology X Y) = {}"
1.1573 +    by simp
1.1574 +  then show ?thesis
1.1575 +    by (auto simp: contractible_space_empty)
1.1576 +next
1.1577 +  case False
1.1578 +  have "contractible_space(prod_topology X Y) \<longleftrightarrow> contractible_space X \<and> contractible_space Y"
1.1579 +  proof safe
1.1580 +    assume XY: "contractible_space (prod_topology X Y)"
1.1581 +    with False have "retraction_map (prod_topology X Y) X fst"
1.1582 +      by (auto simp: contractible_space False retraction_map_fst)
1.1583 +    then show "contractible_space X"
1.1584 +      by (rule contractible_space_retraction_map_image [OF _ XY])
1.1585 +    have "retraction_map (prod_topology X Y) Y snd"
1.1586 +      using False XY  by (auto simp: contractible_space False retraction_map_snd)
1.1587 +    then show "contractible_space Y"
1.1588 +      by (rule contractible_space_retraction_map_image [OF _ XY])
1.1589 +  next
1.1590 +    assume "contractible_space X" and "contractible_space Y"
1.1591 +    with False obtain a b
1.1592 +      where "a \<in> topspace X" and a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
1.1593 +        and "b \<in> topspace Y" and b: "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. b)"
1.1594 +      by (auto simp: contractible_space)
1.1595 +    with False show "contractible_space (prod_topology X Y)"
1.1596 +      apply (simp add: contractible_space)
1.1597 +      apply (rule_tac x=a in bexI)
1.1598 +       apply (rule_tac x=b in bexI)
1.1599 +      using homotopic_with_prod_topology [OF a b]
1.1600 +    	  apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff)
1.1601 +    	 apply auto
1.1602 +    	done
1.1603 +  qed
1.1604 +  with False show ?thesis
1.1605 +    by auto
1.1606 +qed
1.1607 +
1.1608 +
1.1609 +
1.1610 +
1.1611 +lemma contractible_space_product_topology:
1.1612 +  "contractible_space(product_topology X I) \<longleftrightarrow>
1.1613 +    topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. contractible_space(X i))"
1.1614 +proof (cases "topspace (product_topology X I) = {}")
1.1615 +  case False
1.1616 +  have 1: "contractible_space (X i)"
1.1617 +    if XI: "contractible_space (product_topology X I)" and "i \<in> I"
1.1618 +    for i
1.1619 +  proof (rule contractible_space_retraction_map_image [OF _ XI])
1.1620 +    show "retraction_map (product_topology X I) (X i) (\<lambda>x. x i)"
1.1621 +      using False by (simp add: retraction_map_product_projection \<open>i \<in> I\<close>)
1.1622 +  qed
1.1623 +  have 2: "contractible_space (product_topology X I)"
1.1624 +    if "x \<in> topspace (product_topology X I)" and cs: "\<forall>i\<in>I. contractible_space (X i)"
1.1625 +    for x :: "'a \<Rightarrow> 'b"
1.1626 +  proof -
1.1627 +    obtain f where f: "\<And>i. i\<in>I \<Longrightarrow> homotopic_with (\<lambda>x. True) (X i) (X i) id (\<lambda>x. f i)"
1.1628 +      using cs unfolding contractible_space_def by metis
1.1629 +    have "homotopic_with (\<lambda>x. True)
1.1630 +                         (product_topology X I) (product_topology X I) id (\<lambda>x. restrict f I)"
1.1631 +      by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto simp: topspace_product_topology)
1.1632 +    then show ?thesis
1.1633 +      by (auto simp: contractible_space_def)
1.1634 +  qed
1.1635 +  show ?thesis
1.1636 +    using False 1 2 by blast
1.1638 +
1.1639 +
1.1640 +lemma contractible_space_subtopology_euclideanreal [simp]:
1.1641 +  "contractible_space(subtopology euclideanreal S) \<longleftrightarrow> is_interval S"
1.1642 +  (is "?lhs = ?rhs")
1.1643 +proof
1.1644 +  assume ?lhs
1.1645 +  then have "path_connectedin (subtopology euclideanreal S) S"
1.1646 +    using contractible_imp_path_connected_space path_connectedin_topspace path_connectedin_absolute
1.1647 +    by (simp add: contractible_imp_path_connected)
1.1648 +  then show ?rhs
1.1649 +    by (simp add: is_interval_path_connected_1)
1.1650 +next
1.1651 +  assume ?rhs
1.1652 +  then have "convex S"
1.1653 +    by (simp add: is_interval_convex_1)
1.1654 +  show ?lhs
1.1655 +  proof (cases "S = {}")
1.1656 +    case False
1.1657 +    then obtain z where "z \<in> S"
1.1658 +      by blast
1.1659 +    show ?thesis
1.1660 +      unfolding contractible_space_def homotopic_with_def
1.1661 +    proof (intro exI conjI allI)
1.1662 +      show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set S)) (top_of_set S)
1.1663 +                           (\<lambda>(t,x). (1 - t) * x + t * z)"
1.1664 +        apply (auto simp: case_prod_unfold)
1.1665 +         apply (intro continuous_intros)
1.1666 +        using  \<open>z \<in> S\<close> apply (auto intro: convexD [OF \<open>convex S\<close>, simplified])
1.1667 +        done
1.1668 +    qed auto
1.1669 +  qed (simp add: contractible_space_empty)
1.1670 +qed
1.1671 +
1.1672 +
1.1673 +corollary contractible_space_euclideanreal: "contractible_space euclideanreal"
1.1674 +proof -
1.1675 +  have "contractible_space (subtopology euclideanreal UNIV)"
1.1676 +    using contractible_space_subtopology_euclideanreal by blast
1.1677 +  then show ?thesis
1.1678 +    by simp
1.1679 +qed
1.1680 +
1.1681 +
1.1682 +abbreviation%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
1.1683 +             (infix "homotopy'_eqv" 50)
1.1684 +  where "S homotopy_eqv T \<equiv> top_of_set S homotopy_equivalent_space top_of_set T"
1.1685 +
1.1686 +
1.1687 +
1.1688 +
1.1689 +
1.1690 +lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
1.1691 +  unfolding homeomorphic_def homeomorphism_def homotopy_equivalent_space_def
1.1692 +  apply (erule ex_forward)+
1.1693 +  apply auto
1.1694 +   apply (metis homotopic_with_id2 topspace_euclidean_subtopology)
1.1695 +  by (metis (full_types) homotopic_with_id2 imageE topspace_euclidean_subtopology)
1.1696 +
1.1697 +
1.1698  lemma homotopy_eqv_inj_linear_image:
1.1699    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.1700    assumes "linear f" "inj f"
1.1701 @@ -3436,33 +3935,33 @@
1.1702        and g: "continuous_on U g" "g ` U \<subseteq> T"
1.1703        and homUS: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
1.1704                           continuous_on U g; g ` U \<subseteq> S\<rbrakk>
1.1705 -                         \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
1.1706 -    shows "homotopic_with (\<lambda>x. True) U T f g"
1.1707 +                         \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g"
1.1708 +    shows "homotopic_with_canon (\<lambda>x. True) U T f g"
1.1709  proof -
1.1710    obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
1.1711                 and k: "continuous_on T k" "k ` T \<subseteq> S"
1.1712 -               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
1.1713 -                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
1.1714 -    using assms by (auto simp: homotopy_eqv_def)
1.1715 -  have "homotopic_with (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
1.1716 +               and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
1.1717 +                        "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
1.1718 +    using assms by (auto simp: homotopy_equivalent_space_def)
1.1719 +  have "homotopic_with_canon (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
1.1720      apply (rule homUS)
1.1721      using f g k
1.1722      apply (safe intro!: continuous_on_compose h k f elim!: continuous_on_subset)
1.1723      apply (force simp: o_def)+
1.1724      done
1.1725 -  then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
1.1726 +  then have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
1.1727      apply (rule homotopic_with_compose_continuous_left)
1.1729      done
1.1730 -  moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
1.1731 +  moreover have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
1.1732      apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
1.1733      apply (auto simp: hom f)
1.1734      done
1.1735 -  moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
1.1736 +  moreover have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
1.1737      apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
1.1738      apply (auto simp: hom g)
1.1739      done
1.1740 -  ultimately show "homotopic_with (\<lambda>x. True) U T f g"
1.1741 +  ultimately show "homotopic_with_canon (\<lambda>x. True) U T f g"
1.1743      using homotopic_with_trans homotopic_with_sym by blast
1.1744  qed
1.1745 @@ -3474,13 +3973,24 @@
1.1746    assumes "S homotopy_eqv T"
1.1747      shows "(\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> S \<and>
1.1748                     continuous_on U g \<and> g ` U \<subseteq> S
1.1749 -                   \<longrightarrow> homotopic_with (\<lambda>x. True) U S f g) \<longleftrightarrow>
1.1750 +                   \<longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g) \<longleftrightarrow>
1.1751             (\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> T \<and>
1.1752                    continuous_on U g \<and> g ` U \<subseteq> T
1.1753 -                  \<longrightarrow> homotopic_with (\<lambda>x. True) U T f g)"
1.1754 -apply (rule iffI)
1.1755 -apply (metis assms homotopy_eqv_homotopic_triviality_imp)
1.1756 -by (metis (no_types) assms homotopy_eqv_homotopic_triviality_imp homotopy_eqv_sym)
1.1757 +                  \<longrightarrow> homotopic_with_canon (\<lambda>x. True) U T f g)"
1.1758 +      (is "?lhs = ?rhs")
1.1759 +proof
1.1760 +  assume ?lhs
1.1761 +  then show ?rhs
1.1762 +    by (metis assms homotopy_eqv_homotopic_triviality_imp)
1.1763 +next
1.1764 +  assume ?rhs
1.1765 +  moreover
1.1766 +  have "T homotopy_eqv S"
1.1767 +    using assms homotopy_equivalent_space_sym by blast
1.1768 +  ultimately show ?lhs
1.1769 +    by (blast intro: homotopy_eqv_homotopic_triviality_imp)
1.1770 +qed
1.1771 +
1.1772
1.1773  lemma homotopy_eqv_cohomotopic_triviality_null_imp:
1.1774    fixes S :: "'a::real_normed_vector set"
1.1775 @@ -3489,23 +3999,23 @@
1.1776    assumes "S homotopy_eqv T"
1.1777        and f: "continuous_on T f" "f ` T \<subseteq> U"
1.1778        and homSU: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U\<rbrakk>
1.1779 -                      \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c)"
1.1780 -  obtains c where "homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)"
1.1781 +                      \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) S U f (\<lambda>x. c)"
1.1782 +  obtains c where "homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. c)"
1.1783  proof -
1.1784    obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
1.1785                 and k: "continuous_on T k" "k ` T \<subseteq> S"
1.1786 -               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
1.1787 -                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
1.1788 -    using assms by (auto simp: homotopy_eqv_def)
1.1789 -  obtain c where "homotopic_with (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
1.1790 +               and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
1.1791 +                        "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
1.1792 +    using assms by (auto simp: homotopy_equivalent_space_def)
1.1793 +  obtain c where "homotopic_with_canon (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
1.1794      apply (rule exE [OF homSU [of "f \<circ> h"]])
1.1795      apply (intro continuous_on_compose h)
1.1796      using h f  apply (force elim!: continuous_on_subset)+
1.1797      done
1.1798 -  then have "homotopic_with (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
1.1799 +  then have "homotopic_with_canon (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
1.1800      apply (rule homotopic_with_compose_continuous_right [where X=S])
1.1801      using k by auto
1.1802 -  moreover have "homotopic_with (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
1.1803 +  moreover have "homotopic_with_canon (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
1.1804      apply (rule homotopic_with_compose_continuous_left [where Y=T])
1.1805        apply (simp add: hom homotopic_with_symD)
1.1806       using f apply auto
1.1807 @@ -3522,12 +4032,12 @@
1.1808      and U :: "'c::real_normed_vector set"
1.1809    assumes "S homotopy_eqv T"
1.1810      shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> U
1.1811 -                \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow>
1.1812 +                \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow>
1.1813             (\<forall>f. continuous_on T f \<and> f ` T \<subseteq> U
1.1814 -                \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)))"
1.1815 +                \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. c)))"
1.1816  apply (rule iffI)
1.1817  apply (metis assms homotopy_eqv_cohomotopic_triviality_null_imp)
1.1818 -by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_eqv_sym)
1.1819 +by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_equivalent_space_sym)
1.1820
1.1821  lemma homotopy_eqv_homotopic_triviality_null_imp:
1.1822    fixes S :: "'a::real_normed_vector set"
1.1823 @@ -3536,23 +4046,23 @@
1.1824    assumes "S homotopy_eqv T"
1.1825        and f: "continuous_on U f" "f ` U \<subseteq> T"
1.1826        and homSU: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
1.1827 -                      \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
1.1828 -    shows "\<exists>c. homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
1.1829 +                      \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c)"
1.1830 +    shows "\<exists>c. homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)"
1.1831  proof -
1.1832    obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
1.1833                 and k: "continuous_on T k" "k ` T \<subseteq> S"
1.1834 -               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
1.1835 -                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
1.1836 -    using assms by (auto simp: homotopy_eqv_def)
1.1837 -  obtain c::'a where "homotopic_with (\<lambda>x. True) U S (k \<circ> f) (\<lambda>x. c)"
1.1838 +               and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
1.1839 +                        "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
1.1840 +    using assms by (auto simp: homotopy_equivalent_space_def)
1.1841 +  obtain c::'a where "homotopic_with_canon (\<lambda>x. True) U S (k \<circ> f) (\<lambda>x. c)"
1.1842      apply (rule exE [OF homSU [of "k \<circ> f"]])
1.1843      apply (intro continuous_on_compose h)
1.1844      using k f  apply (force elim!: continuous_on_subset)+
1.1845      done
1.1846 -  then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
1.1847 +  then have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
1.1848      apply (rule homotopic_with_compose_continuous_left [where Y=S])
1.1849      using h by auto
1.1850 -  moreover have "homotopic_with (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
1.1851 +  moreover have "homotopic_with_canon (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
1.1852      apply (rule homotopic_with_compose_continuous_right [where X=T])
1.1853        apply (simp add: hom homotopic_with_symD)
1.1854       using f apply auto
1.1855 @@ -3567,12 +4077,12 @@
1.1856      and U :: "'c::real_normed_vector set"
1.1857    assumes "S homotopy_eqv T"
1.1858      shows "(\<forall>f. continuous_on U f \<and> f ` U \<subseteq> S
1.1859 -                  \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c))) \<longleftrightarrow>
1.1860 +                  \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c))) \<longleftrightarrow>
1.1861             (\<forall>f. continuous_on U f \<and> f ` U \<subseteq> T
1.1862 -                  \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)))"
1.1863 +                  \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)))"
1.1864  apply (rule iffI)
1.1865  apply (metis assms homotopy_eqv_homotopic_triviality_null_imp)
1.1866 -by (metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_eqv_sym)
1.1867 +by (metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_equivalent_space_sym)
1.1868
1.1869  lemma homotopy_eqv_contractible_sets:
1.1870    fixes S :: "'a::real_normed_vector set"
1.1871 @@ -3587,7 +4097,7 @@
1.1872    with assms obtain a b where "a \<in> S" "b \<in> T"
1.1873      by auto
1.1874    then show ?thesis
1.1875 -    unfolding homotopy_eqv_def
1.1876 +    unfolding homotopy_equivalent_space_def
1.1877      apply (rule_tac x="\<lambda>x. b" in exI)
1.1878      apply (rule_tac x="\<lambda>x. a" in exI)
1.1879      apply (intro assms conjI continuous_on_id' homotopic_into_contractible)
1.1880 @@ -3598,20 +4108,19 @@
1.1881  lemma homotopy_eqv_empty1 [simp]:
1.1882    fixes S :: "'a::real_normed_vector set"
1.1883    shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}"
1.1884 -apply (rule iffI)
1.1885 -using homotopy_eqv_def apply fastforce
1.1887 +  apply (rule iffI)
1.1888 +   apply (metis Abstract_Topology.continuous_map_subtopology_eu emptyE equals0I homotopy_equivalent_space_def image_subset_iff)
1.1889 +  by (simp add: homotopy_eqv_contractible_sets)
1.1890
1.1891  lemma homotopy_eqv_empty2 [simp]:
1.1892    fixes S :: "'a::real_normed_vector set"
1.1893    shows "({}::'b::real_normed_vector set) homotopy_eqv S \<longleftrightarrow> S = {}"
1.1894 -by (metis homotopy_eqv_empty1 homotopy_eqv_sym)
1.1895 +  using homotopy_equivalent_space_sym homotopy_eqv_empty1 by blast
1.1896
1.1897  lemma homotopy_eqv_contractibility:
1.1898    fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
1.1899    shows "S homotopy_eqv T \<Longrightarrow> (contractible S \<longleftrightarrow> contractible T)"
1.1900 -unfolding homotopy_eqv_def
1.1901 -by (blast intro: homotopy_dominated_contractibility)
1.1902 +  by (meson contractible_space_top_of_set homotopy_equivalent_space_contractibility)
1.1903
1.1904  lemma homotopy_eqv_sing:
1.1905    fixes S :: "'a::real_normed_vector set" and a :: "'b::real_normed_vector"
1.1906 @@ -5034,11 +5543,15 @@
1.1907
1.1908  proposition nullhomotopic_from_sphere_extension:
1.1909    fixes f :: "'M::euclidean_space \<Rightarrow> 'a::real_normed_vector"
1.1910 -  shows  "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
1.1911 +  shows  "(\<exists>c. homotopic_with_canon (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
1.1912            (\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
1.1913                 (\<forall>x \<in> sphere a r. g x = f x))"
1.1914           (is "?lhs = ?rhs")
1.1915  proof (cases r "0::real" rule: linorder_cases)
1.1916 +  case less
1.1917 +  then show ?thesis
1.1918 +    by (simp add: homotopic_on_emptyI)
1.1919 +next
1.1920    case equal
1.1921    then show ?thesis
1.1922      apply (auto simp: homotopic_with)
1.1923 @@ -5051,9 +5564,11 @@
1.1924    have ?P if ?lhs using that
1.1925    proof
1.1926      fix c
1.1927 -    assume c: "homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)"
1.1928 -    then have contf: "continuous_on (sphere a r) f" and fim: "f ` sphere a r \<subseteq> S"
1.1929 -      by (auto simp: homotopic_with_imp_subset1 homotopic_with_imp_continuous)
1.1930 +    assume c: "homotopic_with_canon (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)"
1.1931 +    then have contf: "continuous_on (sphere a r) f"
1.1932 +      by (metis homotopic_with_imp_continuous)
1.1933 +    moreover have fim: "f ` sphere a r \<subseteq> S"
1.1934 +      by (meson continuous_map_subtopology_eu c homotopic_with_imp_continuous_maps)
1.1935      show ?P
1.1936        using contf fim by (auto simp: sphere_def dist_norm norm_minus_commute)
1.1937    qed
1.1938 @@ -5070,7 +5585,7 @@
1.1939    moreover have ?thesis if ?P
1.1940    proof
1.1941      assume ?lhs
1.1942 -    then obtain c where "homotopic_with (\<lambda>x. True) (sphere a r) S (\<lambda>x. c) f"
1.1943 +    then obtain c where "homotopic_with_canon (\<lambda>x. True) (sphere a r) S (\<lambda>x. c) f"
1.1944        using homotopic_with_sym by blast
1.1945      then obtain h where conth: "continuous_on ({0..1::real} \<times> sphere a r) h"
1.1946                      and him: "h ` ({0..1} \<times> sphere a r) \<subseteq> S"
1.1947 @@ -5159,6 +5674,6 @@
1.1948    qed
1.1949    ultimately
1.1950    show ?thesis by meson
1.1951 -qed simp
1.1952 +qed
1.1953
1.1954  end
1.1955 \ No newline at end of file
```