Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Analysis/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 277 kB image not shown  

Quelle  Homotopy.thy

  Sprache: Isabelle
 

(*  Title:      HOL/Analysis/Path_Connected.thy
  Authors: LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light
*)

section Homotopy of Maps

theory Homotopy
  imports Path_Connected Product_Topology Uncountable_Sets
begin

definition🍋tag important homotopic_with
where
 "homotopic_with P X Y f g
   (h. continuous_map (prod_topology (top_of_set {0..1::real}) X) Y h
       (x. h(0, x) = f x)
       (x. h(1, x) = g x)
       (t {0..1}. P(λx. h(t,x))))"

textp, q are functions X Y, and the property P restricts all intermediate maps.
 We often just want to require that P fixes some subset, but to include the case of a loop homotopy,
 it is convenient to have a general property P.

abbreviation homotopic_with_canon ::
  "[('a::topological_space ==> 'b::topological_space) ==> bool, 'a set, 'b set, 'a ==> 'b, 'a ==> 'b] ==> bool"
where
 "homotopic_with_canon P S T p q homotopic_with P (top_of_set S) (top_of_set T) p q"

lemma split_01: "{0..1::real} = {0..1/2} {1/2..1}"
  by force

lemma split_01_prod: "{0..1::real} × X = ({0..1/2} × X) ({1/2..1} × X)"
  by force

lemma image_Pair_const: "(λx. (x, c)) ` A = A × {c}"
  by auto

lemma fst_o_paired [simp]: "fst (λ(x,y). (f x y, g x y)) = (λ(x,y). f x y)"
  by auto

lemma snd_o_paired [simp]: "snd (λ(x,y). (f x y, g x y)) = (λ(x,y). g x y)"
  by auto

lemma continuous_on_o_Pair: "[continuous_on (T × X) h; t T] ==> continuous_on X (h Pair t)"
  by (fast intro: continuous_intros elim!: continuous_on_subset)

lemma continuous_map_o_Pair: 
  assumes h: "continuous_map (prod_topology X Y) Z h" and t: "t topspace X"
  shows "continuous_map Y Z (h Pair t)"
  by (intro continuous_map_compose [OF _ h] continuous_intros; simp add: t)

subsection🍋tag unimportant\<open>Trivial properties

text We often want to just localize the ending function equality or whatever.
text🍋tag important %whitespace
proposition homotopic_with:
  assumes "h k. (x. x topspace X ==> h x = k x) ==> (P h P k)"
  shows "homotopic_with P X Y p q
           (h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h
              (x topspace X. h(0,x) = p x)
              (x topspace X. h(1,x) = q x)
              (t {0..1}. P(λx. h(t, x))))"
  unfolding homotopic_with_def
  apply (rule iffI, blast, clarify)
  apply (rule_tac x="λ(u,v). if v topspace X then h(u,v) else if u = 0 then p v else q v" in exI)
  apply simp
  by (smt (verit, best) SigmaE assms case_prod_conv continuous_map_eq topspace_prod_topology)

lemma homotopic_with_mono:
  assumes hom: "homotopic_with P X Y f g"
    and Q: "h. [continuous_map X Y h; P h] ==> Q h"
  shows "homotopic_with Q X Y f g"
  using hom unfolding homotopic_with_def
  by (force simp: o_def dest: continuous_map_o_Pair intro: Q)

lemma homotopic_with_imp_continuous_maps:
    assumes "homotopic_with P X Y f g"
    shows "continuous_map X Y f continuous_map X Y g"
proof -
  obtain h :: "real × 'a ==> 'b"
    where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) Y h"
      and h: "x. h (0, x) = f x" "x. h (1, x) = g x"
    using assms by (auto simp: homotopic_with_def)
  have *: "t {0..1} ==> continuous_map X Y (h (λx. (t,x)))" for t
    by (rule continuous_map_compose [OF _ conth]) (simp add: o_def continuous_map_pairwise)
  show ?thesis
    using h *[of 0] *[of 1] by (simp add: continuous_map_eq)
qed

lemma homotopic_with_imp_continuous:
    assumes "homotopic_with_canon P X Y f g"
    shows "continuous_on X f continuous_on X g"
  by (meson assms continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)

lemma homotopic_with_imp_property:
  assumes "homotopic_with P X Y f g"
  shows "P f P g"
proof
  obtain h where h: "x. h(0, x) = f x" "x. h(1, x) = g x" and P: "t. t {0..1::real} ==> P(λx. h(t,x))"
    using assms by (force simp: homotopic_with_def)
  show "P f" "P g"
    using P [of 0] P [of 1] by (force simp: h)+
qed

lemma homotopic_with_equal:
  assumes "P f" "P g" and contf: "continuous_map X Y f" and fg: "x. x topspace X ==> f x = g x"
  shows "homotopic_with P X Y f g"
  unfolding homotopic_with_def
proof (intro exI conjI allI ballI)
  let ?h = "λ(t::real,x). if t = 1 then g x else f x"
  show "continuous_map (prod_topology (top_of_set {0..1}) X) Y ?h"
  proof (rule continuous_map_eq)
    show "continuous_map (prod_topology (top_of_set {0..1}) X) Y (f snd)"
      by (simp add: contf continuous_map_of_snd)
  qed (auto simp: fg)
  show "P (λx. ?h (t, x))" if "t {0..1}" for t
    by (cases "t = 1") (simp_all add: assms)
qed auto

lemma homotopic_with_imp_funspace1:
     "homotopic_with_canon P X Y f g ==> f X Y"
  using homotopic_with_imp_continuous_maps by fastforce

lemma homotopic_with_imp_subset1:
     "homotopic_with_canon P X Y f g ==> f ` X Y"
  using homotopic_with_imp_funspace1 by blast

lemma homotopic_with_imp_funspace2:
     "homotopic_with_canon P X Y f g ==> g X Y"
  using homotopic_with_imp_continuous_maps by force

lemma homotopic_with_imp_subset2:
     "homotopic_with_canon P X Y f g ==> g ` X Y"
  using homotopic_with_imp_funspace2 by blast

lemma homotopic_with_subset_left:
     "[homotopic_with_canon P X Y f g; Z X] ==> homotopic_with_canon P Z Y f g"
  unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward)

lemma homotopic_with_subset_right:
     "[homotopic_with_canon P X Y f g; Y Z] ==> homotopic_with_canon P X Z f g"
  unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward)

subsectionHomotopy with P is an equivalence relation

text (on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)

lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f continuous_map X Y f P f"
  by (metis homotopic_with_equal homotopic_with_imp_continuous_maps homotopic_with_imp_property)

lemma homotopic_with_symD:
    assumes "homotopic_with P X Y f g"
      shows "homotopic_with P X Y g f"
proof -
  let ?I01 = "subtopology euclideanreal {0..1}"
  let ?j = "λy. (1 - fst y, snd y)"
  have 1: "continuous_map (prod_topology ?I01 X) (prod_topology euclideanreal X) ?j"
    by (intro continuous_intros; simp add: continuous_map_subtopology_fst prod_topology_subtopology)
  have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j"
  proof -
    have "continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} × topspace X)) ?j"
      by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff flip: image_subset_iff_funcset)
    then show ?thesis
      by (simp add: prod_topology_subtopology(1))
  qed
  show ?thesis
    using assms
    apply (clarsimp simp: homotopic_with_def)
    subgoal for h
      by (rule_tac x="h (λy. (1 - fst y, snd y))" in exI) (simp add: continuous_map_compose [OF *])
    done
qed

lemma homotopic_with_sym:
   "homotopic_with P X Y f g homotopic_with P X Y g f"
  by (metis homotopic_with_symD)

proposition homotopic_with_trans:
    assumes "homotopic_with P X Y f g"  "homotopic_with P X Y g h"
    shows "homotopic_with P X Y f h"
proof -
  let ?X01 = "prod_topology (subtopology euclideanreal {0..1}) X"
  obtain k1 k2
    where contk1: "continuous_map ?X01 Y k1" and contk2: "continuous_map ?X01 Y k2"
      and k12: "x. k1 (1, x) = g x" "x. k2 (0, x) = g x"
      "x. k1 (0, x) = f x" "x. k2 (1, x) = h x"
      and P:   "t{0..1}. P (λx. k1 (t, x))" "t{0..1}. P (λx. k2 (t, x))"
    using assms by (auto simp: homotopic_with_def)
  define k where "k λy. if fst y 1/2
                             then (k1 (λx. (2 *🪙R fst x, snd x))) y
                             else (k2 (λx. (2 *🪙R fst x -1, snd x))) y"
  have keq: "k1 (2 * u, v) = k2 (2 * u -1, v)" if "u = 1/2"  for u v
    by (simp add: k12 that)
  show ?thesis
    unfolding homotopic_with_def
  proof (intro exI conjI)
    show "continuous_map ?X01 Y k"
      unfolding k_def
    proof (rule continuous_map_cases_le)
      show fst: "continuous_map ?X01 euclideanreal fst"
        using continuous_map_fst continuous_map_in_subtopology by blast
      show "continuous_map ?X01 euclideanreal (λx. 1/2)"
        by simp
      show "continuous_map (subtopology ?X01 {y topspace ?X01. fst y 1/2}) Y
               (k1 (λx. (2 *🪙R fst x, snd x)))"
        apply (intro fst continuous_map_compose [OF _ contk1] continuous_intros continuous_map_into_subtopology continuous_map_from_subtopology | simp)+
        by (force simp: prod_topology_subtopology)
      show "continuous_map (subtopology ?X01 {y topspace ?X01. 1/2 fst y}) Y
               (k2 (λx. (2 *🪙R fst x -1, snd x)))"
        apply (intro fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology continuous_map_from_subtopology | simp)+
        by (force simp: prod_topology_subtopology)
      show "(k1 (λx. (2 *🪙R fst x, snd x))) y = (k2 (λx. (2 *🪙R fst x -1, snd x))) y"
        if "y topspace ?X01" and "fst y = 1/2" for y
        using that by (simp add: keq)
    qed
    show "x. k (0, x) = f x"
      by (simp add: k12 k_def)
    show "x. k (1, x) = h x"
      by (simp add: k12 k_def)
    show "t{0..1}. P (λx. k (t, x))"
    proof 
      fix t show "t{0..1} ==> P (λx. k (t, x))"
        by (cases "t 1/2") (auto simp: k_def P)
    qed
  qed
qed

lemma homotopic_with_id2: 
  "(x. x topspace X ==> g (f x) = x) ==> homotopic_with (λx. True) X X (g f) id"
  by (metis comp_apply continuous_map_id eq_id_iff homotopic_with_equal homotopic_with_symD)

subsectionContinuity lemmas

lemma homotopic_with_compose_continuous_map_left:
  "[homotopic_with p X1 X2 f g; continuous_map X2 X3 h; j. p j ==> q(h j)]
   ==> homotopic_with q X1 X3 (h f) (h g)"
  unfolding homotopic_with_def
  apply clarify
  subgoal for k
    by (rule_tac x="h k" in exI) (rule conjI continuous_map_compose | simp add: o_def)+
  done

lemma homotopic_with_compose_continuous_map_right:
  assumes hom: "homotopic_with p X2 X3 f g" and conth: "continuous_map X1 X2 h"
    and q: "j. p j ==> q(j h)"
  shows "homotopic_with q X1 X3 (f h) (g h)"
proof -
  obtain k
    where contk: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) X3 k"
      and k: "x. k (0, x) = f x" "x. k (1, x) = g x" and p: "t. t{0..1} ==> p (λx. k (t, x))"
    using hom unfolding homotopic_with_def by blast
  have hsnd: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X2 (h snd)"
    by (rule continuous_map_compose [OF continuous_map_snd conth])
  let ?h = "k (λ(t,x). (t,h x))"
  show ?thesis
    unfolding homotopic_with_def
  proof (intro exI conjI allI ballI)
    have "continuous_map (prod_topology (top_of_set {0..1}) X1)
     (prod_topology (top_of_set {0..1::real}) X2) (λ(t, x). (t, h x))"
      by (metis (mono_tags, lifting) case_prod_beta' comp_def continuous_map_eq continuous_map_fst continuous_map_pairedI hsnd)
    then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X3 ?h"
      by (intro conjI continuous_map_compose [OF _ contk])
    show "q (λx. ?h (t, x))" if "t {0..1}" for t
      using q [OF p [OF that]] by (simp add: o_def)
  qed (auto simp: k)
qed

corollary homotopic_compose:
  assumes "homotopic_with (λx. True) X Y f f'" "homotopic_with (λx. True) Y Z g g'"
  shows "homotopic_with (λx. True) X Z (g f) (g' f')"
  by (metis assms homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps homotopic_with_trans)

proposition homotopic_with_compose_continuous_right:
    "[homotopic_with_canon (λf. p (f h)) X Y f g; continuous_on W h; h W X]
     ==> homotopic_with_canon p W Y (f h) (g h)"
  by (simp add: homotopic_with_compose_continuous_map_right image_subset_iff_funcset)

proposition homotopic_with_compose_continuous_left:
     "[homotopic_with_canon (λf. p (h f)) X Y f g; continuous_on Y h; h Y Z]
      ==> homotopic_with_canon p X Z (h f) (h g)"
  by (simp add: homotopic_with_compose_continuous_map_left image_subset_iff_funcset)

lemma homotopic_from_subtopology:
   "homotopic_with P X X' f g ==> homotopic_with P (subtopology X S) X' f g"
  by (metis continuous_map_id_subt homotopic_with_compose_continuous_map_right o_id)

lemma homotopic_on_emptyI:
  assumes "P f" "P g"
  shows "homotopic_with P trivial_topology X f g"
  by (metis assms continuous_map_on_empty empty_iff homotopic_with_equal topspace_discrete_topology)

lemma homotopic_on_empty:
   "(homotopic_with P trivial_topology X f g P f P g)"
  using homotopic_on_emptyI homotopic_with_imp_property by metis

lemma homotopic_with_canon_on_empty: "homotopic_with_canon (λx. True) {} t f g"
  by (auto intro: homotopic_with_equal)

lemma homotopic_constant_maps:
   "homotopic_with (λx. True) X X' (λx. a) (λx. b)
    X = trivial_topology path_component_of X' a b" (is "?lhs = ?rhs")
proof (cases "X = trivial_topology")
  case False
  then obtain c where c: "c topspace X"
    by fastforce
  have "g. continuous_map (top_of_set {0..1::real}) X' g g 0 = a g 1 = b"
    if "x topspace X" and hom: "homotopic_with (λx. True) X X' (λx. a) (λx. b)" for x
  proof -
    obtain h :: "real × 'a ==> 'b"
      where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X' h"
        and h: "x. h (0, x) = a" "x. h (1, x) = b"
      using hom by (auto simp: homotopic_with_def)
    have cont: "continuous_map (top_of_set {0..1}) X' (h (λt. (t, c)))"
      by (rule continuous_map_compose [OF _ conth] continuous_intros | simp add: c)+
    then show ?thesis
      by (force simp: h)
  qed
  moreover have "homotopic_with (λx. True) X X' (λx. g 0) (λx. g 1)"
    if "x topspace X" "a = g 0" "b = g 1" "continuous_map (top_of_set {0..1}) X' g"
    for x and g :: "real ==> 'b"
    unfolding homotopic_with_def
    by (force intro!: continuous_map_compose continuous_intros c that)
  ultimately show ?thesis
    using False
    by (metis c path_component_of_set pathin_def)
qed (simp add: homotopic_on_empty)

proposition homotopic_with_eq:
   assumes h: "homotopic_with P X Y f g"
       and f': "x. x topspace X ==> f' x = f x"
       and g': "x. x topspace X ==> g' x = g x"
       and P:  "(h k. (x. x topspace X ==> h x = k x) ==> P h P k)"
   shows "homotopic_with P X Y f' g'"
  by (smt (verit, ccfv_SIG) assms homotopic_with)

lemma homotopic_with_prod_topology:
  assumes "homotopic_with p X1 Y1 f f'" and "homotopic_with q X2 Y2 g g'"
    and r: "i j. [p i; q j] ==> r(λ(x,y). (i x, j y))"
  shows "homotopic_with r (prod_topology X1 X2) (prod_topology Y1 Y2)
                          (λz. (f(fst z),g(snd z))) (λz. (f'(fst z), g'(snd z)))"
proof -
  obtain h
    where h: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) Y1 h"
      and h0: "x. h (0, x) = f x"
      and h1: "x. h (1, x) = f' x"
      and p: "t. [0 t; t 1] ==> p (λx. h (t,x))"
    using assms unfolding homotopic_with_def by auto
  obtain k
    where k: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) Y2 k"
      and k0: "x. k (0, x) = g x"
      and k1: "x. k (1, x) = g' x"
      and q: "t. [0 t; t 1] ==> q (λx. k (t,x))"
    using assms unfolding homotopic_with_def by auto
  let ?hk = "λ(t,x,y). (h(t,x), k(t,y))"
  show ?thesis
    unfolding homotopic_with_def
  proof (intro conjI allI exI)
    show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (prod_topology X1 X2))
                         (prod_topology Y1 Y2) ?hk"
      unfolding continuous_map_pairwise case_prod_unfold
      by (rule conjI continuous_map_pairedI continuous_intros continuous_map_id [unfolded id_def]
          continuous_map_fst_of [unfolded o_def] continuous_map_snd_of [unfolded o_def]
          continuous_map_compose [OF _ h, unfolded o_def]
          continuous_map_compose [OF _ k, unfolded o_def])+
  next
    fix x
    show "?hk (0, x) = (f (fst x), g (snd x))" "?hk (1, x) = (f' (fst x), g' (snd x))"
      by (auto simp: case_prod_beta h0 k0 h1 k1)
  qed (auto simp: p q r)
qed


lemma homotopic_with_product_topology:
  assumes ht: "i. i I ==> homotopic_with (p i) (X i) (Y i) (f i) (g i)"
    and pq: "h. (i. i I ==> p i (h i)) ==> q(λx. (λiI. h i (x i)))"
  shows "homotopic_with q (product_topology X I) (product_topology Y I)
                          (λz. (λiI. (f i) (z i))) (λz. (λiI. (g i) (z i)))"
proof -
  obtain h
    where h: "i. i I ==> continuous_map (prod_topology (subtopology euclideanreal {0..1}) (X i)) (Y i) (h i)"
      and h0: "i x. i I ==> h i (0, x) = f i x"
      and h1: "i x. i I ==> h i (1, x) = g i x"
      and p: "i t. [i I; t {0..1}] ==> p i (λx. h i (t,x))"
    using ht unfolding homotopic_with_def by metis
  show ?thesis
    unfolding homotopic_with_def
  proof (intro conjI allI exI)
    let ?h = "λ(t,z). λiI. h i (t,z i)"
    have "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
                         (Y i) (λx. h i (fst x, snd x i))" if "i I" for i
    proof -
      have 🍋"continuous_map (prod_topology (top_of_set {0..1}) (product_topology X I)) (X i) (λx. snd x i)"
        using continuous_map_componentwise continuous_map_snd that by fastforce
      show ?thesis
        unfolding continuous_map_pairwise case_prod_unfold
        by (intro conjI that 🍋 continuous_intros continuous_map_compose [OF _ h, unfolded o_def])
    qed
    then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
         (product_topology Y I) ?h"
      by (auto simp: continuous_map_componentwise case_prod_beta)
    show "?h (0, x) = (λiI. f i (x i))" "?h (1, x) = (λiI. g i (x i))" for x
      by (auto simp: case_prod_beta h0 h1)
    show "t{0..1}. q (λx. ?h (t, x))"
      by (force intro: p pq)
  qed
qed

textHomotopic triviality implicitly incorporates path-connectedness.
lemma homotopic_triviality:
  shows  "(f g. continuous_on S f f S T
                 continuous_on S g g S T
                  homotopic_with_canon (λx. True) S T f g)
          (S = {} path_connected T)
          (f. continuous_on S f f S T (c. homotopic_with_canon (λx. True) S T f (λx. c)))"
          (is "?lhs = ?rhs")
proof (cases "S = {} T = {}")
  case True then show ?thesis
    by (auto simp: homotopic_on_emptyI simp flip: image_subset_iff_funcset)
next
  case False show ?thesis
  proof
    assume LHS [rule_format]: ?lhs
    have pab: "path_component T a b" if "a T" "b T" for a b
    proof -
      have "homotopic_with_canon (λx. True) S T (λx. a) (λx. b)"
        by (simp add: LHS image_subset_iff that)
      then show ?thesis
        using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b]
        by (metis path_component_of_canon_iff topspace_discrete_topology topspace_euclidean_subtopology)
    qed
    moreover
    have "c. homotopic_with_canon (λx. True) S T f (λx. c)" if "continuous_on S f" "f S T" for f
      using False LHS continuous_on_const that by blast
    ultimately show ?rhs
      by (simp add: path_connected_component)
  next
    assume RHS: ?rhs
    with False have T: "path_connected T"
      by blast
    show ?lhs
    proof clarify
      fix f g
      assume "continuous_on S f" "f S T" "continuous_on S g" "g S T"
      obtain c d where c: "homotopic_with_canon (λx. True) S T f (λx. c)" and d: "homotopic_with_canon (λx. True) S T g (λx. d)"
        using RHS continuous_on S f continuous_on S g f S T g S T by presburger
      with T have "path_component T c d"
        by (metis False ex_in_conv homotopic_with_imp_subset2 image_subset_iff path_connected_component)
      then have "homotopic_with_canon (λx. True) S T (λx. c) (λx. d)"
        by (simp add: homotopic_constant_maps)
      with c d show "homotopic_with_canon (λx. True) S T f g"
        by (meson homotopic_with_symD homotopic_with_trans)
    qed
  qed
qed


subsectionHomotopy of paths, maintaining the same endpoints


definition🍋tag important homotopic_paths :: "['a set, real ==> 'a, real ==> 'a::topological_space] ==> bool"
  where
     "homotopic_paths S p q
       homotopic_with_canon (λr. pathstart r = pathstart p pathfinish r = pathfinish p) {0..1} S p q"

lemma homotopic_paths:
   "homotopic_paths S p q
      (h. continuous_on ({0..1} × {0..1}) h
          h ({0..1} × {0..1}) S
          (x {0..1}. h(0,x) = p x)
          (x {0..1}. h(1,x) = q x)
          (t {0..1::real}. pathstart(h Pair t) = pathstart p
                        pathfinish(h Pair t) = pathfinish p))"
  by (auto simp: homotopic_paths_def homotopic_with pathstart_def pathfinish_def)

proposition homotopic_paths_imp_pathstart:
     "homotopic_paths S p q ==> pathstart p = pathstart q"
  by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property)

proposition homotopic_paths_imp_pathfinish:
     "homotopic_paths S p q ==> pathfinish p = pathfinish q"
  by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property)

lemma homotopic_paths_imp_path:
     "homotopic_paths S p q ==> path p path q"
  using homotopic_paths_def homotopic_with_imp_continuous_maps path_def continuous_map_subtopology_eu by blast

lemma homotopic_paths_imp_subset:
     "homotopic_paths S p q ==> path_image p S path_image q S"
  by (simp add: homotopic_paths_def homotopic_with_imp_subset1 homotopic_with_imp_subset2
      path_image_def)

proposition homotopic_paths_refl [simp]: "homotopic_paths S p p path p path_image p S"
  by (auto simp add: homotopic_paths_def path_def path_image_def)

proposition homotopic_paths_sym: "homotopic_paths S p q ==> homotopic_paths S q p"
  by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)

proposition homotopic_paths_sym_eq: "homotopic_paths S p q homotopic_paths S q p"
  by (metis homotopic_paths_sym)

proposition homotopic_paths_trans [trans]:
  assumes "homotopic_paths S p q" "homotopic_paths S q r"
  shows "homotopic_paths S p r"
  using assms homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart unfolding homotopic_paths_def
  by (smt (verit, ccfv_SIG) homotopic_with_mono homotopic_with_trans)

proposition homotopic_paths_eq:
     "[path p; path_image p S; t. t {0..1} ==> p t = q t] ==> homotopic_paths S p q"
  by (smt (verit, best) homotopic_paths homotopic_paths_refl)

proposition homotopic_paths_reparametrize:
  assumes "path p"
      and pips: "path_image p S"
      and contf: "continuous_on {0..1} f"
      and f01 :"f {0..1} {0..1}"
      and [simp]: "f(0) = 0" "f(1) = 1"
      and q: "t. t {0..1} ==> q(t) = p(f t)"
    shows "homotopic_paths S p q"
proof -
  have contp: "continuous_on {0..1} p"
    by (metis path p path_def)
  then have "continuous_on {0..1} (p f)"
    by (meson assms(4) contf continuous_on_compose continuous_on_subset image_subset_iff_funcset)
  then have "path q"
    by (simp add: path_def) (metis q continuous_on_cong)
  have piqs: "path_image q S"
    by (smt (verit, ccfv_threshold) Pi_iff assms(2) assms(4) assms(7) image_subset_iff path_defs(4))
  have fb0: "a b. [0 a; a 1; 0 b; b 1] ==> 0 (1 - a) * f b + a * b"
    using f01 by force
  have fb1: "[0 a; a 1; 0 b; b 1] ==> (1 - a) * f b + a * b 1" for a b
    by (intro convex_bound_le) (use f01 in auto)
  have "homotopic_paths S q p"
  proof (rule homotopic_paths_trans)
    show "homotopic_paths S q (p f)"
      using q by (force intro: homotopic_paths_eq [OF  path q piqs])
  next
    show "homotopic_paths S (p f) p"
      using pips [unfolded path_image_def]
      apply (simp add: homotopic_paths_def homotopic_with_def)
      apply (rule_tac x="p (λy. (1 - (fst y)) *🪙R ((f snd) y) + (fst y) *🪙R snd y)"  in exI)
      apply (rule conjI contf continuous_intros continuous_on_subset [OF contp] | simp)+
      by (auto simp: fb0 fb1 pathstart_def pathfinish_def)
  qed
  then show ?thesis
    by (simp add: homotopic_paths_sym)
qed

lemma homotopic_paths_subset: "[homotopic_paths S p q; S t] ==> homotopic_paths t p q"
  unfolding homotopic_paths by fast


text A slightly ad-hoc but useful lemma in constructing homotopies.
lemma continuous_on_homotopic_join_lemma:
  fixes q :: "[real,real] ==> 'a::topological_space"
  assumes p: "continuous_on ({0..1} × {0..1}) (λy. p (fst y) (snd y))" (is "continuous_on ?A ?p")
      and q: "continuous_on ({0..1} × {0..1}) (λy. q (fst y) (snd y))" (is "continuous_on ?A ?q")
      and pf: "t. t {0..1} ==> pathfinish(p t) = pathstart(q t)"
    shows "continuous_on ({0..1} × {0..1}) (λy. (p(fst y) +++ q(fst y)) (snd y))"
proof -
  have 🍋"(λt. p (fst t) (2 * snd t)) = ?p (λy. (fst y, 2 * snd y))"
          "(λt. q (fst t) (2 * snd t - 1)) = ?q (λy. (fst y, 2 * snd y - 1))"
    by force+
  show ?thesis
    unfolding joinpaths_def
  proof (rule continuous_on_cases_le)
    show "continuous_on {y ?A. snd y 1/2} (λt. p (fst t) (2 * snd t))" 
         "continuous_on {y ?A. 1/2 snd y} (λt. q (fst t) (2 * snd t - 1))"
         "continuous_on ?A snd"
      unfolding 🍋
      by (rule continuous_intros continuous_on_subset [OF p] continuous_on_subset [OF q] | force)+
  qed (use pf in auto simp: mult.commute pathstart_def pathfinish_def)
qed

text Congruence properties of homotopy w.r.t. path-combining operations.

lemma homotopic_paths_reversepath_D:
      assumes "homotopic_paths S p q"
      shows   "homotopic_paths S (reversepath p) (reversepath q)"
  using assms
  apply (simp add: homotopic_paths_def homotopic_with_def, clarify)
  apply (rule_tac x="h (λx. (fst x, 1 - snd x))" in exI)
  apply (rule conjI continuous_intros)+
  apply (auto simp: reversepath_def pathstart_def pathfinish_def elim!: continuous_on_subset)
  done

proposition homotopic_paths_reversepath:
     "homotopic_paths S (reversepath p) (reversepath q) homotopic_paths S p q"
  using homotopic_paths_reversepath_D by force


proposition homotopic_paths_join:
    "[homotopic_paths S p p'; homotopic_paths S q q'; pathfinish p = pathstart q] ==> homotopic_paths S (p +++ q) (p' +++ q')"
  apply (clarsimp simp: homotopic_paths_def homotopic_with_def)
  apply (rename_tac k1 k2)
  apply (rule_tac x="(λy. ((k1 Pair (fst y)) +++ (k2 Pair (fst y))) (snd y))" in exI)
  apply (intro conjI continuous_intros continuous_on_homotopic_join_lemma; force simp: joinpaths_def pathstart_def pathfinish_def path_image_def)
  done

proposition homotopic_paths_continuous_image:
    "[homotopic_paths S f g; continuous_on S h; h S t] ==> homotopic_paths t (h f) (h g)"
  unfolding homotopic_paths_def
  by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose image_subset_iff_funcset)


subsectionGroup properties for homotopy of paths

text🍋tag important\<open>So taking equivalence classes under homotopy would give the fundamental group

proposition homotopic_paths_rid:
  assumes "path p" "path_image p S"
  shows "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p)) p"
proof -
  have 🍋"continuous_on {0..1} (λt::real. if t 1/2 then 2 *🪙R t else 1)"
    unfolding split_01
    by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
  show ?thesis
    apply (rule homotopic_paths_sym)
    using assms unfolding pathfinish_def joinpaths_def
    by (intro 🍋 continuous_on_cases continuous_intros homotopic_paths_reparametrize [where f = "λt. if t 1/2 then 2 *🪙R t else 1"]; force)
qed

proposition homotopic_paths_lid:
   "[path p; path_image p S] ==> homotopic_paths S (linepath (pathstart p) (pathstart p) +++ p) p"
  using homotopic_paths_rid [of "reversepath p" S]
  by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
        pathfinish_reversepath reversepath_joinpaths reversepath_linepath)

lemma homotopic_paths_rid':
  assumes "path p" "path_image p s" "x = pathfinish p"
  shows "homotopic_paths s (p +++ linepath x x) p"
  using homotopic_paths_rid[of p s] assms by simp

lemma homotopic_paths_lid':
   "[path p; path_image p s; x = pathstart p] ==> homotopic_paths s (linepath x x +++ p) p"
  using homotopic_paths_lid[of p s] by simp

proposition homotopic_paths_assoc:
   "[path p; path_image p S; path q; path_image q S; path r; path_image r S; pathfinish p = pathstart q;
     pathfinish q = pathstart r]
    ==> homotopic_paths S (p +++ (q +++ r)) ((p +++ q) +++ r)"
  apply (subst homotopic_paths_sym)
  apply (rule homotopic_paths_reparametrize
           [where f = "λt. if t 1/2 then inverse 2 *🪙R t
                           else if t 3 / 4 then t - (1 / 4)
                           else 2 *🪙R t - 1"])
  apply (simp_all del: le_divide_eq_numeral1 add: subset_path_image_join)
  apply (rule continuous_on_cases_1 continuous_intros | auto simp: joinpaths_def)+
  done

proposition homotopic_paths_rinv:
  assumes "path p" "path_image p S"
    shows "homotopic_paths S (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
proof -
  have p: "continuous_on {0..1} p" 
    using assms by (auto simp: path_def)
  let ?A = "{0..1} × {0..1}"
  have "continuous_on ?A (λx. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))"
    unfolding joinpaths_def subpath_def reversepath_def path_def add_0_right diff_0_right
  proof (rule continuous_on_cases_le)
    show "continuous_on {x ?A. snd x 1/2} (λt. p (fst t * (2 * snd t)))"
         "continuous_on {x ?A. 1/2 snd x} (λt. p (fst t * (1 - (2 * snd t - 1))))"
         "continuous_on ?A snd"
      by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp: mult_le_one)+
  qed (auto simp: algebra_simps)
  then show ?thesis
    using assms
    apply (subst homotopic_paths_sym_eq)
    unfolding homotopic_paths_def homotopic_with_def
    apply (rule_tac x="(λy. (subpath 0 (fst y) p +++ reversepath(subpath 0 (fst y) p)) (snd y))" in exI)
    apply (force simp: mult_le_one path_defs joinpaths_def subpath_def reversepath_def)
    done
qed

proposition homotopic_paths_linv:
  assumes "path p" "path_image p S"
    shows "homotopic_paths S (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))"
  using homotopic_paths_rinv [of "reversepath p" S] assms by simp


subsectionHomotopy of loops without requiring preservation of endpoints

definition🍋tag important homotopic_loops :: "'a::topological_space set ==> (real ==> 'a) ==> (real ==> 'a) ==> bool"  where
 "homotopic_loops S p q
     homotopic_with_canon (λr. pathfinish r = pathstart r) {0..1} S p q"

lemma homotopic_loops:
   "homotopic_loops S p q
      (h. continuous_on ({0..1::real} × {0..1}) h
          h ({0..1} × {0..1}) S
          (x {0..1}. h(0,x) = p x)
          (x {0..1}. h(1,x) = q x)
          (t {0..1}. pathfinish(h Pair t) = pathstart(h Pair t)))"
  by (simp add: homotopic_loops_def pathstart_def pathfinish_def homotopic_with)

proposition homotopic_loops_imp_loop:
     "homotopic_loops S p q ==> pathfinish p = pathstart p pathfinish q = pathstart q"
using homotopic_with_imp_property homotopic_loops_def by blast

proposition homotopic_loops_imp_path:
     "homotopic_loops S p q ==> path p path q"
  unfolding homotopic_loops_def path_def
  using homotopic_with_imp_continuous_maps continuous_map_subtopology_eu by blast

proposition homotopic_loops_imp_subset:
     "homotopic_loops S p q ==> path_image p S path_image q S"
  unfolding homotopic_loops_def path_image_def
  by (simp add: homotopic_with_imp_subset1 homotopic_with_imp_subset2)

proposition homotopic_loops_refl:
     "homotopic_loops S p p
      path p path_image p S pathfinish p = pathstart p"
  by (metis (mono_tags, lifting) homotopic_loops_def homotopic_paths_def
      homotopic_paths_refl homotopic_with_refl)

proposition homotopic_loops_sym: "homotopic_loops S p q ==> homotopic_loops S q p"
  by (simp add: homotopic_loops_def homotopic_with_sym)

proposition homotopic_loops_sym_eq: "homotopic_loops S p q homotopic_loops S q p"
  by (metis homotopic_loops_sym)

proposition homotopic_loops_trans:
   "[homotopic_loops S p q; homotopic_loops S q r] ==> homotopic_loops S p r"
  unfolding homotopic_loops_def by (blast intro: homotopic_with_trans)

proposition homotopic_loops_subset:
   "[homotopic_loops S p q; S t] ==> homotopic_loops t p q"
  by (fastforce simp: homotopic_loops)

proposition homotopic_loops_eq:
   "[path p; path_image p S; pathfinish p = pathstart p; t. t {0..1} ==> p(t) = q(t)]
          ==> homotopic_loops S p q"
  unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def image_subset_iff_funcset
  using homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]]
  by fastforce

proposition homotopic_loops_continuous_image:
   "[homotopic_loops S f g; continuous_on S h; h S t] ==> homotopic_loops t (h f) (h g)"
  unfolding homotopic_loops_def
  by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def image_subset_iff_funcset)


subsectionRelations between the two variants of homotopy

proposition homotopic_paths_imp_homotopic_loops:
    "[homotopic_paths S p q; pathfinish p = pathstart p; pathfinish q = pathstart p] ==> homotopic_loops S p q"
  by (auto simp: homotopic_with_def homotopic_paths_def homotopic_loops_def)

proposition homotopic_loops_imp_homotopic_paths_null:
  assumes "homotopic_loops S p (linepath a a)"
    shows "homotopic_paths S p (linepath (pathstart p) (pathstart p))"
proof -
  have "path p" by (metis assms homotopic_loops_imp_path)
  have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop)
  have pip: "path_image p S" by (metis assms homotopic_loops_imp_subset)
  let ?A = "{0..1::real} × {0..1::real}"
  obtain h where conth: "continuous_on ?A h"
             and hs: "h ?A S"
             and h0[simp]: "x. x {0..1} ==> h(0,x) = p x"
             and h1[simp]: "x. x {0..1} ==> h(1,x) = a"
             and ends: "t. t {0..1} ==> pathfinish (h Pair t) = pathstart (h Pair t)"
    using assms by (auto simp: homotopic_loops homotopic_with image_subset_iff_funcset)
  have conth0: "path (λu. h (u, 0))"
    unfolding path_def
  proof (rule continuous_on_compose [of _ _ h, unfolded o_def])
    show "continuous_on ((λx. (x, 0)) ` {0..1}) h"
      by (force intro: continuous_on_subset [OF conth])
  qed (force intro: continuous_intros)
  have pih0: "path_image (λu. h (u, 0)) S"
    using hs by (force simp: path_image_def)
  have c1: "continuous_on ?A (λx. h (fst x * snd x, 0))"
  proof (rule continuous_on_compose [of _ _ h, unfolded o_def])
    show "continuous_on ((λx. (fst x * snd x, 0)) ` ?A) h"
      by (force simp: mult_le_one intro: continuous_on_subset [OF conth])
  qed (force intro: continuous_intros)+
  have c2: "continuous_on ?A (λx. h (fst x - fst x * snd x, 0))"
  proof (rule continuous_on_compose [of _ _ h, unfolded o_def])
    show "continuous_on ((λx. (fst x - fst x * snd x, 0)) ` ?A) h"
      by (auto simp: algebra_simps add_increasing2 mult_left_le intro: continuous_on_subset [OF conth])
  qed (force intro: continuous_intros)
  have [simp]: "t. [0 t t 1] ==> h (t, 1) = h (t, 0)"
    using ends by (simp add: pathfinish_def pathstart_def)
  have adhoc_le: "c * 4 1 + c * (d * 4)" if "¬ d * 4 3" "0 c" "c 1" for c d::real
  proof -
    have "c * 3 c * (d * 4)" using that less_eq_real_def by auto
    with c 1 show ?thesis by fastforce
  qed
  have *: "p x. [path p path(reversepath p);
                  path_image p S path_image(reversepath p) S;
                  pathfinish p = pathstart(linepath a a +++ reversepath p)
                   pathstart(reversepath p) = a pathstart p = x]
                  ==> homotopic_paths S (p +++ linepath a a +++ reversepath p) (linepath x x)"
    by (metis homotopic_paths_lid homotopic_paths_join
              homotopic_paths_trans homotopic_paths_sym homotopic_paths_rinv)
  have 1: "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))"
    using path p homotopic_paths_rid homotopic_paths_sym pip by blast
  moreover have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p))
                                   (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))"
    using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" S]
    by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_sym pathstart_join)
  moreover 
  have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))
                                   ((λu. h (u, 0)) +++ linepath a a +++ reversepath (λu. h (u, 0)))"
    unfolding homotopic_paths_def homotopic_with_def
  proof (intro exI strip conjI)
    let ?h = "λy. (subpath 0 (fst y) (λu. h (u, 0)) +++ (λu. h (Pair (fst y) u))
               +++ subpath (fst y) 0 (λu. h (u, 0))) (snd y)" 
    have "continuous_on ?A ?h"
      by (intro continuous_on_homotopic_join_lemma; simp add: path_defs joinpaths_def subpath_def conth c1 c2)
    moreover have "?h ?A S"
      using hs
      unfolding joinpaths_def subpath_def
      by (force simp: algebra_simps mult_le_one mult_left_le  intro: adhoc_le)
  ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))
                         (top_of_set S) ?h"
    by (simp add: subpath_reversepath image_subset_iff_funcset)
  qed (use ploop in simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2)
  moreover have "homotopic_paths S ((λu. h (u, 0)) +++ linepath a a +++ reversepath (λu. h (u, 0)))
                                   (linepath (pathstart p) (pathstart p))"
    by (rule *; simp add: pih0 pathstart_def pathfinish_def conth0; simp add: reversepath_def joinpaths_def)
  ultimately show ?thesis
    by (blast intro: homotopic_paths_trans)
qed

proposition homotopic_loops_conjugate:
  fixes S :: "'a::real_normed_vector set"
  assumes "path p" "path q" and pip: "path_image p S" and piq: "path_image q S"
      and pq: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
    shows "homotopic_loops S (p +++ q +++ reversepath p) q"
proof -
  have contp: "continuous_on {0..1} p"  using path p [unfolded path_def] by blast
  have contq: "continuous_on {0..1} q"  using path q [unfolded path_def] by blast
  let ?A = "{0..1::real} × {0..1::real}"
  have c1: "continuous_on ?A (λx. p ((1 - fst x) * snd x + fst x))"
  proof (rule continuous_on_compose [of _ _ p, unfolded o_def])
    show "continuous_on ((λx. (1 - fst x) * snd x + fst x) ` ?A) p"
      by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_right_le_one_le sum_le_prod1)
  qed (force intro: continuous_intros)
  have c2: "continuous_on ?A (λx. p ((fst x - 1) * snd x + 1))"
  proof (rule continuous_on_compose [of _ _ p, unfolded o_def])
    show "continuous_on ((λx. (fst x - 1) * snd x + 1) ` ?A) p"
      by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_left_le_one_le)
  qed (force intro: continuous_intros)

  have ps1: "a b. [b * 2 1; 0 b; 0 a; a 1] ==> p ((1 - a) * (2 * b) + a) S"
    using sum_le_prod1
    by (force simp: algebra_simps add_increasing2 mult_left_le intro: pip [unfolded path_image_def, THEN subsetD])
  have ps2: "a b. [¬ 4 * b 3; b 1; 0 a; a 1] ==> p ((a - 1) * (4 * b - 3) + 1) S"
    apply (rule pip [unfolded path_image_def, THEN subsetD])
    apply (rule image_eqI, blast)
    apply (simp add: algebra_simps)
    by (metis add_mono affine_ineq linear mult.commute mult.left_neutral mult_right_mono
              add.commute zero_le_numeral)
  have qs: "a b. [4 * b 3; ¬ b * 2 1] ==> q (4 * b - 2) S"
    using path_image_def piq by fastforce
  have "homotopic_loops S (p +++ q +++ reversepath p)
                          (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q))"
    unfolding homotopic_loops_def homotopic_with_def
  proof (intro exI strip conjI)
    let ?h = "(λy. (subpath (fst y) 1 p +++ q +++ subpath 1 (fst y) p) (snd y))" 
    have "continuous_on ?A (λy. q (snd y))"
      by (force simp: contq intro: continuous_on_compose [of _ _ q, unfolded o_def] continuous_on_id continuous_on_snd)
    then have "continuous_on ?A ?h"
      using pq qloop
      by (intro continuous_on_homotopic_join_lemma) (auto simp: path_defs joinpaths_def subpath_def c1 c2)
    then show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set S) ?h"
      by (auto simp: joinpaths_def subpath_def  ps1 ps2 qs)
    show "?h (1,x) = (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) x"  for x
      using pq by (simp add: pathfinish_def subpath_refl)
  qed (auto simp: subpath_reversepath)
  moreover have "homotopic_loops S (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) q"
  proof -
    have "homotopic_paths S (linepath (pathfinish q) (pathfinish q) +++ q) q"
      using path q homotopic_paths_lid qloop piq by auto
    hence 1: "f. homotopic_paths S f q ¬ homotopic_paths S f (linepath (pathfinish q) (pathfinish q) +++ q)"
      using homotopic_paths_trans by blast
    hence "homotopic_paths S (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q"
      by (smt (verit, best) path q homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_lid 
          homotopic_paths_rid homotopic_paths_trans pathstart_join piq qloop)
    thus ?thesis
      by (metis (no_types) qloop homotopic_loops_sym homotopic_paths_imp_homotopic_loops homotopic_paths_imp_pathfinish homotopic_paths_sym)
  qed
  ultimately show ?thesis
    by (blast intro: homotopic_loops_trans)
qed

lemma homotopic_paths_loop_parts:
  assumes loops: "homotopic_loops S (p +++ reversepath q) (linepath a a)" and "path q"
  shows "homotopic_paths S p q"
proof -
  have paths: "homotopic_paths S (p +++ reversepath q) (linepath (pathstart p) (pathstart p))"
    using homotopic_loops_imp_homotopic_paths_null [OF loops] by simp
  then have "path p"
    using path q homotopic_loops_imp_path loops path_join path_join_path_ends path_reversepath by blast
  show ?thesis
  proof (cases "pathfinish p = pathfinish q")
    case True
    obtain pipq: "path_image p S" "path_image q S"
      by (metis Un_subset_iff paths path p path q homotopic_loops_imp_subset homotopic_paths_imp_path loops
           path_image_join path_image_reversepath path_imp_reversepath path_join_eq)
    have "homotopic_paths S p (p +++ (linepath (pathfinish p) (pathfinish p)))"
      using path p path_image p S homotopic_paths_rid homotopic_paths_sym by blast
    moreover have "homotopic_paths S (p +++ (linepath (pathfinish p) (pathfinish p))) (p +++ (reversepath q +++ q))"
      by (simp add: True path p path q pipq homotopic_paths_join homotopic_paths_linv homotopic_paths_sym)
    moreover have "homotopic_paths S (p +++ (reversepath q +++ q)) ((p +++ reversepath q) +++ q)"
      by (simp add: True path p path q homotopic_paths_assoc pipq)
    moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)"
      by (simp add: path q homotopic_paths_join paths pipq)
    ultimately show ?thesis
      by (metis path q homotopic_paths_imp_path homotopic_paths_lid homotopic_paths_trans path_join_path_ends pathfinish_linepath pipq(2))
  next
    case False
    then show ?thesis
      using path q homotopic_loops_imp_path loops path_join_path_ends by fastforce
  qed
qed


subsection🍋tag unimportant\<open>Homotopy of "nearby" function, paths and loops

lemma homotopic_with_linear:
  fixes f g :: "_ ==> 'b::real_normed_vector"
  assumes contf: "continuous_on S f"
      and contg:"continuous_on S g"
      and sub: "x. x S ==> closed_segment (f x) (g x) t"
    shows "homotopic_with_canon (λz. True) S t f g"
  unfolding homotopic_with_def
  apply (rule_tac x="λy. ((1 - (fst y)) *🪙R f(snd y) + (fst y) *🪙R g(snd y))" in exI)
  using sub closed_segment_def
     by (fastforce intro: continuous_intros continuous_on_subset [OF contf] continuous_on_compose2 [where g=f]
            continuous_on_subset [OF contg] continuous_on_compose2 [where g=g])

lemma homotopic_paths_linear:
  fixes g h :: "real ==> 'a::real_normed_vector"
  assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
          "t. t {0..1} ==> closed_segment (g t) (h t) S"
    shows "homotopic_paths S g h"
  using assms
  unfolding path_def
  apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
  apply (rule_tac x="λy. ((1 - (fst y)) *🪙R (g snd) y + (fst y) *🪙R (h snd) y)" in exI)
  apply (intro conjI subsetI continuous_intros; force)
  done

lemma homotopic_loops_linear:
  fixes g h :: "real ==> 'a::real_normed_vector"
  assumes "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h"
          "t x. t {0..1} ==> closed_segment (g t) (h t) S"
    shows "homotopic_loops S g h"
  using assms
  unfolding path_defs homotopic_loops_def homotopic_with_def
  apply (rule_tac x="λy. ((1 - (fst y)) *🪙R g(snd y) + (fst y) *🪙R h(snd y))" in exI)
  by (force simp: closed_segment_def intro!: continuous_intros intro: continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h])

lemma homotopic_paths_nearby_explicit:
  assumes 🍋"path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
      and no: "t x. [t {0..1}; x S] ==> norm(h t - g t) < norm(g t - x)"
    shows "homotopic_paths S g h"
  using homotopic_paths_linear [OF 🍋by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI)

lemma homotopic_loops_nearby_explicit:
  assumes 🍋"path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h"
      and no: "t x. [t {0..1}; x S] ==> norm(h t - g t) < norm(g t - x)"
    shows "homotopic_loops S g h"
  using homotopic_loops_linear [OF 🍋by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI)

lemma homotopic_nearby_paths:
  fixes g h :: "real ==> 'a::euclidean_space"
  assumes "path g" "open S" "path_image g S"
    shows "e. 0 < e
               (h. path h
                    pathstart h = pathstart g pathfinish h = pathfinish g
                    (t {0..1}. norm(h t - g t) < e) homotopic_paths S g h)"
proof -
  obtain e where "e > 0" and e: "x y. x path_image g ==> y - S ==> e dist x y"
    using separate_compact_closed [of "path_image g" "-S"] assms by force
  show ?thesis
    using e [unfolded dist_norm] e > 0
    by (fastforce simp: path_image_def intro!: homotopic_paths_nearby_explicit assms exI)
qed

lemma homotopic_nearby_loops:
  fixes g h :: "real ==> 'a::euclidean_space"
  assumes "path g" "open S" "path_image g S" "pathfinish g = pathstart g"
    shows "e. 0 < e
               (h. path h pathfinish h = pathstart h
                    (t {0..1}. norm(h t - g t) < e) homotopic_loops S g h)"
proof -
  obtain e where "e > 0" and e: "x y. x path_image g ==> y - S ==> e dist x y"
    using separate_compact_closed [of "path_image g" "-S"] assms by force
  show ?thesis
    using e [unfolded dist_norm] e > 0
    by (fastforce simp: path_image_def intro!: homotopic_loops_nearby_explicit assms exI)
qed


subsection Homotopy and subpaths

lemma homotopic_join_subpaths1:
  assumes "path g" and pag: "path_image g S"
      and u: "u {0..1}" and v: "v {0..1}" and w: "w {0..1}" "u v" "v w"
    shows "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)"
proof -
  have 1: "t * 2 1 ==> u + t * (v * 2) v + t * (u * 2)" for t
    using affine_ineq u v by fastforce
  have 2: "t * 2 > 1 ==> u + (2*t - 1) * v v + (2*t - 1) * w" for t
    by (metis add_mono_thms_linordered_semiring(1) diff_gt_0_iff_gt less_eq_real_def mult.commute mult_right_mono u v v w)
  have t2: "t::real. t*2 = 1 ==> t = 1/2" by auto
  have "homotopic_paths (path_image g) (subpath u v g +++ subpath v w g) (subpath u w g)"
  proof (cases "w = u")
    case True
    then show ?thesis
      by (metis path g homotopic_paths_rinv path_image_subpath_subset path_subpath pathstart_subpath reversepath_subpath subpath_refl u v)
  next
    case False
    let ?f = "λt. if t 1/2 then inverse((w - u)) *🪙R (2 * (v - u)) *🪙R t
                               else inverse((w - u)) *🪙R ((v - u) + (w - v) *🪙R (2 *🪙R t - 1))"
    show ?thesis
    proof (rule homotopic_paths_sym [OF homotopic_paths_reparametrize [where f = ?f]])
      show "path (subpath u w g)"
        using assms(1) path_subpath u w(1) by blast
      show "path_image (subpath u w g) path_image g"
        by (meson path_image_subpath_subset u w(1))
      show "continuous_on {0..1} ?f"
        unfolding split_01
        by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def dest!: t2)+
      show "?f {0..1} {0..1}"
        using False assms
        by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2)
      show "(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)" if "t {0..1}" for t 
        using assms
        unfolding joinpaths_def subpath_def by (auto simp: divide_simps add.commute mult.commute mult.left_commute)
    qed (use False in auto)
  qed
  then show ?thesis
    by (rule homotopic_paths_subset [OF _ pag])
qed

lemma homotopic_join_subpaths2:
  assumes "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)"
  shows "homotopic_paths S (subpath w v g +++ subpath v u g) (subpath w u g)"
  by (metis assms homotopic_paths_reversepath_D pathfinish_subpath pathstart_subpath reversepath_joinpaths reversepath_subpath)

lemma homotopic_join_subpaths3:
  assumes hom: "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)"
      and "path g" and pag: "path_image g S"
      and u: "u {0..1}" and v: "v {0..1}" and w: "w {0..1}"
    shows "homotopic_paths S (subpath v w g +++ subpath w u g) (subpath v u g)"
proof -
  obtain wvg: "path (subpath w v g)" "path_image (subpath w v g) S" 
     and wug: "path (subpath w u g)" "path_image (subpath w u g) S"
     and vug: "path (subpath v u g)" "path_image (subpath v u g) S"
    by (meson path g pag path_image_subpath_subset path_subpath subset_trans u v w)
  have "homotopic_paths S (subpath u w g +++ subpath w v g)
                          ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
    by (simp add: hom homotopic_paths_join homotopic_paths_sym wvg)
  also have "homotopic_paths S (subpath u v g +++ subpath v w g +++ subpath w v g)"
    using wvg vug path g
    by (metis homotopic_paths_assoc homotopic_paths_sym path_image_subpath_commute path_subpath
        pathfinish_subpath pathstart_subpath u v w)
  also have "homotopic_paths S (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))"
    using wvg vug path g
    by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl path_image_subpath_commute
        path_subpath pathfinish_subpath pathstart_join pathstart_subpath reversepath_subpath u v)
  also have "homotopic_paths S (subpath u v g)"
    using vug path g by (metis homotopic_paths_rid path_image_subpath_commute path_subpath u v)
  finally have "homotopic_paths S (subpath u w g +++ subpath w v g) (subpath u v g)" .
  then show ?thesis
    using homotopic_join_subpaths2 by blast
qed

proposition homotopic_join_subpaths:
   "[path g; path_image g S; u {0..1}; v {0..1}; w {0..1}]
    ==> homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)"
  by (smt (verit, del_insts) homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3)

textRelating homotopy of trivial loops to path-connectedness.

lemma path_component_imp_homotopic_points:
  assumes "path_component S a b"
  shows "homotopic_loops S (linepath a a) (linepath b b)"
proof -
  obtain g :: "real ==> 'a" where g: "continuous_on {0..1} g" "g {0..1} S" "g 0 = a" "g 1 = b"
    using assms by (auto simp: path_defs)
  then have "continuous_on ({0..1} × {0..1}) (g fst)"
    by (fastforce intro!: continuous_intros)+
  with g show ?thesis
    by (auto simp: homotopic_loops_def homotopic_with_def path_defs Pi_iff)
qed

lemma homotopic_loops_imp_path_component_value:
  "[homotopic_loops S p q; 0 t; t 1] ==> path_component S (p t) (q t)"
  apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs)
  apply (rule_tac x="h (λu. (u, t))" in exI)
  apply (fastforce elim!: continuous_on_subset intro!: continuous_intros)
  done

lemma homotopic_points_eq_path_component:
   "homotopic_loops S (linepath a a) (linepath b b) path_component S a b"
  using homotopic_loops_imp_path_component_value path_component_imp_homotopic_points by fastforce

lemma path_connected_eq_homotopic_points:
  "path_connected S
      (a b. a S b S homotopic_loops S (linepath a a) (linepath b b))"
  by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)


subsectionSimply connected sets

text🍋tag important\<open>defined as "all loops are homotopic (as loops)

definition🍋tag important simply_connected where
  "simply_connected S 
        p q. path p  pathfinish p = pathstart p  path_image p  S 
              path q  pathfinish q = pathstart q  path_image q  S
               homotopic_loops S p q"

lemma simply_connected_empty [iff]: "simply_connected {}"
  by (simp add: simply_connected_def)

lemma simply_connected_imp_path_connected:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S ==> path_connected S"
  by (simp add: simply_connected_def path_connected_eq_homotopic_points)

lemma simply_connected_imp_connected:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S ==> connected S"
  by (simp add: path_connected_imp_connected simply_connected_imp_path_connected)

lemma simply_connected_eq_contractible_loop_any:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S 
            (p a. path p  path_image p  S  pathfinish p = pathstart p  a  S
                   homotopic_loops S p (linepath a a))"
        (is "?lhs = ?rhs")
proof
  assume ?rhs then show ?lhs
    unfolding simply_connected_def
    by (metis pathfinish_in_path_image subsetD homotopic_loops_trans homotopic_loops_sym)
qed (force simp: simply_connected_def)

lemma simply_connected_eq_contractible_loop_some:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S 
                path_connected S 
                (p. path p  path_image p  S  pathfinish p = pathstart p
                     (a. a  S  homotopic_loops S p (linepath a a)))"
     (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
  using simply_connected_eq_contractible_loop_any by (blast intro: simply_connected_imp_path_connected)
next
  assume ?rhs
  then show ?lhs
    by (meson homotopic_loops_trans path_connected_eq_homotopic_points simply_connected_eq_contractible_loop_any)
qed

lemma simply_connected_eq_contractible_loop_all:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S 
         S = {} 
         ( S. p. path p  path_image p  S  pathfinish p = pathstart p
                 homotopic_loops S p (linepath a a))"
  by (meson ex_in_conv homotopic_loops_sym homotopic_loops_trans simply_connected_def simply_connected_eq_contractible_loop_any)

lemma simply_connected_eq_contractible_path:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S 
           path_connected S 
           (p. path p  path_image p  S  pathfinish p = pathstart p
             homotopic_paths S p (linepath (pathstart p) (pathstart p)))"
     (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    unfolding simply_connected_imp_path_connected
    by (metis simply_connected_eq_contractible_loop_some homotopic_loops_imp_homotopic_paths_null)
next
  assume ?rhs
  then show ?lhs
    using homotopic_paths_imp_homotopic_loops simply_connected_eq_contractible_loop_some by fastforce
qed

lemma simply_connected_eq_homotopic_paths:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S 
          path_connected S 
          (p q. path p  path_image p  S 
                path q  path_image q  S 
                pathstart q = pathstart p  pathfinish q = pathfinish p
                 homotopic_paths S p q)"
         (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have pc: "path_connected S"
        and *: "p. [path p; path_image p  S;
                       pathfinish p = pathstart p]
                      ==> homotopic_paths S p (linepath (pathstart p) (pathstart p))"
    by (auto simp: simply_connected_eq_contractible_path)
  have "homotopic_paths S p q"
        if "path p" "path_image p  S" "path q"
           "path_image q  S" "pathstart q = pathstart p"
           "pathfinish q = pathfinish p" for p q
  proof -
    have "homotopic_paths S p (p +++ reversepath q +++ q)"
      using that
      by (smt (verit, best) homotopic_paths_join homotopic_paths_linv homotopic_paths_rid homotopic_paths_sym
          homotopic_paths_trans pathstart_linepath)
    also have "homotopic_paths S  ((p +++ reversepath q) +++ q)"
      by (simp add: that homotopic_paths_assoc)
    also have "homotopic_paths S  (linepath (pathstart q) (pathstart q) +++ q)"
      using * [of "p +++ reversepath q"] that
      by (simp add: homotopic_paths_assoc homotopic_paths_join path_image_join)
    also have "homotopic_paths S  q"
      using that homotopic_paths_lid by blast
    finally show ?thesis .
  qed
  then show ?rhs
    by (blast intro: pc *)
next
  assume ?rhs
  then show ?lhs
    by (force simp: simply_connected_eq_contractible_path)
qed

proposition simply_connected_Times:
  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
  assumes S: "simply_connected S" and T: "simply_connected T"
    shows "simply_connected(S × T)"
proof -
  have "homotopic_loops (S × T) p (linepath (a, b) (a, b))"
       if "path p" "path_image p  S × T" "p 1 = p 0" " S" " T"
       for p a b
  proof -
    have "path (fst  p)"
      by (simp add: continuous_on_fst Path_Connected.path_continuous_image [OF path p])
    moreover have "path_image (fst  p)  S"
      using that by (force simp: path_image_def)
    ultimately have p1: "homotopic_loops S (fst  p) (linepath a a)"
      using S that
      by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
    have "path (snd  p)"
      by (simp add: continuous_on_snd Path_Connected.path_continuous_image [OF path p])
    moreover have "path_image (snd  p)  T"
      using that by (force simp: path_image_def)
    ultimately have p2: "homotopic_loops T (snd  p) (linepath b b)"
      using T that
      by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
    show ?thesis
      using p1 p2 unfolding homotopic_loops
      apply clarify
      subgoal for h k
        by (rule_tac x="λz. (h z, k z)" in exI) (auto intro: continuous_intros simp: path_defs)
      done
  qed
  with assms show ?thesis
    by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
qed


subsectionContractible sets

definition🍋tag important contractible where
 "contractible S  a. homotopic_with_canon (λx. True) S S id (λx. a)"

proposition contractible_imp_simply_connected:
  fixes S :: "_::real_normed_vector set"
  assumes "contractible S" shows "simply_connected S"
proof (cases "S = {}")
  case True then show ?thesis by force
next
  case False
  obtain a where a: "homotopic_with_canon (λx. True) S S id (λx. a)"
    using assms by (force simp: contractible_def)
  then have " S"
    using False homotopic_with_imp_funspace2 by fastforce
  have "p. path p 
            path_image p  S  pathfinish p = pathstart p 
            homotopic_loops S p (linepath a a)"
    using a apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs)
    apply (rule_tac x="(h  (λy. (fst y, (p  snd) y)))" in exI)
    apply (intro conjI continuous_on_compose continuous_intros; force elim: continuous_on_subset)
    done
  with a S show ?thesis
    by (auto simp: simply_connected_eq_contractible_loop_all False)
qed

corollary contractible_imp_connected:
  fixes S :: "_::real_normed_vector set"
  shows "contractible S ==> connected S"
  by (simp add: contractible_imp_simply_connected simply_connected_imp_connected)

lemma contractible_imp_path_connected:
  fixes S :: "_::real_normed_vector set"
  shows "contractible S ==> path_connected S"
  by (simp add: contractible_imp_simply_connected simply_connected_imp_path_connected)

lemma nullhomotopic_through_contractible:
  fixes S :: "_::topological_space set"
  assumes f: "continuous_on S f" " S  T"
      and g: "continuous_on T g" " T  U"
      and T: "contractible T"
    obtains c where "homotopic_with_canon (λh. True) S U (g  f) (λx. c)"
proof -
  obtain b where b: "homotopic_with_canon (λx. True) T T id (λx. b)"
    using assms by (force simp: contractible_def)
  have "homotopic_with_canon (λf. True) T U (g  id) (g  (λx. b))"
    by (metis b continuous_map_subtopology_eu g homotopic_with_compose_continuous_map_left image_subset_iff_funcset)
  then have "homotopic_with_canon (λf. True) S U (g  id  f) (g  (λx. b)  f)"
    by (simp add: f homotopic_with_compose_continuous_map_right image_subset_iff_funcset)
  then show ?thesis
    by (simp add: comp_def that)
qed

lemma nullhomotopic_into_contractible:
  assumes f: "continuous_on S f" " S  T"
      and T: "contractible T"
    obtains c where "homotopic_with_canon (λh. True) S T f (λx. c)"
  by (rule nullhomotopic_through_contractible [OF f, of id T]) (use assms in auto)

lemma nullhomotopic_from_contractible:
  assumes f: "continuous_on S f" " S  T"
      and S: "contractible S"
    obtains c where "homotopic_with_canon (λh. True) S T f (λx. c)"
  by (auto simp: comp_def intro: nullhomotopic_through_contractible [OF continuous_on_id _ f S])

lemma homotopic_through_contractible:
  fixes S :: "_::real_normed_vector set"
  assumes "continuous_on S f1" "f1  S  T"
          "continuous_on T g1" "g1  T  U"
          "continuous_on S f2" "f2  S  T"
          "continuous_on T g2" "g2  T  U"
          "contractible T" "path_connected U"
   shows "homotopic_with_canon (λh. True) S U (g1  f1) (g2  f2)"
proof -
  obtain c1 where c1: "homotopic_with_canon (λh. True) S U (g1  f1) (λx. c1)"
    by (rule nullhomotopic_through_contractible [of S f1 T g1 U]) (use assms in auto)
  obtain c2 where c2: "homotopic_with_canon (λh. True) S U (g2  f2) (λx. c2)"
    by (rule nullhomotopic_through_contractible [of S f2 T g2 U]) (use assms in auto)
  have "S = {}  (t. path_connected t  t  U  c2  t  c1  t)"
  proof (cases "S = {}")
    case True then show ?thesis by force
  next
    case False
    with c1 c2 have "c1  U" "c2  U"
      using homotopic_with_imp_continuous_maps
       by (metis PiE equals0I homotopic_with_imp_funspace2)+
    with path_connected U show ?thesis by blast
  qed
  then have "homotopic_with_canon (λh. True) S U (λx. c2) (λx. c1)"
    by (auto simp: path_component homotopic_constant_maps)
  then show ?thesis
    using c1 c2 homotopic_with_symD homotopic_with_trans by blast
qed

lemma homotopic_into_contractible:
  fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
  assumes f: "continuous_on S f" " S  T"
    and g: "continuous_on S g" " S  T"
    and T: "contractible T"
  shows "homotopic_with_canon (λh. True) S T f g"
  using homotopic_through_contractible [of S f T id T g id]
  by (simp add: assms contractible_imp_path_connected)

lemma homotopic_from_contractible:
  fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
  assumes f: "continuous_on S f" " S  T"
    and g: "continuous_on S g" " S  T"
    and "contractible S" "path_connected T"
  shows "homotopic_with_canon (λh. True) S T f g"
  using homotopic_through_contractible [of S id S f T id g]
  by (simp add: assms contractible_imp_path_connected)

subsectionStarlike sets

definition🍋tag important "starlike S  (aS. xS. closed_segment a x  S)"

lemma starlike_UNIV [simp]: "starlike UNIV"
  by (simp add: starlike_def)

lemma convex_imp_starlike:
  "convex S ==> S  {} ==> starlike S"
  unfolding convex_contains_segment starlike_def by auto

lemma starlike_convex_tweak_boundary_points:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" " {}" and ST: "rel_interior S  T" and TS: " closure S"
  shows "starlike T"
proof -
  have "rel_interior S  {}"
    by (simp add: assms rel_interior_eq_empty)
  with ST obtain a where a: " rel_interior S" and " T" by blast
  have "x. x  T ==> open_segment a x  rel_interior S"
    by (rule rel_interior_closure_convex_segment [OF convex S a]) (use assms in auto)
  then have "xT. a  T  open_segment a x  T"
    using ST by (blast intro: a a T rel_interior_closure_convex_segment [OF convex S a])
  then show ?thesis
    unfolding starlike_def using bexI [OF _ a T]
    by (simp add: closed_segment_eq_open)
qed

lemma starlike_imp_contractible_gen:
  fixes S :: "'a::real_normed_vector set"
  assumes S: "starlike S"
      and P: "a T. [ S; 0  T; T  1] ==> P(λx. (1 - T) *🪙R x + T *🪙R a)"
    obtains a where "homotopic_with_canon P S S (λx. x) (λx. a)"
proof -
  obtain a where " S" and a: "x. x  S ==> closed_segment a x  S"
    using S by (auto simp: starlike_def)
  have "t b. 0  t  t  1 ==>
              u. (1 - t) *🪙R b + t *🪙R a = (1 - u) *🪙R a + u *🪙R b  0  u  u  1"
    by (metis add_diff_cancel_right' diff_ge_0_iff_ge le_add_diff_inverse pth_c(1))
  then have "(λy. (1 - fst y) *🪙R snd y + fst y *🪙R a) ` ({0..1} × S)  S"
    using a [unfolded closed_segment_def] by force
  then have "homotopic_with_canon P S S (λx. x) (λx. a)"
    using a S
    unfolding homotopic_with_def
    apply (rule_tac x="λy. (1 - (fst y)) *🪙R snd y + (fst y) *🪙R a" in exI)
    apply (force simp: P intro: continuous_intros)
    done
  then show ?thesis
    using that by blast
qed

lemma starlike_imp_contractible:
  fixes S :: "'a::real_normed_vector set"
  shows "starlike S ==> contractible S"
  using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def)

lemma contractible_UNIV [simp]: "contractible (UNIV :: 'a::real_normed_vector set)"
  by (simp add: starlike_imp_contractible)

lemma starlike_imp_simply_connected:
  fixes S :: "'a::real_normed_vector set"
  shows "starlike S ==> simply_connected S"
  by (simp add: contractible_imp_simply_connected starlike_imp_contractible)

lemma convex_imp_simply_connected:
  fixes S :: "'a::real_normed_vector set"
  shows "convex S ==> simply_connected S"
  using convex_imp_starlike starlike_imp_simply_connected by blast

lemma starlike_imp_path_connected:
  fixes S :: "'a::real_normed_vector set"
  shows "starlike S ==> path_connected S"
  by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected)

lemma starlike_imp_connected:
  fixes S :: "'a::real_normed_vector set"
  shows "starlike S ==> connected S"
  by (simp add: path_connected_imp_connected starlike_imp_path_connected)

lemma is_interval_simply_connected_1:
  fixes S :: "real set"
  shows "is_interval S  simply_connected S"
  by (meson convex_imp_simply_connected is_interval_connected_1 is_interval_convex_1 simply_connected_imp_connected)


subsection The slotted complex plane

lemma closed_slot_left: "closed (complex_of_real ` {..c})"
  by (intro closed_injective_linear_image) (auto simp: inj_def)

lemma closed_slot_right: "closed (complex_of_real ` {c..})"
  by (intro closed_injective_linear_image) (auto simp: inj_def)

lemma complex_slot_left_eq: "complex_of_real ` {..c} = {z. Re z  c  Im z = 0}"
  by (auto simp: image_iff complex_eq_iff)

lemma complex_slot_right_eq: "complex_of_real ` {c..} = {z. Re z  c  Im z = 0}"
  by (auto simp: image_iff complex_eq_iff)

lemma complex_double_slot_eq:
  "complex_of_real ` ({..c1}  {c2..}) = {z. Im z = 0  (Re z  c1  Re z  c2)}"
  by (auto simp: image_iff complex_eq_iff)

lemma starlike_slotted_complex_plane_left_aux:
  assumes z: " -(complex_of_real ` {..c})" and c: "c < c'"
  shows "closed_segment (complex_of_real c') z  -(complex_of_real ` {..c})"
proof -
  show "closed_segment c' z  -of_real ` {..c}"
  proof (cases "Im z = 0")
    case True
    thus ?thesis using z c
      by (auto simp: closed_segment_same_Im closed_segment_eq_real_ivl complex_slot_left_eq)
  next
    case False
    show ?thesis
    proof
      fix x assume x: " closed_segment (of_real c') z"
      consider "x = of_real c'" | "x = z" | " open_segment (of_real c') z"
        unfolding open_segment_def using x by blast
      thus " -complex_of_real ` {..c}"
      proof cases
        assume " open_segment (of_real c') z"
        hence "Im x  open_segment (Im (complex_of_real c')) (Im z)"
          by (intro in_open_segment_imp_Im_in_open_segment) (use False in auto)
        hence "Im x  0"
          by (auto simp: open_segment_eq_real_ivl split: if_splits)
        thus ?thesis
          by (auto simp: complex_slot_right_eq)
      qed (use z c in auto simp: complex_slot_left_eq)
    qed
  qed
qed

lemma starlike_slotted_complex_plane_left: "starlike (-(complex_of_real ` {..c}))"
  unfolding starlike_def
proof (rule bexI[of _ "of_real c + 1"]; (intro ballI)?)
  show "complex_of_real c + 1  -complex_of_real ` {..c}"
    by (auto simp: complex_eq_iff)
  show "closed_segment (complex_of_real c + 1) z  - complex_of_real ` {..c}"
    if " - complex_of_real ` {..c}" for z
    using starlike_slotted_complex_plane_left_aux[OF that, of "c + 1"] by simp
qed


lemma starlike_slotted_complex_plane_right_aux:
  assumes z: " -(complex_of_real ` {c..})" and c: "c > c'"
  shows "closed_segment (complex_of_real c') z  -(complex_of_real ` {c..})"
proof -
  show "closed_segment c' z  -of_real ` {c..}"
  proof (cases "Im z = 0")
    case True
    thus ?thesis using z c
      by (auto simp: closed_segment_same_Im closed_segment_eq_real_ivl complex_slot_right_eq)
  next
    case False
    show ?thesis
    proof
      fix x assume x: " closed_segment (of_real c') z"
      consider "x = of_real c'" | "x = z" | " open_segment (of_real c') z"
        unfolding open_segment_def using x by blast
      thus " -complex_of_real ` {c..}"
      proof cases
        assume " open_segment (of_real c') z"
        hence "Im x  open_segment (Im (complex_of_real c')) (Im z)"
          by (intro in_open_segment_imp_Im_in_open_segment) (use False in auto)
        hence "Im x  0"
          by (auto simp: open_segment_eq_real_ivl split: if_splits)
        thus ?thesis
          by (auto simp: complex_slot_right_eq)
      qed (use z c in auto simp: complex_slot_right_eq)
    qed
  qed
qed

lemma starlike_slotted_complex_plane_right: "starlike (-(complex_of_real ` {c..}))"
  unfolding starlike_def
proof (rule bexI[of _ "of_real c - 1"]; (intro ballI)?)
  show "complex_of_real c - 1  -complex_of_real ` {c..}"
    by (auto simp: complex_eq_iff)
  show "closed_segment (complex_of_real c - 1) z  - complex_of_real ` {c..}"
    if " - complex_of_real ` {c..}" for z
    using starlike_slotted_complex_plane_right_aux[OF that, of "c - 1"] by simp
qed


lemma starlike_doubly_slotted_complex_plane_aux:
  assumes z: " -(complex_of_real ` ({..c1}  {c2..}))" and c: "c1 < c" "c < c2"
  shows "closed_segment (complex_of_real c) z  -(complex_of_real ` ({..c1}  {c2..}))"
proof -
  show "closed_segment c z  -of_real ` ({..c1}  {c2..})"
  proof (cases "Im z = 0")
    case True
    thus ?thesis using z c
      by (auto simp: closed_segment_same_Im closed_segment_eq_real_ivl complex_double_slot_eq)
  next
    case False
    show ?thesis
    proof
      fix x assume x: " closed_segment (of_real c) z"
      consider "x = of_real c" | "x = z" | " open_segment (of_real c) z"
        unfolding open_segment_def using x by blast
      thus " -complex_of_real ` ({..c1}  {c2..})"
      proof cases
        assume " open_segment (of_real c) z"
        hence "Im x  open_segment (Im (complex_of_real c)) (Im z)"
          by (intro in_open_segment_imp_Im_in_open_segment) (use False in auto)
        hence "Im x  0"
          by (auto simp: open_segment_eq_real_ivl split: if_splits)
        thus ?thesis
          by (auto simp: complex_slot_right_eq)
      qed (use z c in auto simp: complex_slot_right_eq)
    qed
  qed
qed

lemma starlike_doubly_slotted_complex_plane:
  assumes "c1 < c2"
  shows "starlike (-(complex_of_real ` ({..c1}  {c2..})))"
proof -
  from assms obtain c where c: "c1 < c" "c < c2"
    using dense by blast
  show ?thesis
    unfolding starlike_def
  proof (rule bexI[of _ "of_real c"]; (intro ballI)?)
    show "complex_of_real c  -complex_of_real ` ({..c1}  {c2..})"
      using c by (auto simp: complex_eq_iff)
    show "closed_segment (complex_of_real c) z  - complex_of_real ` ({..c1}  {c2..})"
      if " - complex_of_real ` ({..c1}  {c2..})" for z
      using starlike_doubly_slotted_complex_plane_aux[OF that, of c] c by simp
  qed
qed

lemma simply_connected_slotted_complex_plane_left:
  "simply_connected (-(complex_of_real ` {..c}))"
  by (intro starlike_imp_simply_connected starlike_slotted_complex_plane_left)

lemma simply_connected_slotted_complex_plane_right:
  "simply_connected (-(complex_of_real ` {c..}))"
  by (intro starlike_imp_simply_connected starlike_slotted_complex_plane_right)

lemma simply_connected_doubly_slotted_complex_plane:
  "c1 < c2 ==> simply_connected (-(complex_of_real ` ({..c1}  {c2..})))"
  by (intro starlike_imp_simply_connected starlike_doubly_slotted_complex_plane)

subsection Contractible sets

lemma contractible_empty [simp]: "contractible {}"
  by (simp add: contractible_def homotopic_on_emptyI)

lemma contractible_convex_tweak_boundary_points:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" and TS: "rel_interior S  T" " closure S"
  shows "contractible T"
  by (metis assms closure_eq_empty contractible_empty empty_subsetI
      starlike_convex_tweak_boundary_points starlike_imp_contractible subset_antisym)

lemma convex_imp_contractible:
  fixes S :: "'a::real_normed_vector set"
  shows "convex S ==> contractible S"
  using contractible_empty convex_imp_starlike starlike_imp_contractible by blast

lemma contractible_sing [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "contractible {a}"
  by (rule convex_imp_contractible [OF convex_singleton])

lemma is_interval_contractible_1:
  fixes S :: "real set"
  shows "is_interval S  contractible S"
  using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1
    is_interval_simply_connected_1 by auto

lemma contractible_Times:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes S: "contractible S" and T: "contractible T"
  shows "contractible (S × T)"
proof -
  obtain a h where conth: "continuous_on ({0..1} × S) h"
             and hsub: " ({0..1} × S)  S"
             and [simp]: "x. x  S ==> h (0, x) = x"
             and [simp]: "x. x  S ==>  h (1::real, x) = a"
    using S by (force simp: contractible_def homotopic_with)
  obtain b k where contk: "continuous_on ({0..1} × T) k"
             and ksub: " ({0..1} × T)  T"
             and [simp]: "x. x  T ==> k (0, x) = x"
             and [simp]: "x. x  T ==>  k (1::real, x) = b"
    using T by (force simp: contractible_def homotopic_with)
  show ?thesis
    apply (simp add: contractible_def homotopic_with)
    apply (rule exI [where x=a])
    apply (rule exI [where x=b])
    apply (rule exI [where x = "λz. (h (fst z, fst(snd z)), k (fst z, snd(snd z)))"])
    using hsub ksub
    apply (fastforce intro!: continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF contk])
    done
qed


subsectionLocal versions of topological properties in general

definition🍋tag important locally :: "('a::topological_space set ==> bool) ==> 'a se==> bool"
where
 "locally P S 
        w x. openin (top_of_set S) w  x  w
               (U V. openin (top_of_set S) U  P V  x  U  U  V  V  w)"

lemma locallyI:
  assumes "w x. [openin (top_of_set S) w; x  w]
                  ==> U V. openin (top_of_set S) U  P V  x  U  U  V  V  w"
    shows "locally P S"
using assms by (force simp: locally_def)

lemma locallyE:
  assumes "locally P S" "openin (top_of_set S) w" " w"
  obtains U V where "openin (top_of_set S) U" "P V" " U" " V" " w"
  using assms unfolding locally_def by meson

lemma locally_mono:
  assumes "locally P S" "T. P T ==> Q T"
    shows "locally Q S"
by (metis assms locally_def)

lemma locally_open_subset:
  assumes "locally P S" "openin (top_of_set S) t"
    shows "locally P t"
  by (smt (verit, ccfv_SIG) assms order.trans locally_def openin_imp_subset openin_subset_trans openin_trans)

lemma locally_diff_closed:
    "[locally P S; closedin (top_of_set S) t] ==> locally P (S - t)"
  using locally_open_subset closedin_def by fastforce

lemma locally_empty [iff]: "locally P {}"
  by (simp add: locally_def openin_subtopology)

lemma locally_singleton [iff]:
  fixes a :: "'a::metric_space"
  shows "locally P {a}  P {a}"
proof -
  have "x::real. ¬ 0 < x ==> P {a}"
    using zero_less_one by blast
  then show ?thesis
    unfolding locally_def
    by (auto simp: openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR)
qed

lemma locally_iff:
    "locally P S 
     (T x. open T  x  S  T  (U. open U  (V. P V  x  S  U  S  U  V  V  S  T)))"
  by (smt (verit) locally_def openin_open)

lemma locally_Int:
  assumes S: "locally P S" and T: "locally P T"
      and P: "S T. P S  P T ==> P(S  T)"
  shows "locally P (S  T)"
  unfolding locally_iff
proof clarify
  fix A x
  assume "open A" " A" " S" " T"
  then obtain U1 V1 U2 V2
    where "open U1" "P V1" " S  U1" " U1  V1  V1  S  A"
          "open U2" "P V2" " T  U2" " U2  V2  V2  T  A"
    using S T unfolding locally_iff by (meson IntI)
  then have " T  (U1  U2)  V1  V2" "V1  V2  S  T  A" " S  T  (U1  U2)"
    by blast+
  moreover have "P (V1  V2)"
    by (simp add: P P V1 P V2)
  ultimately show "U. open U  (V. P V  x  S  T  U  S  T  U  V  V  S  T  A)"
    using open U1 open U2 by blast
qed


lemma locally_Times:
  fixes S :: "('a::metric_space) set" and T :: "('b::metric_space) set"
  assumes PS: "locally P S" and QT: "locally Q T" and R: "S T. P S  Q T ==> R(S × T)"
  shows "locally R (S × T)"
    unfolding locally_def
proof (clarify)
  fix W x y
  assume W: "openin (top_of_set (S × T)) W" and xy: "(x, y)  W"
  then obtain U V where "openin (top_of_set S) U" " U"
                        "openin (top_of_set T) V" " V" "× V  W"
    using Times_in_interior_subtopology by metis
  then obtain U1 U2 V1 V2
         where opeS: "openin (top_of_set S) U1  P U2  x  U1  U1  U2  U2  U"
           and opeT: "openin (top_of_set T) V1  Q V2  y  V1  V1  V2  V2  V"
    by (meson PS QT locallyE)
  then have "openin (top_of_set (S × T)) (U1 × V1)"
    by (simp add: openin_Times)
  moreover have "R (U2 × V2)"
    by (simp add: R opeS opeT)
  moreover have "U1 × V1  U2 × V2  U2 × V2  W"
    using opeS opeT U × V W by auto
  ultimately show "U V. openin (top_of_set (S × T)) U  R V  (x,y)  U  U  V  V  W"
    using opeS opeT by auto
qed


proposition homeomorphism_locally_imp:
  fixes S :: "'a::metric_space set" and T :: "'b::t2_space set"
  assumes S: "locally P S" and hom: "homeomorphism S T f g"
      and Q: "S S'. [P S; homeomorphism S S' f g] ==> Q S'"
    shows "locally Q T"
proof (clarsimp simp: locally_def)
  fix W y
  assume " W" and "openin (top_of_set T) W"
  then obtain A where T: "open A" "W = T  A"
    by (force simp: openin_open)
  then have " T" by auto
  have f: "x. x  S ==> g(f x) = x" "f ` S = T" "continuous_on S f"
   and g: "y. y  T ==> f(g y) = y" "g ` T = S" "continuous_on T g"
    using hom by (auto simp: homeomorphism_def)
  have gw: "g ` W = S  f -` W"
    using W T g by force
  have "openin (top_of_set S) (g ` W)"
    using openin (top_of_set T) W continuous_on_open f gw by auto
  then obtain U V
    where osu: "openin (top_of_set S) U" and uv: "P V" "g y  U" " V" " g ` W"
    by (metis S y W image_eqI locallyE)
  have " S" using uv by (simp add: gw)
  have fv: "f ` V = T  {x. g x  V}"
    using f ` S = T f V S by auto
  have contvf: "continuous_on V f"
    using V S continuous_on_subset f(3) by blast
  have "openin (top_of_set (g ` T)) U"
    using g ` T = S by (simp add: osu)
  then have "openin (top_of_set T) (T  g -` U)"
    using continuous_on T g continuous_on_open [THEN iffD1] by blast
  moreover have "V. Q V  y  (T  g -` U)  (T  g -` U)  V  V  W"
  proof (intro exI conjI)
    show "f ` V  W"
      using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto
    then have contvg: "continuous_on (f ` V) g"
      using W T continuous_on_subset [OF g(3)] by blast
    have " g ` f ` V"
      by (metis V S hom homeomorphism_def homeomorphism_of_subsets order_refl)
    then have homv: "homeomorphism V (f ` V) f g"
      using V S f by (auto simp: homeomorphism_def contvf contvg)
    show "Q (f ` V)"
      using Q homv P V by blast
    show " T  g -` U"
      using T(2) y W g y U by blast
    show " g -` U  f ` V"
      using g(1) image_iff uv(3) by fastforce
  qed
  ultimately show "U. openin (top_of_set T) U  (v. Q v  y  U  U  v  v  W)"
    by meson
qed

lemma homeomorphism_locally:
  fixes f:: "'a::metric_space ==> 'b::metric_space"
  assumes "homeomorphism S T f g"
      and "S T. homeomorphism S T f g ==> (P S  Q T)"
    shows "locally P S  locally Q T"
  by (smt (verit) assms homeomorphism_locally_imp homeomorphism_symD)

lemma homeomorphic_locally:
  fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
  assumes hom: "S homeomorphic T"
          and iff: "X Y. X homeomorphic Y ==> (P X  Q Y)"
    shows "locally P S  locally Q T"
  by (smt (verit, ccfv_SIG) hom homeomorphic_def homeomorphism_locally homeomorphism_locally_imp iff)

lemma homeomorphic_local_compactness:
  fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
  shows "S homeomorphic T ==> locally compact S  locally compact T"
  by (simp add: homeomorphic_compactness homeomorphic_locally)

lemma locally_translation:
  fixes P :: "'a :: real_normed_vector set ==> bool"
  shows "(S. P ((+) a ` S) = P S) ==> locally P ((+) a ` S) = locally P S"
  using homeomorphism_locally [OF homeomorphism_translation]
  by (metis (full_types) homeomorphism_image2)

lemma locally_injective_linear_image:
  fixes f :: "'a::euclidean_space ==> 'b::euclidean_space"
  assumes f: "linear f" "inj f" and iff: "S. P (f ` S)  Q S"
  shows "locally P (f ` S)  locally Q S"
  by (smt (verit) f homeomorphism_image2 homeomorphism_locally iff linear_homeomorphism_image)

lemma locally_open_map_image:
  fixes f :: "'a::real_normed_vector ==> 'b::real_normed_vector"
  assumes P: "locally P S"
      and f: "continuous_on S f"
      and oo: "T. openin (top_of_set S) T ==> openin (top_of_set (f ` S)) (f ` T)"
      and Q: "T. [ S; P T] ==> Q(f ` T)"
    shows "locally Q (f ` S)"
proof (clarsimp simp: locally_def)
  fix W y
  assume oiw: "openin (top_of_set (f ` S)) W" and " W"
  then have " f ` S" by (simp add: openin_euclidean_subtopology_iff)
  have oivf: "openin (top_of_set S) (S  f -` W)"
    by (rule continuous_on_open [THEN iffD1, rule_format, OF f oiw])
  then obtain x where " S" "f x = y"
    using W f ` S y W by blast
  then obtain U V
    where "openin (top_of_set S) U" "P V" " U" " V" " S  f -` W"
    by (metis IntI P y W locallyE oivf vimageI)
  then have "openin (top_of_set (f ` S)) (f ` U)"
    by (simp add: oo)
  then show "X. openin (top_of_set (f ` S)) X  (Y. Q Y  y  X  X  Y  Y  W)"
    using Q P V U V V S f -` W f x = y x U by blast
qed


subsectionAn induction principle for connected sets

proposition connected_induction:
  assumes "connected S"
      and opD: "T a. [openin (top_of_set S) T; a  T] ==> z. z  T  P z"
      and opI: "a. a  S
             ==> T. openin (top_of_set S) T  a  T 
                     ( T.  T. P x  P y  Q x  Q y)"
      and etc: " S" " S" "P a" "P b" "Q a"
    shows "Q b"
proof -
  let ?A = "{b. T. openin (top_of_set S) T  b  T  (xT. P x  Q x)}"
  let ?B = "{b. T. openin (top_of_set S) T  b  T  (xT. P x  ¬ Q x)}"
  have "?A  ?B = {}"
    by (clarsimp simp: set_eq_iff) (metis (no_types, opaque_lifting) Int_iff opD openin_Int)
  moreover have " ?A  ?B"
    by clarsimp (meson opI)
  moreover have "openin (top_of_set S) ?A"
    by (subst openin_subopen, blast)
  moreover have "openin (top_of_set S) ?B"
    by (subst openin_subopen, blast)
  ultimately have "?A = {}  ?B = {}"
    by (metis (no_types, lifting) connected S connected_openin)
  then show ?thesis
    by clarsimp (meson opI etc)
qed

lemma connected_equivalence_relation_gen:
  assumes "connected S"
      and etc: " S" " S" "P a" "P b"
      and trans: "x y z. [R x y; R y z] ==> R x z"
      and opD: "T a. [openin (top_of_set S) T; a  T] ==> z. z  T  P z"
      and opI: "a. a  S
             ==> T. openin (top_of_set S) T  a  T 
                     ( T.  T. P x  P y  R x y)"
    shows "R a b"
proof -
  have "a b c. [ S; P a; b  S; c  S; P b; P c; R a b] ==> R a c"
    apply (rule connected_induction [OF connected S opD], simp_all)
    by (meson trans opI)
  then show ?thesis by (metis etc opI)
qed

lemma connected_induction_simple:
  assumes "connected S"
      and etc: " S" " S" "P a"
      and opI: "a. a  S
             ==> T. openin (top_of_set S) T  a  T 
                     ( T.  T. P x  P y)"
    shows "P b"
  by (rule connected_induction [OF connected S _, where P = "λx. True"])
     (use opI etc in auto)

lemma connected_equivalence_relation:
  assumes "connected S"
      and etc: " S" " S"
      and sym: "x y. [R x y; x  S; y  S] ==> R y x"
      and trans: "x y z. [R x y; R y z; x  S; y  S; z  S] ==> R x z"
      and opI: "a. a  S ==> T. openin (top_of_set S) T  a  T  ( T. R a x)"
    shows "R a b"
proof -
  have "a b c. [ S; b  S; c  S; R a b] ==> R a c"
    by (smt (verit, ccfv_threshold) connected_induction_simple [OF connected S]
            assms openin_imp_subset subset_eq)
  then show ?thesis by (metis etc opI)
qed

lemma locally_constant_imp_constant:
  assumes "connected S"
      and opI: "a. a  S
             ==> T. openin (top_of_set S) T  a  T  ( T. f x = f a)"
    shows "f constant_on S"
proof -
  have "x y. x  S ==> y  S ==> f x = f y"
    apply (rule connected_equivalence_relation [OF connected S], simp_all)
    by (metis opI)
  then show ?thesis
    by (metis constant_on_def)
qed

lemma locally_constant:
  assumes "connected S"
  shows "locally (λU. f constant_on U) S  f constant_on S" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (smt (verit, del_insts) assms constant_on_def locally_constant_imp_constant locally_def openin_subtopology_self subset_iff)
next
  assume ?rhs then show ?lhs
    by (metis constant_on_subset locallyI openin_imp_subset order_refl)
qed


subsectionBasic properties of local compactness

proposition locally_compact:
  fixes S :: "'a :: metric_space set"
  shows
    "locally compact S 
     ( S. u v. x  u  u  v  v  S 
                    openin (top_of_set S) u  compact v)"
     (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (meson locallyE openin_subtopology_self)
next
  assume r [rule_format]: ?rhs
  have *: "u v.
              openin (top_of_set S) u 
              compact v  x  u  u  v  v  S  T"
          if "open T" " S" " T" for x T
  proof -
    obtain U V where uv: " U" " V" " S" "compact V" "openin (top_of_set S) U"
      using r [OF x S] by auto
    obtain e where "e>0" and e: "cball x e  T"
      using open_contains_cball open T x T by blast
    show ?thesis
      apply (rule_tac x="(S  ball x e)  U" in exI)
      apply (rule_tac x="cball x e  V" in exI)
      using that e > 0 e uv
      apply auto
      done
  qed
  show ?lhs
    by (rule locallyI) (metis "*" Int_iff openin_open)
qed

lemma locally_compactE:
  fixes S :: "'a :: metric_space set"
  assumes "locally compact S"
  obtains u v where "x. x  S ==> x  u x  u x  v x  v x  S 
                             openin (top_of_set S) (u x)  compact (v x)"
  using assms unfolding locally_compact by metis

lemma locally_compact_alt:
  fixes S :: "'a :: heine_borel set"
  shows "locally compact S 
         ( S. U. x  U 
                    openin (top_of_set S) U  compact(closure U)  closure U  S)"
  by (smt (verit, ccfv_threshold) bounded_subset closure_closed closure_mono closure_subset
      compact_closure compact_imp_closed order.trans locally_compact)

lemma locally_compact_Int_cball:
  fixes S :: "'a :: heine_borel set"
  shows "locally compact S  ( S. e. 0 < e  closed(cball x e  S))"
        (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then have "x U V e. [ V; V  S; compact V; 0 < e; cball x e  S  U]
       ==> closed (cball x e  S)"
    by (metis compact_Int compact_cball compact_imp_closed inf.absorb_iff2 inf.assoc inf.orderE)
  with L show ?rhs
    by (meson locally_compactE openin_contains_cball)
next
  assume R: ?rhs
  show ?lhs unfolding locally_compact
  proof
    fix x
    assume " S"
    then obtain e where "e>0" and "compact (cball x e  S)"
      by (metis Int_commute compact_Int_closed compact_cball inf.right_idem R)
    moreover have "yball x e  S. ε>0. cball y ε  S  ball x e"
      by (meson Elementary_Metric_Spaces.open_ball IntD1 le_infI1 open_contains_cball_eq)
    moreover have "openin (top_of_set S) (ball x e  S)"
      by (simp add: inf_commute openin_open_Int)
    ultimately show "U V. x  U  U  V  V  S  openin (top_of_set S) U  compact V"
      by (metis Int_iff 0 < e x S ball_subset_cball centre_in_ball inf_commute inf_le1 inf_mono order_refl)
  qed
qed

lemma locally_compact_compact:
  fixes S :: "'a :: heine_borel set"
  shows "locally compact S 
         (K. K  S  compact K
               (U V. K  U  U  V  V  S 
                         openin (top_of_set S) U  compact V))"
        (is "?lhs = ?rhs")
proof
  assume ?lhs
  then obtain u v where
    uv: "x. x  S ==> x  u x  u x  v x  v x  S 
                             openin (top_of_set S) (u x)  compact (v x)"
    by (metis locally_compactE)
  have *: "U V. K  U  U  V  V  S  openin (top_of_set S) U  compact V"
          if " S" "compact K" for K
  proof -
    have "C. (cC. openin (top_of_set K) c)  K  ==>
                    DC. finite D  K  D"
      using that by (simp add: compact_eq_openin_cover)
    moreover have " (λx. K  u x) ` K. openin (top_of_set K) c"
      using that by clarify (metis subsetD inf.absorb_iff2 openin_subset openin_subtopology_Int_subset topspace_euclidean_subtopology uv)
    moreover have " ((λx. K  u x) ` K)"
      using that by clarsimp (meson subsetCE uv)
    ultimately obtain D where " (λx. K  u x) ` K" "finite D" " D"
      by metis
    then obtain T where T: " K" "finite T" " ((λx. K  u x) ` T)"
      by (metis finite_subset_image)
    have Tuv: "(u ` T)  (v ` T)"
      using T that by (force dest!: uv)
    moreover
    have "openin (top_of_set S) ( (u ` T))"
      using T that uv by fastforce
    moreover
    obtain "compact ( (v ` T))" " (v ` T)  S"
      by (metis T UN_subset_iff K S compact_UN subset_iff uv)
    ultimately show ?thesis
      using T by auto
  qed
  show ?rhs
    by (blast intro: *)
next
  assume ?rhs
  then show ?lhs
    apply (clarsimp simp: locally_compact)
    apply (drule_tac x="{x}" in spec, simp)
    done
qed

lemma open_imp_locally_compact:
  fixes S :: "'a :: heine_borel set"
  assumes "open S"
    shows "locally compact S"
proof -
  have *: "U V. x  U  U  V  V  S  openin (top_of_set S) U  compact V"
          if " S" for x
  proof -
    obtain e where "e>0" and e: "cball x e  S"
      using open_contains_cball assms x S by blast
    have ope: "openin (top_of_set S) (ball x e)"
      by (meson e open_ball ball_subset_cball dual_order.trans open_subset)
    show ?thesis
      by (meson 0 < e ball_subset_cball centre_in_ball compact_cball e ope)
  qed
  show ?thesis
    unfolding locally_compact by (blast intro: *)
qed

lemma closed_imp_locally_compact:
  fixes S :: "'a :: heine_borel set"
  assumes "closed S"
    shows "locally compact S"
proof -
  have *: "U V. x  U  U  V  V  S  openin (top_of_set S) U  compact V"
          if " S" for x
    apply (rule_tac x = " ball x 1" in exI, rule_tac x = " cball x 1" in exI)
    using x S assms by auto
  show ?thesis
    unfolding locally_compact by (blast intro: *)
qed

lemma locally_compact_UNIV: "locally compact (UNIV :: 'a :: heine_borel set)"
  by (simp add: closed_imp_locally_compact)

lemma locally_compact_Int:
  fixes S :: "'a :: t2_space set"
  shows "[locally compact S; locally compact T] ==> locally compact (S  T)"
  by (simp add: compact_Int locally_Int)

lemma locally_compact_closedin:
  fixes S :: "'a :: heine_borel set"
  shows "[closedin (top_of_set S) T; locally compact S]
        ==> locally compact T"
  unfolding closedin_closed
  using closed_imp_locally_compact locally_compact_Int by blast

lemma locally_compact_delete:
     fixes S :: "'a :: t1_space set"
     shows "locally compact S ==> locally compact (S - {a})"
  by (auto simp: openin_delete locally_open_subset)

lemma locally_closed:
  fixes S :: "'a :: heine_borel set"
  shows "locally closed S  locally compact S"
        (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    unfolding locally_def
    apply (elim all_forward imp_forward asm_rl exE)
    apply (rename_tac U V)
    apply (rule_tac x = " ball x 1" in exI)
    apply (rule_tac x = " cball x 1" in exI)
    apply (force intro: openin_trans)
    done
next
  assume ?rhs then show ?lhs
    using compact_eq_bounded_closed locally_mono by blast
qed

lemma locally_compact_openin_Un:
  fixes S :: "'a::euclidean_space set"
  assumes LCS: "locally compact S" and LCT: "locally compact T"
      and opS: "openin (top_of_set (S  T)) S"
      and opT: "openin (top_of_set (S  T)) T"
    shows "locally compact (S  T)"
proof -
  have "e>0. closed (cball x e  (S  T))" if " S" for x
  proof -
    obtain e1 where "e1 > 0" and e1: "closed (cball x e1  S)"
      using LCS x S unfolding locally_compact_Int_cball by blast
    moreover obtain e2 where "e2 > 0" and e2: "cball x e2  (S  T)  S"
      by (meson x S opS openin_contains_cball)
    then have "cball x e2  (S  T) = cball x e2  S"
      by force
    ultimately have "closed (cball x (min e1 e2)  (S  T))"
      by (metis (no_types, lifting) cball_min_Int closed_Int closed_cball inf_assoc inf_commute)
    then show ?thesis
      by (metis 0 < e1 0 < e2 min_def)
  qed
  moreover have "e>0. closed (cball x e  (S  T))" if " T" for x
  proof -
    obtain e1 where "e1 > 0" and e1: "closed (cball x e1  T)"
      using LCT x T unfolding locally_compact_Int_cball by blast
    moreover obtain e2 where "e2 > 0" and e2: "cball x e2  (S  T)  T"
      by (meson x T opT openin_contains_cball)
    then have "cball x e2  (S  T) = cball x e2  T"
      by force
    moreover have "closed (cball x e1  (cball x e2  T))"
      by (metis closed_Int closed_cball e1 inf_left_commute)
    ultimately show ?thesis
      by (rule_tac x="min e1 e2" in exI) (simp add: 0 < e2 cball_min_Int inf_assoc)
  qed
  ultimately show ?thesis
    by (force simp: locally_compact_Int_cball)
qed

lemma locally_compact_closedin_Un:
  fixes S :: "'a::euclidean_space set"
  assumes LCS: "locally compact S" and LCT:"locally compact T"
      and clS: "closedin (top_of_set (S  T)) S"
      and clT: "closedin (top_of_set (S  T)) T"
    shows "locally compact (S  T)"
proof -
  have "e>0. closed (cball x e  (S  T))" if " S" " T" for x
  proof -
    obtain e1 where "e1 > 0" and e1: "closed (cball x e1  S)"
      using LCS x S unfolding locally_compact_Int_cball by blast
    moreover
    obtain e2 where "e2 > 0" and e2: "closed (cball x e2  T)"
      using LCT x T unfolding locally_compact_Int_cball by blast
    moreover have "closed (cball x (min e1 e2)  (S  T))"
      by (smt (verit) Int_Un_distrib2 Int_commute cball_min_Int closed_Int closed_Un closed_cball e1 e2 inf_left_commute)
    ultimately show ?thesis
      by (rule_tac x="min e1 e2" in exI) linarith
  qed
  moreover
  have "e>0. closed (cball x e  (S  T))" if x: " S" " T" for x
  proof -
    obtain e1 where "e1 > 0" and e1: "closed (cball x e1  S)"
      using LCS x S unfolding locally_compact_Int_cball by blast
    moreover
    obtain e2 where "e2>0" and "cball x e2  (S  T)  S - T"
      using clT x by (fastforce simp: openin_contains_cball closedin_def)
    then have "closed (cball x e2  T)"
    proof -
      have "{} = T - (T - cball x e2)"
        using Diff_subset Int_Diff cball x e2 (S T) S - T by auto
      then show ?thesis
        by (simp add: Diff_Diff_Int inf_commute)
    qed
    with e1 have "closed ((cball x e1  cball x e2)  (S  T))"
      apply (simp add: inf_commute inf_sup_distrib2)
      by (metis closed_Int closed_Un closed_cball inf_assoc inf_left_commute)
    then have "closed (cball x (min e1 e2)  (S  T))"
      by (simp add: cball_min_Int inf_commute)
    ultimately show ?thesis
      using 0 < e2 by (rule_tac x="min e1 e2" in exI) linarith
  qed
  moreover
  have "e>0. closed (cball x e  (S  T))" if x: " S" " T" for x
  proof -
    obtain e1 where "e1 > 0" and e1: "closed (cball x e1  T)"
      using LCT x T unfolding locally_compact_Int_cball by blast
    moreover
    obtain e2 where "e2>0" and "cball x e2  (S  T)  S  T - S"
      using clS x by (fastforce simp: openin_contains_cball closedin_def)
    then have "closed (cball x e2  S)"
      by (metis Diff_disjoint Int_empty_right closed_empty inf.left_commute inf.orderE inf_sup_absorb)
    with e1 have "closed ((cball x e1  cball x e2)  (S  T))"
      apply (simp add: inf_commute inf_sup_distrib2)
      by (metis closed_Int closed_Un closed_cball inf_assoc inf_left_commute)
    then have "closed (cball x (min e1 e2)  (S  T))"
      by (auto simp: cball_min_Int)
    ultimately show ?thesis
      using 0 < e2 by (rule_tac x="min e1 e2" in exI) linarith
  qed
  ultimately show ?thesis
    by (auto simp: locally_compact_Int_cball)
qed

lemma locally_compact_Times:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  shows "[locally compact S; locally compact T] ==> locally compact (S × T)"
  by (auto simp: compact_Times locally_Times)

lemma locally_compact_compact_subopen:
  fixes S :: "'a :: heine_borel set"
  shows
   "locally compact S 
    (K T. K  S  compact K  open T  K  T
           (U V. K  U  U  V  U  T  V  S 
                     openin (top_of_set S) U  compact V))"
   (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  show ?rhs
  proof clarify
    fix K :: "'a set" and T :: "'a set"
    assume " S" and "compact K" and "open T" and " T"
    obtain U V where " U" " V" " S" "compact V"
                 and ope: "openin (top_of_set S) U"
      using L unfolding locally_compact_compact by (meson K S compact K)
    show "U V. K  U  U  V  U  T  V  S 
                openin (top_of_set S) U  compact V"
    proof (intro exI conjI)
      show " U  T"
        by (simp add: K T K U)
      show " T  closure(U  T)"
        by (rule closure_subset)
      show "closure (U  T)  S"
        by (metis U V V S compact V closure_closed closure_mono compact_imp_closed inf.cobounded1 subset_trans)
      show "openin (top_of_set S) (U  T)"
        by (simp add: open T ope openin_Int_open)
      show "compact (closure (U  T))"
        by (meson Int_lower1 U V compact V bounded_subset compact_closure compact_eq_bounded_closed)
    qed auto
  qed
next
  assume ?rhs then show ?lhs
    unfolding locally_compact_compact
    by (metis open_openin openin_topspace subtopology_superset top.extremum topspace_euclidean_subtopology)
qed


subsectionSura-Bura's results about compact components of sets

proposition Sura_Bura_compact:
  fixes S :: "'a::euclidean_space set"
  assumes "compact S" and C: " components S"
  shows "C = {T. C  T  openin (top_of_set S) T 
                           closedin (top_of_set S) T}"
         (is "C = ?T")
proof
  obtain x where x: "C = connected_component_set S x" and " S"
    using C by (auto simp: components_def)
  have " S"
    by (simp add: C in_components_subset)
  have "?T  connected_component_set S x"
  proof (rule connected_component_maximal)
    have " C"
      by (simp add: x S x)
    then show " ?T"
      by blast
    have clo: "closed (?T)"
      by (simp add: compact S closed_Inter closedin_compact_eq compact_imp_closed)
    have False
      if K1: "closedin (top_of_set (?T)) K1" and
         K2: "closedin (top_of_set (?T)) K2" and
         K12_Int: "K1  K2 = {}" and K12_Un: "K1  K2 = ?T" and "K1  {}" "K2  {}"
       for K1 K2
    proof -
      have "closed K1" "closed K2"
        using closedin_closed_trans clo K1 K2 by blast+
      then obtain V1 V2 where "open V1" "open V2" "K1  V1" "K2  V2" and V12: "V1  V2 = {}"
        using separation_normal K1 K2 = {} by metis
      have SV12_ne: "(S - (V1  V2))  (?T {}"
      proof (rule compact_imp_fip)
        show "compact (S - (V1  V2))"
          by (simp add: open V1 open V2 compact S compact_diff open_Un)
        show cloT: "closed T" if " ?T" for T
          using that compact S
          by (force intro: closedin_closed_trans simp add: compact_imp_closed)
        show "(S - (V1  V2))  F  {}" if "finite F" and F: "F  ?T" for F
        proof
          assume djo: "(S - (V1  V2))  F = {}"
          obtain D where opeD: "openin (top_of_set S) D"
                   and cloD: "closedin (top_of_set S) D"
                   and " D" and DV12: " V1  V2"
          proof (cases "F = {}")
            case True
            with C S djo that show ?thesis
              by force
          next
            case False show ?thesis
            proof
              show ope: "openin (top_of_set S) (F)"
                using openin_Inter finite F False F by blast
              then show "closedin (top_of_set S) (F)"
                by (meson cloT F closed_Inter closed_subset openin_imp_subset subset_eq)
              show " F"
                using F by auto
              show "F  V1  V2"
                using ope djo openin_imp_subset by fastforce
            qed
          qed
          have "connected C"
            by (simp add: x)
          have "closed D"
            using compact S cloD closedin_closed_trans compact_imp_closed by blast
          have cloV1: "closedin (top_of_set D) (D  closure V1)"
            and cloV2: "closedin (top_of_set D) (D  closure V2)"
            by (simp_all add: closedin_closed_Int)
          moreover have " closure V1 = D  V1" " closure V2 = D  V2"
            using D V1 V2 open V1 open V2 V12
            by (auto simp: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
          ultimately have cloDV1: "closedin (top_of_set D) (D  V1)"
                      and cloDV2: "closedin (top_of_set D) (D  V2)"
            by metis+
          then obtain U1 U2 where "closed U1" "closed U2"
               and D1: " V1 = D  U1" and D2: " V2 = D  U2"
            by (auto simp: closedin_closed)
          have " U1  C  {}"
          proof
            assume " U1  C = {}"
            then have *: " D  V2"
              using D1 DV12 C D by auto
            have 1: "openin (top_of_set S) (D  V2)"
              by (simp add: open V2 opeD openin_Int_open)
            have 2: "closedin (top_of_set S) (D  V2)"
              using cloD cloDV2 closedin_trans by blast
            have " ?T  D  V2"
              by (rule Inter_lower) (use * 1 2 in simp)
            then show False
              using K1 V12 K1 {} K1 V1 closedin_imp_subset by blast
          qed
          moreover have " U2  C  {}"
          proof
            assume " U2  C = {}"
            then have *: " D  V1"
              using D2 DV12 C D by auto
            have 1: "openin (top_of_set S) (D  V1)"
              by (simp add: open V1 opeD openin_Int_open)
            have 2: "closedin (top_of_set S) (D  V1)"
              using cloD cloDV1 closedin_trans by blast
            have "?T  D  V1"
              by (rule Inter_lower) (use * 1 2 in simp)
            then show False
              using K2 V12 K2 {} K2 V2 closedin_imp_subset by blast
          qed
          ultimately show False
            using connected C [unfolded connected_closed, simplified, rule_format, of concl: " U1" " U2"]
            using C D D1 D2 V12 DV12 closed U1 closed U2 closed D
            by blast
        qed
      qed
      show False
        by (metis (full_types) DiffE UnE Un_upper2 SV12_ne K1 V1 K2 V2 disjoint_iff_not_equal subsetCE sup_ge1 K12_Un)
    qed
    then show "connected (?T)"
      by (auto simp: connected_closedin_eq)
    show "?T  S"
      by (fastforce simp: C in_components_subset)
  qed
  with x show "?T  C" by simp
qed auto


corollary Sura_Bura_clopen_subset:
  fixes S :: "'a::euclidean_space set"
  assumes S: "locally compact S" and C: " components S" and "compact C"
      and U: "open U" " U"
  obtains K where "openin (top_of_set S) K" "compact K" " K" " U"
proof (rule ccontr)
  assume "¬ thesis"
  with that have neg: "K. openin (top_of_set S) K  compact K  C  K  K  U"
    by metis
  obtain V K where " V" " U" " K" " S" "compact K"
               and opeSV: "openin (top_of_set S) V"
    using S U compact C by (meson C in_components_subset locally_compact_compact_subopen)
  let ?T = "{T. C  T  openin (top_of_set K) T  compact T  T  K}"
  have CK: " components K"
    by (meson C C V K S V K components_intermediate_subset subset_trans)
  with compact K
  have "C = {T. C  T  openin (top_of_set K) T  closedin (top_of_set K) T}"
    by (simp add: Sura_Bura_compact)
  then have Ceq: "C = ?T"
    by (simp add: closedin_compact_eq compact K)
  obtain W where "open W" and W: "V = S  W"
    using opeSV by (auto simp: openin_open)
  have "-(U  W)  ?T  {}"
  proof (rule closed_imp_fip_compact)
    show "- (U  W)  F  {}"
      if "finite F" and F: "F  ?T" for F
    proof (cases "F = {}")
      case True
      have False if "U = UNIV" "W = UNIV"
      proof -
        have "V = S"
          by (simp add: W W = UNIV)
        with neg show False
          using C V K S V K V U compact K by auto
      qed
      with True show ?thesis
        by auto
    next
      case False
      show ?thesis
      proof
        assume "- (U  W)  F = {}"
        then have FUW: "F  U  W"
          by blast
        have " F"
          using F by auto
        moreover have "compact (F)"
          by (metis (no_types, lifting) compact_Inter False mem_Collect_eq subsetCE F)
        moreover have "F  K"
          using False that(2) by fastforce
        moreover have opeKF: "openin (top_of_set K) (F)"
          using False F finite F by blast
        then have opeVF: "openin (top_of_set V) (F)"
          using W K S V K opeKF F K FUW openin_subset_trans by fastforce
        then have "openin (top_of_set S) (F)"
          by (metis opeSV openin_trans)
        moreover have "F  U"
          by (meson V U opeVF dual_order.trans openin_imp_subset)
        ultimately show False
          using neg by blast
      qed
    qed
  qed (use open W open U in auto)
  with W Ceq C V C U show False
    by auto
qed


corollary Sura_Bura_clopen_subset_alt:
  fixes S :: "'a::euclidean_space set"
  assumes S: "locally compact S" and C: " components S" and "compact C"
      and opeSU: "openin (top_of_set S) U" and " U"
  obtains K where "openin (top_of_set S) K" "compact K" " K" " U"
proof -
  obtain V where "open V" "U = S  V"
    using opeSU by (auto simp: openin_open)
  with C U have " V"
    by auto
  then show ?thesis
    using Sura_Bura_clopen_subset [OF S C compact C open V]
    by (metis U = S V inf.bounded_iff openin_imp_subset that)
qed

corollary Sura_Bura:
  fixes S :: "'a::euclidean_space set"
  assumes "locally compact S" " components S" "compact C"
  shows "C =  {K. C  K  compact K  openin (top_of_set S) K}"
         (is "C = ?rhs")
proof
  show "?rhs  C"
  proof (clarsimp, rule ccontr)
    fix x
    assume *: "X. C  X  compact X  openin (top_of_set S) X  x  X"
      and " C"
    obtain U V where "open U" "open V" "{x}  U" " V" " V = {}"
      using separation_normal [of "{x}" C]
      by (metis Int_empty_left x C compact C closed_empty closed_insert compact_imp_closed insert_disjoint(1))
    have " V"
      using U V = {} {x} U by blast
    then show False
      by (meson "*" Sura_Bura_clopen_subset C V open V assms(1) assms(2) assms(3) subsetCE)
  qed
qed blast


subsectionSpecial cases of local connectedness and path connectedness

lemma locally_connected_1:
  assumes
    "V x. [openin (top_of_set S) V; x  V] ==> U. openin (top_of_set S) U  connected U  x  U  U  V"
   shows "locally connected S"
  by (metis assms locally_def)

lemma locally_connected_2:
  assumes "locally connected S"
          "openin (top_of_set S) t"
          " t"
   shows "openin (top_of_set S) (connected_component_set t x)"
proof -
  { fix y :: 'a
    let ?SS = "top_of_set S"
    assume 1: "openin ?SS t"
              "w x. openin ?SS w  x  w  (u. openin ?SS u  (v. connected v  x  u  u  v  v  w))"
    and "connected_component t x y"
    then have " t" and y: " connected_component_set t x"
      using connected_component_subset by blast+
    obtain F where
      "x y. (w. openin ?SS w  (u. connected u  x  w  w  u  u  y)) = (openin ?SS (F x y)  (u. connected u   F x y  F x y  u  u  y))"
      by moura
    then obtain G where
       "a A. (U. openin ?SS U  (V. connected V  a  U  U  V  V  A)) = (openin ?SS (F a A)  connected (G a A)   F a A  F a A  G a A  G a A  A)"
      by moura
    then have *: "openin ?SS (F y t)  connected (G y t)  y  F y t  F y t  G y t  G y t  t"
      using 1 y t by presburger
    have "G y t  connected_component_set t y"
      by (metis (no_types) * connected_component_eq_self connected_component_mono contra_subsetD)
    then have "A. openin ?SS A  y  A  A  connected_component_set t x"
      by (metis (no_types) * connected_component_eq dual_order.trans y)
  }
  then show ?thesis
    using assms openin_subopen by (force simp: locally_def)
qed

lemma locally_connected_3:
  assumes "t x. [openin (top_of_set S) t; x  t]
              ==> openin (top_of_set S)
                          (connected_component_set t x)"
          "openin (top_of_set S) v" " v"
   shows "u. openin (top_of_set S) u  connected u  x  u  u  v"
using assms connected_component_subset by fastforce

lemma locally_connected:
  "locally connected S 
   (v x. openin (top_of_set S) v  x  v
           (u. openin (top_of_set S) u  connected u  x  u  u  v))"
by (metis locally_connected_1 locally_connected_2 locally_connected_3)

lemma locally_connected_open_connected_component:
  "locally connected S 
   (t x. openin (top_of_set S) t  x  t
           openin (top_of_set S) (connected_component_set t x))"
by (metis locally_connected_1 locally_connected_2 locally_connected_3)

lemma locally_path_connected_1:
  assumes
    "v x. [openin (top_of_set S) v; x  v]
              ==> u. openin (top_of_set S) u  path_connected u  x  u  u  v"
   shows "locally path_connected S"
  by (force simp: locally_def dest: assms)

lemma locally_path_connected_2:
  assumes "locally path_connected S"
          "openin (top_of_set S) t"
          " t"
   shows "openin (top_of_set S) (path_component_set t x)"
proof -
  { fix y :: 'a
    let ?SS = "top_of_set S"
    assume 1: "openin ?SS t"
              "w x. openin ?SS w  x  w  (u. openin ?SS u  (v. path_connected v  x  u  u  v  v  w))"
    and "path_component t x y"
    then have " t" and y: " path_component_set t x"
      using path_component_mem(2) by blast+
    obtain F where
      "x y. (w. openin ?SS w  (u. path_connected u  x  w  w  u  u  y)) = (openin ?SS (F x y)  (u. path_connected u  x  F x y  F x y  u  u  y))"
      by moura
    then obtain G where
       "a A. (U. openin ?SS U  (V. path_connected V  a  U  U  V  V  A)) = (openin ?SS (F a A)  path_connected (G a A)  a  F a A  F a A  G a A  G a A  A)"
      by moura
    then have *: "openin ?SS (F y t)  path_connected (G y t)  y  F y t  F y t  G y t  G y t  t"
      using 1 y t by presburger
    have "G y t  path_component_set t y"
      using * path_component_maximal rev_subsetD by blast
    then have "A. openin ?SS A  y  A  A  path_component_set t x"
      by (metis "*" G y t path_component_set t y dual_order.trans path_component_eq y)
  }
  then show ?thesis
    using assms openin_subopen by (force simp: locally_def)
qed

lemma locally_path_connected_3:
  assumes "t x. [openin (top_of_set S) t; x  t]
              ==> openin (top_of_set S) (path_component_set t x)"
          "openin (top_of_set S) v" " v"
   shows "u. openin (top_of_set S) u  path_connected u  x  u  u  v"
proof -
  have "path_component v x x"
    by (meson assms(3) path_component_refl)
  then show ?thesis
    by (metis assms mem_Collect_eq path_component_subset path_connected_path_component)
qed

proposition locally_path_connected:
  "locally path_connected S 
   (V x. openin (top_of_set S) V  x  V
           (U. openin (top_of_set S) U  path_connected U  x  U  U  V))"
  by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)

proposition locally_path_connected_open_path_component:
  "locally path_connected S 
   (t x. openin (top_of_set S) t  x  t
           openin (top_of_set S) (path_component_set t x))"
  by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)

lemma locally_connected_open_component:
  "locally connected S 
   (t c. openin (top_of_set S) t  c  components t
           openin (top_of_set S) c)"
by (metis components_iff locally_connected_open_connected_component)

proposition locally_connected_im_kleinen:
  "locally connected S 
   (v x. openin (top_of_set S) v  x  v
        (u. openin (top_of_set S) u 
                x  u  u  v 
                (y. y  u  (c. connected c  c  v  x  c  y  c))))"
   (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (fastforce simp: locally_connected)
next
  assume ?rhs
  have *: "T. openin (top_of_set S) T  x  T  T  c"
       if "openin (top_of_set S) t" and c: " components t" and " c" for t c x
  proof -
    from that ?rhs [rule_format, of t x]
    obtain u where u:
      "openin (top_of_set S) u  x  u  u  t 
       (y. y  u  (c. connected c  c  t  x  c  y  c))"
      using in_components_subset by auto
    obtain F :: "'a set ==> 'a set ==> 'a" where
      "x y. (z. z  x  y = connected_component_set x z) = (F x y  x  y = connected_component_set x (F x y))"
      by moura
    then have F: "F t c  t  c = connected_component_set t (F t c)"
      by (meson components_iff c)
    obtain G :: "'a set ==> 'a set ==> 'a" where
        G: "x y. (z. z  y  z  x) = (G x y  y  G x y  x)"
      by moura
     have "G c u  u  G c u  c"
      using F by (metis (full_types) u connected_componentI connected_component_eq mem_Collect_eq that(3))
    then show ?thesis
      using G u by auto
  qed
  show ?lhs
    unfolding locally_connected_open_component by (meson "*" openin_subopen)
qed

proposition locally_path_connected_im_kleinen:
  "locally path_connected S 
   (v x. openin (top_of_set S) v  x  v
        (u. openin (top_of_set S) u 
                x  u  u  v 
                (y. y  u  (p. path p  path_image p  v 
                                pathstart p = x  pathfinish p = y))))"
   (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    apply (simp add: locally_path_connected path_connected_def)
    apply (erule all_forward ex_forward imp_forward conjE | simp)+
    by (meson dual_order.trans)
next
  assume ?rhs
  have *: "T. openin (top_of_set S) T 
               x  T  T  path_component_set u z"
       if "openin (top_of_set S) u" and " u" and c: "path_component u z x" for u z x
  proof -
    have " u"
      by (meson c path_component_mem(2))
    with that ?rhs [rule_format, of u x]
    obtain U where U:
      "openin (top_of_set S) U  x  U  U  u 
       (y. y  U  (p. path p  path_image p  u  pathstart p = x  pathfinish p = y))"
       by blast
    show ?thesis
      by (metis U c mem_Collect_eq path_component_def path_component_eq subsetI)
  qed
  show ?lhs
    unfolding locally_path_connected_open_path_component
    using "*" openin_subopen by fastforce
qed

lemma locally_path_connected_imp_locally_connected:
  "locally path_connected S ==> locally connected S"
using locally_mono path_connected_imp_connected by blast

lemma locally_connected_components:
  "[locally connected S; c  components S] ==> locally connected c"
by (meson locally_connected_open_component locally_open_subset openin_subtopology_self)

lemma locally_path_connected_components:
  "[locally path_connected S; c  components S] ==> locally path_connected c"
by (meson locally_connected_open_component locally_open_subset locally_path_connected_imp_locally_connected openin_subtopology_self)

lemma locally_path_connected_connected_component:
  "locally path_connected S ==> locally path_connected (connected_component_set S x)"
by (metis components_iff connected_component_eq_empty locally_empty locally_path_connected_components)

lemma open_imp_locally_path_connected:
  fixes S :: "'a :: real_normed_vector set"
  assumes "open S"
  shows "locally path_connected S"
proof (rule locally_mono)
  show "locally convex S"
    using assms unfolding locally_def
    by (meson open_ball centre_in_ball convex_ball openE open_subset openin_imp_subset openin_open_trans subset_trans)
  show "T::'a set. convex T ==> path_connected T"
    using convex_imp_path_connected by blast
qed

lemma open_imp_locally_connected:
  fixes S :: "'a :: real_normed_vector set"
  shows "open S ==> locally connected S"
by (simp add: locally_path_connected_imp_locally_connected open_imp_locally_path_connected)

lemma locally_path_connected_UNIV: "locally path_connected (UNIV::'a :: real_normed_vector set)"
  by (simp add: open_imp_locally_path_connected)

lemma locally_connected_UNIV: "locally connected (UNIV::'a :: real_normed_vector set)"
  by (simp add: open_imp_locally_connected)

lemma openin_connected_component_locally_connected:
    "locally connected S
     ==> openin (top_of_set S) (connected_component_set S x)"
  by (metis connected_component_eq_empty locally_connected_2 openin_empty openin_subtopology_self)

lemma openin_components_locally_connected:
    "[locally connected S; c  components S] ==> openin (top_of_set S) c"
  using locally_connected_open_component openin_subtopology_self by blast

lemma openin_path_component_locally_path_connected:
  "locally path_connected S
        ==> openin (top_of_set S) (path_component_set S x)"
by (metis (no_types) empty_iff locally_path_connected_2 openin_subopen openin_subtopology_self path_component_eq_empty)

lemma closedin_path_component_locally_path_connected:
  assumes "locally path_connected S"
  shows "closedin (top_of_set S) (path_component_set S x)"
proof -
  have "openin (top_of_set S) ( ({path_component_set S y |y. y  S} - {path_component_set S x}))"
    using locally_path_connected_2 assms by fastforce
  then show ?thesis
    by (simp add: closedin_def path_component_subset complement_path_component_Union)
qed

lemma convex_imp_locally_path_connected:
  fixes S :: "'a:: real_normed_vector set"
  assumes "convex S"
  shows "locally path_connected S"
proof (clarsimp simp: locally_path_connected)
  fix V x
  assume "openin (top_of_set S) V" and " V"
  then obtain T e where "V = S  T" " S" "0 < e" "ball x e  T"
    by (metis Int_iff openE openin_open)
  then have "openin (top_of_set S) (S  ball x e)" "path_connected (S  ball x e)"
    by (simp_all add: assms convex_Int convex_imp_path_connected openin_open_Int)
  then show "U. openin (top_of_set S) U  path_connected U  x  U  U  V"
    using 0 < e V = S T ball x e T x S by auto
qed

lemma convex_imp_locally_connected:
  fixes S :: "'a:: real_normed_vector set"
  shows "convex S ==> locally connected S"
  by (simp add: locally_path_connected_imp_locally_connected convex_imp_locally_path_connected)


subsectionRelations between components and path components

lemma path_component_eq_connected_component:
  assumes "locally path_connected S"
    shows "(path_component S x = connected_component S x)"
proof (cases " S")
  case True
  have "openin (top_of_set (connected_component_set S x)) (path_component_set S x)"
  proof (rule openin_subset_trans)
    show "openin (top_of_set S) (path_component_set S x)"
      by (simp add: True assms locally_path_connected_2)
    show "connected_component_set S x  S"
      by (simp add: connected_component_subset)
  qed (simp add: path_component_subset_connected_component)
  moreover have "closedin (top_of_set (connected_component_set S x)) (path_component_set S x)"
    proof (rule closedin_subset_trans [of S])
  show "closedin (top_of_set S) (path_component_set S x)"
    by (simp add: assms closedin_path_component_locally_path_connected)
  show "connected_component_set S x  S"
    by (simp add: connected_component_subset)
  qed (simp add: path_component_subset_connected_component)
  ultimately have *: "path_component_set S x = connected_component_set S x"
    by (metis connected_connected_component connected_clopen True path_component_eq_empty)
  then show ?thesis
    by blast
next
  case False then show ?thesis
    by (metis Collect_empty_eq_bot connected_component_eq_empty path_component_eq_empty)
qed

lemma path_component_eq_connected_component_set:
     "locally path_connected S ==> (path_component_set S x = connected_component_set S x)"
by (simp add: path_component_eq_connected_component)

lemma locally_path_connected_path_component:
     "locally path_connected S ==> locally path_connected (path_component_set S x)"
using locally_path_connected_connected_component path_component_eq_connected_component by fastforce

lemma open_path_connected_component:
  fixes S :: "'a :: real_normed_vector set"
  shows "open S ==> path_component S x = connected_component S x"
by (simp add: path_component_eq_connected_component open_imp_locally_path_connected)

lemma open_path_connected_component_set:
  fixes S :: "'a :: real_normed_vector set"
  shows "open S ==> path_component_set S x = connected_component_set S x"
by (simp add: open_path_connected_component)

proposition locally_connected_quotient_image:
  assumes lcS: "locally connected S"
      and oo: "T. T  f ` S
                ==> openin (top_of_set S) (S  f -` T) 
                    openin (top_of_set (f ` S)) T"
    shows "locally connected (f ` S)"
proof (clarsimp simp: locally_connected_open_component)
  fix U C
  assume opefSU: "openin (top_of_set (f ` S)) U" and " components U"
  then have " U" " f ` S"
    by (meson in_components_subset openin_imp_subset)+
  then have "openin (top_of_set (f ` S)) C 
             openin (top_of_set S) (S  f -` C)"
    by (auto simp: oo)
  moreover have "openin (top_of_set S) (S  f -` C)"
  proof (subst openin_subopen, clarify)
    fix x
    assume " S" "f x  C"
    show "T. openin (top_of_set S) T  x  T  T  (S  f -` C)"
    proof (intro conjI exI)
      show "openin (top_of_set S) (connected_component_set (S  f -` U) x)"
      proof (rule ccontr)
        assume **: "¬ openin (top_of_set S) (connected_component_set (S  f -` U) x)"
        then have " (S  f -` U)"
          using U f ` S opefSU lcS locally_connected_2 oo by blast
        with ** show False
          by (metis (no_types) connected_component_eq_empty empty_iff openin_subopen)
      qed
    next
      show " connected_component_set (S  f -` U) x"
        using C U f x C x S by auto
    next
      have contf: "continuous_on S f"
        by (simp add: continuous_on_open oo openin_imp_subset)
      then have "continuous_on (connected_component_set (S  f -` U) x) f"
        by (meson connected_component_subset continuous_on_subset inf.boundedE)
      then have "connected (f ` connected_component_set (S  f -` U) x)"
        by (rule connected_continuous_image [OF _ connected_connected_component])
      moreover have "f ` connected_component_set (S  f -` U) x  U"
        using connected_component_in by blast
      moreover have " f ` connected_component_set (S  f -` U) x  {}"
        using C U f x C x S by fastforce
      ultimately have fC: "f ` (connected_component_set (S  f -` U) x)  C"
        by (rule components_maximal [OF C components U])
      have cUC: "connected_component_set (S  f -` U) x  (S  f -` C)"
        using connected_component_subset fC by blast
      have "connected_component_set (S  f -` U) x  connected_component_set (S  f -` C) x"
      proof -
        { assume " connected_component_set (S  f -` U) x"
          then have ?thesis
            using cUC connected_component_idemp connected_component_mono by blast }
        then show ?thesis
          using connected_component_eq_empty by auto
      qed
      also have "  (S  f -` C)"
        by (rule connected_component_subset)
      finally show "connected_component_set (S  f -` U) x  (S  f -` C)" .
    qed
  qed
  ultimately show "openin (top_of_set (f ` S)) C"
    by metis
qed

textThe proof resembles that above but is not identical!
proposition locally_path_connected_quotient_image:
  assumes lcS: "locally path_connected S"
      and oo: "T. T  f ` S
                ==> openin (top_of_set S) (S  f -` T)  openin (top_of_set (f ` S)) T"
    shows "locally path_connected (f ` S)"
proof (clarsimp simp: locally_path_connected_open_path_component)
  fix U y
  assume opefSU: "openin (top_of_set (f ` S)) U" and " U"
  then have "path_component_set U y  U" " f ` S"
    by (meson path_component_subset openin_imp_subset)+
  then have "openin (top_of_set (f ` S)) (path_component_set U y) 
             openin (top_of_set S) (S  f -` path_component_set U y)"
  proof -
    have "path_component_set U y  f ` S"
      using U f ` S path_component_set U y U by blast
    then show ?thesis
      using oo by blast
  qed
  moreover have "openin (top_of_set S) (S  f -` path_component_set U y)"
  proof (subst openin_subopen, clarify)
    fix x
    assume " S" and Uyfx: "path_component U y (f x)"
    then have "f x  U"
      using path_component_mem by blast
    show "T. openin (top_of_set S) T  x  T  T  (S  f -` path_component_set U y)"
    proof (intro conjI exI)
      show "openin (top_of_set S) (path_component_set (S  f -` U) x)"
      proof (rule ccontr)
        assume **: "¬ openin (top_of_set S) (path_component_set (S  f -` U) x)"
        then have " (S  f -` U)"
          by (metis (no_types, lifting) U f ` S opefSU lcS oo locally_path_connected_open_path_component)
        then show False
          using ** path_component_set U y U x S path_component U y (f x) by blast
      qed
    next
      show " path_component_set (S  f -` U) x"
        by (simp add: f x U x S path_component_refl)
    next
      have contf: "continuous_on S f"
        by (simp add: continuous_on_open oo openin_imp_subset)
      then have "continuous_on (path_component_set (S  f -` U) x) f"
        by (meson Int_lower1 continuous_on_subset path_component_subset)
      then have "path_connected (f ` path_component_set (S  f -` U) x)"
        by (simp add: path_connected_continuous_image)
      moreover have "f ` path_component_set (S  f -` U) x  U"
        using path_component_mem by fastforce
      moreover have "f x  f ` path_component_set (S  f -` U) x"
        by (force simp: x S f x U path_component_refl_eq)
      ultimately have "f ` (path_component_set (S  f -` U) x)  path_component_set U (f x)"
        by (meson path_component_maximal)
       also have "  path_component_set U y"
        by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym)
      finally have fC: "f ` (path_component_set (S  f -` U) x)  path_component_set U y" .
      have cUC: "path_component_set (S  f -` U) x  (S  f -` path_component_set U y)"
        using path_component_subset fC by blast
      have "path_component_set (S  f -` U) x  path_component_set (S  f -` path_component_set U y) x"
      proof -
        have "a. path_component_set (path_component_set (S  f -` U) x) a  path_component_set (S  f -` path_component_set U y) a"
          using cUC path_component_mono by blast
        then show ?thesis
          using path_component_path_component by blast
      qed
      also have "  (S  f -` path_component_set U y)"
        by (rule path_component_subset)
      finally show "path_component_set (S  f -` U) x  (S  f -` path_component_set U y)" .
    qed
  qed
  ultimately show "openin (top_of_set (f ` S)) (path_component_set U y)"
    by metis
qed

subsection🍋tag unimportant\Components, continuity, openin, closedin

lemma continuous_on_components_gen:
 fixes f :: "'a::topological_space ==> 'b::topological_space"
  assumes "C. C  components S ==>
              openin (top_of_set S) C  continuous_on C f"
    shows "continuous_on S f"
proof (clarsimp simp: continuous_openin_preimage_eq)
  fix t :: "'b set"
  assume "open t"
  have *: " f -` t = ( components S. c  f -` t)"
    by auto
  show "openin (top_of_set S) (S  f -` t)"
    unfolding * using open t assms continuous_openin_preimage_gen openin_trans openin_Union by blast
qed

lemma continuous_on_components:
 fixes f :: "'a::topological_space ==> 'b::topological_space"
  assumes "locally connected S " "C. C  components S ==> continuous_on C f"
  shows "continuous_on S f"
proof (rule continuous_on_components_gen)
  fix C
  assume " components S"
  then show "openin (top_of_set S) C  continuous_on C f"
    by (simp add: assms openin_components_locally_connected)
qed

lemma continuous_on_components_eq:
    "locally connected S
     ==> (continuous_on S f  ( components S. continuous_on c f))"
by (meson continuous_on_components continuous_on_subset in_components_subset)

lemma continuous_on_components_open:
 fixes S :: "'a::real_normed_vector set"
  assumes "open S "
          "c. c  components S ==> continuous_on c f"
    shows "continuous_on S f"
using continuous_on_components open_imp_locally_connected assms by blast

lemma continuous_on_components_open_eq:
  fixes S :: "'a::real_normed_vector set"
  shows "open S ==> (continuous_on S f  ( components S. continuous_on c f))"
using continuous_on_subset in_components_subset
by (blast intro: continuous_on_components_open)

lemma closedin_union_complement_components:
  assumes U: "locally connected U"
      and S: "closedin (top_of_set U) S"
      and cuS: " components(U - S)"
    shows "closedin (top_of_set U) (S  c)"
proof -
  have di: "(S T. S  c  T  c' ==> disjnt S T) ==> disjnt ( c) ( c')" for c'
    by (simp add: disjnt_def) blast
  have " U"
    using S closedin_imp_subset by blast
  moreover have "U - S =  (components (U - S) - c)"
    by (metis Diff_partition Union_components Union_Un_distrib assms(3))
  moreover have "disjnt (c) ((components (U - S) - c))"
    apply (rule di)
    by (metis di DiffD1 DiffD2 assms(3) components_nonoverlap disjnt_def subsetCE)
  ultimately have eq: " c = U - ((components(U - S) - c))"
    by (auto simp: disjnt_def)
  have *: "openin (top_of_set U) ((components (U - S) - c))"
  proof (rule openin_Union [OF openin_trans [of "U - S"]])
    show "openin (top_of_set (U - S)) T" if " components (U - S) - c" for T
      using that by (simp add: U S locally_diff_closed openin_components_locally_connected)
    show "openin (top_of_set U) (U - S)" if " components (U - S) - c" for T
      using that by (simp add: openin_diff S)
  qed
  have "closedin (top_of_set U) (U -  (components (U - S) - c))"
    by (metis closedin_diff closedin_topspace topspace_euclidean_subtopology *)
  then have "openin (top_of_set U) (U - (U - (components (U - S) - c)))"
    by (simp add: openin_diff)
  then show ?thesis
    by (force simp: eq closedin_def)
qed

lemma closed_union_complement_components:
  fixes S :: "'a::real_normed_vector set"
  assumes S: "closed S" and c: " components(- S)"
    shows "closed(S   c)"
proof -
  have "closedin (top_of_set UNIV) (S  c)"
    by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_union_complement_components locally_connected_UNIV subtopology_UNIV)
  then show ?thesis by simp
qed

lemma closedin_Un_complement_component:
  fixes S :: "'a::real_normed_vector set"
  assumes u: "locally connected u"
      and S: "closedin (top_of_set u) S"
      and c: " c  components(u - S)"
    shows "closedin (top_of_set u) (S  c)"
proof -
  have "closedin (top_of_set u) (S  {c})"
    using c by (blast intro: closedin_union_complement_components [OF u S])
  then show ?thesis
    by simp
qed

lemma closed_Un_complement_component:
  fixes S :: "'a::real_normed_vector set"
  assumes S: "closed S" and c: " c  components(-S)"
    shows "closed (S  c)"
  by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component
      locally_connected_UNIV subtopology_UNIV)


subsectionExistence of isometry between subspaces of same dimension

lemma isometry_subset_subspace:
  fixes S :: "'a::euclidean_space set"
    and T :: "'b::euclidean_space set"
  assumes S: "subspace S"
      and T: "subspace T"
      and d: "dim S  dim T"
  obtains f where "linear f" " S  T" "x. x  S ==> norm(f x) = norm x"
proof -
  obtain B where " S" and Borth: "pairwise orthogonal B"
             and B1: "x. x  B ==> norm x = 1"
             and "independent B" "finite B" "card B = dim S" "span B = S"
    by (metis orthonormal_basis_subspace [OF S] independent_imp_finite)
  obtain C where " T" and Corth: "pairwise orthogonal C"
             and C1:"x. x  C ==> norm x = 1"
             and "independent C" "finite C" "card C = dim T" "span C = T"
    by (metis orthonormal_basis_subspace [OF T] independent_imp_finite)
  obtain fb where "fb ` B  C" "inj_on fb B"
    by (metis card B = dim S card C = dim T finite B finite C card_le_inj d)
  then have pairwise_orth_fb: "pairwise (λv j. orthogonal (fb v) (fb j)) B"
    using Corth unfolding pairwise_def inj_on_def
    by (blast intro: orthogonal_clauses)
  obtain f where "linear f" and ffb: "x. x  B ==> f x = fb x"
    using linear_independent_extend independent B by fastforce
  have "span (f ` B)  span C"
    by (metis fb ` B C ffb image_cong span_mono)
  then have "f ` S  T"
    unfolding span B = S span C = T span_linear_image[OF linear f] .
  have [simp]: "x. x  B ==> norm (fb x) = norm x"
    using B1 C1 fb ` B C by auto
  have "norm (f x) = norm x" if " S" for x
  proof -
    interpret linear f by fact
    obtain a where x: "x = ( B. a v *🪙R v)"
      using finite B span B = S x S span_finite by fastforce
    have "norm (f x)^2 = norm (vB. a v *🪙R fb v)^2" by (simp add: sum scale ffb x)
    also have " = (vB. norm ((a v *🪙R fb v))^2)"
    proof (rule norm_sum_Pythagorean [OF finite B])
      show "pairwise (λv j. orthogonal (a v *🪙R fb v) (a j *🪙R fb j)) B"
        by (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
    qed
    also have " = norm x ^2"
      by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF finite B])
    finally show ?thesis
      by (simp add: norm_eq_sqrt_inner)
  qed
  then show ?thesis
    by (meson f ` S T linear f image_subset_iff_funcset that)
qed

proposition isometries_subspaces:
  fixes S :: "'a::euclidean_space set"
    and T :: "'b::euclidean_space set"
  assumes S: "subspace S"
      and T: "subspace T"
      and d: "dim S = dim T"
  obtains f g where "linear f" "linear g" "f ` S = T" "g ` T = S"
                    "x. x  S ==> norm(f x) = norm x"
                    "x. x  T ==> norm(g x) = norm x"
                    "x. x  S ==> g(f x) = x"
                    "x. x  T ==> f(g x) = x"
proof -
  obtain B where " S" and Borth: "pairwise orthogonal B"
             and B1: "x. x  B ==> norm x = 1"
             and "independent B" "finite B" "card B = dim S" "span B = S"
    by (metis orthonormal_basis_subspace [OF S] independent_imp_finite)
  obtain C where " T" and Corth: "pairwise orthogonal C"
             and C1:"x. x  C ==> norm x = 1"
             and "independent C" "finite C" "card C = dim T" "span C = T"
    by (metis orthonormal_basis_subspace [OF T] independent_imp_finite)
  obtain fb where "bij_betw fb B C"
    by (metis finite B finite C bij_betw_iff_card card B = dim S card C = dim T d)
  then have pairwise_orth_fb: "pairwise (λv j. orthogonal (fb v) (fb j)) B"
    using Corth unfolding pairwise_def inj_on_def bij_betw_def
    by (blast intro: orthogonal_clauses)
  obtain f where "linear f" and ffb: "x. x  B ==> f x = fb x"
    using linear_independent_extend independent B by fastforce
  interpret f: linear f by fact
  define gb where "gb  inv_into B fb"
  then have pairwise_orth_gb: "pairwise (λv j. orthogonal (gb v) (gb j)) C"
    using Borth bij_betw fb B C unfolding pairwise_def bij_betw_def by force
  obtain g where "linear g" and ggb: "x. x  C ==> g x = gb x"
    using linear_independent_extend independent C by fastforce
  interpret g: linear g by fact
  have "span (f ` B)  span C"
    by (metis bij_betw fb B C bij_betw_imp_surj_on eq_iff ffb image_cong)
  then have "f ` S  T"
    unfolding span B = S span C = T span_linear_image[OF linear f] .
  have [simp]: "x. x  B ==> norm (fb x) = norm x"
    using B1 C1 bij_betw fb B C bij_betw_imp_surj_on by fastforce
  have f [simp]: "norm (f x) = norm x" "g (f x) = x" if " S" for x
  proof -
    obtain a where x: "x = ( B. a v *🪙R v)"
      using finite B span B = S x S span_finite by fastforce
    have "f x = ( B. f (a v *🪙R v))"
      using linear_sum [OF linear f] x by auto
    also have " = ( B. a v *🪙R f v)"
      by (simp add: f.sum f.scale)
    also have " = ( B. a v *🪙R fb v)"
      by (simp add: ffb cong: sum.cong)
    finally have *: "f x = (vB. a v *🪙R fb v)" .
    then have "(norm (f x))🪙2 = (norm (vB. a v *🪙R fb v))🪙2" by simp
    also have " = (vB. norm ((a v *🪙R fb v))^2)"
    proof (rule norm_sum_Pythagorean [OF finite B])
      show "pairwise (λv j. orthogonal (a v *🪙R fb v) (a j *🪙R fb j)) B"
        by (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
    qed
    also have " = (norm x)🪙2"
      by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF finite B])
    finally show "norm (f x) = norm x"
      by (simp add: norm_eq_sqrt_inner)
    have "g (f x) = g (vB. a v *🪙R fb v)" by (simp add: *)
    also have " = (vB. g (a v *🪙R fb v))"
      by (simp add: g.sum g.scale)
    also have " = (vB. a v *🪙R g (fb v))"
      by (simp add: g.scale)
    also have " = (vB. a v *🪙R v)"
    proof (rule sum.cong [OF refl])
      show "a x *🪙R g (fb x) = a x *🪙R x" if " B" for x
        using that bij_betw fb B C bij_betwE bij_betw_inv_into_left gb_def ggb by fastforce
    qed
    also have " = x"
      using x by blast
    finally show "g (f x) = x" .
  qed
  have [simp]: "x. x  C ==> norm (gb x) = norm x"
    by (metis B1 C1 bij_betw fb B C bij_betw_imp_surj_on gb_def inv_into_into)
  have g [simp]: "f (g x) = x" if " T" for x
  proof -
    obtain a where x: "x = ( C. a v *🪙R v)"
      using finite C span C = T x T span_finite by fastforce
    have "g x = ( C. g (a v *🪙R v))"
      by (simp add: x g.sum)
    also have " = ( C. a v *🪙R g v)"
      by (simp add: g.scale)
    also have " = ( C. a v *🪙R gb v)"
      by (simp add: ggb cong: sum.cong)
    finally have "f (g x) = f (vC. a v *🪙R gb v)" by simp
    also have " = (vC. f (a v *🪙R gb v))"
      by (simp add: f.scale f.sum)
    also have " = (vC. a v *🪙R f (gb v))"
      by (simp add: f.scale f.sum)
    also have " = (vC. a v *🪙R v)"
      using bij_betw fb B C
      by (simp add: bij_betw_def gb_def bij_betw_inv_into_right ffb inv_into_into)
    also have " = x"
      using x by blast
    finally show "f (g x) = x" .
  qed
  have gim: "g ` T = S"
    by (metis (full_types) S T f ` S T d dim_eq_span dim_image_le f(2) g.linear_axioms
        image_iff linear_subspace_image span_eq_iff subset_iff)
  have fim: "f ` S = T"
    using g ` T = S image_iff by fastforce
  have [simp]: "norm (g x) = norm x" if " T" for x
    using fim that by auto
  show ?thesis
    by (rule that [OF linear f linear g]) (simp_all add: fim gim)
qed

corollary isometry_subspaces:
  fixes S :: "'a::euclidean_space set"
    and T :: "'b::euclidean_space set"
  assumes S: "subspace S"
      and T: "subspace T"
      and d: "dim S = dim T"
  obtains f where "linear f" "f ` S = T" "x. x  S ==> norm(f x) = norm x"
using isometries_subspaces [OF assms]
by metis

corollary isomorphisms_UNIV_UNIV:
  assumes "DIM('M) = DIM('N)"
  obtains f::"'M::euclidean_space ==>'N::euclidean_space" and g
  where "linear f" "linear g"
                    "x. norm(f x) = norm x" "y. norm(g y) = norm y"
                    "x. g (f x) = x" "y. f(g y) = y"
  using assms by (auto intro: isometries_subspaces [of "UNIV::'M set" "UNIV::'N set"])

lemma homeomorphic_subspaces:
  fixes S :: "'a::euclidean_space set"
    and T :: "'b::euclidean_space set"
  assumes S: "subspace S"
      and T: "subspace T"
      and d: "dim S = dim T"
    shows "S homeomorphic T"
proof -
  obtain f g where "linear f" "linear g" "f ` S = T" "g ` T = S"
                   "x. x  S ==> g(f x) = x" "x. x  T ==> f(g x) = x"
    by (blast intro: isometries_subspaces [OF assms])
  then show ?thesis
    unfolding homeomorphic_def homeomorphism_def
    apply (rule_tac x=f in exI, rule_tac x=g in exI)
    apply (auto simp: linear_continuous_on linear_conv_bounded_linear)
    done
qed

lemma homeomorphic_affine_sets:
  assumes "affine S" "affine T" "aff_dim S = aff_dim T"
    shows "S homeomorphic T"
proof (cases "S = {}  T = {}")
  case True with assms aff_dim_empty homeomorphic_empty show ?thesis
    by metis
next
  case False
  then obtain a b where ab: " S" " T" by auto
  then have ss: "subspace ((+) (- a) ` S)" "subspace ((+) (- b) ` T)"
    using affine_diffs_subspace assms by blast+
  have dd: "dim ((+) (- a) ` S) = dim ((+) (- b) ` T)"
    using assms ab by (simp add: aff_dim_eq_dim [OF hull_inc] image_def)
  have "S homeomorphic ((+) (- a) ` S)"
    by (fact homeomorphic_translation)
  also have " homeomorphic ((+) (- b) ` T)"
    by (rule homeomorphic_subspaces [OF ss dd])
  also have " homeomorphic T"
    using homeomorphic_translation [of T "- b"] by (simp add: homeomorphic_sym [of T])
  finally show ?thesis .
qed


subsectionRetracts, in a general sense, preserve (co)homotopic triviality)

locale🍋tag important Retracts =
  fixes S h t k
  assumes conth: "continuous_on S h"
      and imh: "h ` S = t"
      and contk: "continuous_on t k"
      and imk: " t  S"
      and idhk: "y. y  t ==> h(k y) = y"

begin

lemma homotopically_trivial_retraction_gen:
  assumes P: "f. [continuous_on U f; f  U  t; Q f] ==> P(k  f)"
      and Q: "f. [continuous_on U f; f  U  S; P f] ==> Q(h  f)"
      and Qeq: "h k. (x. x  U ==> h x = k x) ==> Q h = Q k"
      and hom: "f g. [continuous_on U f; f  U  S; P f;
                       continuous_on U g; g  U  S; P g]
                       ==> homotopic_with_canon P U S f g"
      and contf: "continuous_on U f" and imf: " U  t" and Qf: "Q f"
      and contg: "continuous_on U g" and img: " U  t" and Qg: "Q g"
    shows "homotopic_with_canon Q U t f g"
proof -
  have "continuous_on U (k  f)"
    by (meson contf continuous_on_compose continuous_on_subset contk funcset_image imf)
  moreover have "(k  f) ` U  S"
    using imf imk by fastforce
  moreover have "P (k  f)"
    by (simp add: P Qf contf imf)
  moreover have "continuous_on U (k  g)"
    by (meson contg continuous_on_compose continuous_on_subset contk funcset_image img)
  moreover have "(k  g) ` U  S"
    using img imk by fastforce
  moreover have "P (k  g)"
    by (simp add: P Qg contg img)
  ultimately have "homotopic_with_canon P U S (k  f) (k  g)"
    by (simp add: hom image_subset_iff)
  then have "homotopic_with_canon Q U t (h  (k  f)) (h  (k  g))"
    apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
    using Q conth imh by force+
  then show ?thesis
  proof (rule homotopic_with_eq; simp)
    show "h k. (x. x  U ==> h x = k x) ==> Q h = Q k"
      using Qeq topspace_euclidean_subtopology by blast
    show "x. x  U ==> f x = h (k (f x))" "x. x  U ==> g x = h (k (g x))"
      using idhk imf img by fastforce+
  qed
qed

lemma homotopically_trivial_retraction_null_gen:
  assumes P: "f. [continuous_on U f; f  U  t; Q f] ==> P(k  f)"
      and Q: "f. [continuous_on U f; f  U  S; P f] ==> Q(h  f)"
      and Qeq: "h k. (x. x  U ==> h x = k x) ==> Q h = Q k"
      and hom: "f. [continuous_on U f; f  U  S; P f]
                     ==> c. homotopic_with_canon P U S f (λx. c)"
      and contf: "continuous_on U f" and imf:" U  t" and Qf: "Q f"
  obtains c where "homotopic_with_canon Q U t f (λx. c)"
proof -
  have feq: "x. x  U ==> (h  (k  f)) x = f x" using idhk imf by auto
  have "continuous_on U (k  f)"
    by (meson contf continuous_on_compose continuous_on_subset contk funcset_image imf)
  moreover have "(k  f)  U  S"
    using imf imk by fastforce
  moreover have "P (k  f)"
    by (simp add: P Qf contf imf)
  ultimately obtain c where "homotopic_with_canon P U S (k  f) (λx. c)"
    by (metis hom)
  then have "homotopic_with_canon Q U t (h  (k  f)) (h  (λx. c))"
    apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
    using Q conth imh by force+
  then have "homotopic_with_canon Q U t f (λx. h c)"
  proof (rule homotopic_with_eq)
    show "x. x  topspace (top_of_set U) ==> f x = (h  (k  f)) x"
      using feq by auto
    show "h k. (x. x  topspace (top_of_set U) ==> h x = k x) ==> Q h = Q k"
      using Qeq topspace_euclidean_subtopology by blast
  qed auto
  then show ?thesis
    using that by blast
qed

lemma cohomotopically_trivial_retraction_gen:
  assumes P: "f. [continuous_on t f; f  t  U; Q f] ==> P(f  h)"
      and Q: "f. [continuous_on S f; f  S  U; P f] ==> Q(f  k)"
      and Qeq: "h k. (x. x  t ==> h x = k x) ==> Q h = Q k"
      and hom: "f g. [continuous_on S f; f  S  U; P f;
                       continuous_on S g; g  S  U; P g]
                       ==> homotopic_with_canon P S U f g"
      and contf: "continuous_on t f" and imf: " t  U" and Qf: "Q f"
      and contg: "continuous_on t g" and img: " t  U" and Qg: "Q g"
    shows "homotopic_with_canon Q t U f g"
proof -
  have feq: "x. x  t ==> (f  h  k) x = f x" using idhk imf by auto
  have geq: "x. x  t ==> (g  h  k) x = g x" using idhk img by auto
  have "continuous_on S (f  h)"
    using contf conth continuous_on_compose imh by blast
  moreover have "(f  h)  S  U"
    using imf imh by fastforce
  moreover have "P (f  h)"
    by (simp add: P Qf contf imf)
  moreover have "continuous_on S (g  h)"
    using contg continuous_on_compose continuous_on_subset conth imh by blast
  moreover have "(g  h)  S  U"
    using img imh by fastforce
  moreover have "P (g  h)"
    by (simp add: P Qg contg img)
  ultimately have "homotopic_with_canon P S U (f  h) (g  h)"
    by (simp add: hom)
  then have "homotopic_with_canon Q t U (f  h  k) (g  h  k)"
    apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
    using Q contk imk by force+
  then show ?thesis
  proof (rule homotopic_with_eq)
    show "f x = (f  h  k) x" "g x = (g  h  k) x"
      if " topspace (top_of_set t)" for x
      using feq geq that by force+
  qed (use Qeq topspace_euclidean_subtopology in blast)
qed

lemma cohomotopically_trivial_retraction_null_gen:
  assumes P: "f. [continuous_on t f; f  t  U; Q f] ==> P(f  h)"
      and Q: "f. [continuous_on S f; f  S  U; P f] ==> Q(f  k)"
      and Qeq: "h k. (x. x  t ==> h x = k x) ==> Q h = Q k"
      and hom: "f g. [continuous_on S f; f  S  U; P f]
                       ==> c. homotopic_with_canon P S U f (λx. c)"
      and contf: "continuous_on t f" and imf: " t  U" and Qf: "Q f"
  obtains c where "homotopic_with_canon Q t U f (λx. c)"
proof -
  have feq: "x. x  t ==> (f  h  k) x = f x" using idhk imf by auto
  have "continuous_on S (f  h)"
    using contf conth continuous_on_compose imh by blast
  moreover have "(f  h)  S  U"
    using imf imh by fastforce
  moreover have "P (f  h)"
    by (simp add: P Qf contf imf)
  ultimately obtain c where "homotopic_with_canon P S U (f  h) (λx. c)"
    by (metis hom)
  then have 🍋: "homotopic_with_canon Q t U (f  h  k) ((λx. c)  k)"
  proof (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
    show "h. [continuous_map (top_of_set S) (top_of_set U) h; P h] ==> Q (h  k)"
      using Q by auto
  qed (use contk imk in force)+
  moreover have "homotopic_with_canon Q t U f (λx. c)"
    using homotopic_with_eq [OF 🍋] feq Qeq by fastforce
  ultimately show ?thesis
    using that by blast
qed

end

lemma simply_connected_retraction_gen:
  shows "[simply_connected S; continuous_on S h; h ` S = T;
          continuous_on T k; k  T  S; y. y  T ==> h(k y) = y]
        ==> simply_connected T"
apply (simp add: simply_connected_def path_def path_image_def homotopic_loops_def, clarify)
apply (rule Retracts.homotopically_trivial_retraction_gen
        [of S h _ k _ "λp. pathfinish p = pathstart p" "λp. pathfinish p = pathstart p"])
apply (simp_all add: Retracts_def pathfinish_def pathstart_def image_subset_iff_funcset)
done

lemma homeomorphic_simply_connected:
    "[S homeomorphic T; simply_connected S] ==> simply_connected T"
  by (auto simp: homeomorphic_def homeomorphism_def intro: simply_connected_retraction_gen)

lemma homeomorphic_simply_connected_eq:
    "S homeomorphic T ==> (simply_connected S  simply_connected T)"
  by (metis homeomorphic_simply_connected homeomorphic_sym)


subsectionHomotopy equivalence

subsectionHomotopy equivalence of topological spaces.

definition🍋tag important homotopy_equivalent_space
             (infix homotopy'_equivalent'_space 50)
  where "X homotopy_equivalent_space Y 
        (f g. continuous_map X Y f 
              continuous_map Y X g 
              homotopic_with (λx. True) X X (g  f) id 
              homotopic_with (λx. True) Y Y (f  g) id)"

lemma homeomorphic_imp_homotopy_equivalent_space:
  "X homeomorphic_space Y ==> X homotopy_equivalent_space Y"
  unfolding homeomorphic_space_def homotopy_equivalent_space_def
  apply (erule ex_forward)+
  by (simp add: homotopic_with_equal homotopic_with_sym homeomorphic_maps_def)

lemma homotopy_equivalent_space_refl:
   "X homotopy_equivalent_space X"
  by (simp add: homeomorphic_imp_homotopy_equivalent_space homeomorphic_space_refl)

lemma homotopy_equivalent_space_sym:
   "X homotopy_equivalent_space Y  Y homotopy_equivalent_space X"
  by (meson homotopy_equivalent_space_def)

lemma homotopy_eqv_trans [trans]:
  assumes 1: "X homotopy_equivalent_space Y" and 2: "Y homotopy_equivalent_space U"
    shows "X homotopy_equivalent_space U"
proof -
  obtain f1 g1 where f1: "continuous_map X Y f1"
                 and g1: "continuous_map Y X g1"
                 and hom1: "homotopic_with (λx. True) X X (g1  f1) id"
                           "homotopic_with (λx. True) Y Y (f1  g1) id"
    using 1 by (auto simp: homotopy_equivalent_space_def)
  obtain f2 g2 where f2: "continuous_map Y U f2"
                 and g2: "continuous_map U Y g2"
                 and hom2: "homotopic_with (λx. True) Y Y (g2  f2) id"
                           "homotopic_with (λx. True) U U (f2  g2) id"
    using 2 by (auto simp: homotopy_equivalent_space_def)
  have "homotopic_with (λf. True) X Y (g2  f2  f1) (id  f1)"
    using f1 hom2(1) homotopic_with_compose_continuous_map_right by metis
  then have "homotopic_with (λf. True) X Y (g2  (f2  f1)) (id  f1)"
    by (simp add: o_assoc)
  then have "homotopic_with (λx. True) X X
         (g1  (g2  (f2  f1))) (g1  (id  f1))"
    by (simp add: g1 homotopic_with_compose_continuous_map_left)
  moreover have "homotopic_with (λx. True) X X (g1  id  f1) id"
    using hom1 by simp
  ultimately have SS: "homotopic_with (λx. True) X X (g1  g2  (f2  f1)) id"
    by (metis comp_assoc homotopic_with_trans id_comp)
  have "homotopic_with (λf. True) U Y (f1  g1  g2) (id  g2)"
    using g2 hom1(2) homotopic_with_compose_continuous_map_right by fastforce
  then have "homotopic_with (λf. True) U Y (f1  (g1  g2)) (id  g2)"
    by (simp add: o_assoc)
  then have "homotopic_with (λx. True) U U
         (f2  (f1  (g1  g2))) (f2  (id  g2))"
    by (simp add: f2 homotopic_with_compose_continuous_map_left)
  moreover have "homotopic_with (λx. True) U U (f2  id  g2) id"
    using hom2 by simp
  ultimately have UU: "homotopic_with (λx. True) U U (f2  f1  (g1  g2)) id"
    by (simp add: fun.map_comp hom2(2) homotopic_with_trans)
  show ?thesis
    unfolding homotopy_equivalent_space_def
    by (blast intro: f1 f2 g1 g2 continuous_map_compose SS UU)
qed

lemma deformation_retraction_imp_homotopy_equivalent_space:
  "[homotopic_with (λx. True) X X (S  r) id; retraction_maps X Y r S]
    ==> X homotopy_equivalent_space Y"
  unfolding homotopy_equivalent_space_def retraction_maps_def
  using homotopic_with_id2 by fastforce

lemma deformation_retract_imp_homotopy_equivalent_space:
   "[homotopic_with (λx. True) X X r id; retraction_maps X Y r id]
    ==> X homotopy_equivalent_space Y"
  using deformation_retraction_imp_homotopy_equivalent_space by force

lemma deformation_retract_of_space:
  " topspace X 
   (r. homotopic_with (λx. True) X X id r  retraction_maps X (subtopology X S) r id) 
   S retract_of_space X  (f. homotopic_with (λx. True) X X id f  f ` (topspace X)  S)"
proof (cases " topspace X")
  case True
  moreover have "(r. homotopic_with (λx. True) X X id r  retraction_maps X (subtopology X S) r id)
              (S retract_of_space X  (f. homotopic_with (λx. True) X X id f  f ` topspace X  S))"
    unfolding retract_of_space_def
  proof safe
    fix f r
    assume f: "homotopic_with (λx. True) X X id f"
      and fS: "f ` topspace X  S"
      and r: "continuous_map X (subtopology X S) r"
      and req: "xS. r x = x"
    show "r. homotopic_with (λx. True) X X id r  retraction_maps X (subtopology X S) r id"
    proof (intro exI conjI)
      have "homotopic_with (λx. True) X X f r"
        proof (rule homotopic_with_eq)
          show "homotopic_with (λx. True) X X (r  f) (r  id)"
            by (metis continuous_map_into_fulltopology f homotopic_with_compose_continuous_map_left homotopic_with_symD r)
          show "f x = (r  f) x" if " topspace X" for x
            using that fS req by auto
        qed auto
      then show "homotopic_with (λx. True) X X id r"
        by (rule homotopic_with_trans [OF f])
    next
      show "retraction_maps X (subtopology X S) r id"
        by (simp add: r req retraction_maps_def)
    qed
  qed (use True in auto simp: retraction_maps_def topspace_subtopology_subset continuous_map_in_subtopology)
  ultimately show ?thesis by simp
qed (auto simp: retract_of_space_def retraction_maps_def)



subsectionContractible spaces

textThe definition (which agrees with "contractible" on subsets of Euclidean space)
 is a little cryptic because we don't in fact assume that the constant "a" is in the space.
 This forces the convention that the empty space / set is contractible, avoiding some special cases.

definition contractible_space where
  "contractible_space X  a. homotopic_with (λx. True) X X id (λx. a)"

lemma contractible_space_top_of_set [simp]:"contractible_space (top_of_set S)  contractible S"
  by (auto simp: contractible_space_def contractible_def)

lemma contractible_space_empty [simp]:
   "contractible_space trivial_topology"
  unfolding contractible_space_def homotopic_with_def
  apply (rule_tac x=undefined in exI)
  apply (rule_tac x="λ(t,x). if t = 0 then x else undefined" in exI)
  apply (auto simp: continuous_map_on_empty)
  done

lemma contractible_space_singleton [simp]:
  "contractible_space (discrete_topology{a})"
  unfolding contractible_space_def homotopic_with_def
  apply (rule_tac x=a in exI)
  apply (rule_tac x="λ(t,x). if t = 0 then x else a" in exI)
  apply (auto intro: continuous_map_eq [where f = "λz. a"])
  done

lemma contractible_space_subset_singleton:
   "topspace X  {a} ==> contractible_space X"
  by (metis contractible_space_empty contractible_space_singleton null_topspace_iff_trivial subset_singletonD subtopology_eq_discrete_topology_sing)

lemma contractible_space_subtopology_singleton [simp]:
   "contractible_space (subtopology X {a})"
  by (meson contractible_space_subset_singleton insert_subset path_connectedin_singleton path_connectedin_subtopology subsetI)

lemma contractible_space:
   "contractible_space X 
        X = trivial_topology 
        ( topspace X. homotopic_with (λx. True) X X id (λx. a))"
proof (cases "X = trivial_topology")
  case False
  then show ?thesis
    using homotopic_with_imp_continuous_maps by (fastforce simp: contractible_space_def)
qed (simp add: contractible_space_empty)

lemma contractible_imp_path_connected_space:
  assumes "contractible_space X" shows "path_connected_space X"
proof (cases "X = trivial_topology")
  case False
  have *: "path_connected_space X"
    if " topspace X" and conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X h"
      and h: "x. h (0, x) = x" "x. h (1, x) = a"
    for a and h :: "real × 'a ==> 'a"
  proof -
    have "path_component_of X b a" if " topspace X" for b
      unfolding path_component_of_def
    proof (intro exI conjI)
      let ?g = " (λx. (x,b))"
      show "pathin X ?g"
        unfolding pathin_def
      proof (rule continuous_map_compose [OF _ conth])
        show "continuous_map (top_of_set {0..1}) (prod_topology (top_of_set {0..1}) X) (λx. (x, b))"
          using that by (auto intro!: continuous_intros)
      qed
    qed (use h in auto)
  then show ?thesis
    by (metis path_component_of_equiv path_connected_space_iff_path_component)
  qed
  show ?thesis
    using assms False by (auto simp: contractible_space homotopic_with_def *)
qed (simp add: path_connected_space_topspace_empty)

lemma contractible_imp_connected_space:
   "contractible_space X ==> connected_space X"
  by (simp add: contractible_imp_path_connected_space path_connected_imp_connected_space)

lemma contractible_space_alt:
   "contractible_space X  ( topspace X. homotopic_with (λx. True) X X id (λx. a))" (is "?lhs = ?rhs")
proof
  assume X: ?lhs
  then obtain a where a: "homotopic_with (λx. True) X X id (λx. a)"
    by (auto simp: contractible_space_def)
  show ?rhs
  proof
    show "homotopic_with (λx. True) X X id (λx. b)" if " topspace X" for b
    proof (rule homotopic_with_trans [OF a])
      show "homotopic_with (λx. True) X X (λx. a) (λx. b)"
        using homotopic_constant_maps path_connected_space_imp_path_component_of
        by (metis X a contractible_imp_path_connected_space homotopic_with_sym homotopic_with_trans path_component_of_equiv that)
    qed
  qed
next
  assume R: ?rhs
  then show ?lhs
    using contractible_space_def by fastforce
qed


lemma compose_const [simp]: " (λx. a) = (λx. f a)" "(λx. a)  g = (λx. a)"
  by (simp_all add: o_def)

lemma nullhomotopic_through_contractible_space:
  assumes f: "continuous_map X Y f" and g: "continuous_map Y Z g" and Y: "contractible_space Y"
  obtains c where "homotopic_with (λh. True) X Z (g  f) (λx. c)"
proof -
  obtain b where b: "homotopic_with (λx. True) Y Y id (λx. b)"
    using Y by (auto simp: contractible_space_def)
  show thesis
    using homotopic_with_compose_continuous_map_right
           [OF homotopic_with_compose_continuous_map_left [OF b g] f]
    by (force simp: that)
qed

lemma nullhomotopic_into_contractible_space:
  assumes f: "continuous_map X Y f" and Y: "contractible_space Y"
  obtains c where "homotopic_with (λh. True) X Y f (λx. c)"
  using nullhomotopic_through_contractible_space [OF f _ Y]
  by (metis continuous_map_id id_comp)

lemma nullhomotopic_from_contractible_space:
  assumes f: "continuous_map X Y f" and X: "contractible_space X"
  obtains c where "homotopic_with (λh. True) X Y f (λx. c)"
  using nullhomotopic_through_contractible_space [OF _ f X]
  by (metis comp_id continuous_map_id)

lemma homotopy_dominated_contractibility:
  assumes f: "continuous_map X Y f" and g: "continuous_map Y X g"
    and hom: "homotopic_with (λx. True) Y Y (f  g) id" and X: "contractible_space X"
  shows "contractible_space Y"
proof -
  obtain c where c: "homotopic_with (λh. True) X Y f (λx. c)"
    using nullhomotopic_from_contractible_space [OF f X] .
  have "homotopic_with (λx. True) Y Y (f  g) (λx. c)"
    using homotopic_with_compose_continuous_map_right [OF c g] by fastforce
  then have "homotopic_with (λx. True) Y Y id (λx. c)"
    using homotopic_with_trans [OF _ hom] homotopic_with_symD by blast
  then show ?thesis
    unfolding contractible_space_def ..
qed

lemma homotopy_equivalent_space_contractibility:
   "X homotopy_equivalent_space Y ==> (contractible_space X  contractible_space Y)"
  unfolding homotopy_equivalent_space_def
  by (blast intro: homotopy_dominated_contractibility)

lemma homeomorphic_space_contractibility:
   "X homeomorphic_space Y
        ==> (contractible_space X  contractible_space Y)"
  by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)

lemma homotopic_through_contractible_space:
   "continuous_map X Y f 
        continuous_map X Y f' 
        continuous_map Y Z g 
        continuous_map Y Z g' 
        contractible_space Y  path_connected_space Z
        ==> homotopic_with (λh. True) X Z (g  f) (g'  f')"
  using nullhomotopic_through_contractible_space [of X Y f Z g]
  using nullhomotopic_through_contractible_space [of X Y f' Z g']
  by (smt (verit) continuous_map_const homotopic_constant_maps homotopic_with_imp_continuous_maps
      homotopic_with_symD homotopic_with_trans path_connected_space_imp_path_component_of)

lemma homotopic_from_contractible_space:
   "continuous_map X Y f  continuous_map X Y g 
        contractible_space X  path_connected_space Y
        ==> homotopic_with (λx. True) X Y f g"
  by (metis comp_id continuous_map_id homotopic_through_contractible_space)

lemma homotopic_into_contractible_space:
   "continuous_map X Y f  continuous_map X Y g 
        contractible_space Y
        ==> homotopic_with (λx. True) X Y f g"
  by (metis continuous_map_id contractible_imp_path_connected_space homotopic_through_contractible_space id_comp)

lemma contractible_eq_homotopy_equivalent_singleton_subtopology:
   "contractible_space X 
        X = trivial_topology  ( topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is "?lhs = ?rhs")
proof (cases "X = trivial_topology")
  case False
  show ?thesis
  proof
    assume ?lhs
    then obtain a where a: "homotopic_with (λx. True) X X id (λx. a)"
      by (auto simp: contractible_space_def)
    then have " topspace X"
      by (metis False continuous_map_const homotopic_with_imp_continuous_maps)
    then have "homotopic_with (λx. True) (subtopology X {a}) (subtopology X {a}) id (λx. a)"
      using connectedin_absolute connectedin_sing contractible_space_alt contractible_space_subtopology_singleton by fastforce
    then have "X homotopy_equivalent_space subtopology X {a}"
      unfolding homotopy_equivalent_space_def using a topspace X
      by (metis (full_types) a comp_id continuous_map_const continuous_map_id_subt empty_subsetI homotopic_with_symD
           id_comp insertI1 insert_subset topspace_subtopology_subset)
    with a topspace X show ?rhs
      by blast
  next
    assume ?rhs
    then show ?lhs
      by (meson False contractible_space_subtopology_singleton homotopy_equivalent_space_contractibility)
  qed
qed (simp add: contractible_space_empty)

lemma contractible_space_retraction_map_image:
  assumes "retraction_map X Y f" and X: "contractible_space X"
  shows "contractible_space Y"
proof -
  obtain g where f: "continuous_map X Y f" and g: "continuous_map Y X g" and fg: " topspace Y. f(g y) = y"
    using assms by (auto simp: retraction_map_def retraction_maps_def)
  obtain a where a: "homotopic_with (λx. True) X X id (λx. a)"
    using X by (auto simp: contractible_space_def)
  have "homotopic_with (λx. True) Y Y id (λx. f a)"
  proof (rule homotopic_with_eq)
    show "homotopic_with (λx. True) Y Y (f  id  g) (f  (λx. a)  g)"
      using f g a homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right by metis
  qed (use fg in auto)
  then show ?thesis
    unfolding contractible_space_def by blast
qed

lemma contractible_space_prod_topology:
   "contractible_space(prod_topology X Y) 
    X = trivial_topology  Y = trivial_topology  contractible_space X  contractible_space Y"
proof (cases "X = trivial_topology  Y = trivial_topology")
  case True
  then have "(prod_topology X Y) = trivial_topology"
    by simp
  then show ?thesis
    by (auto simp: contractible_space_empty)
next
  case False
  have "contractible_space(prod_topology X Y)  contractible_space X  contractible_space Y"
  proof safe
    assume XY: "contractible_space (prod_topology X Y)"
    with False have "retraction_map (prod_topology X Y) X fst"
      by (auto simp: contractible_space False retraction_map_fst)
    then show "contractible_space X"
      by (rule contractible_space_retraction_map_image [OF _ XY])
    have "retraction_map (prod_topology X Y) Y snd"
      using False XY by (auto simp: contractible_space False retraction_map_snd)
    then show "contractible_space Y"
      by (rule contractible_space_retraction_map_image [OF _ XY])
  next
    assume "contractible_space X" and "contractible_space Y"
    with False obtain a b
      where " topspace X" and a: "homotopic_with (λx. True) X X id (λx. a)"
        and " topspace Y" and b: "homotopic_with (λx. True) Y Y id (λx. b)"
      by (auto simp: contractible_space)
    with False show "contractible_space (prod_topology X Y)"
      apply (simp add: contractible_space)
      apply (rule_tac x=a in bexI)
       apply (rule_tac x=b in bexI)
      using homotopic_with_prod_topology [OF a b]
        apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff)
       apply auto
      done
  qed
  with False show ?thesis
    by auto
qed


lemma contractible_space_product_topology:
  "contractible_space(product_topology X I) 
    (product_topology X I) = trivial_topology  ( I. contractible_space(X i))"
proof (cases "(product_topology X I) = trivial_topology")
  case False
  have 1: "contractible_space (X i)"
    if XI: "contractible_space (product_topology X I)" and " I"
    for i
  proof (rule contractible_space_retraction_map_image [OF _ XI])
    show "retraction_map (product_topology X I) (X i) (λx. x i)"
      using False by (simp add: retraction_map_product_projection i I)
  qed
  have 2: "contractible_space (product_topology X I)"
    if " topspace (product_topology X I)" and cs: "iI. contractible_space (X i)"
    for x :: "'a ==> 'b"
  proof -
    obtain f where f: "i. i==> homotopic_with (λx. True) (X i) (X i) id (λx. f i)"
      using cs unfolding contractible_space_def by metis
    have "homotopic_with (λx. True)
                         (product_topology X I) (product_topology X I) id (λx. restrict f I)"
      by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto)
    then show ?thesis
      by (auto simp: contractible_space_def)
  qed
  show ?thesis
    using False 1 2 by (meson equals0I subtopology_eq_discrete_topology_empty)
qed auto


lemma contractible_space_subtopology_euclideanreal [simp]:
  "contractible_space(subtopology euclideanreal S)  is_interval S"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have "path_connectedin (subtopology euclideanreal S) S"
    using contractible_imp_path_connected_space path_connectedin_topspace path_connectedin_absolute
    by (simp add: contractible_imp_path_connected)
  then show ?rhs
    by (simp add: is_interval_path_connected_1)
next
  assume ?rhs
  then have "convex S"
    by (simp add: is_interval_convex_1)
  show ?lhs
  proof (cases "S = {}")
    case False
    then obtain z where " S"
      by blast
    show ?thesis
      unfolding contractible_space_def homotopic_with_def
    proof (intro exI conjI allI)
      note 🍋 = convexD [OF convex S, simplified]
      show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set S)) (top_of_set S)
                           (λ(t,x). (1 - t) * x + t * z)"
        using z S
        by (auto simp: case_prod_unfold intro!: continuous_intros 🍋)
    qed auto
  qed (simp add: contractible_space_empty)
qed


corollary contractible_space_euclideanreal: "contractible_space euclideanreal"
proof -
  have "contractible_space (subtopology euclideanreal UNIV)"
    using contractible_space_subtopology_euclideanreal by blast
  then show ?thesis
    by simp
qed


abbreviation🍋tag important homotopy_eqv :: "'a::topological_space set ==> 'b::topological_space set ==> bool"
             (infix homotopy'_eqv 50)
  where "S homotopy_eqv T  top_of_set S homotopy_equivalent_space top_of_set T"

lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T ==> S homotopy_eqv T"
  unfolding homeomorphic_def homeomorphism_def homotopy_equivalent_space_def
  apply (erule ex_forward)+
  by (metis continuous_map_subtopology_eu homotopic_with_id2 openin_imp_subset openin_subtopology_self topspace_euclidean_subtopology
      image_subset_iff_funcset)

lemma homotopy_eqv_inj_linear_image:
  fixes f :: "'a::euclidean_space ==> 'b::euclidean_space"
  assumes "linear f" "inj f"
    shows "(f ` S) homotopy_eqv S"
  by (metis assms homeomorphic_sym homeomorphic_imp_homotopy_eqv linear_homeomorphic_image)

lemma homotopy_eqv_translation:
    fixes S :: "'a::real_normed_vector set"
    shows "(+) a ` S homotopy_eqv S"
  using homeomorphic_imp_homotopy_eqv homeomorphic_translation homeomorphic_sym by blast

lemma homotopy_eqv_homotopic_triviality_imp:
  fixes S :: "'a::real_normed_vector set"
    and T :: "'b::real_normed_vector set"
    and U :: "'c::real_normed_vector set"
  assumes "S homotopy_eqv T"
      and f: "continuous_on U f" " U  T"
      and g: "continuous_on U g" " U  T"
      and homUS: "f g. [continuous_on U f; f  U  S;
                         continuous_on U g; g  U  S]
                         ==> homotopic_with_canon (λx. True) U S f g"
    shows "homotopic_with_canon (λx. True) U T f g"
proof -
  obtain h k where h: "continuous_on S h" " S  T"
               and k: "continuous_on T k" " T  S"
               and hom: "homotopic_with_canon (λx. True) S S (k  h) id"
                        "homotopic_with_canon (λx. True) T T (h  k) id"
    using assms by (force simp: homotopy_equivalent_space_def image_subset_iff_funcset)
  have "homotopic_with_canon (λf. True) U S (k  f) (k  g)"
  proof (rule homUS)
    show "continuous_on U (k  f)" "continuous_on U (k  g)"
      using continuous_on_compose continuous_on_subset f g k by (metis funcset_image)+
  qed (use f g k in (force simp: o_def)+ )
  then have "homotopic_with_canon (λx. True) U T (h  (k  f)) (h  (k  g))"
    by (simp add: h homotopic_with_compose_continuous_map_left image_subset_iff_funcset)
  moreover have "homotopic_with_canon (λx. True) U T (h  k  f) (id  f)"
    by (rule homotopic_with_compose_continuous_right [where X=T and Y=T]; simp add: hom f)
  moreover have "homotopic_with_canon (λx. True) U T (h  k  g) (id  g)"
    by (rule homotopic_with_compose_continuous_right [where X=T and Y=T]; simp add: hom g)
  ultimately show "homotopic_with_canon (λx. True) U T f g"
    unfolding o_assoc
    by (metis homotopic_with_trans homotopic_with_sym id_comp)
qed

lemma homotopy_eqv_homotopic_triviality:
  fixes S :: "'a::real_normed_vector set"
    and T :: "'b::real_normed_vector set"
    and U :: "'c::real_normed_vector set"
  assumes "S homotopy_eqv T"
    shows "(f g. continuous_on U f  f  U  S 
                   continuous_on U g  g  U  S
                    homotopic_with_canon (λx. True) U S f g) 
           (f g. continuous_on U f  f  U  T 
                  continuous_on U g  g  U  T
                   homotopic_with_canon (λx. True) U T f g)"
      (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (metis assms homotopy_eqv_homotopic_triviality_imp)
next
  assume ?rhs
  moreover
  have "T homotopy_eqv S"
    using assms homotopy_equivalent_space_sym by blast
  ultimately show ?lhs
    by (blast intro: homotopy_eqv_homotopic_triviality_imp)
qed


lemma homotopy_eqv_cohomotopic_triviality_null_imp:
  fixes S :: "'a::real_normed_vector set"
    and T :: "'b::real_normed_vector set"
    and U :: "'c::real_normed_vector set"
  assumes "S homotopy_eqv T"
      and f: "continuous_on T f" " T  U"
      and homSU: "f. [continuous_on S f; f  S  U]
                      ==> c. homotopic_with_canon (λx. True) S U f (λx. c)"
  obtains c where "homotopic_with_canon (λx. True) T U f (λx. c)"
proof -
  obtain h k where h: "continuous_on S h" " S  T"
               and k: "continuous_on T k" " T  S"
               and hom: "homotopic_with_canon (λx. True) S S (k  h) id"
                        "homotopic_with_canon (λx. True) T T (h  k) id"
    using assms by (force simp: homotopy_equivalent_space_def image_subset_iff_funcset)
  obtain c where "homotopic_with_canon (λx. True) S U (f  h) (λx. c)"
  proof (rule exE [OF homSU])
    show "continuous_on S (f  h)"
      by (metis continuous_on_compose continuous_on_subset f h funcset_image)
  qed (use f h in force)
  then have "homotopic_with_canon (λx. True) T U ((f  h)  k) ((λx. c)  k)"
    by (rule homotopic_with_compose_continuous_right [where X=S]) (use k in auto)
  moreover have "homotopic_with_canon (λx. True) T U (f  id) (f  (h  k))"
    by (rule homotopic_with_compose_continuous_left [where Y=T])
       (use f in auto simp: hom homotopic_with_symD)
  ultimately show ?thesis
    using that homotopic_with_trans by (fastforce simp: o_def)
qed

lemma homotopy_eqv_cohomotopic_triviality_null:
  fixes S :: "'a::real_normed_vector set"
    and T :: "'b::real_normed_vector set"
    and U :: "'c::real_normed_vector set"
  assumes "S homotopy_eqv T"
    shows "(f. continuous_on S f  f  S  U
                 (c. homotopic_with_canon (λx. True) S U f (λx. c))) 
           (f. continuous_on T f  f  T  U
                 (c. homotopic_with_canon (λx. True) T U f (λx. c)))"
by (rule iffI; metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_equivalent_space_sym)

text Similar to the proof above
lemma homotopy_eqv_homotopic_triviality_null_imp:
  fixes S :: "'a::real_normed_vector set"
    and T :: "'b::real_normed_vector set"
    and U :: "'c::real_normed_vector set"
  assumes "S homotopy_eqv T"
      and f: "continuous_on U f" " U  T"
      and homSU: "f. [continuous_on U f; f  U  S]
                      ==> c. homotopic_with_canon (λx. True) U S f (λx. c)"
    shows "c. homotopic_with_canon (λx. True) U T f (λx. c)"
proof -
  obtain h k where h: "continuous_on S h" " S  T"
               and k: "continuous_on T k" " T  S"
               and hom: "homotopic_with_canon (λx. True) S S (k  h) id"
                        "homotopic_with_canon (λx. True) T T (h  k) id"
    using assms by (force simp: homotopy_equivalent_space_def image_subset_iff_funcset)
  obtain c::'a where "homotopic_with_canon (λx. True) U S (k  f) (λx. c)"
  proof (rule exE [OF homSU [of " f"]])
    show "continuous_on U (k  f)"
      using continuous_on_compose continuous_on_subset f k by (metis funcset_image)
  qed (use f k in force)
  then have "homotopic_with_canon (λx. True) U T (h  (k  f)) (h  (λx. c))"
    by (rule homotopic_with_compose_continuous_left [where Y=S]) (use h in auto)
  moreover have "homotopic_with_canon (λx. True) U T (id  f) ((h  k)  f)"
    by (rule homotopic_with_compose_continuous_right [where X=T])
       (use f in auto simp: hom homotopic_with_symD)
  ultimately show ?thesis
    using homotopic_with_trans by (fastforce simp: o_def)
qed

lemma homotopy_eqv_homotopic_triviality_null:
  fixes S :: "'a::real_normed_vector set"
    and T :: "'b::real_normed_vector set"
    and U :: "'c::real_normed_vector set"
  assumes "S homotopy_eqv T"
    shows "(f. continuous_on U f  f  U  S
                   (c. homotopic_with_canon (λx. True) U S f (λx. c))) 
           (f. continuous_on U f  f  U  T
                   (c. homotopic_with_canon (λx. True) U T f (λx. c)))"
by (rule iffI; metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_equivalent_space_sym)

lemma homotopy_eqv_contractible_sets:
  fixes S :: "'a::real_normed_vector set"
    and T :: "'b::real_normed_vector set"
  assumes "contractible S" "contractible T" "S = {}  T = {}"
    shows "S homotopy_eqv T"
proof (cases "S = {}")
  case True with assms show ?thesis
    using homeomorphic_imp_homotopy_eqv by fastforce
next
  case False
  with assms obtain a b where " S" " T"
    by auto
  then show ?thesis
    unfolding homotopy_equivalent_space_def
    apply (rule_tac x="λx. b" in exI, rule_tac x="λx. a" in exI)
    apply (intro assms conjI continuous_on_id' homotopic_into_contractible; force)
    done
qed

lemma homotopy_eqv_empty1 [simp]:
  fixes S :: "'a::real_normed_vector set"
  shows "S homotopy_eqv ({}::'b::real_normed_vector set)  S = {}" (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    by (meson continuous_map_subtopology_eu equals0D equals0I funcset_mem
        homotopy_equivalent_space_def)
qed (use homeomorphic_imp_homotopy_eqv in force)

lemma homotopy_eqv_empty2 [simp]:
  fixes S :: "'a::real_normed_vector set"
  shows "({}::'b::real_normed_vector set) homotopy_eqv S  S = {}"
  using homotopy_equivalent_space_sym homotopy_eqv_empty1 by blast

lemma homotopy_eqv_contractibility:
  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
  shows "S homotopy_eqv T ==> (contractible S  contractible T)"
  by (meson contractible_space_top_of_set homotopy_equivalent_space_contractibility)

lemma homotopy_eqv_sing:
  fixes S :: "'a::real_normed_vector set" and a :: "'b::real_normed_vector"
  shows "S homotopy_eqv {a}  S  {}  contractible S"
  by (metis contractible_sing empty_not_insert homotopy_eqv_contractibility homotopy_eqv_contractible_sets homotopy_eqv_empty2)

lemma homeomorphic_contractible_eq:
  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
  shows "S homeomorphic T ==> (contractible S  contractible T)"
by (simp add: homeomorphic_imp_homotopy_eqv homotopy_eqv_contractibility)

lemma homeomorphic_contractible:
  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
  shows "[contractible S; S homeomorphic T] ==> contractible T"
  by (metis homeomorphic_contractible_eq)


subsection🍋tag unimportant\Misc other results

lemma bounded_connected_Compl_real:
  fixes S :: "real set"
  assumes "bounded S" and conn: "connected(- S)"
    shows "S = {}"
proof -
  obtain a b where " box a b"
    by (meson assms bounded_subset_box_symmetric)
  then have " S" " S"
    by auto
  then have "x. a  x  x  b  x  - S"
    by (meson Compl_iff conn connected_iff_interval)
  then show ?thesis
    using S box a b by auto
qed

corollary bounded_path_connected_Compl_real:
  fixes S :: "real set"
  assumes "bounded S" "path_connected(- S)" shows "S = {}"
  by (simp add: assms bounded_connected_Compl_real path_connected_imp_connected)

lemma bounded_connected_Compl_1:
  fixes S :: "'a::{euclidean_space} set"
  assumes "bounded S" and conn: "connected(- S)" and 1: "DIM('a) = 1"
    shows "S = {}"
proof -
  have "DIM('a) = DIM(real)"
    by (simp add: "1")
  then obtain f::"'a ==> real" and g
  where "linear f" "x. norm(f x) = norm x" and fg: "x. g(f x) = x" "y. f(g y) = y"
    by (rule isomorphisms_UNIV_UNIV) blast
  with bounded S have "bounded (f ` S)"
    using bounded_linear_image linear_linear by blast
  have "bij f" by (metis fg bijI')
  have "connected (f ` (-S))"
    using connected_linear_image assms linear f by blast
  moreover have "f ` (-S) = - (f ` S)"
    by (simp add: bij f bij_image_Compl_eq)
  finally have "connected (- (f ` S))"
    by simp
  then have "f ` S = {}"
    using bounded (f ` S) bounded_connected_Compl_real by blast
  then show ?thesis
    by blast
qed

lemma connected_card_eq_iff_nontrivial:
  fixes S :: "'a::metric_space set"
  shows "connected S ==> uncountable S  ¬(a. S  {a})"
  by (metis connected_uncountable finite.emptyI finite.insertI rev_finite_subset singleton_iff subsetI uncountable_infinite)

lemma connected_finite_iff_sing:
  fixes S :: "'a::metric_space set"
  assumes "connected S"
  shows "finite S  S = {}  (a. S = {a})"
  using assms connected_uncountable countable_finite by blast

subsection🍋tag unimportant\ Some simple positive connection theorems

proposition path_connected_convex_diff_countable:
  fixes U :: "'a::euclidean_space set"
  assumes "convex U" "¬ collinear U" "countable S"
    shows "path_connected(U - S)"
proof (clarsimp simp: path_connected_def)
  fix a b
  assume " U" " S" " U" " S"
  let ?m = "midpoint a b"
  show "g. path g  path_image g  U - S  pathstart g = a  pathfinish g = b"
  proof (cases "a = b")
    case True
    then show ?thesis
      by (metis DiffI a U a S path_component_def path_component_refl)
  next
    case False
    then have " ?m" " ?m"
      using midpoint_eq_endpoint by fastforce+
    have "?m  U"
      using a U b U convex U convex_contains_segment by force
    obtain c where " U" and nc_abc: "¬ collinear {a,b,c}"
      by (metis False a U b U ¬ collinear U collinear_triples insert_absorb)
    have ncoll_mca: "¬ collinear {?m,c,a}"
      by (metis (full_types) a ?m collinear_3_trans collinear_midpoint insert_commute nc_abc)
    have ncoll_mcb: "¬ collinear {?m,c,b}"
      by (metis (full_types) b ?m collinear_3_trans collinear_midpoint insert_commute nc_abc)
    have " ?m"
      by (metis collinear_midpoint insert_commute nc_abc)
    then have "closed_segment ?m c  U"
      by (simp add: c U ?m U convex U closed_segment_subset)
    then obtain z where z: " closed_segment ?m c"
                    and disjS: "(closed_segment a z  closed_segment z b)  S = {}"
    proof -
      have False if "closed_segment ?m c  {z. (closed_segment a z  closed_segment z b)  S  {}}"
      proof -
        have closb: "closed_segment ?m c 
                 {z  closed_segment ?m c. closed_segment a z  S  {}}  {z  closed_segment ?m c. closed_segment z  S  {}}"
          using that by blast
        have *: "countable {z  closed_segment ?m c. closed_segment z u  S  {}}"
          if " U" " S" and ncoll: "¬ collinear {?m, c, u}" for u
        proof -
          have **: False if x1: "x1  closed_segment ?m c" and x2: "x2  closed_segment ?m c"
                            and "x1  x2" "x1  u"
                            and w: " closed_segment x1 u" " closed_segment x2 u"
                            and " S" for x1 x2 w
          proof -
            have "x1  affine hull {?m,c}" "x2  affine hull {?m,c}"
              using segment_as_ball x1 x2 by auto
            then have coll_x1: "collinear {x1, ?m, c}" and coll_x2: "collinear {?m, c, x2}"
              by (simp_all add: affine_hull_3_imp_collinear) (metis affine_hull_3_imp_collinear insert_commute)
            have "¬ collinear {x1, u, x2}"
            proof
              assume "collinear {x1, u, x2}"
              then have "collinear {?m, c, u}"
                by (metis (full_types) c ?m coll_x1 coll_x2 collinear_3_trans insert_commute ncoll x1 x2)
              with ncoll show False ..
            qed
            then have "closed_segment x1 u  closed_segment u x2 = {u}"
              by (blast intro!: Int_closed_segment)
            then have "w = u"
              using closed_segment_commute w by auto
            show ?thesis
              using u S w = u that(7) by auto
          qed
          then have disj: "disjoint ((zclosed_segment ?m c. {closed_segment z u  S}))"
            by (fastforce simp: pairwise_def disjnt_def)
          have cou: "countable (( closed_segment ?m c. {closed_segment z u  S}) - {{}})"
            apply (rule pairwise_disjnt_countable_Union [OF _ pairwise_subset [OF disj]])
             apply (rule countable_subset [OF _ countable S], auto)
            done
          define f where " λX. (THE z. z  closed_segment ?m c  X = closed_segment z u  S)"
          show ?thesis
          proof (rule countable_subset [OF _ countable_image [OF cou, where f=f]], clarify)
            fix x
            assume x: " closed_segment ?m c" "closed_segment x u  S  {}"
            show " f ` ((zclosed_segment ?m c. {closed_segment z u  S}) - {{}})"
            proof (rule_tac x="closed_segment x u  S" in image_eqI)
              show "x = f (closed_segment x u  S)"
                unfolding f_def
                by (rule the_equality [symmetric]) (use x in auto dest: **)
            qed (use x in auto)
          qed
        qed
        have "uncountable (closed_segment ?m c)"
          by (metis c ?m uncountable_closed_segment)
        then show False
          using closb * [OF a U a S ncoll_mca] * [OF b U b S ncoll_mcb]
          by (simp add: closed_segment_commute countable_subset)
      qed
      then show ?thesis
        by (force intro: that)
    qed
    show ?thesis
    proof (intro exI conjI)
      have "path_image (linepath a z +++ linepath z b)  U"
        by (metis a U b U closed_segment ?m c U z convex U closed_segment_subset contra_subsetD path_image_linepath subset_path_image_join)
      with disjS show "path_image (linepath a z +++ linepath z b)  U - S"
        by (force simp: path_image_join)
    qed auto
  qed
qed


corollary connected_convex_diff_countable:
  fixes U :: "'a::euclidean_space set"
  assumes "convex U" "¬ collinear U" "countable S"
  shows "connected(U - S)"
  by (simp add: assms path_connected_convex_diff_countable path_connected_imp_connected)

lemma path_connected_punctured_convex:
  assumes "convex S" and aff: "aff_dim S  1"
    shows "path_connected(S - {a})"
proof -
  consider "aff_dim S = -1" | "aff_dim S = 0" | "aff_dim S  2"
    using assms aff_dim_geq [of S] by linarith
  then show ?thesis
  proof cases
    assume "aff_dim S = -1"
    then show ?thesis
      by (metis aff_dim_empty empty_Diff path_connected_empty)
  next
    assume "aff_dim S = 0"
    then show ?thesis
      by (metis aff_dim_eq_0 Diff_cancel Diff_empty Diff_insert0 convex_empty convex_imp_path_connected path_connected_singleton singletonD)
  next
    assume ge2: "aff_dim S  2"
    then have "¬ collinear S"
    proof (clarsimp simp: collinear_affine_hull)
      fix u v
      assume " affine hull {u, v}"
      then have "aff_dim S  aff_dim {u, v}"
        by (metis (no_types) aff_dim_affine_hull aff_dim_subset)
      with ge2 show False
        by (metis (no_types) aff_dim_2 antisym aff not_numeral_le_zero one_le_numeral order_trans)
    qed
    moreover have "countable {a}"
      by simp
    ultimately show ?thesis
      by (metis path_connected_convex_diff_countable [OF convex S])
  qed
qed

lemma connected_punctured_convex:
  shows "[convex S; aff_dim S  1] ==> connected(S - {a})"
  using path_connected_imp_connected path_connected_punctured_convex by blast

lemma path_connected_complement_countable:
  fixes S :: "'a::euclidean_space set"
  assumes " DIM('a)" "countable S"
  shows "path_connected(- S)"
proof -
  have "¬ collinear (UNIV::'a set)"
    using assms by (auto simp: collinear_aff_dim [of "UNIV :: 'a set"])
  then have "path_connected(UNIV - S)"
    by (simp add: countable S path_connected_convex_diff_countable)
  then show ?thesis
    by (simp add: Compl_eq_Diff_UNIV)
qed

proposition path_connected_openin_diff_countable:
  fixes S :: "'a::euclidean_space set"
  assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S"
      and "¬ collinear S" "countable T"
    shows "path_connected(S - T)"
proof (clarsimp simp: path_connected_component)
  fix x y
  assume xy: " S" " T" " S" " T"
  show "path_component (S - T) x y"
  proof (rule connected_equivalence_relation_gen [OF connected S, where P = "λx. x  T"])
    show "z. z  U  z  T" if opeU: "openin (top_of_set S) U" and " U" for U x
    proof -
      have "openin (top_of_set (affine hull S)) U"
        using opeU ope openin_trans by blast
      with x U obtain r where Usub: " affine hull S" and "r > 0"
                              and subU: "ball x r  affine hull S  U"
        by (auto simp: openin_contains_ball)
      with x U have x: " ball x r  affine hull S"
        by auto
      have "¬ S  {x}"
        using ¬ collinear S collinear_subset by blast
      then obtain x' where "x'  x" "x'  S"
        by blast
      obtain y where y: " x" " ball x r  affine hull S"
      proof
        show "x + (r / 2 / norm(x' - x)) *🪙R (x' - x)  x"
          using x' x r > 0 by auto
        show "x + (r / 2 / norm (x' - x)) *🪙R (x' - x)  ball x r  affine hull S"
          using x' x r > 0 x' S x
          by (simp add: dist_norm mem_affine_3_minus hull_inc)
      qed
      have "convex (ball x r  affine hull S)"
        by (simp add: affine_imp_convex convex_Int)
      with x y subU have "uncountable U"
        by (meson countable_subset uncountable_convex)
      then have "¬ U  T"
        using countable T countable_subset by blast
      then show ?thesis by blast
    qed
    show "U. openin (top_of_set S) U  x  U 
              (xU. yU. x  T  y  T  path_component (S - T) x y)"
          if " S" for x
    proof -
      obtain r where Ssub: " affine hull S" and "r > 0"
                 and subS: "ball x r  affine hull S  S"
        using ope x S by (auto simp: openin_contains_ball)
      then have conv: "convex (ball x r  affine hull S)"
        by (simp add: affine_imp_convex convex_Int)
      have "¬ aff_dim (affine hull S)  1"
        using ¬ collinear S collinear_aff_dim by auto
      then have "¬ aff_dim (ball x r  affine hull S)  1"
        by (metis (no_types, opaque_lifting) aff_dim_convex_Int_open IntI open_ball 0 < r aff_dim_affine_hull affine_affine_hull affine_imp_convex centre_in_ball empty_iff hull_subset inf_commute subsetCE that)
      then have "¬ collinear (ball x r  affine hull S)"
        by (simp add: collinear_aff_dim)
      then have *: "path_connected ((ball x r  affine hull S) - T)"
        by (rule path_connected_convex_diff_countable [OF conv _ countable T])
      have ST: "ball x r  affine hull S - T  S - T"
        using subS by auto
      show ?thesis
      proof (intro exI conjI)
        show " ball x r  affine hull S"
          using x S r > 0 by (simp add: hull_inc)
        have "openin (top_of_set (affine hull S)) (ball x r  affine hull S)"
          by (subst inf.commute) (simp add: openin_Int_open)
        then show "openin (top_of_set S) (ball x r  affine hull S)"
          by (rule openin_subset_trans [OF _ subS Ssub])
      qed (use * path_component_trans in auto simp: path_connected_component path_component_of_subset [OF ST])
    qed
  qed (use xy path_component_trans in auto)
qed

corollary connected_openin_diff_countable:
  fixes S :: "'a::euclidean_space set"
  assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S"
      and "¬ collinear S" "countable T"
    shows "connected(S - T)"
  by (metis path_connected_imp_connected path_connected_openin_diff_countable [OF assms])

corollary path_connected_open_diff_countable:
  fixes S :: "'a::euclidean_space set"
  assumes " DIM('a)" "open S" "connected S" "countable T"
  shows "path_connected(S - T)"
proof (cases "S = {}")
  case True
  then show ?thesis
    by (simp)
next
  case False
  show ?thesis
  proof (rule path_connected_openin_diff_countable)
    show "openin (top_of_set (affine hull S)) S"
      by (simp add: assms hull_subset open_subset)
    show "¬ collinear S"
      using assms False by (simp add: collinear_aff_dim aff_dim_open)
  qed (simp_all add: assms)
qed

corollary connected_open_diff_countable:
  fixes S :: "'a::euclidean_space set"
  assumes " DIM('a)" "open S" "connected S" "countable T"
  shows "connected(S - T)"
by (simp add: assms path_connected_imp_connected path_connected_open_diff_countable)



subsection🍋tag unimportant Self-homeomorphisms shuffling points about

subsubsection🍋tag unimportant\The theorem homeomorphism_moving_points_exists\

lemma homeomorphism_moving_point_1:
  fixes a :: "'a::euclidean_space"
  assumes "affine T" " T" and u: " ball a r  T"
  obtains f g where "homeomorphism (cball a r  T) (cball a r  T) f g"
                    "f a = u" "x. x  sphere a r ==> f x = x"
proof -
  have nou: "norm (u - a) < r" and " T"
    using u by (auto simp: dist_norm norm_minus_commute)
  then have "0 < r"
    by (metis DiffD1 Diff_Diff_Int ball_eq_empty centre_in_ball not_le u)
  define f where " λx. (1 - norm(x - a) / r) *🪙R (u - a) + x"
  have *: "False" if eq: "x + (norm y / r) *🪙R u = y + (norm x / r) *🪙R u"
                  and nou: "norm u < r" and yx: "norm y < norm x" for x y and u::'a
  proof -
    have "x = y + (norm x / r - (norm y / r)) *🪙R u"
      using eq by (simp add: algebra_simps)
    then have "norm x = norm (y + ((norm x - norm y) / r) *🪙R u)"
      by (metis diff_divide_distrib)
    also have "  norm y + norm(((norm x - norm y) / r) *🪙R u)"
      using norm_triangle_ineq by blast
    also have " = norm y + (norm x - norm y) * (norm u / r)"
      using yx r > 0
      by (simp add: field_split_simps)
    also have " < norm y + (norm x - norm y) * 1"
    proof (subst add_less_cancel_left)
      show "(norm x - norm y) * (norm u / r) < (norm x - norm y) * 1"
      proof (rule mult_strict_left_mono)
        show "norm u / r < 1"
          using 0 < r divide_less_eq_1_pos nou by blast
      qed (simp add: yx)
    qed
    also have " = norm x"
      by simp
    finally show False by simp
  qed
  have "inj f"
    unfolding f_def
  proof (clarsimp simp: inj_on_def)
    fix x y
    assume "(1 - norm (x - a) / r) *🪙R (u - a) + x =
            (1 - norm (y - a) / r) *🪙R (u - a) + y"
    then have eq: "(x - a) + (norm (y - a) / r) *🪙R (u - a) = (y - a) + (norm (x - a) / r) *🪙R (u - a)"
      by (auto simp: algebra_simps)
    show "x=y"
    proof (cases "norm (x - a) = norm (y - a)")
      case True
      then show ?thesis
        using eq by auto
    next
      case False
      then consider "norm (x - a) < norm (y - a)" | "norm (x - a) > norm (y - a)"
        by linarith
      then have "False"
      proof cases
        case 1 show False
          using * [OF _ nou 1] eq by simp
      next
        case 2 with * [OF eq nou] show False
          by auto
      qed
      then show "x=y" ..
    qed
  qed
  then have inj_onf: "inj_on f (cball a r  T)"
    using inj_on_Int by fastforce
  have contf: "continuous_on (cball a r  T) f"
    unfolding f_def using 0 < r by (intro continuous_intros) blast
  have fim: "f ` (cball a r  T) = cball a r  T"
  proof
    have *: "norm (y + (1 - norm y / r) *🪙R u)  r" if "norm y  r" "norm u < r" for y u::'a
    proof -
      have "norm (y + (1 - norm y / r) *🪙R u)  norm y + norm((1 - norm y / r) *🪙R u)"
        using norm_triangle_ineq by blast
      also have " = norm y + abs(1 - norm y / r) * norm u"
        by simp
      also have "  r"
      proof -
        have "(r - norm u) * (r - norm y)  0"
          using that by auto
        then have "r * norm u + r * norm y  r * r + norm u * norm y"
          by (simp add: algebra_simps)
        then show ?thesis
        using that 0 < r by (simp add: abs_if field_simps)
      qed
      finally show ?thesis .
    qed
    have "f ` (cball a r)  cball a r"
      using * nou
      apply (clarsimp simp: dist_norm norm_minus_commute f_def)
      by (metis diff_add_eq diff_diff_add diff_diff_eq2 norm_minus_commute)
    moreover have "f ` T  T"
      unfolding f_def using affine T a T u T
      by (force simp: add.commute mem_affine_3_minus)
    ultimately show "f ` (cball a r  T)  cball a r  T"
      by blast
  next
    show "cball a r  T  f ` (cball a r  T)"
    proof (clarsimp simp: dist_norm norm_minus_commute)
      fix x
      assume x: "norm (x - a)  r" and " T"
      have " {0..1}. ((1 - v) * r - norm ((x - a) - v *🪙R (u - a)))  1 = 0"
        by (rule ivt_decreasing_component_on_1) (auto simp: x continuous_intros)
      then obtain v where " v" " 1"
        and v: "(1 - v) * r = norm ((x - a) - v *🪙R (u - a))"
        by auto
      then have n: "norm (a - (x - v *🪙R (u - a))) = r - r * v"
        by (simp add: field_simps norm_minus_commute)
      show " f ` (cball a r  T)"
      proof (rule image_eqI)
        show "x = f (x - v *🪙R (u - a))"
          using r > 0 v by (simp add: f_def) (simp add: field_simps)
        have "x - v *🪙R (u - a)  cball a r"
          using r > 0\0 v
          by (simp add: dist_norm n)
        moreover have "x - v *🪙R (u - a)  T"
          by (simp add: f_def u T x T assms mem_affine_3_minus2)
        ultimately show "x - v *🪙R (u - a)  cball a r  T"
          by blast
      qed
    qed
  qed
  have "compact (cball a r  T)"
    by (simp add: affine_closed compact_Int_closed affine T)
  then obtain g where "homeomorphism (cball a r  T) (cball a r  T) f g"
    by (metis homeomorphism_compact [OF _ contf fim inj_onf])
  then show thesis
    apply (rule_tac f=f in that)
    using r > 0 by (simp_all add: f_def dist_norm norm_minus_commute)
qed

corollary🍋tag unimportant homeomorphism_moving_point_2:
  fixes a :: "'a::euclidean_space"
  assumes "affine T" " T" and u: " ball a r  T" and v: " ball a r  T"
  obtains f g where "homeomorphism (cball a r  T) (cball a r  T) f g"
                    "f u = v" "x. [ sphere a r; x  T] ==> f x = x"
proof -
  have "0 < r"
    by (metis DiffD1 Diff_Diff_Int ball_eq_empty centre_in_ball not_le u)
  obtain f1 g1 where hom1: "homeomorphism (cball a r  T) (cball a r  T) f1 g1"
                 and "f1 a = u" and f1: "x. x  sphere a r ==> f1 x = x"
    using homeomorphism_moving_point_1 [OF affine T a T u] by blast
  obtain f2 g2 where hom2: "homeomorphism (cball a r  T) (cball a r  T) f2 g2"
                 and "f2 a = v" and f2: "x. x  sphere a r ==> f2 x = x"
    using homeomorphism_moving_point_1 [OF affine T a T v] by blast
  show ?thesis
  proof
    show "homeomorphism (cball a r  T) (cball a r  T) (f2  g1) (f1  g2)"
      by (metis homeomorphism_compose homeomorphism_symD hom1 hom2)
    have "g1 u = a"
      using 0 < r f1 a = u assms hom1 homeomorphism_apply1 by fastforce
    then show "(f2  g1) u = v"
      by (simp add: f2 a = v)
    show "x. [ sphere a r; x  T] ==> (f2  g1) x = x"
      using f1 f2 hom1 homeomorphism_apply1 by fastforce
  qed
qed


corollary🍋tag unimportant homeomorphism_moving_point_3:
  fixes a :: "'a::euclidean_space"
  assumes "affine T" " T" and ST: "ball a r  T  S" " T"
      and u: " ball a r  T" and v: " ball a r  T"
  obtains f g where "homeomorphism S S f g"
                    "f u = v" "{x. ¬ (f x = x  g x = x)}  ball a r  T"
proof -
  obtain f g where hom: "homeomorphism (cball a r  T) (cball a r  T) f g"
               and "f u = v" and fid: "x. [ sphere a r; x  T] ==> f x = x"
    using homeomorphism_moving_point_2 [OF affine T a T u v] by blast
  have gid: "x. [ sphere a r; x  T] ==> g x = x"
    using fid hom homeomorphism_apply1 by fastforce
  define ff where "ff  λx. if x  ball a r  T then f x else x"
  define gg where "gg  λx. if x  ball a r  T then g x else x"
  show ?thesis
  proof
    show "homeomorphism S S ff gg"
    proof (rule homeomorphismI)
      have "continuous_on ((cball a r  T)  (T - ball a r)) ff"
        unfolding ff_def
        using homeomorphism_cont1 [OF hom]
        by (intro continuous_on_cases) (auto simp: affine_closed affine T fid)
      then show "continuous_on S ff"
        by (rule continuous_on_subset) (use ST in auto)
      have "continuous_on ((cball a r  T)  (T - ball a r)) gg"
        unfolding gg_def
        using homeomorphism_cont2 [OF hom]
        by (intro continuous_on_cases) (auto simp: affine_closed affine T gid)
      then show "continuous_on S gg"
        by (rule continuous_on_subset) (use ST in auto)
      show "ff ` S  S"
      proof (clarsimp simp: ff_def)
        fix x
        assume " S" and x: "dist a x < r" and " T"
        then have "f x  cball a r  T"
          using homeomorphism_image1 [OF hom] by force
        then show "f x  S"
          using ST(1) x T gid hom homeomorphism_def x by fastforce
      qed
      show "gg ` S  S"
      proof (clarsimp simp: gg_def)
        fix x
        assume " S" and x: "dist a x < r" and " T"
        then have "g x  cball a r  T"
          using homeomorphism_image2 [OF hom] by force
        then have "g x  ball a r"
          using homeomorphism_apply2 [OF hom]
            by (metis Diff_Diff_Int Diff_iff x T cball_def fid le_less mem_Collect_eq mem_ball mem_sphere x)
        then show "g x  S"
          using ST(1) g x cball a r T by force
        qed
      show "x. x  S ==> gg (ff x) = x"
        unfolding ff_def gg_def
        using homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom]
        by simp (metis Int_iff homeomorphism_apply1 [OF hom] fid image_eqI less_eq_real_def mem_cball mem_sphere)
      show "x. x  S ==> ff (gg x) = x"
        unfolding ff_def gg_def
        using homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom]
        by simp (metis Int_iff fid image_eqI less_eq_real_def mem_cball mem_sphere)
    qed
    show "ff u = v"
      using u by (auto simp: ff_def f u = v)
    show "{x. ¬ (ff x = x  gg x = x)}  ball a r  T"
      by (auto simp: ff_def gg_def)
  qed
qed


proposition🍋tag unimportant homeomorphism_moving_point:
  fixes a :: "'a::euclidean_space"
  assumes ope: "openin (top_of_set (affine hull S)) S"
      and " T"
      and TS: " affine hull S"
      and S: "connected S" " S" " S"
  obtains f g where "homeomorphism T T f g" "f a = b"
                    "{x. ¬ (f x = x  g x = x)}  S"
                    "bounded {x. ¬ (f x = x  g x = x)}"
proof -
  have 1: "h k. homeomorphism T T h k  h (f d) = d 
              {x. ¬ (h x = x  k x = x)}  S  bounded {x. ¬ (h x = x  k x = x)}"
        if " S" "f d  S" and homfg: "homeomorphism T T f g"
        and S: "{x. ¬ (f x = x  g x = x)}  S"
        and bo: "bounded {x. ¬ (f x = x  g x = x)}" for d f g
  proof (intro exI conjI)
    show homgf: "homeomorphism T T g f"
      by (metis homeomorphism_symD homfg)
    then show "g (f d) = d"
      by (meson S T homeomorphism_def subsetD d S)
    show "{x. ¬ (g x = x  f x = x)}  S"
      using S by blast
    show "bounded {x. ¬ (g x = x  f x = x)}"
      using bo by (simp add: conj_commute)
  qed
  have 2: "f g. homeomorphism T T f g  f x = f2 (f1 x) 
                 {x. ¬ (f x = x  g x = x)}  S  bounded {x. ¬ (f x = x  g x = x)}"
             if " S" "f1 x  S" "f2 (f1 x)  S"
                and hom: "homeomorphism T T f1 g1" "homeomorphism T T f2 g2"
                and sub: "{x. ¬ (f1 x = x  g1 x = x)}  S" "{x. ¬ (f2 x = x  g2 x = x)}  S"
                and bo: "bounded {x. ¬ (f1 x = x  g1 x = x)}" "bounded {x. ¬ (f2 x = x  g2 x = x)}"
             for x f1 f2 g1 g2
  proof (intro exI conjI)
    show homgf: "homeomorphism T T (f2  f1) (g1  g2)"
      by (metis homeomorphism_compose hom)
    then show "(f2  f1) x = f2 (f1 x)"
      by force
    show "{x. ¬ ((f2  f1) x = x  (g1  g2) x = x)}  S"
      using sub by force
    have "bounded ({x. ¬(f1 x = x  g1 x = x)}  {x. ¬(f2 x = x  g2 x = x)})"
      using bo by simp
    then show "bounded {x. ¬ ((f2  f1) x = x  (g1  g2) x = x)}"
      by (rule bounded_subset) auto
  qed
  have 3: "U. openin (top_of_set S) U 
              d  U 
              (xU.
                  f g. homeomorphism T T f g  f d = x 
                        {x. ¬ (f x = x  g x = x)}  S 
                        bounded {x. ¬ (f x = x  g x = x)})"
           if " S" for d
  proof -
    obtain r where "r > 0" and r: "ball d r  affine hull S  S"
      by (metis d S ope openin_contains_ball)
    have *: "f g. homeomorphism T T f g  f d = e 
                   {x. ¬ (f x = x  g x = x)}  S 
                   bounded {x. ¬ (f x = x  g x = x)}" if " S" " ball d r" for e
      apply (rule homeomorphism_moving_point_3 [of "affine hull S" d r T d e])
      using r S T TS that
            apply (auto simp: d S 0 < r hull_inc)
      using bounded_subset by blast
    show ?thesis
      by (rule_tac x=" ball d r" in exI) (fastforce simp: openin_open_Int 0 < r that intro: *)
  qed
  have "f g. homeomorphism T T f g  f a = b 
              {x. ¬ (f x = x  g x = x)}  S  bounded {x. ¬ (f x = x  g x = x)}"
    by (rule connected_equivalence_relation [OF S]; blast intro: 1 2 3)
  then show ?thesis
    using that by auto
qed


lemma homeomorphism_moving_points_exists_gen:
  assumes K: "finite K" "i. i  K ==> x i  S  y i  S"
             "pairwise (λi j. (x i  x j)  (y i  y j)) K"
      and " aff_dim S"
      and ope: "openin (top_of_set (affine hull S)) S"
      and " T" " affine hull S" "connected S"
  shows "f g. homeomorphism T T f g  ( K. f(x i) = y i) 
               {x. ¬ (f x = x  g x = x)}  S  bounded {x. ¬ (f x = x  g x = x)}"
  using assms
proof (induction K)
  case empty
  then show ?case
    by (force simp: homeomorphism_ident)
next
  case (insert i K)
  then have xney: "j. [ K; j  i] ==> x i  x j  y i  y j"
       and pw: "pairwise (λi j. x i  x j  y i  y j) K"
       and "x i  S" "y i  S"
       and xyS: "i. i  K ==> x i  S  y i  S"
    by (simp_all add: pairwise_insert)
  obtain f g where homfg: "homeomorphism T T f g" and feq: "i. i  K ==> f(x i) = y i"
               and fg_sub: "{x. ¬ (f x = x  g x = x)}  S"
               and bo_fg: "bounded {x. ¬ (f x = x  g x = x)}"
    using insert.IH [OF xyS pw] insert.prems by (blast intro: that)
  then have "f g. homeomorphism T T f g  ( K. f(x i) = y i) 
                   {x. ¬ (f x = x  g x = x)}  S  bounded {x. ¬ (f x = x  g x = x)}"
    using insert by blast
  have aff_eq: "affine hull (S - y ` K) = affine hull S"
  proof (rule affine_hull_Diff [OF ope])
    show "finite (y ` K)"
      by (simp add: insert.hyps(1))
    show "y ` K  S"
      using y i S insert.hyps(2) xney xyS by fastforce
  qed
  have f_in_S: "f x  S" if " S" for x
    using homfg fg_sub homeomorphism_apply1 S T
  proof -
    have "(f (f x)  f x  g (f x)  f x)  f x  S"
      by (metis S T homfg subsetD homeomorphism_apply1 that)
    then show ?thesis
      using fg_sub by force
  qed
  obtain h k where homhk: "homeomorphism T T h k" and heq: "h (f (x i)) = y i"
               and hk_sub: "{x. ¬ (h x = x  k x = x)}  S - y ` K"
               and bo_hk: "bounded {x. ¬ (h x = x  k x = x)}"
  proof (rule homeomorphism_moving_point [of "S - y`K" T "f(x i)" "y i"])
    show "openin (top_of_set (affine hull (S - y ` K))) (S - y ` K)"
      by (simp add: aff_eq openin_diff finite_imp_closedin image_subset_iff hull_inc insert xyS)
    show "S - y ` K  T"
      using S T by auto
    show " affine hull (S - y ` K)"
      using insert by (simp add: aff_eq)
    show "connected (S - y ` K)"
    proof (rule connected_openin_diff_countable [OF connected S ope])
      show "¬ collinear S"
        using collinear_aff_dim 2 aff_dim S by force
      show "countable (y ` K)"
        using countable_finite insert.hyps(1) by blast
    qed
    have "k. [f (x i) = y k; k  K] ==> False"
        by (metis feq homfg x i S homeomorphism_def S T i K subsetCE xney xyS)
    then show "f (x i)  S - y ` K"
      by (auto simp: f_in_S x i S)
    show "y i  S - y ` K"
      using insert.hyps xney by (auto simp: y i S)
  qed blast
  show ?case
  proof (intro exI conjI)
    show "homeomorphism T T (h  f) (g  k)"
      using homfg homhk homeomorphism_compose by blast
    show " insert i K. (h  f) (x i) = y i"
      using feq hk_sub by (auto simp: heq)
    show "{x. ¬ ((h  f) x = x  (g  k) x = x)}  S"
      using fg_sub hk_sub by force
    have "bounded ({x. ¬(f x = x  g x = x)}  {x. ¬(h x = x  k x = x)})"
      using bo_fg bo_hk bounded_Un by blast
    then show "bounded {x. ¬ ((h  f) x = x  (g  k) x = x)}"
      by (rule bounded_subset) auto
  qed
qed

proposition🍋tag unimportant homeomorphism_moving_points_exists:
  fixes S :: "'a::euclidean_space set"
  assumes 2: " DIM('a)" "open S" "connected S" " T" "finite K"
      and KS: "i. i  K ==> x i  S  y i  S"
      and pw: "pairwise (λi j. (x i  x j)  (y i  y j)) K"
      and S: " T" " affine hull S" "connected S"
  obtains f g where "homeomorphism T T f g" "i. i  K ==> f(x i) = y i"
                    "{x. ¬ (f x = x  g x = x)}  S" "bounded {x. (¬ (f x = x  g x = x))}"
proof (cases "S = {}")
  case True
  then show ?thesis
    using KS homeomorphism_ident that by fastforce
next
  case False
  then have affS: "affine hull S = UNIV"
    by (simp add: affine_hull_open open S)
  then have ope: "openin (top_of_set (affine hull S)) S"
    using open S open_openin by auto
  have " DIM('a)" by (rule 2)
  also have " = aff_dim (UNIV :: 'a set)"
    by simp
  also have "  aff_dim S"
    by (metis aff_dim_UNIV aff_dim_affine_hull aff_dim_le_DIM affS)
  finally have " aff_dim S"
    by linarith
  then show ?thesis
    using homeomorphism_moving_points_exists_gen [OF finite K KS pw _ ope S] that by fastforce
qed

subsubsection🍋tag unimportant\The theorem homeomorphism_grouping_points_exists\

lemma homeomorphism_grouping_point_1:
  fixes a::real and c::real
  assumes "a < b" "c < d"
  obtains f g where "homeomorphism (cbox a b) (cbox c d) f g" "f a = c" "f b = d"
proof -
  define f where " λx. ((d - c) / (b - a)) * x + (c - a * ((d - c) / (b - a)))"
  have "g. homeomorphism (cbox a b) (cbox c d) f g"
  proof (rule homeomorphism_compact)
    show "continuous_on (cbox a b) f"
      unfolding f_def by (intro continuous_intros)
    have "f ` {a..b} = {c..d}"
      unfolding f_def image_affinity_atLeastAtMost
      using assms sum_sqs_eq by (auto simp: field_split_simps)
    then show "f ` cbox a b = cbox c d"
      by auto
    show "inj_on f (cbox a b)"
      unfolding f_def inj_on_def using assms by auto
  qed auto
  then obtain g where "homeomorphism (cbox a b) (cbox c d) f g" ..
  then show ?thesis
  proof
    show "f a = c"
      by (simp add: f_def)
    show "f b = d"
      using assms sum_sqs_eq [of a b] by (auto simp: f_def field_split_simps)
  qed
qed

lemma homeomorphism_grouping_point_2:
  fixes a::real and w::real
  assumes hom_ab: "homeomorphism (cbox a b) (cbox u v) f1 g1"
      and hom_bc: "homeomorphism (cbox b c) (cbox v w) f2 g2"
      and " cbox a c" " cbox u w"
      and eq: "f1 a = u" "f1 b = v" "f2 b = v" "f2 c = w"
 obtains f g where "homeomorphism (cbox a c) (cbox u w) f g" "f a = u" "f c = w"
                   "x. x  cbox a b ==> f x = f1 x" "x. x  cbox b c ==> f x = f2 x"
proof -
  have le: " b" " c" " v" " w"
    using assms by simp_all
  then have ac: "cbox a c = cbox a b  cbox b c" and uw: "cbox u w = cbox u v  cbox v w"
    by auto
  define f where " λx. if x  b then f1 x else f2 x"
  have "g. homeomorphism (cbox a c) (cbox u w) f g"
  proof (rule homeomorphism_compact)
    have cf1: "continuous_on (cbox a b) f1"
      using hom_ab homeomorphism_cont1 by blast
    have cf2: "continuous_on (cbox b c) f2"
      using hom_bc homeomorphism_cont1 by blast
    show "continuous_on (cbox a c) f"
      unfolding f_def using le eq
      by (force intro: continuous_on_cases_le [OF continuous_on_subset [OF cf1] continuous_on_subset [OF cf2]])
    have "f ` cbox a b = f1 ` cbox a b" "f ` cbox b c = f2 ` cbox b c"
      unfolding f_def using eq by force+
    then show "f ` cbox a c = cbox u w"
      unfolding ac uw image_Un by (metis hom_ab hom_bc homeomorphism_def)
    have neq12: "f1 x  f2 y" if x: " x" " b" and y: "b < y" " c" for x y
    proof -
      have "f1 x  cbox u v"
        by (metis hom_ab homeomorphism_def image_eqI mem_box_real(2) x)
      moreover have "f2 y  cbox v w"
        by (metis (full_types) hom_bc homeomorphism_def image_subset_iff mem_box_real(2) not_le not_less_iff_gr_or_eq order_refl y)
      moreover have "f2 y  f2 b"
        by (metis cancel_comm_monoid_add_class.diff_cancel diff_gt_0_iff_gt hom_bc homeomorphism_def le(2) less_imp_le less_numeral_extra(3) mem_box_real(2) order_refl y)
      ultimately show ?thesis
        using le eq by simp
    qed
    have "inj_on f1 (cbox a b)"
      by (metis (full_types) hom_ab homeomorphism_def inj_onI)
    moreover have "inj_on f2 (cbox b c)"
      by (metis (full_types) hom_bc homeomorphism_def inj_onI)
    ultimately show "inj_on f (cbox a c)"
      apply (simp (no_asm) add: inj_on_def)
      apply (simp add: f_def inj_on_eq_iff)
      using neq12 by force
  qed auto
  then obtain g where "homeomorphism (cbox a c) (cbox u w) f g" ..
  then show ?thesis
    using eq f_def le that by force
qed

lemma homeomorphism_grouping_point_3:
  fixes a::real
  assumes cbox_sub: "cbox c d  box a b" "cbox u v  box a b"
      and box_ne: "box c d  {}" "box u v  {}"
  obtains f g where "homeomorphism (cbox a b) (cbox a b) f g" "f a = a" "f b = b"
                    "x. x  cbox c d ==> f x  cbox u v"
proof -
  have less: "a < c" "a < u" "d < b" "v < b" "c < d" "u < v" "cbox c d  {}"
    using assms
    by (simp_all add: cbox_sub subset_eq)
  obtain f1 g1 where 1: "homeomorphism (cbox a c) (cbox a u) f1 g1"
                   and f1_eq: "f1 a = a" "f1 c = u"
    using homeomorphism_grouping_point_1 [OF a < c a < u] .
  obtain f2 g2 where 2: "homeomorphism (cbox c d) (cbox u v) f2 g2"
                   and f2_eq: "f2 c = u" "f2 d = v"
    using homeomorphism_grouping_point_1 [OF c < d u < v] .
  obtain f3 g3 where 3: "homeomorphism (cbox d b) (cbox v b) f3 g3"
                   and f3_eq: "f3 d = v" "f3 b = b"
    using homeomorphism_grouping_point_1 [OF d < b v < b] .
  obtain f4 g4 where 4: "homeomorphism (cbox a d) (cbox a v) f4 g4" and "f4 a = a" "f4 d = v"
                 and f4_eq: "x. x  cbox a c ==> f4 x = f1 x" "x. x  cbox c d ==> f4 x = f2 x"
    using homeomorphism_grouping_point_2 [OF 1 2] less by (auto simp: f1_eq f2_eq)
  obtain f g where fg: "homeomorphism (cbox a b) (cbox a b) f g" "f a = a" "f b = b"
               and f_eq: "x. x  cbox a d ==> f x = f4 x" "x. x  cbox d b ==> f x = f3 x"
    using homeomorphism_grouping_point_2 [OF 4 3] less by (auto simp: f4_eq f3_eq f2_eq f1_eq)
  show ?thesis
  proof (rule that [OF fg])
    show "f x  cbox u v" if " cbox c d" for x
      using that f4_eq f_eq homeomorphism_image1 [OF 2]
      by (metis atLeastAtMost_iff box_real(2) image_eqI less(1) less_eq_real_def order_trans)
  qed
qed


lemma homeomorphism_grouping_point_4:
  fixes T :: "real set"
  assumes "open U" "open S" "connected S" " {}" "finite K" " S" " S" " T"
  obtains f g where "homeomorphism T T f g"
                    "x. x  K ==> f x  U" "{x. (¬ (f x = x  g x = x))}  S"
                    "bounded {x. (¬ (f x = x  g x = x))}"
proof -
  obtain c d where "box c d  {}" "cbox c d  U"
  proof -
    obtain u where " U"
      using U {} by blast
    then obtain e where "e > 0" "cball u e  U"
      using open U open_contains_cball by blast
    then show ?thesis
      by (rule_tac c=u and d="u+e" in that) (auto simp: dist_norm subset_iff)
  qed
  have "compact K"
    by (simp add: finite K finite_imp_compact)
  obtain a b where "box a b  {}" " cbox a b" "cbox a b  S"
  proof (cases "K = {}")
    case True then show ?thesis
      using box c d {} cbox c d U U S that by blast
  next
    case False
    then obtain a b where " K" " K"
            and a: "x. x  K ==> a  x" and b: "x. x  K ==> x  b"
      using compact_attains_inf compact_attains_sup by (metis compact K)+
    obtain e where "e > 0" "cball b e  S"
      using open S open_contains_cball
      by (metis b K K S subsetD)
    show ?thesis
    proof
      show "box a (b + e)  {}"
        using 0 < e b K a by force
      show " cbox a (b + e)"
        using 0 < e a b by fastforce
      have " S"
        using a K assms(6) by blast
      have "b + e  S"
        using 0 < e cball b e S by (force simp: dist_norm)
      show "cbox a (b + e)  S"
        using a S b + e S connected S connected_contains_Icc by auto
    qed
  qed
  obtain w z where "cbox w z  S" and sub_wz: "cbox a b  cbox c d  box w z"
  proof -
    have " S" " S"
      using box a b {} cbox a b S by auto
    moreover have " S" " S"
      using box c d {} cbox c d U U S by force+
    ultimately have "min a c  S" "max b d  S"
      by linarith+
    then obtain e1 e2 where "e1 > 0" "cball (min a c) e1  S" "e2 > 0" "cball (max b d) e2  S"
      using open S open_contains_cball by metis
    then have *: "min a c - e1  S" "max b d + e2  S"
      by (auto simp: dist_norm)
    show ?thesis
    proof
      show "cbox (min a c - e1) (max b d+ e2)  S"
        using * connected S connected_contains_Icc by auto
      show "cbox a b  cbox c d  box (min a c - e1) (max b d + e2)"
        using 0 < e1 0 < e2 by auto
    qed
  qed
  then
  obtain f g where hom: "homeomorphism (cbox w z) (cbox w z) f g"
               and "f w = w" "f z = z"
               and fin: "x. x  cbox a b ==> f x  cbox c d"
    using homeomorphism_grouping_point_3 [of a b w z c d]
    using box a b {} box c d {} by blast
  have contfg: "continuous_on (cbox w z) f" "continuous_on (cbox w z) g"
    using hom homeomorphism_def by blast+
  define f' where "f'  λx. if x  cbox w z then f x else x"
  define g' where "g'  λx. if x  cbox w z then g x else x"
  show ?thesis
  proof
    have T: "cbox w z  (T - box w z) = T"
      using cbox w z S S T by auto
    show "homeomorphism T T f' g'"
    proof
      have clo: "closedin (top_of_set (cbox w z  (T - box w z))) (T - box w z)"
        by (metis Diff_Diff_Int Diff_subset T closedin_def open_box openin_open_Int topspace_euclidean_subtopology)
      have "x. [ x  x  z; w < x  ¬ x < z] ==> f x = x"
        using f w = w f z = z by auto
      moreover have "x. [ x  x  z; w < x  ¬ x < z] ==> g x = x"
        using f w = w f z = z hom homeomorphism_apply1 by fastforce
      ultimately
      have "continuous_on (cbox w z  (T - box w z)) f'" "continuous_on (cbox w z  (T - box w z)) g'"
        unfolding f'_def g'_def
        by (intro continuous_on_cases_local contfg continuous_on_id clo; auto simp: closed_subset)+
      then show "continuous_on T f'" "continuous_on T g'"
        by (simp_all only: T)
      show "f' ` T  T"
        unfolding f'_def
        by clarsimp (metis cbox w z S S T subsetD hom homeomorphism_def imageI mem_box_real(2))
      show "g' ` T  T"
        unfolding g'_def
        by clarsimp (metis cbox w z S S T subsetD hom homeomorphism_def imageI mem_box_real(2))
      show "x. x  T ==> g' (f' x) = x"
        unfolding f'_def g'_def
        using homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] by fastforce
      show "y. y  T ==> f' (g' y) = y"
        unfolding f'_def g'_def
        using homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] by fastforce
    qed
    show "x. x  K ==> f' x  U"
      using fin sub_wz K cbox a b cbox c d U by (force simp: f'_def)
    show "{x. ¬ (f' x = x  g' x = x)}  S"
      using cbox w z S by (auto simp: f'_def g'_def)
    show "bounded {x. ¬ (f' x = x  g' x = x)}"
    proof (rule bounded_subset [of "cbox w z"])
      show "bounded (cbox w z)"
        using bounded_cbox by blast
      show "{x. ¬ (f' x = x  g' x = x)}  cbox w z"
        by (auto simp: f'_def g'_def)
    qed
  qed
qed

proposition🍋tag unimportant homeomorphism_grouping_points_exists:
  fixes S :: "'a::euclidean_space set"
  assumes "open U" "open S" "connected S" " {}" "finite K" " S" " S" " T"
  obtains f g where "homeomorphism T T f g" "{x. (¬ (f x = x  g x = x))}  S"
                    "bounded {x. (¬ (f x = x  g x = x))}" "x. x  K ==> f x  U"
proof (cases " DIM('a)")
  case True
  have TS: " affine hull S"
    using affine_hull_open assms by blast
  have "infinite U"
    using open U U {} finite_imp_not_open by blast
  then obtain P where " U" "finite P" "card K = card P"
    using infinite_arbitrarily_large by metis
  then obtain γ where γ: "bij_betw γ K P"
    using finite K finite_same_card_bij by blast
  obtain f g where "homeomorphism T T f g" "i. i  K ==> f (id i) = γ i" "{x. ¬ (f x = x  g x = x)}  S" "bounded {x. ¬ (f x = x  g x = x)}"
  proof (rule homeomorphism_moving_points_exists [OF True open S connected S S T finite K])
    show "i. i  K ==> id i  S  γ i  S"
      using P U bij_betw γ K P K S U S bij_betwE by blast
    show "pairwise (λi j. id i  id j  γ i  γ j) K"
      using γ by (auto simp: pairwise_def bij_betw_def inj_on_def)
  qed (use affine_hull_open assms that in auto)
  then show ?thesis
    using γ P U bij_betwE by (fastforce simp: intro!: that)
next
  case False
  with DIM_positive have "DIM('a) = 1"
    by (simp add: dual_order.antisym)
  then obtain h::"'a ==>real" and j
  where "linear h" "linear j"
    and noh: "x. norm(h x) = norm x" and noj: "y. norm(j y) = norm y"
    and hj: "x. j(h x) = x" "y. h(j y) = y"
    and ranh: "surj h"
    using isomorphisms_UNIV_UNIV
    by (metis (mono_tags, opaque_lifting) DIM_real UNIV_eq_I range_eqI)
  obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g"
               and f: "x. x  h ` K ==> f x  h ` U"
               and sub: "{x. ¬ (f x = x  g x = x)}  h ` S"
               and bou: "bounded {x. ¬ (f x = x  g x = x)}"
    apply (rule homeomorphism_grouping_point_4 [of "h ` U" "h ` S" "h ` K" "h ` T"])
    by (simp_all add: assms image_mono linear h open_surjective_linear_image connected_linear_image ranh)
  have jf: "j (f (h x)) = x  f (h x) = h x" for x
    by (metis hj)
  have jg: "j (g (h x)) = x  g (h x) = h x" for x
    by (metis hj)
  have cont_hj: "continuous_on X h" "continuous_on Y j" for X Y
    by (simp_all add: linear h linear j linear_linear linear_continuous_on)
  show ?thesis
  proof
    show "homeomorphism T T (j  f  h) (j  g  h)"
    proof
      show "continuous_on T (j  f  h)" "continuous_on T (j  g  h)"
        using hom homeomorphism_def
        by (blast intro: continuous_on_compose cont_hj)+
      show "(j  f  h) ` T  T" "(j  g  h) ` T  T"
        by auto (metis (mono_tags, opaque_lifting) hj(1) hom homeomorphism_def imageE imageI)+
      show "x. x  T ==> (j  g  h) ((j  f  h) x) = x"
        using hj hom homeomorphism_apply1 by fastforce
      show "y. y  T ==> (j  f  h) ((j  g  h) y) = y"
        using hj hom homeomorphism_apply2 by fastforce
    qed
    show "{x. ¬ ((j  f  h) x = x  (j  g  h) x = x)}  S"
    proof (clarsimp simp: jf jg hj)
      show "f (h x) = h x  g (h x)  h x ==> x  S" for x
        using sub [THEN subsetD, of "h x"] hj by simp (metis imageE)
    qed
    have "bounded (j ` {x. (¬ (f x = x  g x = x))})"
      by (rule bounded_linear_image [OF bou]) (use linear j linear_conv_bounded_linear in auto)
    moreover
    have *: "{x. ¬((j  f  h) x = x  (j  g  h) x = x)} = j ` {x. (¬ (f x = x  g x = x))}"
      using hj by (auto simp: jf jg image_iff, metis+)
    ultimately show "bounded {x. ¬ ((j  f  h) x = x  (j  g  h) x = x)}"
      by metis
    show "x. x  K ==> (j  f  h) x  U"
      using f hj by fastforce
  qed
qed


proposition🍋tag unimportant homeomorphism_grouping_points_exists_gen:
  fixes S :: "'a::euclidean_space set"
  assumes opeU: "openin (top_of_set S) U"
      and opeS: "openin (top_of_set (affine hull S)) S"
      and " {}" "finite K" " S" and S: " T" " affine hull S" "connected S"
  obtains f g where "homeomorphism T T f g" "{x. (¬ (f x = x  g x = x))}  S"
                    "bounded {x. (¬ (f x = x  g x = x))}" "x. x  K ==> f x  U"
proof (cases " aff_dim S")
  case True
  have opeU': "openin (top_of_set (affine hull S)) U"
    using opeS opeU openin_trans by blast
  obtain u where " U" " S"
    using U {} opeU openin_imp_subset by fastforce+
  have "infinite U"
  proof (rule infinite_openin [OF opeU u U])
    show "u islimpt S"
      using True u S assms(8) connected_imp_perfect_aff_dim by fastforce
  qed
  then obtain P where " U" "finite P" "card K = card P"
    using infinite_arbitrarily_large by metis
  then obtain γ where γ: "bij_betw γ K P"
    using finite K finite_same_card_bij by blast
  have "f g. homeomorphism T T f g  ( K. f(id i) = γ i) 
               {x. ¬ (f x = x  g x = x)}  S  bounded {x. ¬ (f x = x  g x = x)}"
  proof (rule homeomorphism_moving_points_exists_gen [OF finite K _ _ True opeS S])
    show "i. i  K ==> id i  S  γ i  S"
      by (metis id_apply opeU openin_contains_cball subsetCE P U bij_betw γ K P K S bij_betwE)
    show "pairwise (λi j. id i  id j  γ i  γ j) K"
      using γ by (auto simp: pairwise_def bij_betw_def inj_on_def)
  qed
  then show ?thesis
    using γ P U bij_betwE by (fastforce simp: intro!: that)
next
  case False
  with aff_dim_geq [of S] consider "aff_dim S = -1" | "aff_dim S = 0" | "aff_dim S = 1" by linarith
  then show ?thesis
  proof cases
    assume "aff_dim S = -1"
    then have "S = {}"
      using aff_dim_empty by blast
    then have "False"
      using U {} K S openin_imp_subset [OF opeU] by blast
    then show ?thesis ..
  next
    assume "aff_dim S = 0"
    then obtain a where "S = {a}"
      using aff_dim_eq_0 by blast
    then have " U"
      using U {} K S openin_imp_subset [OF opeU] by blast
    show ?thesis
      using K U by (intro that [of id id]) (auto intro: homeomorphismI)
  next
    assume "aff_dim S = 1"
    then have "affine hull S homeomorphic (UNIV :: real set)"
      by (auto simp: homeomorphic_affine_sets)
    then obtain h::"'a==>real" and j where homhj: "homeomorphism (affine hull S) UNIV h j"
      using homeomorphic_def by blast
    then have h: "x. x  affine hull S ==> j(h(x)) = x" and j: "y. j y  affine hull S  h(j y) = y"
      by (auto simp: homeomorphism_def)
    have connh: "connected (h ` S)"
      by (meson Topological_Spaces.connected_continuous_image connected S homeomorphism_cont1 homeomorphism_of_subsets homhj hull_subset top_greatest)
    have hUS: "h ` U  h ` S"
      by (meson homeomorphism_imp_open_map homeomorphism_of_subsets homhj hull_subset opeS opeU open_UNIV openin_open_eq)
    have opn: "openin (top_of_set (affine hull S)) U ==> open (h ` U)" for U
      using homeomorphism_imp_open_map [OF homhj] by simp
    have "open (h ` U)" "open (h ` S)"
      by (auto intro: opeS opeU openin_trans opn)
    then obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g"
                 and f: "x. x  h ` K ==> f x  h ` U"
                 and sub: "{x. ¬ (f x = x  g x = x)}  h ` S"
                 and bou: "bounded {x. ¬ (f x = x  g x = x)}"
      apply (rule homeomorphism_grouping_points_exists [of "h ` U" "h ` S" "h ` K" "h ` T"])
      using assms by (auto simp: connh hUS)
    have jf: "x. x  affine hull S ==> j (f (h x)) = x  f (h x) = h x"
      by (metis h j)
    have jg: "x. x  affine hull S ==> j (g (h x)) = x  g (h x) = h x"
      by (metis h j)
    have cont_hj: "continuous_on T h" "continuous_on Y j" for Y
    proof (rule continuous_on_subset [OF _ T affine hull S])
      show "continuous_on (affine hull S) h"
        using homeomorphism_def homhj by blast
    qed (meson continuous_on_subset homeomorphism_def homhj top_greatest)
    define f' where "f'  λx. if x  affine hull S then (j  f  h) x else x"
    define g' where "g'  λx. if x  affine hull S then (j  g  h) x else x"
    show ?thesis
    proof
      show "homeomorphism T T f' g'"
      proof
        have "continuous_on T (j  f  h)"
          using hom homeomorphism_def by (intro continuous_on_compose cont_hj) blast
        then show "continuous_on T f'"
          apply (rule continuous_on_eq)
          using T affine hull S f'_def by auto
        have "continuous_on T (j  g  h)"
          using hom homeomorphism_def by (intro continuous_on_compose cont_hj) blast
        then show "continuous_on T g'"
          apply (rule continuous_on_eq)
          using T affine hull S g'_def by auto
        show "f' ` T  T"
        proof (clarsimp simp: f'_def)
          fix x assume " T"
          then have "f (h x)  h ` T"
            by (metis (no_types) hom homeomorphism_def image_subset_iff subset_refl)
          then show "j (f (h x))  T"
            using T affine hull S h by auto
        qed
        show "g' ` T  T"
        proof (clarsimp simp: g'_def)
          fix x assume " T"
          then have "g (h x)  h ` T"
            by (metis (no_types) hom homeomorphism_def image_subset_iff subset_refl)
          then show "j (g (h x))  T"
            using T affine hull S h by auto
        qed
        show "x. x  T ==> g' (f' x) = x"
          using h j hom homeomorphism_apply1 by (fastforce simp: f'_def g'_def)
        show "y. y  T ==> f' (g' y) = y"
          using h j hom homeomorphism_apply2 by (fastforce simp: f'_def g'_def)
      qed
    next
      have 🍋: "x y. [ affine hull S; h x = h y; y  S] ==> x  S"
        by (metis h hull_inc)
      show "{x. ¬ (f' x = x  g' x = x)}  S"
        using sub by (simp add: f'_def g'_def jf jg) (force elim: 🍋)
    next
      have "compact (j ` closure {x. ¬ (f x = x  g x = x)})"
        using bou by (auto simp: compact_continuous_image cont_hj)
      then have "bounded (j ` {x. ¬ (f x = x  g x = x)})"
        by (rule bounded_closure_image [OF compact_imp_bounded])
      moreover
      have *: "{x  affine hull S. j (f (h x))  x  j (g (h x))  x} = j ` {x. (¬ (f x = x  g x = x))}"
        using h j by (auto simp: image_iff; metis)
      ultimately have "bounded {x  affine hull S. j (f (h x))  x  j (g (h x))  x}"
        by metis
      then show "bounded {x. ¬ (f' x = x  g' x = x)}"
        by (simp add: f'_def g'_def Collect_mono bounded_subset)
    next
      show "f' x  U" if " K" for x
      proof -
        have " S"
          using opeU openin_imp_subset by blast
        then have "j (f (h x))  U"
          using f h hull_subset that by fastforce
        then show "f' x  U"
          using K S S f'_def that by auto
      qed
    qed
  qed
qed


subsectionNullhomotopic mappings

text A mapping out of a sphere is nullhomotopic iff it extends to the ball.
 This even works out in the degenerate cases when the radius is 0
we also don't need to explicitly assume continuity since it's already implicit
in both sides of the equivalence.

lemma nullhomotopic_from_lemma:
  assumes contg: "continuous_on (cball a r - {a}) g"
      and fa: "e. 0 < e
               ==> d. 0 < d  (x. x  a  norm(x - a) < d  norm(g x - f a) < e)"
      and r: "x. x  cball a r  x  a ==> f x = g x"
    shows "continuous_on (cball a r) f"
proof (clarsimp simp: continuous_on_eq_continuous_within Ball_def)
  fix x
  assume x: "dist a x  r"
  show "continuous (at x within cball a r) f"
  proof (cases "x=a")
    case True
    then show ?thesis
      by (metis continuous_within_eps_delta fa dist_norm dist_self r)
  next
    case False
    show ?thesis
    proof (rule continuous_transform_within [where f=g and δ = "norm(x-a)"])
      have "d>0. x'cball a r. dist x' x < d  dist (g x') (g x) < e"
        if "e>0" for e
      proof -
        obtain d where "d > 0"
           and d: "y. [dist y a  r; y  a; dist y x < d] ==> dist (g y) (g x) < e"
          using contg False x e>0
          unfolding continuous_on_iff by (fastforce simp: dist_commute intro: that)
        show ?thesis
          using d > 0 x a
          by (rule_tac x="min d (norm(x - a))" in exI)
             (auto simp: dist_commute dist_norm [symmetric] intro!: d)
      qed
      then show "continuous (at x within cball a r) g"
        using contg False by (auto simp: continuous_within_eps_delta)
      show "0 < norm (x - a)"
        using False by force
      show " cball a r"
        by (simp add: x)
      show "x'. [x'  cball a r; dist x' x < norm (x - a)]
        ==> g x' = f x'"
        by (metis dist_commute dist_norm less_le r)
    qed
  qed
qed

proposition nullhomotopic_from_sphere_extension:
  fixes f :: "'M::euclidean_space ==> 'a::real_normed_vector"
  shows "(c. homotopic_with_canon (λx. True) (sphere a r) S f (λx. c)) 
          (g. continuous_on (cball a r) g  g ` (cball a r)  S 
               ( sphere a r. g x = f x))"
         (is "?lhs = ?rhs")
proof (cases r "0::real" rule: linorder_cases)
  case less
  then show ?thesis
    by (simp add: homotopic_on_emptyI)
next
  case equal
  show ?thesis
  proof
    assume L: ?lhs
    with equal have [simp]: "f a  S"
      using homotopic_with_imp_subset1 by fastforce
    obtain h:: "real × 'M ==> 'a"
      where h: "continuous_on ({0..1} × {a}) h" "h ` ({0..1} × {a})  S" "h (0, a) = f a"
      using L equal by (auto simp: homotopic_with)
    then have "continuous_on (cball a r) (λx. h (0, a))" "(λx. h (0, a)) ` cball a r  S"
      by (auto simp: equal)
    then show ?rhs
      using h(3) local.equal by force
  next
    assume ?rhs
    then show ?lhs
      using equal continuous_on_const by (force simp: homotopic_with)
  qed
next
  case greater
  let ?P = "continuous_on {x. norm(x - a) = r} f  f ` {x. norm(x - a) = r}  S"
  have ?P if ?lhs using that
  proof
    fix c
    assume c: "homotopic_with_canon (λx. True) (sphere a r) S f (λx. c)"
    then have contf: "continuous_on (sphere a r) f"
      by (metis homotopic_with_imp_continuous)
    moreover have fim: " sphere a r  S"
      using homotopic_with_imp_subset1 that by blast
    show ?P
      using contf fim by (auto simp: sphere_def dist_norm norm_minus_commute)
  qed
  moreover have ?P if ?rhs using that
  proof
    fix g
    assume g: "continuous_on (cball a r) g  g ` cball a r  S  (xasphere a r. g xa = f xa)"
    then have "f ` {x. norm (x - a) = r}  S"
      using sphere_cball [of a r] unfolding image_subset_iff sphere_def
      by (metis dist_commute dist_norm mem_Collect_eq subset_eq)
    with g show ?P
      by (auto simp: dist_norm norm_minus_commute elim!: continuous_on_eq [OF continuous_on_subset])
  qed
  moreover have ?thesis if ?P
  proof
    assume ?lhs
    then obtain c where "homotopic_with_canon (λx. True) (sphere a r) S (λx. c) f"
      using homotopic_with_sym by blast
    then obtain h where conth: "continuous_on ({0..1::real} × sphere a r) h"
                    and him: "h ` ({0..1} × sphere a r)  S"
                    and h: "x. h(0, x) = c" "x. h(1, x) = f x"
      by (auto simp: homotopic_with_def)
    obtain b1::'M where "b1  Basis"
      using SOME_Basis by auto
    have " h ` ({0..1} × sphere a r)"
    proof
      show "c = h (0, a + r *🪙R b1)"
        by (simp add: h)
      show "(0, a + r *🪙R b1)  {0..1::real} × sphere a r"
        using greater b1 Basis by (auto simp: dist_norm)
    qed
    then have " S"
      using him by blast
    have uconth: "uniformly_continuous_on ({0..1::real} × (sphere a r)) h"
      by (force intro: compact_Times conth compact_uniformly_continuous)
    let ?g = "λx. h (norm (x - a)/r,
                     a + (if x = a then r *🪙R b1 else (r / norm(x - a)) *🪙R (x - a)))"
    let ?g' = "λx. h (norm (x - a)/r, a + (r / norm(x - a)) *🪙R (x - a))"
    show ?rhs
    proof (intro exI conjI)
      have "continuous_on (cball a r - {a}) ?g'"
        using greater
        by (force simp: dist_norm norm_minus_commute intro: continuous_on_compose2 [OF conth] continuous_intros)
      then show "continuous_on (cball a r) ?g"
      proof (rule nullhomotopic_from_lemma)
        show "d>0. x. x  a  norm (x - a) < d  norm (?g' x - ?g a) < e" if "0 < e" for e
        proof -
          obtain d where "0 < d"
             and d: "x x'. [ {0..1} × sphere a r; x'  {0..1} × sphere a r; norm ( x' - x) < d]
                        ==> norm (h x' - h x) < e"
            using uniformly_continuous_onE [OF uconth 0 < e] by (auto simp: dist_norm)
          have *: "norm (h (norm (x - a) / r,
                         a + (r / norm (x - a)) *🪙R (x - a)) - h (0, a + r *🪙R b1)) < e" (is "norm (?ha - ?hb) < e")
                   if " a" "norm (x - a) < r" "norm (x - a) < d * r" for x
          proof -
            have "norm (?ha - ?hb) = norm (?ha - h (0, a + (r / norm (x - a)) *🪙R (x - a)))"
              by (simp add: h)
            also have " < e"
              using greater 0 < d b1 Basis that
              by (intro d) (simp_all add: dist_norm, simp add: field_simps)
            finally show ?thesis .
          qed
          show ?thesis
            using greater 0 < d
            by (rule_tac x = "min r (d * r)" in exI) (auto simp: *)
        qed
        show "x. x  cball a r  x  a ==> ?g x = ?g' x"
          by auto
      qed
    next
      show "?g ` cball a r  S"
        using greater him c S
        by (force simp: h dist_norm norm_minus_commute)
    next
      show "xsphere a r. ?g x = f x"
        using greater by (auto simp: h dist_norm norm_minus_commute)
    qed
  next
    assume ?rhs
    then obtain g where contg: "continuous_on (cball a r) g"
                    and gim: "g ` cball a r  S"
                    and gf: " sphere a r. g x = f x"
      by auto
    let ?h = "λy. g (a + (fst y) *🪙R (snd y - a))"
    have "continuous_on ({0..1} × sphere a r) ?h"
    proof (rule continuous_on_compose2 [OF contg])
      show "continuous_on ({0..1} × sphere a r) (λx. a + fst x *🪙R (snd x - a))"
        by (intro continuous_intros)
      qed (auto simp: dist_norm norm_minus_commute mult_left_le_one_le)
    moreover
    have "?h  ({0..1} × sphere a r)  S"
      by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gim [THEN subsetD])
    moreover
    have "xsphere a r. ?h (0, x) = g a" "xsphere a r. ?h (1, x) = f x"
      by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gf)
    ultimately have "homotopic_with_canon (λx. True) (sphere a r) S (λx. g a) f"
      by (auto simp: homotopic_with)
    then show ?lhs
      using homotopic_with_symD by blast
  qed
  ultimately
  show ?thesis by meson
qed

end

Messung V0.5 in Prozent
C=94 H=85 G=89

¤ Dauer der Verarbeitung: 0.381 Sekunden  (vorverarbeitet am  2026-05-03) ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.