Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Impressum Starlike.thy

  Sprache: Isabelle
 

(* Title:      HOL/Analysis/Starlike.thy
  Author: L C Paulson, University of Cambridge
  Author: Robert Himmelmann, TU Muenchen
  Author: Bogdan Grechuk, University of Edinburgh
  Author: Armin Heller, TU Muenchen
  Author: Johannes Hoelzl, TU Muenchen
*)
chapter Unsorted

theory Starlike
  imports
    Convex_Euclidean_Space
    Line_Segment
begin

lemma affine_hull_closed_segment [simp]:
     "affine hull (closed_segment a b) = affine hull {a,b}"
  by (simp add: segment_convex_hull)

lemma affine_hull_open_segment [simp]:
    fixes a :: "'a::euclidean_space"
    shows "affine hull (open_segment a b) = (if a = b then {} else affine hull {a,b})"
by (metis affine_hull_convex_hull affine_hull_empty closure_open_segment closure_same_affine_hull segment_convex_hull)

lemma rel_interior_closure_convex_segment:
  fixes S :: "_::euclidean_space set"
  assumes "convex S" "a rel_interior S" "b closure S"
    shows "open_segment a b rel_interior S"
proof
  fix x
  have [simp]: "(1 - u) *🪙R a + u *🪙R b = b - (1 - u) *🪙R (b - a)" for u
    by (simp add: algebra_simps)
  assume "x open_segment a b"
  then show "x rel_interior S"
    unfolding closed_segment_def open_segment_def  using assms
    by (auto intro: rel_interior_closure_convex_shrink)
qed

lemma convex_hull_insert_segments:
   "convex hull (insert a S) =
    (if S = {} then {a} else x convex hull S. closed_segment a x)"
  by (force simp add: convex_hull_insert_alt in_segment)

lemma Int_convex_hull_insert_rel_exterior:
  fixes z :: "'a::euclidean_space"
  assumes "convex C" "T C" and z: "z rel_interior C" and dis: "disjnt S (rel_interior C)"
  shows "S (convex hull (insert z T)) = S (convex hull T)" (is "?lhs = ?rhs")
proof
  have *: "T = {} ==> z S"
    using dis z by (auto simp add: disjnt_def)
  { fix x y
    assume "x S" and y: "y convex hull T" and "x closed_segment z y"
    have "y closure C"
      by (metis y convex C T C closure_subset contra_subsetD convex_hull_eq hull_mono)
    moreover have "x rel_interior C"
      by (meson x S dis disjnt_iff)
    moreover have "x open_segment z y {z, y}"
      using x closed_segment z y closed_segment_eq_open by blast
    ultimately have "x convex hull T"
      using rel_interior_closure_convex_segment [OF convex C z]
      using y z by blast
  }
  with * show "?lhs ?rhs"
    by (auto simp add: convex_hull_insert_segments)
  show "?rhs ?lhs"
    by (meson hull_mono inf_mono subset_insertI subset_refl)
qed

subsection🍋tag unimportant Shrinking towards the interior of a convex set

lemma mem_interior_convex_shrink:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S"
    and "c interior S"
    and "x S"
    and "0 < e"
    and "e 1"
  shows "x - e *🪙R (x - c) interior S"
proof -
  obtain d where "d > 0" and d: "ball c d S"
    using assms(2) unfolding mem_interior by auto
  show ?thesis
    unfolding mem_interior
  proof (intro exI subsetI conjI)
    fix y
    assume "y ball (x - e *🪙R (x - c)) (e*d)"
    then have as: "dist (x - e *🪙R (x - c)) y < e * d"
      by simp
    have *: "y = (1 - (1 - e)) *🪙R ((1 / e) *🪙R y - ((1 - e) / e) *🪙R x) + (1 - e) *🪙R x"
      using e > 0 by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
    have "c - ((1 / e) *🪙R y - ((1 - e) / e) *🪙R x) = (1 / e) *🪙R (e *🪙R c - y + (1 - e) *🪙R x)"
      using e > 0
      by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
    then have "dist c ((1 / e) *🪙R y - ((1 - e) / e) *🪙R x) = 1/e * norm (e *🪙R c - y + (1 - e) *🪙R x)"
      by (simp add: dist_norm)
    also have " = 1/e * norm (x - e *🪙R (x - c) - y)"
      by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
    also have " < d"
      using as[unfolded dist_norm] and e > 0
      by (auto simp add:pos_divide_less_eq[OF e > 0] mult.commute)
    finally have "(1 - (1 - e)) *🪙R ((1 / e) *🪙R y - ((1 - e) / e) *🪙R x) + (1 - e) *🪙R x S"
      using assms(3-5) d
      by (intro convexD_alt [OF convex S]) (auto intro: convexD_alt [OF convex S])
    with e > 0 show "y S"
      by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
  qed (use e>0 d>0 in auto)
qed

lemma mem_interior_closure_convex_shrink:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S"
    and "c interior S"
    and "x closure S"
    and "0 < e"
    and "e 1"
  shows "x - e *🪙R (x - c) interior S"
proof -
  obtain d where "d > 0" and d: "ball c d S"
    using assms(2) unfolding mem_interior by auto
  have "yS. norm (y - x) * (1 - e) < e * d"
  proof (cases "x S")
    case True
    then show ?thesis
      using e > 0 d > 0 by force
  next
    case False
    then have x: "x islimpt S"
      using assms(3)[unfolded closure_def] by auto
    show ?thesis
    proof (cases "e = 1")
      case True
      obtain y where "y S" "y x" "dist y x < 1"
        using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto
      then show ?thesis
        using True 0 🚫 by auto
    next
      case False
      then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
        using e 1 e > 0 d > 0 by auto
      then obtain y where "y S" "y x" "dist y x < e * d / (1 - e)"
        using islimpt_approachable x by blast
      then have "norm (y - x) * (1 - e) < e * d"
        by (metis "*" dist_norm mult_imp_div_pos_le not_less)
      then show ?thesis
        using y S by blast
    qed
  qed
  then obtain y where "y S" and y: "norm (y - x) * (1 - e) < e * d"
    by auto
  define z where "z = c + ((1 - e) / e) *🪙R (x - y)"
  have *: "x - e *🪙R (x - c) = y - e *🪙R (y - z)"
    unfolding z_def using e > 0
    by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
  have "(1 - e) * norm (x - y) / e < d"
    using y 0 🚫 by (simp add: field_simps norm_minus_commute)
  then have "z interior (ball c d)"
    using 0 🚫 e 1 by (simp add: interior_open[OF open_ball] z_def dist_norm)
  then have "z interior S"
    using d interiorI interior_ball by blast
  then show ?thesis
    unfolding * using mem_interior_convex_shrink y S assms by blast
qed

lemma in_interior_closure_convex_segment:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" and a: "a interior S" and b: "b closure S"
  shows "open_segment a b interior S"
proof -
  { fix u::real
    assume u: "0 < u" "u < 1"
    have "(1 - u) *🪙R a + u *🪙R b = b - (1 - u) *🪙R (b - a)"
      by (simp add: algebra_simps)
    also have "... interior S" using mem_interior_closure_convex_shrink [OF assms] u
      by simp
    finally have "(1 - u) *🪙R a + u *🪙R b interior S" .
  }
  then show ?thesis
    by (clarsimp simp: in_segment)
qed

lemma convex_closure_interior:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" and int: "interior S {}"
  shows "closure(interior S) = closure S"
proof -
  obtain a where a: "a interior S"
    using int by auto
  have "closure S closure(interior S)"
  proof
    fix x
    assume x: "x closure S"
    show "x closure (interior S)"
    proof (cases "x=a")
      case True
      then show ?thesis
        using a interior S closure_subset by blast
    next
      case False
      { fix e::real
        assume xnotS: "x interior S" and "0 < e"
        have "x'interior S. x' x dist x' x < e"
        proof (intro bexI conjI)
          show "x - min (e/2 / norm (x - a)) 1 *🪙R (x - a) x"
            using False 0 🚫 by (auto simp: algebra_simps min_def)
          show "dist (x - min (e/2 / norm (x - a)) 1 *🪙R (x - a)) x < e"
            using 0 🚫 by (auto simp: dist_norm min_def)
          show "x - min (e/2 / norm (x - a)) 1 *🪙R (x - a) interior S"
            using 0 🚫 False
            by (auto simp add: min_def a intro: mem_interior_closure_convex_shrink [OF convex S a x])
        qed
      }
      then show ?thesis
        by (auto simp add: closure_def islimpt_approachable)
    qed
  qed
  then show ?thesis
    by (simp add: closure_mono interior_subset subset_antisym)
qed

lemma openin_subset_relative_interior:
  fixes S :: "'a::euclidean_space set"
  shows "openin (top_of_set (affine hull T)) S ==> (S rel_interior T) = (S T)"
  by (meson order.trans rel_interior_maximal rel_interior_subset)

lemma conic_hull_eq_span_affine_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "0 rel_interior S"
  shows "conic hull S = span S conic hull S = affine hull S"
proof -
  obtain ε where "ε>0" and ε: "cball 0 ε affine hull S S"
    using assms mem_rel_interior_cball by blast
  have *: "affine hull S = span S"
    by (meson affine_hull_span_0 assms hull_inc mem_rel_interior_cball)
  moreover
  have "conic hull S span S"
    by (simp add: hull_minimal span_superset)
  moreover
  { fix x
    assume "x affine hull S"
    have "x conic hull S"
    proof (cases "x=0")
      case True
      then show ?thesis
        using x affine hull S by auto
    next
      case False
      then have "(ε / norm x) *🪙R x cball 0 ε affine hull S"
        using 0 🚫ε x affine hull S * span_mul by fastforce
      then have "(ε / norm x) *🪙R x S"
        by (meson ε subsetD)
      then have "c xa. x = c *🪙R xa 0 c xa S"
        by (smt (verit, del_insts) 0 🚫ε divide_nonneg_nonneg eq_vector_fraction_iff norm_eq_zero norm_ge_zero)
      then show ?thesis
        by (simp add: conic_hull_explicit)
    qed
  }
  then have "affine hull S conic hull S"
    by auto
  ultimately show ?thesis
    by blast
qed

lemma conic_hull_eq_span:
  fixes S :: "'a::euclidean_space set"
  assumes "0 rel_interior S"
  shows "conic hull S = span S"
  by (simp add: assms conic_hull_eq_span_affine_hull)

lemma conic_hull_eq_affine_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "0 rel_interior S"
  shows "conic hull S = affine hull S"
  using assms conic_hull_eq_span_affine_hull by blast

lemma conic_hull_eq_span_eq:
  fixes S :: "'a::euclidean_space set"
  shows "0 rel_interior(conic hull S) conic hull S = span S" (is "?lhs = ?rhs")
proof
  show "?lhs ==> ?rhs"
    by (metis conic_hull_eq_span conic_span hull_hull hull_minimal hull_subset span_eq)
  show "?rhs ==> ?lhs"
  by (metis rel_interior_affine subspace_affine subspace_span)
qed

lemma aff_dim_psubset:
   "(affine hull S) (affine hull T) ==> aff_dim S < aff_dim T"
  by (metis aff_dim_affine_hull aff_dim_empty aff_dim_subset affine_affine_hull affine_dim_equal order_less_le)

lemma aff_dim_eq_full_gen:
   "S T ==> (aff_dim S = aff_dim T affine hull S = affine hull T)"
  by (smt (verit, del_insts) aff_dim_affine_hull2 aff_dim_psubset hull_mono psubsetI)

lemma aff_dim_eq_full:
  fixes S :: "'n::euclidean_space set"
  shows "aff_dim S = (DIM('n)) affine hull S = UNIV"
  by (metis aff_dim_UNIV aff_dim_affine_hull affine_hull_UNIV)

lemma closure_convex_Int_superset:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "interior S {}" "interior S closure T"
  shows "closure(S T) = closure S"
proof -
  have "closure S closure(interior S)"
    by (simp add: convex_closure_interior assms)
  also have "... closure (S T)"
    using interior_subset [of S] assms
    by (metis (no_types, lifting) Int_assoc Int_lower2 closure_mono closure_open_Int_superset inf.orderE open_interior)
  finally show ?thesis
    by (simp add: closure_mono dual_order.antisym)
qed


subsection🍋tag unimportant Some obvious but surprisingly hard simplex lemmas

lemma simplex:
  assumes "finite S"
    and "0 S"
  shows "convex hull (insert 0 S) = {y. u. (xS. 0 u x) sum u S 1 sum (λx. u x *🪙R x) S = y}"
proof -
  { fix x and u :: "'a ==> real"
    assume "xS. 0 u x" "sum u S 1"
    then have "v. 0 v 0 (xS. 0 v x) v 0 + sum v S = 1 (xS. v x *🪙R x) = (xS. u x *🪙R x)"
      by (rule_tac x="λx. if x = 0 then 1 - sum u S else u x" in exI) (auto simp: sum_delta_notmem assms if_smult)
  }
  then show ?thesis by (auto simp: convex_hull_finite set_eq_iff assms)
qed

lemma substd_simplex:
  assumes d: "d Basis"
  shows "convex hull (insert 0 d) =
    {x. (iBasis. 0 xi) (id. xi) 1 (iBasis. i d xi = 0)}"
  (is "convex hull (insert 0 ?p) = ?s")
proof -
  let ?D = d
  have "0 ?p"
    using assms by (auto simp: image_def)
  from d have "finite d"
    by (blast intro: finite_subset finite_Basis)
  show ?thesis
    unfolding simplex[OF finite d 0 ?p]
  proof (intro set_eqI; safe)
    fix u :: "'a ==> real"
    assume as: "x?D. 0 u x" "sum u ?D 1" 
    let ?x = "(x?D. u x *🪙R x)"
    have ind: "iBasis. i d u i = ?x i"
      and notind: "(iBasis. i d ?x i = 0)"
      using substdbasis_expansion_unique[OF assms] by blast+
    then have **: "sum u ?D = sum (() ?x) ?D"
      using assms by (meson subset_iff sum.cong)
    show "0 ?x i" if "i Basis" for i
      using as(1) ind notind that by fastforce
    show "sum (() ?x) ?D 1"
      using "**" as(2) by linarith
    show "?x i = 0" if "i Basis" "i d" for i
      using notind that by blast
  next
    fix x 
    assume "iBasis. 0 x i" "sum (() x) ?D 1" "(iBasis. i d x i = 0)"
    with d show "u. (x?D. 0 u x) sum u ?D 1 (x?D. u x *🪙R x) = x"
      unfolding substdbasis_expansion_unique[OF assms] 
      by (rule_tac x="inner x" in exI) auto
  qed
qed

lemma std_simplex:
  "convex hull (insert 0 Basis) =
    {x::'a::euclidean_space. (iBasis. 0 xi) sum (λi. xi) Basis 1}"
  using substd_simplex[of Basis] by auto

lemma interior_std_simplex:
  "interior (convex hull (insert 0 Basis)) =
    {x::'a::euclidean_space. (iBasis. 0 < xi) sum (λi. xi) Basis < 1}"
  unfolding set_eq_iff mem_interior std_simplex
proof (intro allI iffI CollectI; clarify)
  fix x :: 'a
  fix e
  assume "e > 0" and as: "ball x e {x. (iBasis. 0 x i) sum (() x) Basis 1}"
  show "(iBasis. 0 < x i) sum (() x) Basis < 1"
  proof (intro strip conjI)
    fix i :: 'a
    assume i: "i Basis"
    then show "0 < x i"
      using as[THEN subsetD[where c="x - (e/2) *🪙R i"]] and e > 0
      by (force simp add: inner_simps)
  next
    obtain i::'a where i: "i Basis"
      using nonempty_Basis by blast
    have **: "dist x (x + (e/2) *🪙R i) < e" using e > 0
      unfolding dist_norm
      by (auto intro!: mult_strict_left_mono simp: i)
    have "i. i Basis ==> (x + (e/2) *🪙R i) i = xi + (if i = i then e/2 else 0)"
      by (auto simp: inner_simps)
    then have *: "sum (() (x + (e/2) *🪙R i)) Basis = sum (λj. xj + (if j = i then e/2 else 0)) Basis"
      using i by (auto simp: inner_Basis inner_left_distrib intro!: sum.cong)
    have "sum (() x) Basis < sum (() (x + (e/2) *🪙R i)) Basis"
      using e > 0 DIM_positive by (auto simp: i sum.distrib *)
    also have " 1"
      using ** as by force
    finally show "sum (() x) Basis < 1" by auto
  qed 
next
  fix x :: 'a
  assume as: "iBasis. 0 < x i" "sum (() x) Basis < 1"
  obtain a :: 'b where "a UNIV" using UNIV_witness ..
  let ?d = "(1 - sum (() x) Basis) / real (DIM('a))"
  show "e>0. ball x e {x. (iBasis. 0 x i) sum (() x) Basis 1}"
  proof (intro exI conjI subsetI CollectI)
    fix y
    assume y: "y ball x (min (Min (() x ` Basis)) ?d)"
    have "sum (() y) Basis sum (λi. xi + ?d) Basis"
    proof (rule sum_mono)
      fix i :: 'a
      assume i: "i Basis"
      have "yi - xi norm (y - x)"
        by (metis Basis_le_norm i inner_commute inner_diff_right)
      also have "... < ?d"
        using y by (simp add: dist_norm norm_minus_commute)
      finally have "yi - xi < ?d" .
      then show "y i x i + ?d" by auto
    qed
    also have " 1"
      unfolding sum.distrib sum_constant
      by (auto simp add: Suc_le_eq)
    finally show "sum (() y) Basis 1" .
    show "(iBasis. 0 y i)"
    proof (intro strip)
      fix i :: 'a
      assume i: "i Basis"
      have "norm (x - y) < Min ((() x) ` Basis)"
        using y by (auto simp: dist_norm less_eq_real_def)
      also have "... xi"
        using i by auto
      finally have "norm (x - y) < xi" .
      then show "0 yi"
        using Basis_le_norm[OF i, of "x - y"and as(1)[rule_format, OF i]
        by (auto simp: inner_simps)
    qed
  next
    have "Min ((() x) ` Basis) > 0"
      using as by simp
    moreover have "?d > 0"
      using as by (auto simp: Suc_le_eq)
    ultimately show "0 < min (Min (() x ` Basis)) ((1 - sum (() x) Basis) / real DIM('a))"
      by linarith
  qed 
qed

lemma interior_std_simplex_nonempty:
  obtains a :: "'a::euclidean_space" where
    "a interior(convex hull (insert 0 Basis))"
proof -
  let ?D = "Basis :: 'a set"
  let ?a = "sum (λb::'a. inverse (2 * real DIM('a)) *🪙R b) Basis"
  {
    fix i :: 'a
    assume i: "i Basis"
    have "?a i = inverse (2 * real DIM('a))"
      by (rule trans[of _ "sum (λj. if i = j then inverse (2 * real DIM('a)) else 0) ?D"])
         (simp_all add: sum.If_cases i) }
  note ** = this
  show ?thesis
  proof
    show "?a interior(convex hull (insert 0 Basis))"
      unfolding interior_std_simplex mem_Collect_eq
    proof safe
      fix i :: 'a
      assume i: "i Basis"
      show "0 < ?a i"
        unfolding **[OF i] by (auto simp add: Suc_le_eq)
    next
      have "sum (() ?a) ?D = sum (λi. inverse (2 * real DIM('a))) ?D"
        by simp
      also have " < 1"
        unfolding sum_constant divide_inverse[symmetric]
        by (auto simp add: field_simps)
      finally show "sum (() ?a) ?D < 1" by auto
    qed
  qed
qed

lemma rel_interior_substd_simplex:
  assumes D: "D Basis"
  shows "rel_interior (convex hull (insert 0 D)) =
         {x::'a::euclidean_space. (iD. 0 < xi) (iD. xi) < 1 (iBasis. i D xi = 0)}"
     (is "_ = ?s")
proof -
  have "finite D"
    using D finite_Basis finite_subset by blast
  show ?thesis
  proof (cases "D = {}")
    case True
    then show ?thesis
      using rel_interior_sing using euclidean_eq_iff[of _ 0] by auto
  next
    case False
    have h0: "affine hull (convex hull (insert 0 D)) =
              {x::'a::euclidean_space. (iBasis. i D xi = 0)}"
      using affine_hull_convex_hull affine_hull_substd_basis assms by auto
    have aux: "x::'a. iBasis. (iD. 0 xi) (iBasis. i D xi = 0) 0 xi"
      by auto
    {
      fix x :: "'a::euclidean_space"
      assume x: "x rel_interior (convex hull (insert 0 D))"
      then obtain e where "e > 0" and
        "ball x e {xa. (iBasis. i D xai = 0)} convex hull (insert 0 D)"
        using mem_rel_interior_ball[of x "convex hull (insert 0 D)"] h0 by auto
      then have as: "y. [dist x y < e (iBasis. i D yi = 0)] ==>
                            (iD. 0 y i) sum (() y) D 1"
        using assms by (force simp: substd_simplex)
      have x0: "(iBasis. i D xi = 0)"
        using x rel_interior_subset  substd_simplex[OF assms] by auto
      have "(iD. 0 < x i) sum (() x) D < 1 (iBasis. i D xi = 0)"
      proof (intro conjI ballI)
        fix i :: 'a
        assume "i D"
        then have "jD. 0 (x - (e/2) *🪙R i) j"
          using D e > 0 x0
          by (intro as[THEN conjunct1]) (force simp: dist_norm inner_simps inner_Basis)
        then show "0 < x i"
          using e > 0 i D D  by (force simp: inner_simps inner_Basis)
      next
        obtain a where a: "a D"
          using D {} by auto
        then have **: "dist x (x + (e/2) *🪙R a) < e"
          using e > 0 norm_Basis[of a] D by (auto simp: dist_norm)
        have "i. i Basis ==> (x + (e/2) *🪙R a) i = xi + (if i = a then e/2 else 0)"
          using a D by (auto simp: inner_simps inner_Basis)
        then have *: "sum (() (x + (e/2) *🪙R a)) D = sum (λi. xi + (if a = i then e/2 else 0)) D"
          using D by (intro sum.cong) auto
        have "a Basis"
          using a Dby auto
        then have h1: "(iBasis. i D (x + (e/2) *🪙R a) i = 0)"
          using x0 D aD by (auto simp add: inner_add_left inner_Basis)
        have "sum (() x) D < sum (() (x + (e/2) *🪙R a)) D"
          using e > 0 a D finite D by (auto simp add: * sum.distrib)
        also have " 1"
          using ** h1 as[rule_format, of "x + (e/2) *🪙R a"]
          by auto
        finally show "sum (() x) D < 1" "i. iBasis ==> i D xi = 0"
          using x0 by auto
      qed
    }
    moreover
    {
      fix x :: "'a::euclidean_space"
      assume as: "x ?s"
      have "i. 0 < xi 0 = xi 0 xi"
        by auto
      moreover have "i. i D i D" by auto
      ultimately
      have "i. (iD. 0 < xi) (i. i D xi = 0) 0 xi"
        by metis
      then have h2: "x convex hull (insert 0 D)"
        using as assms by (force simp add: substd_simplex)
      obtain a where a: "a D"
        using D {} by auto
      define d where "d (1 - sum (() x) D) / real (card D)"
      have "e>0. ball x e {x. iBasis. i D x i = 0} convex hull insert 0 D"
        unfolding substd_simplex[OF assms]
      proof (intro exI; safe)
        have "0 < card D" using D {} finite D
          by (simp add: card_gt_0_iff)
        have "Min ((() x) ` D) > 0"
          using as D {} finite D by (simp)
        moreover have "d > 0" 
          using as 0 🚫 D by (auto simp: d_def)
        ultimately show "min (Min ((() x) ` D)) d > 0"
          by auto
        fix y :: 'a
        assume y2: "iBasis. i D yi = 0"
        assume "y ball x (min (Min (() x ` D)) d)"
        then have y: "dist x y < min (Min (() x ` D)) d"
          by auto
        have "sum (() y) D sum (λi. xi + d) D"
        proof (rule sum_mono)
          fix i
          assume "i D"
          with D have i: "i Basis"
            by auto
          have "yi - xi norm (y - x)"
            by (metis i inner_commute inner_diff_right norm_bound_Basis_le order_refl)
          also have "... < d"
            by (metis dist_norm min_less_iff_conj norm_minus_commute y)
          finally have "yi - xi < d" .
          then show "y i x i + d" by auto
        qed
        also have " 1"
          unfolding sum.distrib sum_constant d_def using 0 🚫 D
          by auto
        finally show "sum (() y) D 1" .

        fix i :: 'a
        assume i: "i Basis"
        then show "0 yi"
        proof (cases "iD")
          case True
          have "norm (x - y) < xi"
            using y Min_gr_iff[of "() x ` D" "norm (x - y)"0 🚫 D i D
            by (simp add: dist_norm card_gt_0_iff)
          then show "0 yi"
            using Basis_le_norm[OF i, of "x - y"and as(1)[rule_format]
            by (auto simp: inner_simps)
        qed (use y2 in auto)
      qed
      then have "x rel_interior (convex hull (insert 0 D))"
        using h0 h2 rel_interior_ball by force
    }
    ultimately have
      "x. x rel_interior (convex hull insert 0 D)
        x {x. (iD. 0 < x i) sum (() x) D < 1 (iBasis. i D x i = 0)}"
      by blast
    then show ?thesis by (rule set_eqI)
  qed
qed

lemma rel_interior_substd_simplex_nonempty:
  assumes "D {}"
    and "D Basis"
  obtains a :: "'a::euclidean_space"
    where "a rel_interior (convex hull (insert 0 D))"
proof -
  let ?a = "(bD. b /🪙R (2 * real (card D)))"
  have "finite D"
    using assms finite_Basis infinite_super by blast
  then have d1: "0 < real (card D)"
    using D {} by auto
  {
    fix i
    assume "i D"
    have "?a i = (jD. if i = j then inverse (2 * real (card D)) else 0)"
      unfolding inner_sum_left
      using i D by (auto simp: inner_Basis subsetD[OF assms(2)] intro: sum.cong)
    also have "... = inverse (2 * real (card D))"
      using i D finite D by auto
    finally have "?a i = inverse (2 * real (card D))" .
  }
  note ** = this
  show ?thesis
  proof
    show "?a rel_interior (convex hull (insert 0 D))"
      unfolding rel_interior_substd_simplex[OF assms(2)] 
    proof safe
      fix i
      assume "i D"
      have "0 < inverse (2 * real (card D))"
        using d1 by auto
      also have " = ?a i" using **[of i] i D
        by auto
      finally show "0 < ?a i" by auto
    next
      have "sum (() ?a) D = sum (λi. inverse (2 * real (card D))) D"
        by (rule sum.cong [OF refl **]) 
      also have " < 1"
        unfolding sum_constant divide_real_def[symmetric]
        by (auto simp add: field_simps)
      finally show "sum (() ?a) D < 1" by auto
    next
      fix i
      assume "i Basis" and "i D"
      have "?a span D"
      proof (rule span_sum[of D "(λb. b /🪙R (2 * real (card D)))" D])
        {
          fix x :: "'a::euclidean_space"
          assume "x D"
          then have "x span D"
            using span_base[of _ "D"by auto
          then have "x /🪙R (2 * real (card D)) span D"
            using span_mul[of x "D" "(inverse (real (card D)) / 2)"by auto
        }
        then show "x. xD ==> x /🪙R (2 * real (card D)) span D"
          by auto
      qed
      then show "?a i = 0 "
        using i D unfolding span_substd_basis[OF assms(2)] using i Basis by auto
    qed
  qed
qed

subsection🍋tag unimportant Relative interior of convex set

lemma rel_interior_convex_nonempty_aux:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
    and "0 S"
  shows "rel_interior S {}"
proof (cases "S = {0}")
  case True
  then show ?thesis using rel_interior_sing by auto
next
  case False
  obtain B where B: "independent B B S S span B card B = dim S"
    using basis_exists[of S] by metis
  then have "B {}"
    using B assms S {0} span_empty by auto
  have "insert 0 B span B"
    using subspace_span[of B] subspace_0[of "span B"]
      span_superset by auto
  then have "span (insert 0 B) span B"
    using span_span[of B] span_mono[of "insert 0 B" "span B"by blast
  then have "convex hull insert 0 B span B"
    using convex_hull_subset_span[of "insert 0 B"by auto
  then have "span (convex hull insert 0 B) span B"
    using span_span[of B]
      span_mono[of "convex hull insert 0 B" "span B"by blast
  then have *: "span (convex hull insert 0 B) = span B"
    using span_mono[of B "convex hull insert 0 B"] hull_subset[of "insert 0 B"by auto
  then have "span (convex hull insert 0 B) = span S"
    using B span_mono[of B S] span_mono[of S "span B"]
      span_span[of B] by auto
  moreover have "0 affine hull (convex hull insert 0 B)"
    using hull_subset[of "convex hull insert 0 B"] hull_subset[of "insert 0 B"by auto
  ultimately have **: "affine hull (convex hull insert 0 B) = affine hull S"
    using affine_hull_span_0[of "convex hull insert 0 B"] affine_hull_span_0[of "S"]
      assms hull_subset[of S]
    by auto
  obtain d and f :: "'n ==> 'n" where
    fd: "card d = card B" "linear f" "f ` B = d"
      "f ` span B = {x. iBasis. i d x i = (0::real)} inj_on f (span B)"
    and d: "d Basis"
    using basis_to_substdbasis_subspace_isomorphism[of B,OF _ ] B by auto
  then have "bounded_linear f"
    using linear_conv_bounded_linear by auto
  have "d {}"
    using fd B B {} by auto
  have "insert 0 d = f ` (insert 0 B)"
    using fd linear_0 by auto
  then have "(convex hull (insert 0 d)) = f ` (convex hull (insert 0 B))"
    using convex_hull_linear_image[of f "(insert 0 d)"]
      convex_hull_linear_image[of f "(insert 0 B)"linear f
    by auto
  moreover have "rel_interior (f ` (convex hull insert 0 B)) = f ` rel_interior (convex hull insert 0 B)"
  proof (rule rel_interior_injective_on_span_linear_image[OF bounded_linear f])
    show "inj_on f (span (convex hull insert 0 B))"
      using fd * by auto
  qed
  ultimately have "rel_interior (convex hull insert 0 B) {}"
    using rel_interior_substd_simplex_nonempty[OF d {} d] by fastforce
  moreover have "convex hull (insert 0 B) S"
    using B assms hull_mono[of "insert 0 B" "S" "convex"] convex_hull_eq by auto
  ultimately show ?thesis
    using subset_rel_interior[of "convex hull insert 0 B" S] ** by auto
qed

lemma rel_interior_eq_empty:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "rel_interior S = {} S = {}"
proof -
  {
    assume "S {}"
    then obtain a where "a S" by auto
    then have "0 (+) (-a) ` S"
      using assms exI[of "(λx. x S - a + x = 0)" a] by auto
    then have "rel_interior ((+) (-a) ` S) {}"
      using rel_interior_convex_nonempty_aux[of "(+) (-a) ` S"]
        convex_translation[of S "-a"] assms
      by auto
    then have "rel_interior S {}"
      using rel_interior_translation [of "- a"by simp
  }
  then show ?thesis by auto
qed

lemma interior_simplex_nonempty:
  fixes S :: "'N :: euclidean_space set"
  assumes "independent S" "finite S" "card S = DIM('N)"
  obtains a where "a interior (convex hull (insert 0 S))"
proof -
  have "affine hull (insert 0 S) = UNIV"
    by (simp add: hull_inc affine_hull_span_0 dim_eq_full[symmetric]
         assms(1) assms(3) dim_eq_card_independent)
  moreover have "rel_interior (convex hull insert 0 S) {}"
    using rel_interior_eq_empty [of "convex hull (insert 0 S)"by auto
  ultimately have "interior (convex hull insert 0 S) {}"
    by (simp add: rel_interior_interior)
  with that show ?thesis
    by auto
qed

lemma convex_rel_interior:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "convex (rel_interior S)"
proof -
  {
    fix x y and u :: real
    assume assm: "x rel_interior S" "y rel_interior S" "0 u" "u 1"
    then have "x S"
      using rel_interior_subset by auto
    have "x - u *🪙R (x-y) rel_interior S"
    proof (cases "0 = u")
      case False
      then have "0 < u" using assm by auto
      then show ?thesis
        using assm rel_interior_convex_shrink[of S y x u] assms x S by auto
    next
      case True
      then show ?thesis using assm by auto
    qed
    then have "(1 - u) *🪙R x + u *🪙R y rel_interior S"
      by (simp add: algebra_simps)
  }
  then show ?thesis
    unfolding convex_alt by auto
qed

lemma convex_closure_rel_interior:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "closure (rel_interior S) = closure S"
proof -
  have h1: "closure (rel_interior S) closure S"
    using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
  show ?thesis
  proof (cases "S = {}")
    case False
    then obtain a where a: "a rel_interior S"
      using rel_interior_eq_empty assms by auto
    { fix x
      assume x: "x closure S"
      {
        assume "x = a"
        then have "x closure (rel_interior S)"
          using a unfolding closure_def by auto
      }
      moreover
      {
        assume "x a"
         {
           fix e :: real
           assume "e > 0"
           define e1 where "e1 = min 1 (e/norm (x - a))"
           then have e1: "e1 > 0" "e1 1" "e1 * norm (x - a) e"
             using x a e > 0 le_divide_eq[of e1 e "norm (x - a)"]
             by simp_all
           then have *: "x - e1 *🪙R (x - a) rel_interior S"
             using rel_interior_closure_convex_shrink[of S a x e1] assms x a e1_def
             by auto
           have "y. y rel_interior S y x dist y x e"
             using "*" x a e1 by force
        }
        then have "x islimpt rel_interior S"
          unfolding islimpt_approachable_le by auto
        then have "x closure(rel_interior S)"
          unfolding closure_def by auto
      }
      ultimately have "x closure(rel_interior S)" by auto
    }
    then show ?thesis using h1 by auto
  qed auto
qed

lemma empty_interior_subset_hyperplane_aux:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "0 S" and empty_int: "interior S = {}"
  shows "a b. a0 S {x. a x = b}"
proof -
  have False if "a. a = 0 (b. T S. a T b)"
  proof -
    have rel_int: "rel_interior S {}"
      using assms rel_interior_eq_empty by auto
    moreover 
    have "dim S dim (UNIV::'a set)"
      by (metis aff_dim_zero affine_hull_UNIV 0 S dim_UNIV empty_int hull_inc rel_int rel_interior_interior)
    then obtain a where "a 0" and a: "span S {x. a x = 0}"
      using lowdim_subset_hyperplane
      by (metis dim_UNIV dim_subset_UNIV order_less_le)
    have "span UNIV = span S"
      by (metis span_base span_not_UNIV_orthogonal that)
    then have "UNIV affine hull S"
      by (simp add: 0 S hull_inc affine_hull_span_0)
    ultimately show False
      using rel_interior S {} empty_int rel_interior_interior by blast
  qed
  then show ?thesis
    by blast
qed

lemma empty_interior_subset_hyperplane:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" and int: "interior S = {}"
  obtains a b where "a 0" "S {x. a x = b}"
proof (cases "S = {}")
  case True
  then show ?thesis
    using that by blast
next
  case False
  then obtain u where "u S"
    by blast
  have "a b. a 0 (λx. x - u) ` S {x. a x = b}"
  proof (rule empty_interior_subset_hyperplane_aux)
    show "convex ((λx. x - u) ` S)"
      using convex S by force
    show "0 (λx. x - u) ` S"
      by (simp add: u S)
    show "interior ((λx. x - u) ` S) = {}"
      by (simp add: int interior_translation_subtract)
  qed
  then obtain a b where "a 0" and ab: "(λx. x - u) ` S {x. a x = b}"
    by metis
  then have "S {x. a x = b + (a u)}"
    using ab by (auto simp: algebra_simps)
  then show ?thesis
    using a 0 that by auto
qed

lemma rel_interior_same_affine_hull:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "affine hull (rel_interior S) = affine hull S"
  by (metis assms closure_same_affine_hull convex_closure_rel_interior)

lemma rel_interior_aff_dim:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "aff_dim (rel_interior S) = aff_dim S"
  by (metis aff_dim_affine_hull2 assms rel_interior_same_affine_hull)

lemma rel_interior_rel_interior:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "rel_interior (rel_interior S) = rel_interior S"
proof -
  have "openin (top_of_set (affine hull (rel_interior S))) (rel_interior S)"
    using openin_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
  then show ?thesis
    using rel_interior_def by auto
qed

lemma rel_interior_rel_open:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "rel_open (rel_interior S)"
  unfolding rel_open_def using rel_interior_rel_interior assms by auto

lemma convex_rel_interior_closure_aux:
  fixes x y z :: "'n::euclidean_space"
  assumes "0 < a" "0 < b" "(a + b) *🪙R z = a *🪙R x + b *🪙R y"
  obtains e where "0 < e" "e < 1" "z = y - e *🪙R (y - x)"
proof -
  define e where "e = a / (a + b)"
  have "z = (1 / (a + b)) *🪙R ((a + b) *🪙R z)"
    using assms  by (simp add: eq_vector_fraction_iff)
  also have " = (1 / (a + b)) *🪙R (a *🪙R x + b *🪙R y)"
    using assms scaleR_cancel_left[of "1/(a+b)" "(a + b) *🪙R z" "a *🪙R x + b *🪙R y"]
    by auto
  also have " = y - e *🪙R (y-x)"
    using e_def assms
    by (simp add: divide_simps vector_fraction_eq_iff) (simp add: algebra_simps)
  finally have "z = y - e *🪙R (y-x)"
    by auto
  moreover have "e > 0" "e < 1" using e_def assms by auto
  ultimately show ?thesis using that[of e] by auto
qed

lemma convex_rel_interior_closure:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "rel_interior (closure S) = rel_interior S"
proof (cases "S = {}")
  case True
  then show ?thesis
    using assms rel_interior_eq_empty by auto
next
  case False
  have "rel_interior (closure S) 🪙 rel_interior S"
    using subset_rel_interior[of S "closure S"] closure_same_affine_hull closure_subset
    by auto
  moreover
  {
    fix z
    assume z: "z rel_interior (closure S)"
    obtain x where x: "x rel_interior S"
      using S {} assms rel_interior_eq_empty by auto
    have "z rel_interior S"
    proof (cases "x = z")
      case True
      then show ?thesis using x by auto
    next
      case False
      obtain e where e: "e > 0" "cball z e affine hull closure S closure S"
        using z rel_interior_cball[of "closure S"by auto
      hence *: "0 < e/norm(z-x)" using e False by auto
      define y where "y = z + (e/norm(z-x)) *🪙R (z-x)"
      have yball: "y cball z e"
        using y_def dist_norm[of z y] e by auto
      have "x affine hull closure S"
        using x rel_interior_subset_closure hull_inc[of x "closure S"by blast
      moreover have "z affine hull closure S"
        using z rel_interior_subset hull_subset[of "closure S"by blast
      ultimately have "y affine hull closure S"
        using y_def affine_affine_hull[of "closure S"]
          mem_affine_3_minus [of "affine hull closure S" z z x "e/norm(z-x)"by auto
      then have "y closure S" using e yball by auto
      have "(1 + (e/norm(z-x))) *🪙R z = (e/norm(z-x)) *🪙R x + y"
        using y_def by (simp add: algebra_simps)
      then obtain e1 where "0 < e1" "e1 < 1" "z = y - e1 *🪙R (y - x)"
        using * convex_rel_interior_closure_aux[of "e / norm (z - x)" 1 z x y]
        by (auto simp add: algebra_simps)
      then show ?thesis
        using rel_interior_closure_convex_shrink assms x y closure S
        by fastforce
    qed
  }
  ultimately show ?thesis by auto
qed

lemma convex_interior_closure:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "interior (closure S) = interior S"
  using closure_aff_dim[of S] interior_rel_interior_gen[of S]
    interior_rel_interior_gen[of "closure S"]
    convex_rel_interior_closure[of S] assms
  by auto

lemma open_subset_closure_of_interval:
  assumes "open U" "is_interval S"
  shows "U closure S U interior S"
  by (metis assms convex_interior_closure is_interval_convex open_subset_interior)

lemma closure_eq_rel_interior_eq:
  fixes S1 S2 :: "'n::euclidean_space set"
  assumes "convex S1"
    and "convex S2"
  shows "closure S1 = closure S2 rel_interior S1 = rel_interior S2"
  by (metis convex_rel_interior_closure convex_closure_rel_interior assms)

lemma closure_eq_between:
  fixes S1 S2 :: "'n::euclidean_space set"
  assumes "convex S1"
    and "convex S2"
  shows "closure S1 = closure S2 rel_interior S1 S2 S2 closure S1"
  (is "?A ?B")
proof
  assume ?A
  then show ?B
    by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
next
  assume ?B
  then have "closure S1 closure S2"
    by (metis assms(1) convex_closure_rel_interior closure_mono)
  moreover from ?B have "closure S1 🪙 closure S2"
    by (metis closed_closure closure_minimal)
  ultimately show ?A ..
qed

lemma open_inter_closure_rel_interior:
  fixes S A :: "'n::euclidean_space set"
  assumes "convex S"
    and "open A"
  shows "A closure S = {} A rel_interior S = {}"
  by (metis assms convex_closure_rel_interior open_Int_closure_eq_empty)

lemma rel_interior_open_segment:
  fixes a :: "'a :: euclidean_space"
  shows "rel_interior(open_segment a b) = open_segment a b"
proof (cases "a = b")
  case True then show ?thesis by auto
next
  case False then
  have "open_segment a b = affine hull {a, b} ball ((a + b) /🪙R 2) (norm (b - a) / 2)"
    by (simp add: open_segment_as_ball)
  then show ?thesis
    unfolding rel_interior_eq openin_open
    by (metis Elementary_Metric_Spaces.open_ball False affine_hull_open_segment)
qed

lemma rel_interior_closed_segment:
  fixes a :: "'a :: euclidean_space"
  shows "rel_interior(closed_segment a b) =
         (if a = b then {a} else open_segment a b)"
proof (cases "a = b")
  case True then show ?thesis by auto
next
  case False then show ?thesis
    by simp
       (metis closure_open_segment convex_open_segment convex_rel_interior_closure
              rel_interior_open_segment)
qed

lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment

subsectionThe relative frontier of a set

definition🍋tag important "rel_frontier S = closure S - rel_interior S"

lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
  by (simp add: rel_frontier_def)

lemma rel_frontier_eq_empty:
    fixes S :: "'n::euclidean_space set"
    shows "rel_frontier S = {} affine S"
  unfolding rel_frontier_def
  using rel_interior_subset_closure  by (auto simp add: rel_interior_eq_closure [symmetric])

lemma rel_frontier_sing [simp]:
    fixes a :: "'n::euclidean_space"
    shows "rel_frontier {a} = {}"
  by (simp add: rel_frontier_def)

lemma rel_frontier_affine_hull:
  fixes S :: "'a::euclidean_space set"
  shows "rel_frontier S affine hull S"
using closure_affine_hull rel_frontier_def by fastforce

lemma rel_frontier_cball [simp]:
    fixes a :: "'n::euclidean_space"
    shows "rel_frontier(cball a r) = (if r = 0 then {} else sphere a r)"
proof (cases rule: linorder_cases [of r 0])
  case less then show ?thesis
    by (force simp: sphere_def)
next
  case equal then show ?thesis by simp
next
  case greater then show ?thesis
    by simp (metis centre_in_ball empty_iff frontier_cball frontier_def interior_cball interior_rel_interior_gen rel_frontier_def)
qed

lemma rel_frontier_translation:
  fixes a :: "'a::euclidean_space"
  shows "rel_frontier((λx. a + x) ` S) = (λx. a + x) ` (rel_frontier S)"
  by (simp add: rel_frontier_def translation_diff rel_interior_translation closure_translation)

lemma rel_frontier_nonempty_interior:
  fixes S :: "'n::euclidean_space set"
  shows "interior S {} ==> rel_frontier S = frontier S"
  by (metis frontier_def interior_rel_interior_gen rel_frontier_def)

lemma rel_frontier_frontier:
  fixes S :: "'n::euclidean_space set"
  shows "affine hull S = UNIV ==> rel_frontier S = frontier S"
  by (simp add: frontier_def rel_frontier_def rel_interior_interior)

lemma closest_point_in_rel_frontier:
   "[closed S; S {}; x affine hull S - rel_interior S]
   ==> closest_point S x rel_frontier S"
  by (simp add: closest_point_in_rel_interior closest_point_in_set rel_frontier_def)

lemma closed_rel_frontier [iff]:
  fixes S :: "'n::euclidean_space set"
  shows "closed (rel_frontier S)"
proof -
  have *: "closedin (top_of_set (affine hull S)) (closure S - rel_interior S)"
    by (simp add: closed_subset closedin_diff closure_affine_hull openin_rel_interior)
  show ?thesis
  proof (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"])
    show "closedin (top_of_set (affine hull S)) (rel_frontier S)"
      by (simp add: "*" rel_frontier_def)
  qed simp
qed

lemma closed_rel_boundary:
  fixes S :: "'n::euclidean_space set"
  shows "closed S ==> closed(S - rel_interior S)"
  by (metis closed_rel_frontier closure_closed rel_frontier_def)

lemma compact_rel_boundary:
  fixes S :: "'n::euclidean_space set"
  shows "compact S ==> compact(S - rel_interior S)"
  by (metis bounded_diff closed_rel_boundary closure_eq compact_closure compact_imp_closed)

lemma bounded_rel_frontier:
  fixes S :: "'n::euclidean_space set"
  shows "bounded S ==> bounded(rel_frontier S)"
by (simp add: bounded_closure bounded_diff rel_frontier_def)

lemma compact_rel_frontier_bounded:
  fixes S :: "'n::euclidean_space set"
  shows "bounded S ==> compact(rel_frontier S)"
using bounded_rel_frontier closed_rel_frontier compact_eq_bounded_closed by blast

lemma compact_rel_frontier:
  fixes S :: "'n::euclidean_space set"
  shows "compact S ==> compact(rel_frontier S)"
by (meson compact_eq_bounded_closed compact_rel_frontier_bounded)

lemma convex_same_rel_interior_closure:
  fixes S :: "'n::euclidean_space set"
  shows "[convex S; convex T]
         ==> rel_interior S = rel_interior T closure S = closure T"
by (simp add: closure_eq_rel_interior_eq)

lemma convex_same_rel_interior_closure_straddle:
  fixes S :: "'n::euclidean_space set"
  shows "[convex S; convex T]
         ==> rel_interior S = rel_interior T
             rel_interior S T T closure S"
by (simp add: closure_eq_between convex_same_rel_interior_closure)

lemma convex_rel_frontier_aff_dim:
  fixes S1 S2 :: "'n::euclidean_space set"
  assumes "convex S1"
    and "convex S2"
    and "S2 {}"
    and "S1 rel_frontier S2"
  shows "aff_dim S1 < aff_dim S2"
proof -
  have "S1 closure S2"
    using assms unfolding rel_frontier_def by auto
  then have *: "affine hull S1 affine hull S2"
    using hull_mono[of "S1" "closure S2"] closure_same_affine_hull[of S2] by blast
  then have "aff_dim S1 aff_dim S2"
    using * aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2]
      aff_dim_subset[of "affine hull S1" "affine hull S2"]
    by auto
  moreover
  {
    assume eq: "aff_dim S1 = aff_dim S2"
    then have "S1 {}"
      using aff_dim_empty[of S1] aff_dim_empty[of S2] S2 {} by auto
    have **: "affine hull S1 = affine hull S2"
      by (simp_all add: * eq S1 {} affine_dim_equal)
    obtain a where a: "a rel_interior S1"
      using S1 {} rel_interior_eq_empty assms by auto
    obtain T where T: "open T" "a T S1" "T affine hull S1 S1"
       using mem_rel_interior[of a S1] a by auto
    then have "a T closure S2"
      using a assms unfolding rel_frontier_def by auto
    then obtain b where b: "b T rel_interior S2"
      using open_inter_closure_rel_interior[of S2 T] assms T by auto
    then have "b affine hull S1"
      using rel_interior_subset hull_subset[of S2] ** by auto
    then have "b S1"
      using T b by auto
    then have False
      using b assms unfolding rel_frontier_def by auto
  }
  ultimately show ?thesis
    using less_le by auto
qed

lemma convex_rel_interior_if:
  fixes S ::  "'n::euclidean_space set"
  assumes "convex S"
    and "z rel_interior S"
  shows "xaffine hull S. m. m > 1 (e. e > 1 e m (1 - e) *🪙R x + e *🪙R z S)"
proof -
  obtain e1 where e1: "e1 > 0 cball z e1 affine hull S S"
    using mem_rel_interior_cball[of z S] assms by auto
  {
    fix x
    assume x: "x affine hull S"
    {
      assume "x z"
      define m where "m = 1 + e1/norm(x-z)"
      hence "m > 1" using e1 x z by auto
      {
        fix e
        assume e: "e > 1 e m"
        have "z affine hull S"
          using assms rel_interior_subset hull_subset[of S] by auto
        then have *: "(1 - e)*🪙R x + e *🪙R z affine hull S"
          using mem_affine[of "affine hull S" x z "(1-e)" e] affine_affine_hull[of S] x
          by auto
        have "norm (z + e *🪙R x - (x + e *🪙R z)) = norm ((e - 1) *🪙R (x - z))"
          by (simp add: algebra_simps)
        also have " = (e - 1) * norm (x-z)"
          using norm_scaleR e by auto
        also have " (m - 1) * norm (x - z)"
          using e mult_right_mono[of _ _ "norm(x-z)"by auto
        also have " = (e1 / norm (x - z)) * norm (x - z)"
          using m_def by auto
        also have " = e1"
          using x z e1 by simp
        finally have **: "norm (z + e *🪙R x - (x + e *🪙R z)) e1"
          by auto
        have "(1 - e)*🪙R x+ e *🪙R z cball z e1"
          using m_def **
          unfolding cball_def dist_norm
          by (auto simp add: algebra_simps)
        then have "(1 - e) *🪙R x+ e *🪙R z S"
          using e * e1 by auto
      }
      then have "m. m > 1 (e. e > 1 e m (1 - e) *🪙R x + e *🪙R z S )"
        using m> 1 by auto
    }
    moreover
    {
      assume "x = z"
      define m where "m = 1 + e1"
      then have "m > 1"
        using e1 by auto
      {
        fix e
        assume e: "e > 1 e m"
        then have "(1 - e) *🪙R x + e *🪙R z S"
          using e1 x x = z by (auto simp add: algebra_simps)
        then have "(1 - e) *🪙R x + e *🪙R z S"
          using e by auto
      }
      then have "m. m > 1 (e. e > 1 e m (1 - e) *🪙R x + e *🪙R z S)"
        using m > 1 by auto
    }
    ultimately have "m. m > 1 (e. e > 1 e m (1 - e) *🪙R x + e *🪙R z S )"
      by blast
  }
  then show ?thesis by auto
qed

lemma convex_rel_interior_if2:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  assumes "z rel_interior S"
  shows "xaffine hull S. e. e > 1 (1 - e)*🪙R x + e *🪙R z S"
  using convex_rel_interior_if[of S z] assms by auto

lemma convex_rel_interior_only_if:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
    and "S {}"
  assumes "xS. e. e > 1 (1 - e) *🪙R x + e *🪙R z S"
  shows "z rel_interior S"
proof -
  obtain x where x: "x rel_interior S"
    using rel_interior_eq_empty assms by auto
  then have "x S"
    using rel_interior_subset by auto
  then obtain e where e: "e > 1 (1 - e) *🪙R x + e *🪙R z S"
    using assms by auto
  define y where [abs_def]: "y = (1 - e) *🪙R x + e *🪙R z"
  then have "y S" using e by auto
  define e1 where "e1 = 1/e"
  then have "0 < e1 e1 < 1" using e by auto
  then have "z =y - (1 - e1) *🪙R (y - x)"
    using e1_def y_def by (auto simp add: algebra_simps)
  then show ?thesis
    using rel_interior_convex_shrink[of S x y "1-e1"0 🚫 e1 🚫 y S x assms
    by auto
qed

lemma convex_rel_interior_iff:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
    and "S {}"
  shows "z rel_interior S (xS. e. e > 1 (1 - e) *🪙R x + e *🪙R z S)"
  using assms hull_subset[of S "affine"]
    convex_rel_interior_if[of S z] convex_rel_interior_only_if[of S z]
  by auto

lemma convex_rel_interior_iff2:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
    and "S {}"
  shows "z rel_interior S (xaffine hull S. e. e > 1 (1 - e) *🪙R x + e *🪙R z S)"
  using assms hull_subset[of S] convex_rel_interior_if2[of S z] convex_rel_interior_only_if[of S z]
  by auto

lemma convex_interior_iff:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "z interior S (x. e. e > 0 z + e *🪙R x S)"
proof (cases "aff_dim S = int DIM('n)")
  case False
  { assume "z interior S"
    then have False
      using False interior_rel_interior_gen[of S] by auto }
  moreover
  { assume r: "x. e. e > 0 z + e *🪙R x S"
    { fix x
      obtain e1 where e1: "e1 > 0 z + e1 *🪙R (x - z) S"
        using r by auto
      obtain e2 where e2: "e2 > 0 z + e2 *🪙R (z - x) S"
        using r by auto
      define x1 where [abs_def]: "x1 = z + e1 *🪙R (x - z)"
      then have x1: "x1 affine hull S"
        using e1 hull_subset[of S] by auto
      define x2 where [abs_def]: "x2 = z + e2 *🪙R (z - x)"
      then have x2: "x2 affine hull S"
        using e2 hull_subset[of S] by auto
      have *: "e1/(e1+e2) + e2/(e1+e2) = 1"
        using add_divide_distrib[of e1 e2 "e1+e2"] e1 e2 by simp
      then have "z = (e2/(e1+e2)) *🪙R x1 + (e1/(e1+e2)) *🪙R x2"
        by (simp add: x1_def x2_def algebra_simps) (simp add: "*" pth_8)
      then have z: "z affine hull S"
        using mem_affine[of "affine hull S" x1 x2 "e2/(e1+e2)" "e1/(e1+e2)"]
          x1 x2 affine_affine_hull[of S] *
        by auto
      have "x1 - x2 = (e1 + e2) *🪙R (x - z)"
        using x1_def x2_def by (auto simp add: algebra_simps)
      then have "x = z+(1/(e1+e2)) *🪙R (x1-x2)"
        using e1 e2 by simp
      then have "x affine hull S"
        using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"]
          x1 x2 z affine_affine_hull[of S]
        by auto
    }
    then have "affine hull S = UNIV"
      by auto
    then have "aff_dim S = int DIM('n)"
      using aff_dim_affine_hull[of S] by (simp)
    then have False
      using False by auto
  }
  ultimately show ?thesis by auto
next
  case True
  then have "S {}"
    using aff_dim_empty[of S] by auto
  have *: "affine hull S = UNIV"
    using True affine_hull_UNIV by auto
  {
    assume "z interior S"
    then have "z rel_interior S"
      using True interior_rel_interior_gen[of S] by auto
    then have **: "x. e. e > 1 (1 - e) *🪙R x + e *🪙R z S"
      using convex_rel_interior_iff2[of S z] assms S {}by auto
    fix x
    obtain e1 where e1: "e1 > 1" "(1 - e1) *🪙R (z - x) + e1 *🪙R z S"
      using **[rule_format, of "z-x"by auto
    define e where [abs_def]: "e = e1 - 1"
    then have "(1 - e1) *🪙R (z - x) + e1 *🪙R z = z + e *🪙R x"
      by (simp add: algebra_simps)
    then have "e > 0" "z + e *🪙R x S"
      using e1 e_def by auto
    then have "e. e > 0 z + e *🪙R x S"
      by auto
  }
  moreover
  {
    assume r: "x. e. e > 0 z + e *🪙R x S"
    {
      fix x
      obtain e1 where e1: "e1 > 0" "z + e1 *🪙R (z - x) S"
        using r[rule_format, of "z-x"by auto
      define e where "e = e1 + 1"
      then have "z + e1 *🪙R (z - x) = (1 - e) *🪙R x + e *🪙R z"
        by (simp add: algebra_simps)
      then have "e > 1" "(1 - e)*🪙R x + e *🪙R z S"
        using e1 e_def by auto
      then have "e. e > 1 (1 - e) *🪙R x + e *🪙R z S" by auto
    }
    then have "z rel_interior S"
      using convex_rel_interior_iff2[of S z] assms S {} by auto
    then have "z interior S"
      using True interior_rel_interior_gen[of S] by auto
  }
  ultimately show ?thesis by auto
qed


subsubsection🍋tag unimportant Relative interior and closure under common operations

lemma rel_interior_inter_aux: "{rel_interior S |S. S I} I"
proof -
  { fix y
    assume "y {rel_interior S |S. S I}"
    then have y: "S I. y rel_interior S"
      by auto
    { fix S
      assume "S I"
      then have "y S"
        using rel_interior_subset y by auto
    }
    then have "y I" by auto
  }
  then show ?thesis by auto
qed

lemma convex_closure_rel_interior_Int:
  assumes "S. SF ==> convex (S :: 'n::euclidean_space set)"
    and "(rel_interior ` F) {}"
  shows "(closure ` F) closure ((rel_interior ` F))"
proof -
  obtain x where x: "SF. x rel_interior S"
    using assms by auto
  show ?thesis
  proof
    fix y
    assume y: "y (closure ` F)"
    show "y closure ((rel_interior ` F))"
    proof (cases "y=x")
      case True
      with closure_subset x show ?thesis 
        by fastforce
    next
      case False
      show ?thesis
      proof (clarsimp simp: closure_approachable_le)
        fix ε :: real
        assume e: "ε > 0"
        define e1 where "e1 = min 1 (ε/norm (y - x))"
        then have e1: "e1 > 0" "e1 1" "e1 * norm (y - x) ε"
          using y x ε > 0 le_divide_eq[of e1 ε "norm (y - x)"]
          by simp_all
        define z where "z = y - e1 *🪙R (y - x)"
        {
          fix S
          assume "S F"
          then have "z rel_interior S"
            using rel_interior_closure_convex_shrink[of S x y e1] assms x y e1 z_def
            by auto
        }
        then have *: "z (rel_interior ` F)"
          by auto
        show "x (rel_interior ` F). dist x y ε"
          using y x z_def * e1 e dist_norm[of z y]
          by force
      qed
    qed
  qed
qed


lemma closure_Inter_convex:
  fixes F :: "'n::euclidean_space set set"
  assumes "S. S F ==> convex S" and "(rel_interior ` F) {}"
  shows "closure(F) = (closure ` F)"
proof -
  have "(closure ` F) closure ((rel_interior ` F))"
    by (meson assms convex_closure_rel_interior_Int)
  moreover
  have "closure ((rel_interior ` F)) closure (F)"
    using rel_interior_inter_aux closure_mono[of "(rel_interior ` F)" "F"]
    by auto
  ultimately show ?thesis
    using closure_Int[of Fby blast
qed

lemma closure_Inter_convex_open:
    "(S::'n::euclidean_space set. S F ==> convex S open S)
        ==> closure(F) = (if F = {} then {} else (closure ` F))"
  by (simp add: closure_Inter_convex rel_interior_open)

lemma convex_Inter_rel_interior_same_closure:
  fixes F :: "'n::euclidean_space set set"
  assumes "S. S F ==> convex S"
    and "(rel_interior ` F) {}"
  shows "closure ((rel_interior ` F)) = closure (F)"
proof -
  have "(closure ` F) closure ((rel_interior ` F))"
    by (meson assms convex_closure_rel_interior_Int)
  moreover
  have "closure ((rel_interior ` F)) closure (F)"
    by (metis Setcompr_eq_image closure_mono rel_interior_inter_aux)
  ultimately show ?thesis
    by (simp add: assms closure_Inter_convex)
qed

lemma convex_rel_interior_Inter:
  fixes F :: "'n::euclidean_space set set"
  assumes "S. S F ==> convex S"
    and "(rel_interior ` F) {}"
  shows "rel_interior (F) (rel_interior ` F)"
proof -
  have "convex (F)"
    using assms convex_Inter by auto
  moreover
  have "convex ((rel_interior ` F))"
    using assms by (metis convex_rel_interior convex_INT)
  ultimately
  have "rel_interior ((rel_interior ` F)) = rel_interior (F)"
    using convex_Inter_rel_interior_same_closure assms
      closure_eq_rel_interior_eq[of "(rel_interior ` F)" "F"]
    by blast
  then show ?thesis
    using rel_interior_subset[of "(rel_interior ` F)"by auto
qed

lemma convex_rel_interior_finite_Inter:
  fixes F :: "'n::euclidean_space set set"
  assumes "S. S F ==> convex S"
    and "(rel_interior ` F) {}"
    and "finite F"
  shows "rel_interior (F) = (rel_interior ` F)"
proof -
  have "F {}"
    using assms rel_interior_inter_aux[of Fby auto
  have "convex (F)"
    using convex_Inter assms by auto
  show ?thesis
  proof (cases "F = {}")
    case True
    then show ?thesis
      using Inter_empty rel_interior_UNIV by auto
  next
    case False
    {
      fix z
      assume z: "z (rel_interior ` F)"
      {
        fix x
        assume x: "x F"
        {
          fix S
          assume S: "S F"
          then have "z rel_interior S" "x S"
            using z x by auto
          then have "m. m > 1 (e. e > 1 e m (1 - e)*🪙R x + e *🪙R z S)"
            using convex_rel_interior_if[of S z] S assms hull_subset[of S] by auto
        }
        then obtain mS where
          mS: "SF. mS S > 1 (e. e > 1 e mS S (1 - e) *🪙R x + e *🪙R z S)" by metis
        define e where "e = Min (mS ` F)"
        then have "e mS ` F" using assms F {} by simp
        then have "e > 1" using mS by auto
        moreover have "SF. e mS S"
          using e_def assms by auto
        ultimately have "e > 1. (1 - e) *🪙R x + e *🪙R z F"
          using mS by auto
      }
      then have "z rel_interior (F)"
        using convex_rel_interior_iff[of "F" z] F {} convex (F) by auto
    }
    then show ?thesis
      using convex_rel_interior_Inter[of F] assms by auto
  qed
qed

lemma closure_Int_convex:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "convex T"
  assumes "rel_interior S rel_interior T {}"
  shows "closure (S T) = closure S closure T"
  using closure_Inter_convex[of "{S,T}"] assms by auto

lemma convex_rel_interior_inter_two:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "convex T"
    and "rel_interior S rel_interior T {}"
  shows "rel_interior (S T) = rel_interior S rel_interior T"
  using convex_rel_interior_finite_Inter[of "{S,T}"] assms by auto

lemma convex_affine_closure_Int:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "affine T"
    and "rel_interior S T {}"
  shows "closure (S T) = closure S T"
  by (metis affine_imp_convex assms closure_Int_convex rel_interior_affine rel_interior_eq_closure)

lemma connected_component_1_gen:
  fixes S :: "'a :: euclidean_space set"
  assumes "DIM('a) = 1"
  shows "connected_component S a b closed_segment a b S"
unfolding connected_component_def
by (metis (no_types, lifting) assms subsetD subsetI convex_contains_segment convex_segment(1)
            ends_in_segment connected_convex_1_gen)

lemma connected_component_1:
  fixes S :: "real set"
  shows "connected_component S a b closed_segment a b S"
by (simp add: connected_component_1_gen)

lemma convex_affine_rel_interior_Int:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "affine T"
    and "rel_interior S T {}"
  shows "rel_interior (S T) = rel_interior S T"
  by (simp add: affine_imp_convex assms convex_rel_interior_inter_two rel_interior_affine)

lemma convex_affine_rel_frontier_Int:
   fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "affine T"
    and "interior S T {}"
  shows "rel_frontier(S T) = frontier S T"
using assms
  unfolding rel_frontier_def  frontier_def
  using convex_affine_closure_Int convex_affine_rel_interior_Int rel_interior_nonempty_interior by fastforce

lemma rel_interior_convex_Int_affine:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "affine T" "interior S T {}"
  shows "rel_interior(S T) = interior S T"
  by (metis Int_emptyI assms convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen)

lemma subset_rel_interior_convex:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "convex T"
    and "S closure T"
    and "¬ S rel_frontier T"
  shows "rel_interior S rel_interior T"
proof -
  have *: "S closure T = S"
    using assms by auto
  have "¬ rel_interior S rel_frontier T"
    using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
      closure_closed[of S] convex_closure_rel_interior[of S] closure_subset[of S] assms
    by auto
  then have "rel_interior S rel_interior (closure T) {}"
    using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T]
    by auto
  then have "rel_interior S rel_interior T = rel_interior (S closure T)"
    using assms convex_closure convex_rel_interior_inter_two[of S "closure T"]
      convex_rel_interior_closure[of T]
    by auto
  also have " = rel_interior S"
    using * by auto
  finally show ?thesis
    by auto
qed

lemma rel_interior_convex_linear_image:
  fixes f :: "'m::euclidean_space ==> 'n::euclidean_space"
  assumes "linear f"
    and "convex S"
  shows "f ` (rel_interior S) = rel_interior (f ` S)"
proof (cases "S = {}")
  case True
  then show ?thesis
    using assms by auto
next
  case False
  interpret linear f by fact
  have *: "f ` (rel_interior S) f ` S"
    unfolding image_mono using rel_interior_subset by auto
  have "f ` S f ` (closure S)"
    unfolding image_mono using closure_subset by auto
  also have " = f ` (closure (rel_interior S))"
    using convex_closure_rel_interior assms by auto
  also have " closure (f ` (rel_interior S))"
    using closure_linear_image_subset assms by auto
  finally have "closure (f ` S) = closure (f ` rel_interior S)"
    using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
      closure_mono[of "f ` rel_interior S" "f ` S"] *
    by auto
  then have "rel_interior (f ` S) = rel_interior (f ` rel_interior S)"
    using assms convex_rel_interior
      linear_conv_bounded_linear[of f] convex_linear_image[of _ S]
      convex_linear_image[of _ "rel_interior S"]
      closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"]
    by auto
  then have "rel_interior (f ` S) f ` rel_interior S"
    using rel_interior_subset by auto
  moreover
  {
    fix z
    assume "z f ` rel_interior S"
    then obtain z1 where z1: "z1 rel_interior S" "f z1 = z" by auto
    {
      fix x
      assume "x f ` S"
      then obtain x1 where x1: "x1 S" "f x1 = x" by auto
      then obtain e where e: "e > 1" "(1 - e) *🪙R x1 + e *🪙R z1 S"
        using convex_rel_interior_iff[of S z1] convex S x1 z1 by auto
      moreover have "f ((1 - e) *🪙R x1 + e *🪙R z1) = (1 - e) *🪙R x + e *🪙R z"
        using x1 z1 by (simp add: linear_add linear_scale linear f)
      ultimately have "(1 - e) *🪙R x + e *🪙R z f ` S"
        using imageI[of "(1 - e) *🪙R x1 + e *🪙R z1" S f] by auto
      then have "e. e > 1 (1 - e) *🪙R x + e *🪙R z f ` S"
        using e by auto
    }
    then have "z rel_interior (f ` S)"
      using convex_rel_interior_iff[of "f ` S" z] convex S linear f
        S {} convex_linear_image[of f S]  linear_conv_bounded_linear[of f]
      by auto
  }
  ultimately show ?thesis by auto
qed

lemma rel_interior_convex_linear_preimage:
  fixes f :: "'m::euclidean_space ==> 'n::euclidean_space"
  assumes "linear f"
    and "convex S"
    and "f -` (rel_interior S) {}"
  shows "rel_interior (f -` S) = f -` (rel_interior S)"
proof -
  interpret linear f by fact
  have "S {}"
    using assms by auto
  have nonemp: "f -` S {}"
    by (metis assms(3) rel_interior_subset subset_empty vimage_mono)
  then have "S (range f) {}"
    by auto
  have conv: "convex (f -` S)"
    using convex_linear_vimage assms by auto
  then have "convex (S range f)"
    by (simp add: assms(2) convex_Int convex_linear_image linear_axioms)
  {
    fix z
    assume "z f -` (rel_interior S)"
    then have z: "f z rel_interior S"
      by auto
    {
      fix x
      assume "x f -` S"
      then have "f x S" by auto
      then obtain e where e: "e > 1" "(1 - e) *🪙R f x + e *🪙R f z S"
        using convex_rel_interior_iff[of S "f z"] z assms S {} by auto
      moreover have "(1 - e) *🪙R f x + e *🪙R f z = f ((1 - e) *🪙R x + e *🪙R z)"
        using linear f by (simp add: linear_iff)
      ultimately have "e. e > 1 (1 - e) *🪙R x + e *🪙R z f -` S"
        using e by auto
    }
    then have "z rel_interior (f -` S)"
      using convex_rel_interior_iff[of "f -` S" z] conv nonemp by auto
  }
  moreover
  {
    fix z
    assume z: "z rel_interior (f -` S)"
    {
      fix x
      assume "x S range f"
      then obtain y where y: "f y = x" "y f -` S" by auto
      then obtain e where e: "e > 1" "(1 - e) *🪙R y + e *🪙R z f -` S"
        using convex_rel_interior_iff[of "f -` S" z] z conv by auto
      moreover have "(1 - e) *🪙R x + e *🪙R f z = f ((1 - e) *🪙R y + e *🪙R z)"
        using linear fby (simp add: linear_iff)
      ultimately have "e. e > 1 (1 - e) *🪙R x + e *🪙R f z S range f"
        using e by auto
    }
    then have "f z rel_interior (S range f)"
      using convex (S (range f)) S range f {}
        convex_rel_interior_iff[of "S (range f)" "f z"]
      by auto
    moreover have "affine (range f)"
      by (simp add: linear_axioms linear_subspace_image subspace_imp_affine)
    ultimately have "f z rel_interior S"
      using convex_affine_rel_interior_Int[of S "range f"] assms by auto
    then have "z f -` (rel_interior S)"
      by auto
  }
  ultimately show ?thesis by auto
qed

lemma rel_interior_Times:
  fixes S :: "'n::euclidean_space set"
    and T :: "'m::euclidean_space set"
  assumes "convex S"
    and "convex T"
  shows "rel_interior (S × T) = rel_interior S × rel_interior T"
proof (cases "S = {} T = {}")
  case True
  then show ?thesis 
    by auto
next
  case False
  then have "S {}" "T {}"
    by auto
  then have ri: "rel_interior S {}" "rel_interior T {}"
    using rel_interior_eq_empty assms by auto
  then have "fst -` rel_interior S {}"
    using fst_vimage_eq_Times[of "rel_interior S"by auto
  then have "rel_interior ((fst :: 'n * 'm ==> 'n) -` S) = fst -` rel_interior S"
    using linear_fst convex S rel_interior_convex_linear_preimage[of fst S] by auto
  then have s: "rel_interior (S × (UNIV :: 'm set)) = rel_interior S × UNIV"
    by (simp add: fst_vimage_eq_Times)
  from ri have "snd -` rel_interior T {}"
    using snd_vimage_eq_Times[of "rel_interior T"by auto
  then have "rel_interior ((snd :: 'n * 'm ==> 'm) -` T) = snd -` rel_interior T"
    using linear_snd convex T rel_interior_convex_linear_preimage[of snd T] by auto
  then have t: "rel_interior ((UNIV :: 'n set) × T) = UNIV × rel_interior T"
    by (simp add: snd_vimage_eq_Times)
  from s t have *: "rel_interior (S × (UNIV :: 'm set)) rel_interior ((UNIV :: 'n set) × T) =
      rel_interior S × rel_interior T" by auto
  have "S × T = S × (UNIV :: 'm set) (UNIV :: 'n set) × T"
    by auto
  then have "rel_interior (S × T) = rel_interior ((S × (UNIV :: 'm set)) ((UNIV :: 'n set) × T))"
    by auto
  also have " = rel_interior (S × (UNIV :: 'm set)) rel_interior ((UNIV :: 'n set) × T)"
    using * ri assms convex_Times
    by (subst convex_rel_interior_inter_two) auto
  finally show ?thesis using * by auto
qed

lemma rel_interior_scaleR:
  fixes S :: "'n::euclidean_space set"
  assumes "c 0"
  shows "((*🪙R) c) ` (rel_interior S) = rel_interior (((*🪙R) c) ` S)"
  using rel_interior_injective_linear_image[of "((*🪙R) c)" S]
    linear_conv_bounded_linear[of "(*\<^sub>R) c"] linear_scaleR injective_scaleR[of c] assms
  by auto

lemma rel_interior_convex_scaleR:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "((*\<^sub>R) c) ` (rel_interior S) = rel_interior (((*\<^sub>R) c) ` S)"
  by (metis assms linear_scaleR rel_interior_convex_linear_image)
 
 lemma convex_rel_open_scaleR:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  and "rel_open S"
  shows "convex (((*🪙R) c) ` S) rel_open (((*🪙R) c) ` S)"
  by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)
 
 lemma convex_rel_open_finite_Inter:
  fixes F :: "'n::euclidean_space set set"
  assumes "S. S F ==> convex S rel_open S"
  and "finite F"
  shows "convex (F) rel_open (F)"
 proof (cases "{rel_interior S |S. S F} = {}")
  case True
  then have "F = {}"
  using assms unfolding rel_open_def by auto
  then show ?thesis
  unfolding rel_open_def by auto
 next
  case False
  then have "rel_open (F)"
  using assms convex_rel_interior_finite_Inter[of F] by (force simp: rel_open_def)
  then show ?thesis
  using convex_Inter assms by auto
 qed
 
 lemma convex_rel_open_linear_image:
  fixes f :: "'m::euclidean_space ==> 'n::euclidean_space"
  assumes "linear f"
  and "convex S"
  and "rel_open S"
  shows "convex (f ` S) rel_open (f ` S)"
  by (metis assms convex_linear_image rel_interior_convex_linear_image rel_open_def)
 
 lemma convex_rel_open_linear_preimage:
  fixes f :: "'m::euclidean_space ==> 'n::euclidean_space"
  assumes "linear f"
  and "convex S"
  and "rel_open S"
  shows "convex (f -` S) rel_open (f -` S)"
 proof (cases "f -` (rel_interior S) = {}")
  case True
  then have "f -` S = {}"
  using assms unfolding rel_open_def by auto
  then show ?thesis
  unfolding rel_open_def by auto
 next
  case False
  then have "rel_open (f -` S)"
  using assms unfolding rel_open_def
  using rel_interior_convex_linear_preimage[of f S]
  by auto
  then show ?thesis
  using convex_linear_vimage assms
  by auto
 qed
 
 lemma rel_interior_projection:
  fixes S :: "('m::euclidean_space × 'n::euclidean_space) set"
  and f :: "'m::euclidean_space ==> 'n::euclidean_space set"
  assumes "convex S"
  and "f = (λy. {z. (y, z) S})"
  shows "(y, z) rel_interior S (y rel_interior {y. (f y {})} z rel_interior (f y))"
 proof -
  {
  fix y
  assume "y {y. f y {}}"
  then obtain z where "(y, z) S"
  using assms by auto
  then have "x. x S y = fst x"
  by auto
  then obtain x where "x S" "y = fst x"
  by blast
  then have "y fst ` S"
  unfolding image_def by auto
  }
  then have "fst ` S = {y. f y {}}"
  unfolding fst_def using assms by auto
  then have h1: "fst ` rel_interior S = rel_interior {y. f y {}}"
  using rel_interior_convex_linear_image[of fst S] assms linear_fst by auto
  {
  fix y
  assume "y rel_interior {y. f y {}}"
  then have "y fst ` rel_interior S"
  using h1 by auto
  then have *: "rel_interior S fst -` {y} {}"
  by auto
  moreover have aff: "affine (fst -` {y})"
  unfolding affine_alt by (simp add: algebra_simps)
  ultimately have **: "rel_interior (S fst -` {y}) = rel_interior S fst -` {y}"
  using convex_affine_rel_interior_Int[of S "fst -` {y}"] assms by auto
  have conv: "convex (S fst -` {y})"
  using convex_Int assms aff affine_imp_convex by auto
  {
  fix x
  assume "x f y"
  then have "(y, x) S (fst -` {y})"
  using assms by auto
  moreover have "x = snd (y, x)" by auto
  ultimately have "x snd ` (S fst -` {y})"
  by blast
  }
  then have "snd ` (S fst -` {y}) = f y"
  using assms by auto
  then have ***: "rel_interior (f y) = snd ` rel_interior (S fst -` {y})"
  using rel_interior_convex_linear_image[of snd "S fst -` {y}"] linear_snd conv
  by auto
  {
  fix z
  assume "z rel_interior (f y)"
  then have "z snd ` rel_interior (S fst -` {y})"
  using *** by auto
  moreover have "{y} = fst ` rel_interior (S fst -` {y})"
  using * ** rel_interior_subset by auto
  ultimately have "(y, z) rel_interior (S fst -` {y})"
  by force
  then have "(y,z) rel_interior S"
  using ** by auto
  }
  moreover
  {
  fix z
  assume "(y, z) rel_interior S"
  then have "(y, z) rel_interior (S fst -` {y})"
  using ** by auto
  then have "z snd ` rel_interior (S fst -` {y})"
  by (metis Range_iff snd_eq_Range)
  then have "z rel_interior (f y)"
  using *** by auto
  }
  ultimately have "z. (y, z) rel_interior S z rel_interior (f y)"
  by auto
  }
  then have h2: "y z. y rel_interior {t. f t {}} ==>
  (y, z) rel_interior S z rel_interior (f y)"
  by auto
  {
  fix y z
  assume asm: "(y, z) rel_interior S"
  then have "y fst ` rel_interior S"
  by (metis Domain_iff fst_eq_Domain)
  then have "y rel_interior {t. f t {}}"
  using h1 by auto
  then have "y rel_interior {t. f t {}}" and "(z rel_interior (f y))"
  using h2 asm by auto
  }
  then show ?thesis using h2 by blast
 qed
 
 lemma rel_frontier_Times:
  fixes S :: "'n::euclidean_space set"
  and T :: "'m::euclidean_space set"
  assumes "convex S"
  and "convex T"
  shows "rel_frontier S × rel_frontier T rel_frontier (S × T)"
  by (force simp: rel_frontier_def rel_interior_Times assms closure_Times)
 
 
 subsubsection🍋tag unimportant Relative interior of convex cone
 
 lemma cone_rel_interior:
  fixes S :: "'m::euclidean_space set"
  assumes "cone S"
  shows "cone ({0} rel_interior S)"
 proof (cases "S = {}")
  case True
  then show ?thesis
  by (simp add: cone_0)
 next
  case False
  then have *: "0 S (c. c > 0 (*🪙R) c ` S = S)"
  using cone_iff[of S] assms by auto
  then have *: "0 ({0} rel_interior S)"
  and "c. c > 0 (*🪙R) c ` ({0} rel_interior S) = ({0} rel_interior S)"
  by (auto simp add: rel_interior_scaleR)
  then show ?thesis
  using cone_iff[of "{0} rel_interior S"] by auto
 qed
 
 lemma rel_interior_convex_cone_aux:
  fixes S :: "'m::euclidean_space set"
  assumes "convex S"
  shows "(c, x) rel_interior (cone hull ({(1 :: real)} × S))
  c > 0 x (((*🪙R) c) ` (rel_interior S))"
 proof (cases "S = {}")
  case True
  then show ?thesis
  by (simp add: cone_hull_empty)
 next
  case False
  then obtain s where "s S" by auto
  have conv: "convex ({(1 :: real)} × S)"
  using convex_Times[of "{(1 :: real)}" S] assms convex_singleton[of "1 :: real"]
  by auto
  define f where "f y = {z. (y, z) cone hull ({1 :: real} × S)}" for y
  then have *: "(c, x) rel_interior (cone hull ({(1 :: real)} × S)) =
  (c rel_interior {y. f y {}} x rel_interior (f c))"
  using convex_cone_hull[of "{(1 :: real)} × S"] conv
  by (subst rel_interior_projection) auto
  {
  fix y :: real
  assume "y 0"
  then have "y *🪙R (1,s) cone hull ({1 :: real} × S)"
  using cone_hull_expl[of "{(1 :: real)} × S"] s S by auto
  then have "f y {}"
  using f_def by auto
  }
  then have "{y. f y {}} = {0..}"
  using f_def cone_hull_expl[of "{1 :: real} × S"] by auto
  then have **: "rel_interior {y. f y {}} = {0🚫}"
  using rel_interior_real_semiline by auto
  {
  fix c :: real
  assume "c > 0"
  then have "f c = ((*🪙R) c ` S)"
  using f_def cone_hull_expl[of "{1 :: real} × S"] by auto
  then have "rel_interior (f c) = (*🪙R) c ` rel_interior S"
  using rel_interior_convex_scaleR[of S c] assms by auto
  }
  then show ?thesis using * ** by auto
 qed
 
 lemma rel_interior_convex_cone:
  fixes S :: "'m::euclidean_space set"
  assumes "convex S"
  shows "rel_interior (cone hull ({1 :: real} × S)) =
  {(c, c *🪙R x) | c x. c > 0 x rel_interior S}"
  (is "?lhs = ?rhs")
 proof -
  {
  fix z
  assume "z ?lhs"
  have *: "z = (fst z, snd z)"
  by auto
  then have "z ?rhs"
  using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms z ?lhs by fastforce
  }
  moreover
  {
  fix z
  assume "z ?rhs"
  then have "z ?lhs"
  using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms
  by auto
  }
  ultimately show ?thesis by blast
 qed
 
 lemma convex_hull_finite_union:
  assumes "finite I"
  assumes "iI. convex (S i) (S i) {}"
  shows "convex hull ((S ` I)) =
  {sum (λi. c i *🪙R s i) I | c s. (iI. c i 0) sum c I = 1 (iI. s i S i)}"
  (is "?lhs = ?rhs")
 proof -
  have "?lhs 🪙 ?rhs"
  proof
  fix x
  assume "x ?rhs"
  then obtain c s where *: "sum (λi. c i *🪙R s i) I = x" "sum c I = 1"
  "(iI. c i 0) (iI. s i S i)" by auto
  then have "iI. s i convex hull ((S ` I))"
  using hull_subset[of "(S ` I)" convex] by auto
  then show "x ?lhs"
  unfolding *(1)[symmetric]
  using * assms convex_convex_hull
  by (subst convex_sum) auto
  qed
  {
  fix i
  assume "i I"
  with assms have "p. p S i" by auto
  }
  then obtain p where p: "iI. p i S i" by metis
  {
  fix i
  assume "i I"
  {
  fix x
  assume "x S i"
  define c where "c j = (if j = i then 1::real else 0)" for j
  then have *: "sum c I = 1"
  using finite I i I sum.delta[of I i "λj::'a. 1::real"]
  by auto
  define s where "s j = (if j = i then x else p j)" for j
  then have "j. c j *🪙R s j = (if j = i then x else 0)"
  using c_def by (auto simp add: algebra_simps)
  then have "x = sum (λi. c i *🪙R s i) I"
  using s_def c_def finite I i I sum.delta[of I i "λj::'a. x"]
  by auto
  moreover have "(iI. 0 c i) sum c I = 1 (iI. s i S i)"
  using * c_def s_def p x S i by auto
  ultimately have "x ?rhs"
  by force
  }
  then have "?rhs 🪙 S i" by auto
  }
  then have *: "?rhs 🪙 (S ` I)" by auto
 
  {
  fix u v :: real
  assume uv: "u 0 v 0 u + v = 1"
  fix x y
  assume xy: "x ?rhs y ?rhs"
  from xy obtain c s where
  xc: "x = sum (λi. c i *🪙R s i) I (iI. c i 0) sum c I = 1 (iI. s i S i)"
  by auto
  from xy obtain d t where
  yc: "y = sum (λi. d i *🪙R t i) I (iI. d i 0) sum d I = 1 (iI. t i S i)"
  by auto
  define e where "e i = u * c i + v * d i" for i
  have ge0: "iI. e i 0"
  using e_def xc yc uv by simp
  have "sum (λi. u * c i) I = u * sum c I"
  by (simp add: sum_distrib_left)
  moreover have "sum (λi. v * d i) I = v * sum d I"
  by (simp add: sum_distrib_left)
  ultimately have sum1: "sum e I = 1"
  using e_def xc yc uv by (simp add: sum.distrib)
  define q where "q i = (if e i = 0 then p i else (u * c i / e i) *🪙R s i + (v * d i / e i) *🪙R t i)"
  for i
  {
  fix i
  assume i: "i I"
  have "q i S i"
  proof (cases "e i = 0")
  case True
  then show ?thesis using i p q_def by auto
  next
  case False
  then show ?thesis
  using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"]
  mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"]
  assms q_def e_def i False xc yc uv
  by (auto simp del: mult_nonneg_nonneg)
  qed
  }
  then have qs: "iI. q i S i" by auto
  {
  fix i
  assume i: "i I"
  have "(u * c i) *🪙R s i + (v * d i) *🪙R t i = e i *🪙R q i"
  proof (cases "e i = 0")
  case True
  have ge: "u * (c i) 0 v * d i 0"
  using xc yc uv i by simp
  moreover from ge have "u * c i 0 v * d i 0"
  using True e_def i by simp
  ultimately have "u * c i = 0 v * d i = 0" by auto
  with True show ?thesis by auto
  next
  case False
  then have "(u * (c i)/(e i))*🪙R (s i)+(v * (d i)/(e i))*🪙R (t i) = q i"
  using q_def by auto
  then have "e i *🪙R ((u * (c i)/(e i))*🪙R (s i)+(v * (d i)/(e i))*🪙R (t i))
  = (e i) *🪙R (q i)" by auto
  with False show ?thesis by (simp add: algebra_simps)
  qed
  }
  then have *: "iI. (u * c i) *🪙R s i + (v * d i) *🪙R t i = e i *🪙R q i"
  by auto
  have "u *🪙R x + v *🪙R y = sum (λi. (u * c i) *🪙R s i + (v * d i) *🪙R t i) I"
  using xc yc by (simp add: algebra_simps scaleR_right.sum sum.distrib)
  also have " = sum (λi. e i *🪙R q i) I"
  using * by auto
  finally have "u *🪙R x + v *🪙R y = sum (λi. (e i) *🪙R (q i)) I"
  by auto
  then have "u *🪙R x + v *🪙R y ?rhs"
  using ge0 sum1 qs by auto
  }
  then have "convex ?rhs" unfolding convex_def by auto
  then show ?thesis
  using ?lhs 🪙 ?rhs * hull_minimal[of "(S ` I)" ?rhs convex]
  by blast
 qed
 
 lemma convex_hull_union_two:
  fixes S T :: "'m::euclidean_space set"
  assumes "convex S"
  and "S {}"
  and "convex T"
  and "T {}"
  shows "convex hull (S T) =
  {u *🪙R s + v *🪙R t | u v s t. u 0 v 0 u + v = 1 s S t T}"
  (is "?lhs = ?rhs")
 proof
  define I :: "nat set" where "I = {1, 2}"
  define s where "s i = (if i = (1::nat) then S else T)" for i
  have "(s ` I) = S T"
  using s_def I_def by auto
  then have "convex hull ((s ` I)) = convex hull (S T)"
  by auto
  moreover have "convex hull (s ` I) =
  { iI. c i *🪙R sa i | c sa. (iI. 0 c i) sum c I = 1 (iI. sa i s i)}"
  using assms s_def I_def
  by (subst convex_hull_finite_union) auto
  moreover have
  "{iI. c i *🪙R sa i | c sa. (iI. 0 c i) sum c I = 1 (iI. sa i s i)} ?rhs"
  using s_def I_def by auto
  ultimately show "?lhs ?rhs" by auto
  {
  fix x
  assume "x ?rhs"
  then obtain u v s t where *: "x = u *🪙R s + v *🪙R t u 0 v 0 u + v = 1 s S t T"
  by auto
  then have "x convex hull {s, t}"
  using convex_hull_2[of s t] by auto
  then have "x convex hull (S T)"
  using * hull_mono[of "{s, t}" "S T"] by auto
  }
  then show "?lhs 🪙 ?rhs" by blast
 qed
 
 proposition ray_to_rel_frontier:
  fixes a :: "'a::real_inner"
  assumes "bounded S"
  and a: "a rel_interior S"
  and aff: "(a + l) affine hull S"
  and "l 0"
  obtains d where "0 🚫" "(a + d *🪙R l) rel_frontier S"
  "e. [0 e; e 🚫] ==> (a + e *🪙R l) rel_interior S"
 proof -
  have aaff: "a affine hull S"
  by (meson a hull_subset rel_interior_subset rev_subsetD)
  let ?D = "{d. 0 🚫 a + d *🪙R l rel_interior S}"
  obtain B where "B > 0" and B: "S ball a B"
  using bounded_subset_ballD [OF bounded S] by blast
  have "a + (B / norm l) *🪙R l ball a B"
  by (simp add: dist_norm l 0)
  with B have "a + (B / norm l) *🪙R l rel_interior S"
  using rel_interior_subset subsetCE by blast
  with B > 0 l 0 have nonMT: "?D {}"
  using divide_pos_pos zero_less_norm_iff by fastforce
  have bdd: "bdd_below ?D"
  by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq)
  have relin_Ex: "x. x rel_interior S ==>
  e>0. x'affine hull S. dist x' x 🚫 x' rel_interior S"
  using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff)
  define d where "d = Inf ?D"
  obtain ε where "0 🚫ε" and ε: "🪙. [0 🪙; 🪙 🚫ε] ==> (a + 🪙 *🪙R l) rel_interior S"
  proof -
  obtain e where "e>0"
  and e: "x'. x' affine hull S ==> dist x' a 🚫 ==> x' rel_interior S"
  using relin_Ex a by blast
  show thesis
  proof (rule_tac ε = "e / norm l" in that)
  show "0 🚫 / norm l" by (simp add: 0 🚫 l 0)
  next
  show "a + 🪙 *🪙R l rel_interior S" if "0 🪙" "🪙 🚫 / norm l" for 🪙
  proof (rule e)
  show "a + 🪙 *🪙R l affine hull S"
  by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
  show "dist (a + 🪙 *🪙R l) a 🚫"
  using that by (simp add: l 0 dist_norm pos_less_divide_eq)
  qed
  qed
  qed
  have inint: "e. [0 e; e 🚫] ==> a + e *🪙R l rel_interior S"
  unfolding d_def using cInf_lower [OF _ bdd]
  by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left)
  have "ε d"
  unfolding d_def
  using ε dual_order.strict_implies_order le_less_linear
  by (blast intro: cInf_greatest [OF nonMT])
  with 0 🚫ε have "0 🚫" by simp
  have "a + d *🪙R l rel_interior S"
  proof
  assume adl: "a + d *🪙R l rel_interior S"
  obtain e where "e > 0"
  and e: "x'. x' affine hull S ==> dist x' (a + d *🪙R l) 🚫 ==> x' rel_interior S"
  using relin_Ex adl by blast
  have "d + e / norm l x"
  if "0 🚫" and nonrel: "a + x *🪙R l rel_interior S" for x
  proof (cases "x 🚫")
  case True with inint nonrel 0 🚫
  show ?thesis by auto
  next
  case False
  then have dle: "x 🚫 + e / norm l ==> dist (a + x *🪙R l) (a + d *🪙R l) ??"
  by (simp add: field_simps l 0)
  have ain: "a + x *🪙R l affine hull S"
  by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
  show ?thesis
  using e [OF ain] nonrel dle by force
  qed
  then
  have "d + e / norm l Inf {d. 0 🚫 a + d *🪙R l rel_interior S}"
  by (force simp add: intro: cInf_greatest [OF nonMT])
  then show False
  using 0 🚫 l 0 by (simp add: d_def [symmetric] field_simps)
  qed
  moreover
  have "yS. dist y (a + d *🪙R l) 🚫🪙" if "0 🚫🪙" for 🪙::real
  proof -
  have 1: "a + (d - min d (🪙 / 2 / norm l)) *🪙R l S"
  proof (rule subsetD [OF rel_interior_subset inint])
  show "d - min d (🪙 / 2 / norm l) 🚫"
  using l 0 0 🚫 0 🚫🪙 by auto
  qed auto
  have "norm l * min d (🪙 / (norm l * 2)) norm l * (🪙 / (norm l * 2))"
  by (metis min_def mult_left_mono norm_ge_zero order_refl)
  also have "... 🚫🪙"
  using l 0 0 🚫🪙 by (simp add: field_simps)
  finally have 2: "norm l * min d (🪙 / (norm l * 2)) 🚫🪙" .
  show ?thesis
  using 1 2 0 🚫 0 🚫🪙
  by (rule_tac x="a + (d - min d (🪙 / 2 / norm l)) *🪙R l" in bexI) (auto simp: algebra_simps)
  qed
  then have "a + d *🪙R l closure S"
  by (auto simp: closure_approachable)
  ultimately have infront: "a + d *🪙R l rel_frontier S"
  by (simp add: rel_frontier_def)
  show ?thesis
  by (rule that [OF 0 🚫 infront inint])
 qed
 
 corollary ray_to_frontier:
  fixes a :: "'a::euclidean_space"
  assumes "bounded S"
  and a: "a interior S"
  and "l 0"
  obtains d where "0 🚫" "(a + d *🪙R l) frontier S"
  "e. [0 e; e 🚫] ==> (a + e *🪙R l) interior S"
 proof -
  have 🍋: "interior S = rel_interior S"
  using a rel_interior_nonempty_interior by auto
  then have "a rel_interior S"
  using a by simp
  moreover have "a + l affine hull S"
  using a affine_hull_nonempty_interior by blast
  ultimately show thesis
  by (metis 🍋 bounded S l 0 frontier_def ray_to_rel_frontier rel_frontier_def that)
 qed
 
 
 lemma segment_to_rel_frontier_aux:
  fixes x :: "'a::euclidean_space"
  assumes "convex S" "bounded S" and x: "x rel_interior S" and y: "y S" and xy: "x y"
  obtains z where "z rel_frontier S" "y closed_segment x z"
  "open_segment x z rel_interior S"
 proof -
  have "x + (y - x) affine hull S"
  using hull_inc [OF y] by auto
  then obtain d where "0 🚫" and df: "(x + d *🪙R (y-x)) rel_frontier S"
  and di: "e. [0 e; e 🚫] ==> (x + e *🪙R (y-x)) rel_interior S"
  by (rule ray_to_rel_frontier [OF bounded S x]) (use xy in auto)
  show ?thesis
  proof
  show "x + d *🪙R (y - x) rel_frontier S"
  by (simp add: df)
  next
  have "open_segment x y rel_interior S"
  using rel_interior_closure_convex_segment [OF convex S x] closure_subset y by blast
  moreover have "x + d *🪙R (y - x) open_segment x y" if "d 🚫"
  using xy 0 🚫 that by (force simp: in_segment algebra_simps)
  ultimately have "1 d"
  using df rel_frontier_def by fastforce
  moreover have "x = (1 / d) *🪙R x + ((d - 1) / d) *🪙R x"
  by (metis 0 🚫 add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one)
  ultimately show "y closed_segment x (x + d *🪙R (y - x))"
  unfolding in_segment
  by (rule_tac x="1/d" in exI) (auto simp: algebra_simps)
  next
  show "open_segment x (x + d *🪙R (y - x)) rel_interior S"
  proof (rule rel_interior_closure_convex_segment [OF convex S x])
  show "x + d *🪙R (y - x) closure S"
  using df rel_frontier_def by auto
  qed
  qed
 qed
 
 lemma segment_to_rel_frontier:
  fixes x :: "'a::euclidean_space"
  assumes S: "convex S" "bounded S" and x: "x rel_interior S"
  and y: "y S" and xy: "¬(x = y S = {x})"
  obtains z where "z rel_frontier S" "y closed_segment x z"
  "open_segment x z rel_interior S"
 proof (cases "x=y")
  case True
  with xy have "S {x}"
  by blast
  with True show ?thesis
  by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y)
 next
  case False
  then show ?thesis
  using segment_to_rel_frontier_aux [OF S x y] that by blast
 qed
 
 proposition rel_frontier_not_sing:
  fixes a :: "'a::euclidean_space"
  assumes "bounded S"
  shows "rel_frontier S {a}"
 proof (cases "S = {}")
  case True then show ?thesis by simp
 next
  case False
  then obtain z where "z S"
  by blast
  then show ?thesis
  proof (cases "S = {z}")
  case True then show ?thesis by simp
  next
  case False
  then obtain w where "w S" "w z"
  using z S by blast
  show ?thesis
  proof
  assume "rel_frontier S = {a}"
  then consider "w rel_frontier S" | "z rel_frontier S"
  using w z by auto
  then show False
  proof cases
  case 1
  then have w: "w rel_interior S"
  using w S closure_subset rel_frontier_def by fastforce
  have "w + (w - z) affine hull S"
  by (metis w S z S affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
  then obtain e where "0 🚫" "(w + e *🪙R (w - z)) rel_frontier S"
  using w z z S by (metis assms ray_to_rel_frontier right_minus_eq w)
  moreover obtain d where "0 🚫" "(w + d *🪙R (z - w)) rel_frontier S"
  using ray_to_rel_frontier [OF bounded S w, of "1 *🪙R (z - w)"] w z z S
  by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
  ultimately have "d *🪙R (z - w) = e *🪙R (w - z)"
  using rel_frontier S = {a} by force
  moreover have "e -d "
  using 0 🚫 0 🚫 by force
  ultimately show False
  by (metis (no_types, lifting) w z eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
  next
  case 2
  then have z: "z rel_interior S"
  using z S closure_subset rel_frontier_def by fastforce
  have "z + (z - w) affine hull S"
  by (metis z S w S affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
  then obtain e where "0 🚫" "(z + e *🪙R (z - w)) rel_frontier S"
  using w z w S by (metis assms ray_to_rel_frontier right_minus_eq z)
  moreover obtain d where "0 🚫" "(z + d *🪙R (w - z)) rel_frontier S"
  using ray_to_rel_frontier [OF bounded S z, of "1 *🪙R (w - z)"] w z w S
  by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
  ultimately have "d *🪙R (w - z) = e *🪙R (z - w)"
  using rel_frontier S = {a} by force
  moreover have "e -d "
  using 0 🚫 0 🚫 by force
  ultimately show False
  by (metis (no_types, lifting) w z eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
  qed
  qed
  qed
 qed
 
 
 subsection🍋tag unimportant Convexity on direct sums
 
 lemma closure_sum:
  fixes S T :: "'a::real_normed_vector set"
  shows "closure S + closure T closure (S + T)"
  unfolding set_plus_image closure_Times [symmetric] split_def
  by (intro closure_bounded_linear_image_subset bounded_linear_add
  bounded_linear_fst bounded_linear_snd)
 
 lemma fst_snd_linear: "linear (λ(x,y). x + y)"
  unfolding linear_iff by (simp add: algebra_simps)
 
 lemma rel_interior_sum:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
  and "convex T"
  shows "rel_interior (S + T) = rel_interior S + rel_interior T"
 proof -
  have "rel_interior S + rel_interior T = (λ(x,y). x + y) ` (rel_interior S × rel_interior T)"
  by (simp add: set_plus_image)
  also have " = (λ(x,y). x + y) ` rel_interior (S × T)"
  using rel_interior_Times assms by auto
  also have " = rel_interior (S + T)"
  using fst_snd_linear convex_Times assms
  rel_interior_convex_linear_image[of "(λ(x,y). x + y)" "S × T"]
  by (auto simp add: set_plus_image)
  finally show ?thesis ..
 qed
 
 lemma rel_interior_sum_gen:
  fixes S :: "'a ==> 'n::euclidean_space set"
  assumes "i. iI ==> convex (S i)"
  shows "rel_interior (sum S I) = sum (λi. rel_interior (S i)) I"
  using rel_interior_sum rel_interior_sing[of "0"] assms
  by (subst sum_set_cond_linear[of convex], auto simp add: convex_set_plus)
 
 lemma convex_rel_open_direct_sum:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
  and "rel_open S"
  and "convex T"
  and "rel_open T"
  shows "convex (S × T) rel_open (S × T)"
  by (metis assms convex_Times rel_interior_Times rel_open_def)
 
 lemma convex_rel_open_sum:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
  and "rel_open S"
  and "convex T"
  and "rel_open T"
  shows "convex (S + T) rel_open (S + T)"
  by (metis assms convex_set_plus rel_interior_sum rel_open_def)
 
 lemma convex_hull_finite_union_cones:
  assumes "finite I"
  and "I {}"
  assumes "i. iI ==> convex (S i) cone (S i) S i {}"
  shows "convex hull ((S ` I)) = sum S I"
  (is "?lhs = ?rhs")
 proof -
  {
  fix x
  assume "x ?lhs"
  then obtain c xs where
  x: "x = sum (λi. c i *🪙R xs i) I (iI. c i 0) sum c I = 1 (iI. xs i S i)"
  using convex_hull_finite_union[of I S] assms by auto
  define s where "s i = c i *🪙R xs i" for i
  have "iI. s i S i"
  using s_def x assms by (simp add: mem_cone)
  moreover have "x = sum s I" using x s_def by auto
  ultimately have "x ?rhs"
  using set_sum_alt[of I S] assms by auto
  }
  moreover
  {
  fix x
  assume "x ?rhs"
  then obtain s where x: "x = sum s I (iI. s i S i)"
  using set_sum_alt[of I S] assms by auto
  define xs where "xs i = of_nat(card I) *🪙R s i" for i
  then have "x = sum (λi. ((1 :: real) / of_nat(card I)) *🪙R xs i) I"
  using x assms by auto
  moreover have "iI. xs i S i"
  using x xs_def assms by (simp add: cone_def)
  moreover have "iI. (1 :: real) / of_nat (card I) 0"
  by auto
  moreover have "sum (λi. (1 :: real) / of_nat (card I)) I = 1"
  using assms by auto
  ultimately have "x ?lhs"
  using assms
  apply (simp add: convex_hull_finite_union[of I S])
  by (rule_tac x = "(λi. 1 / (card I))" in exI) auto
  }
  ultimately show ?thesis by auto
 qed
 
 lemma convex_hull_union_cones_two:
  fixes S T :: "'m::euclidean_space set"
  assumes "convex S"
  and "cone S"
  and "S {}"
  assumes "convex T"
  and "cone T"
  and "T {}"
  shows "convex hull (S T) = S + T"
 proof -
  define I :: "nat set" where "I = {1, 2}"
  define A where "A i = (if i = (1::nat) then S else T)" for i
  have "(A ` I) = S T"
  using A_def I_def by auto
  then have "convex hull ((A ` I)) = convex hull (S T)"
  by auto
  moreover have "convex hull (A ` I) = sum A I"
  using A_def I_def
  by (metis assms convex_hull_finite_union_cones empty_iff finite.emptyI finite.insertI insertI1)
  moreover have "sum A I = S + T"
  using A_def I_def by (force simp add: set_plus_def)
  ultimately show ?thesis by auto
 qed
 
 lemma rel_interior_convex_hull_union:
  fixes S :: "'a ==> 'n::euclidean_space set"
  assumes "finite I"
  and "iI. convex (S i) S i {}"
  shows "rel_interior (convex hull ((S ` I))) =
  {sum (λi. c i *🪙R s i) I | c s. (iI. c i > 0) sum c I = 1
  (iI. s i rel_interior(S i))}"
  (is "?lhs = ?rhs")
 proof (cases "I = {}")
  case True
  then show ?thesis
  using convex_hull_empty by auto
 next
  case False
  define C0 where "C0 = convex hull ((S ` I))"
  have "iI. C0 S i"
  unfolding C0_def using hull_subset[of "(S ` I)"] by auto
  define K0 where "K0 = cone hull ({1 :: real} × C0)"
  define K where "K i = cone hull ({1 :: real} × S i)" for i
  have "iI. K i {}"
  unfolding K_def using assms
  by (simp add: cone_hull_empty_iff[symmetric])
  have convK: "iI. convex (K i)"
  unfolding K_def
  by (simp add: assms(2) convex_Times convex_cone_hull)
  have "K0 🪙 K i" if "i I" for i
  unfolding K0_def K_def
  by (simp add: Sigma_mono iI. S i C0 hull_mono that)
  then have "K0 🪙 (K ` I)" by auto
  moreover have "convex K0"
  unfolding K0_def by (simp add: C0_def convex_Times convex_cone_hull)
  ultimately have geq: "K0 🪙 convex hull ((K ` I))"
  using hull_minimal[of _ "K0" "convex"] by blast
  have "iI. K i 🪙 {1 :: real} × S i"
  using K_def by (simp add: hull_subset)
  then have "(K ` I) 🪙 {1 :: real} × (S ` I)"
  by auto
  then have "convex hull (K ` I) 🪙 convex hull ({1 :: real} × (S ` I))"
  by (simp add: hull_mono)
  then have "convex hull (K ` I) 🪙 {1 :: real} × C0"
  unfolding C0_def
  using convex_hull_Times[of "{(1 :: real)}" "(S ` I)"] convex_hull_singleton
  by auto
  moreover have "cone (convex hull ((K ` I)))"
  by (simp add: K_def cone_Union cone_cone_hull cone_convex_hull)
  ultimately have "convex hull ((K ` I)) 🪙 K0"
  unfolding K0_def
  using hull_minimal[of _ "convex hull ((K ` I))" "cone"]
  by blast
  then have "K0 = convex hull ((K ` I))"
  using geq by auto
  also have " = sum K I"
  using assms False iI. K i {} cone_hull_eq convK
  by (intro convex_hull_finite_union_cones; fastforce simp: K_def)
  finally have "K0 = sum K I" by auto
  then have *: "rel_interior K0 = sum (λi. (rel_interior (K i))) I"
  using rel_interior_sum_gen[of I K] convK by auto
  {
  fix x
  assume "x ?lhs"
  then have "(1::real, x) rel_interior K0"
  using K0_def C0_def rel_interior_convex_cone_aux[of C0 "1::real" x] convex_convex_hull
  by auto
  then obtain k where k: "(1::real, x) = sum k I (iI. k i rel_interior (K i))"
  using finite I * set_sum_alt[of I "λi. rel_interior (K i)"] by auto
  {
  fix i
  assume "i I"
  then have "convex (S i) k i rel_interior (cone hull {1} × S i)"
  using k K_def assms by auto
  then have "ci si. k i = (ci, ci *🪙R si) 0 🚫 si rel_interior (S i)"
  using rel_interior_convex_cone[of "S i"] by auto
  }
  then obtain c s where cs: "iI. k i = (c i, c i *🪙R s i) 0 🚫 i s i rel_interior (S i)"
  by metis
  then have "x = (iI. c i *🪙R s i) sum c I = 1"
  using k by (simp add: sum_prod)
  then have "x ?rhs"
  using k cs by auto
  }
  moreover
  {
  fix x
  assume "x ?rhs"
  then obtain c s where cs: "x = sum (λi. c i *🪙R s i) I
  (iI. c i > 0) sum c I = 1 (iI. s i rel_interior (S i))"
  by auto
  define k where "k i = (c i, c i *🪙R s i)" for i
  {
  fix i assume "i I"
  then have "k i rel_interior (K i)"
  using k_def K_def assms cs rel_interior_convex_cone[of "S i"]
  by auto
  }
  then have "(1, x) rel_interior K0"
  using * set_sum_alt[of I "(λi. rel_interior (K i))"] assms cs
  by (simp add: k_def) (metis (mono_tags, lifting) sum_prod)
  then have "x ?lhs"
  using K0_def C0_def rel_interior_convex_cone_aux[of C0 1 x]
  by auto
  }
  ultimately show ?thesis by blast
 qed
 
 
 lemma convex_le_Inf_differential:
  fixes f :: "real ==> real"
  assumes "convex_on I f"
  and "x interior I"
  and "y I"
  shows "f y f x + Inf ((λt. (f x - f t) / (x - t)) ` ({x🚫} I)) * (y - x)"
  (is "_ _ + Inf (?F x) * (y - x)")
 proof (cases rule: linorder_cases)
  assume "x 🚫"
  moreover
  have "open (interior I)" by auto
  from openE[OF this x interior I]
  obtain e where e: "0 🚫" "ball x e interior I" .
  moreover define t where "t = min (x + e / 2) ((x + y) / 2)"
  ultimately have "x 🚫" "t 🚫" "t ball x e"
  by (auto simp: dist_real_def field_simps split: split_min)
  with x interior I e interior_subset[of I] have "t I" "x I" by auto
 
  define K where "K = x - e / 2"
  with 0 🚫 have "K ball x e" "K 🚫"
  by (auto simp: dist_real_def)
  then have "K I"
  using interior I I e(2) by blast
 
  have "Inf (?F x) (f x - f y) / (x - y)"
  proof (intro bdd_belowI cInf_lower2)
  show "(f x - f t) / (x - t) ?F x"
  using t I x 🚫 by auto
  show "(f x - f t) / (x - t) (f x - f y) / (x - y)"
  using convex_on I f x I y I x 🚫 t 🚫
  by (rule convex_on_slope_le)
  next
  fix y
  assume "y ?F x"
  with order_trans[OF convex_on_slope_le[OF convex_on I f K I _ K 🚫 _]]
  show "(f K - f x) / (K - x) y" by auto
  qed
  then show ?thesis
  using x 🚫 by (simp add: field_simps)
 next
  assume "y 🚫"
  moreover
  have "open (interior I)" by auto
  from openE[OF this x interior I]
  obtain e where e: "0 🚫" "ball x e interior I" .
  moreover define t where "t = x + e / 2"
  ultimately have "x 🚫" "t ball x e"
  by (auto simp: dist_real_def field_simps)
  with x interior I e interior_subset[of I] have "t I" "x I" by auto
 
  have "(f x - f y) / (x - y) Inf (?F x)"
  proof (rule cInf_greatest)
  have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
  using y 🚫 by (auto simp: field_simps)
  also
  fix z
  assume "z ?F x"
  with order_trans[OF convex_on_slope_le[OF convex_on I f y I _ y 🚫]]
  have "(f y - f x) / (y - x) z"
  by auto
  finally show "(f x - f y) / (x - y) z" .
  next
  have "x + e / 2 ball x e"
  using e by (auto simp: dist_real_def)
  with e interior_subset[of I] have "x + e / 2 {x🚫} I"
  by auto
  then show "?F x {}"
  by blast
  qed
  then show ?thesis
  using y 🚫 by (simp add: field_simps)
 qed simp
 
 subsection🍋tag unimportant\Explicit formulas for interior and relative interior of convex hull
 
 lemma at_within_cbox_finite:
  assumes "x box a b" "x S" "finite S"
  shows "(at x within cbox a b - S) = at x"
 proof -
  have "interior (cbox a b - S) = box a b - S"
  using finite S by (simp add: interior_diff finite_imp_closed)
  then show ?thesis
  using at_within_interior assms by fastforce
 qed
 
 lemma affine_independent_convex_affine_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S" "T S"
  shows "convex hull T = affine hull T convex hull S"
 proof -
  have fin: "finite S" "finite T" using assms aff_independent_finite finite_subset by auto
  have "convex hull T affine hull T"
  using convex_hull_subset_affine_hull by blast
  moreover have "convex hull T convex hull S"
  using assms hull_mono by blast
  moreover have "affine hull T convex hull S convex hull T"
  proof -
  have 0: "u. sum u S = 0 ==> (vS. u v = 0) (vS. u v *🪙R v) 0"
  using affine_dependent_explicit_finite assms(1) fin(1) by auto
  show ?thesis
  proof (clarsimp simp add: affine_hull_finite fin)
  fix u
  assume S: "(vT. u v *🪙R v) convex hull S"
  and T1: "sum u T = 1"
  then obtain v where v: "xS. 0 v x" "sum v S = 1" "(xS. v x *🪙R x) = (vT. u v *🪙R v)"
  by (auto simp add: convex_hull_finite fin)
  { fix x
  assume"x T"
  then have S: "S = (S - T) T" 🍋 split into separate cases
  using assms by auto
  have [simp]: "(xT. v x *🪙R x) + (xS - T. v x *🪙R x) = (xT. u x *🪙R x)"
  "sum v T + sum v (S - T) = 1"
  using v fin S
  by (auto simp: sum.union_disjoint [symmetric] Un_commute)
  have "(xS. if x T then v x - u x else v x) = 0"
  "(xS. (if x T then v x - u x else v x) *🪙R x) = 0"
  using v fin T1
  by (subst S, subst sum.union_disjoint, auto simp: algebra_simps sum_subtractf)+
  } note [simp] = this
  have "(xT. 0 u x)"
  using 0 [of "λx. if x T then v x - u x else v x"] T S v(1) by fastforce
  then show "(vT. u v *🪙R v) convex hull T"
  using 0 [of "λx. if x T then v x - u x else v x"] T S T1
  by (fastforce simp add: convex_hull_finite fin)
  qed
  qed
  ultimately show ?thesis
  by blast
 qed
 
 lemma affine_independent_span_eq:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S" "card S = Suc (DIM ('a))"
  shows "affine hull S = UNIV"
 proof (cases "S = {}")
  case True then show ?thesis
  using assms by simp
 next
  case False
  then obtain a T where T: "a T" "S = insert a T"
  by blast
  then have fin: "finite T" using assms
  by (metis finite_insert aff_independent_finite)
  have "UNIV (+) a ` span ((λx. x - a) ` T)"
  proof (intro card_ge_dim_independent Fun.vimage_subsetD)
  show "independent ((λx. x - a) ` T)"
  using T affine_dependent_iff_dependent assms(1) by auto
  show "dim ((+) a -` UNIV) card ((λx. x - a) ` T)"
  using assms T fin by (auto simp: card_image inj_on_def)
  qed (use surj_plus in auto)
  then show ?thesis
  using T(2) affine_hull_insert_span_gen equalityI by fastforce
 qed
 
 lemma affine_independent_span_gt:
  fixes S :: "'a::euclidean_space set"
  assumes ind: "¬ affine_dependent S" and dim: "DIM ('a) 🚫 S"
  shows "affine hull S = UNIV"
 proof (intro affine_independent_span_eq [OF ind] antisym)
  show "card S Suc DIM('a)"
  using aff_independent_finite affine_dependent_biggerset ind by fastforce
  show "Suc DIM('a) card S"
  using Suc_leI dim by blast
 qed
 
 lemma empty_interior_affine_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "finite S" and dim: "card S DIM ('a)"
  shows "interior(affine hull S) = {}"
  using assms
 proof (induct S rule: finite_induct)
  case (insert x S)
  then have "dim (span ((λy. y - x) ` S)) 🚫('a)"
  by (auto simp: Suc_le_lessD card_image_le dual_order.trans intro!: dim_le_card'[THEN le_less_trans])
  then show ?case
  by (simp add: empty_interior_lowdim affine_hull_insert_span_gen interior_translation)
 qed auto
 
 lemma empty_interior_convex_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "finite S" and dim: "card S DIM ('a)"
  shows "interior(convex hull S) = {}"
  by (metis Diff_empty Diff_eq_empty_iff convex_hull_subset_affine_hull
  interior_mono empty_interior_affine_hull [OF assms])
 
 lemma explicit_subset_rel_interior_convex_hull:
  fixes S :: "'a::euclidean_space set"
  shows "finite S
  ==> {y. u. (x S. 0 🚫 x u x 🚫) sum u S = 1 sum (λx. u x *🪙R x) S = y}
  rel_interior (convex hull S)"
  by (force simp add: rel_interior_convex_hull_union [where S="λx. {x}" and I=S, simplified])
 
 lemma explicit_subset_rel_interior_convex_hull_minimal:
  fixes S :: "'a::euclidean_space set"
  shows "finite S
  ==> {y. u. (x S. 0 🚫 x) sum u S = 1 sum (λx. u x *🪙R x) S = y}
  rel_interior (convex hull S)"
  by (force simp add: rel_interior_convex_hull_union [where S="λx. {x}" and I=S, simplified])
 
 lemma rel_interior_convex_hull_explicit:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S"
  shows "rel_interior(convex hull S) =
  {y. u. (x S. 0 🚫 x) sum u S = 1 sum (λx. u x *🪙R x) S = y}"
  (is "?lhs = ?rhs")
 proof
  show "?rhs ?lhs"
  by (simp add: aff_independent_finite explicit_subset_rel_interior_convex_hull_minimal assms)
 next
  show "?lhs ?rhs"
  proof (cases "a. S = {a}")
  case True then show "?lhs ?rhs"
  by force
  next
  case False
  have fs: "finite S"
  using assms by (simp add: aff_independent_finite)
  { fix a b and d::real
  assume ab: "a S" "b S" "a b"
  then have S: "S = (S - {a,b}) {a,b}" 🍋 split into separate cases
  by auto
  have "(xS. if x = a then - d else if x = b then d else 0) = 0"
  "(xS. (if x = a then - d else if x = b then d else 0) *🪙R x) = d *🪙R b - d *🪙R a"
  using ab fs
  by (subst S, subst sum.union_disjoint, auto)+
  } note [simp] = this
  { fix y
  assume y: "y convex hull S" "y ?rhs"
  have *: False if
  ua: "xS. 0 u x" "sum u S = 1" "¬ 0 🚫 a" "a S"
  and yT: "y = (xS. u x *🪙R x)" "y T" "open T"
  and sb: "T affine hull S {w. u. (xS. 0 u x) sum u S = 1 (xS. u x *🪙R x) = w}"
  for u T a
  proof -
  have ua0: "u a = 0"
  using ua by auto
  obtain b where b: "bS" "a b"
  using ua False by auto
  obtain e where e: "0 🚫" "ball (xS. u x *🪙R x) e T"
  using yT by (auto elim: openE)
  with b obtain d where d: "0 🚫" "norm(d *🪙R (a-b)) 🚫"
  by (auto intro: that [of "e / 2 / norm(a-b)"])
  have "(xS. u x *🪙R x) affine hull S"
  using yT y by (metis affine_hull_convex_hull hull_redundant_eq)
  then have "(xS. u x *🪙R x) - d *🪙R (a - b) affine hull S"
  using ua b by (auto simp: hull_inc intro: mem_affine_3_minus2)
  then have "y - d *🪙R (a - b) T affine hull S"
  using d e yT by auto
  then obtain v where v: "xS. 0 v x"
  "sum v S = 1"
  "(xS. v x *🪙R x) = (xS. u x *🪙R x) - d *🪙R (a - b)"
  using subsetD [OF sb] yT
  by auto
  have aff: "u. sum u S = 0 ==> (vS. u v = 0) (vS. u v *🪙R v) 0"
  using assms by (simp add: affine_dependent_explicit_finite fs)
  show False
  using ua b d v aff [of "λx. (v x - u x) - (if x = a then -d else if x = b then d else 0)"]
  by (auto simp: algebra_simps sum_subtractf sum.distrib)
  qed
  have "y rel_interior (convex hull S)"
  using y convex_hull_finite [OF fs] *
  apply simp
  by (metis (no_types, lifting) IntD1 affine_hull_convex_hull mem_rel_interior)
  } with rel_interior_subset show "?lhs ?rhs"
  by blast
  qed
 qed
 
 lemma interior_convex_hull_explicit_minimal:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S"
  shows
  "interior(convex hull S) =
  (if card(S) DIM('a) then {}
  else {y. u. (x S. 0 🚫 x) sum u S = 1 (xS. u x *🪙R x) = y})"
  (is "_ = (if _ then _ else ?rhs)")
 proof -
  { assume S: "¬ card S DIM('a)"
  have "interior (convex hull S) = rel_interior(convex hull S)"
  using assms S by (simp add: affine_independent_span_gt rel_interior_interior)
  then have "interior(convex hull S) = ?rhs"
  by (simp add: assms S rel_interior_convex_hull_explicit)
  }
  then show ?thesis
  by (auto simp: aff_independent_finite empty_interior_convex_hull assms)
 qed
 
 lemma interior_convex_hull_explicit:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S"
  shows
  "interior(convex hull S) =
  (if card(S) DIM('a) then {}
  else {y. u. (x S. 0 🚫 x u x 🚫) sum u S = 1 (xS. u x *🪙R x) = y})"
 proof -
  { fix u :: "'a ==> real" and a
  assume "card Basis 🚫 S" and u: "x. xS ==> 0 🚫 x" "sum u S = 1" and a: "a S"
  then have cs: "Suc 0 🚫 S"
  by (metis DIM_positive less_trans_Suc)
  obtain b where b: "b S" "a b"
  proof (cases "S {a}")
  case True
  then show thesis
  using cs subset_singletonD by fastforce
  qed blast
  have "u a + u b sum u {a,b}"
  using a b by simp
  also have "... sum u S"
  using a b u
  by (intro Groups_Big.sum_mono2) (auto simp: less_imp_le aff_independent_finite assms)
  finally have "u a 🚫"
  using b S u by fastforce
  } note [simp] = this
  show ?thesis
  using assms by (force simp add: not_le interior_convex_hull_explicit_minimal)
 qed
 
 lemma interior_closed_segment_ge2:
  fixes a :: "'a::euclidean_space"
  assumes "2 DIM('a)"
  shows "interior(closed_segment a b) = {}"
 using assms unfolding segment_convex_hull
 proof -
  have "card {a, b} DIM('a)"
  using assms
  by (simp add: card_insert_if linear not_less_eq_eq numeral_2_eq_2)
  then show "interior (convex hull {a, b}) = {}"
  by (metis empty_interior_convex_hull finite.insertI finite.emptyI)
 qed
 
 lemma interior_open_segment:
  fixes a :: "'a::euclidean_space"
  shows "interior(open_segment a b) =
  (if 2 DIM('a) then {} else open_segment a b)"
 proof (cases "2 DIM('a)")
  case True
  then have "interior (open_segment a b) = {}"
  using interior_closed_segment_ge2 interior_mono segment_open_subset_closed by blast
  with True show ?thesis
  by auto
 next
  case ge2: False
  have "interior (open_segment a b) = open_segment a b"
  proof (cases "a = b")
  case True then show ?thesis by auto
  next
  case False
  with ge2 have "affine hull (open_segment a b) = UNIV"
  by (simp add: False affine_independent_span_gt)
  then show "interior (open_segment a b) = open_segment a b"
  using rel_interior_interior rel_interior_open_segment by blast
  qed
  with ge2 show ?thesis
  by auto
 qed
 
 lemma interior_closed_segment:
  fixes a :: "'a::euclidean_space"
  shows "interior(closed_segment a b) =
  (if 2 DIM('a) then {} else open_segment a b)"
 proof (cases "a = b")
  case True then show ?thesis by simp
 next
  case False
  then have "closure (open_segment a b) = closed_segment a b"
  by simp
  then show ?thesis
  by (metis (no_types) convex_interior_closure convex_open_segment interior_open_segment)
 qed
 
 lemmas interior_segment = interior_closed_segment interior_open_segment
 
 lemma closed_segment_eq [simp]:
  fixes a :: "'a::euclidean_space"
  shows "closed_segment a b = closed_segment c d {a,b} = {c,d}"
 proof
  assume abcd: "closed_segment a b = closed_segment c d"
  show "{a,b} = {c,d}"
  proof (cases "a=b c=d")
  case True with abcd show ?thesis by force
  next
  case False
  then have neq: "a b c d" by force
  have *: "closed_segment c d - {a, b} = rel_interior (closed_segment c d)"
  using neq abcd by (metis (no_types) open_segment_def rel_interior_closed_segment)
  have "b {c, d}"
  proof -
  have "insert b (closed_segment c d) = closed_segment c d"
  using abcd by blast
  then show ?thesis
  by (metis DiffD2 Diff_insert2 False * insertI1 insert_Diff_if open_segment_def rel_interior_closed_segment)
  qed
  moreover have "a {c, d}"
  by (metis Diff_iff False * abcd ends_in_segment(1) insertI1 open_segment_def rel_interior_closed_segment)
  ultimately show "{a, b} = {c, d}"
  using neq by fastforce
  qed
 next
  assume "{a,b} = {c,d}"
  then show "closed_segment a b = closed_segment c d"
  by (simp add: segment_convex_hull)
 qed
 
 lemma closed_open_segment_eq [simp]:
  fixes a :: "'a::euclidean_space"
  shows "closed_segment a b open_segment c d"
 by (metis DiffE closed_segment_neq_empty closure_closed_segment closure_open_segment ends_in_segment(1) insertI1 open_segment_def)
 
 lemma open_closed_segment_eq [simp]:
  fixes a :: "'a::euclidean_space"
  shows "open_segment a b closed_segment c d"
 using closed_open_segment_eq by blast
 
 lemma open_segment_eq [simp]:
  fixes a :: "'a::euclidean_space"
  shows "open_segment a b = open_segment c d a = b c = d {a,b} = {c,d}"
  (is "?lhs = ?rhs")
 proof
  assume abcd: ?lhs
  show ?rhs
  proof (cases "a=b c=d")
  case True with abcd show ?thesis
  using finite_open_segment by fastforce
  next
  case False
  then have a2: "a b c d" by force
  with abcd show ?rhs
  unfolding open_segment_def
  by (metis (no_types) abcd closed_segment_eq closure_open_segment)
  qed
 next
  assume ?rhs
  then show ?lhs
  by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
 qed
 
 subsection🍋tag unimportant\Similar results for closure and (relative or absolute) frontier
 
 lemma closure_convex_hull [simp]:
  fixes S :: "'a::euclidean_space set"
  shows "compact S ==> closure(convex hull S) = convex hull S"
  by (simp add: compact_imp_closed compact_convex_hull)
 
 lemma rel_frontier_convex_hull_explicit:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S"
  shows "rel_frontier(convex hull S) =
  {y. u. (x S. 0 u x) (x S. u x = 0) sum u S = 1 sum (λx. u x *🪙R x) S = y}"
 proof -
  have fs: "finite S"
  using assms by (simp add: aff_independent_finite)
  have "u y v.
  [y S; u y = 0; sum u S = 1; xS. 0 🚫 x;
  sum v S = 1; (xS. v x *🪙R x) = (xS. u x *🪙R x)]
  ==> u. sum u S = 0 (vS. u v 0) (vS. u v *🪙R v) = 0"
  apply (rule_tac x = "λx. u x - v x" in exI)
  apply (force simp: sum_subtractf scaleR_diff_left)
  done
  then show ?thesis
  using fs assms
  apply (simp add: rel_frontier_def finite_imp_compact rel_interior_convex_hull_explicit)
  apply (auto simp: convex_hull_finite)
  apply (metis less_eq_real_def)
  by (simp add: affine_dependent_explicit_finite)
 qed
 
 lemma frontier_convex_hull_explicit:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S"
  shows "frontier(convex hull S) =
  {y. u. (x S. 0 u x) (DIM ('a) 🚫 S (x S. u x = 0))
  sum u S = 1 sum (λx. u x *🪙R x) S = y}"
 proof -
  have fs: "finite S"
  using assms by (simp add: aff_independent_finite)
  show ?thesis
  proof (cases "DIM ('a) 🚫 S")
  case True
  with assms fs show ?thesis
  by (simp add: rel_frontier_def frontier_def rel_frontier_convex_hull_explicit [symmetric]
  interior_convex_hull_explicit_minimal rel_interior_convex_hull_explicit)
  next
  case False
  then have "card S DIM ('a)"
  by linarith
  then show ?thesis
  using assms fs
  apply (simp add: frontier_def interior_convex_hull_explicit finite_imp_compact)
  apply (simp add: convex_hull_finite)
  done
  qed
 qed
 
 lemma rel_frontier_convex_hull_cases:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S"
  shows "rel_frontier(convex hull S) = {convex hull (S - {x}) |x. x S}"
 proof -
  have fs: "finite S"
  using assms by (simp add: aff_independent_finite)
  { fix u a
  have "xS. 0 u x ==> a S ==> u a = 0 ==> sum u S = 1 ==>
  x v. x S
  (xS - {x}. 0 v x)
  sum v (S - {x}) = 1 (xS - {x}. v x *🪙R x) = (xS. u x *🪙R x)"
  apply (rule_tac x=a in exI)
  apply (rule_tac x=u in exI)
  apply (simp add: Groups_Big.sum_diff1 fs)
  done }
  moreover
  { fix a u
  have "a S ==> xS - {a}. 0 u x ==> sum u (S - {a}) = 1 ==>
  v. (xS. 0 v x)
  (xS. v x = 0) sum v S = 1 (xS. v x *🪙R x) = (xS - {a}. u x *🪙R x)"
  apply (rule_tac x="λx. if x = a then 0 else u x" in exI)
  apply (auto simp: sum.If_cases Diff_eq if_smult fs)
  done }
  ultimately show ?thesis
  using assms
  apply (simp add: rel_frontier_convex_hull_explicit)
  apply (auto simp add: convex_hull_finite fs Union_SetCompr_eq)
  done
 qed
 
 lemma frontier_convex_hull_eq_rel_frontier:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S"
  shows "frontier(convex hull S) =
  (if card S DIM ('a) then convex hull S else rel_frontier(convex hull S))"
  using assms
  unfolding rel_frontier_def frontier_def
  by (simp add: affine_independent_span_gt rel_interior_interior
  finite_imp_compact empty_interior_convex_hull aff_independent_finite)
 
 lemma frontier_convex_hull_cases:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S"
  shows "frontier(convex hull S) =
  (if card S DIM ('a) then convex hull S else {convex hull (S - {x}) |x. x S})"
 by (simp add: assms frontier_convex_hull_eq_rel_frontier rel_frontier_convex_hull_cases)
 
 lemma in_frontier_convex_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "finite S" "card S Suc (DIM ('a))" "x S"
  shows "x frontier(convex hull S)"
 proof (cases "affine_dependent S")
  case True
  with assms obtain y where "y S" and y: "y affine hull (S - {y})"
  by (auto simp: affine_dependent_def)
  moreover have "x closure (convex hull S)"
  by (meson closure_subset hull_inc subset_eq x S)
  moreover have "x interior (convex hull S)"
  using assms
  by (metis Suc_mono affine_hull_convex_hull affine_hull_nonempty_interior y S y card.remove empty_iff empty_interior_affine_hull finite_Diff hull_redundant insert_Diff interior_UNIV not_less)
  ultimately show ?thesis
  unfolding frontier_def by blast
 next
  case False
  { assume "card S = Suc (card Basis)"
  then have cs: "Suc 0 🚫 S"
  by (simp)
  with subset_singletonD have "y S. y x"
  by (cases "S {x}") fastforce+
  } note [dest!] = this
  show ?thesis using assms
  unfolding frontier_convex_hull_cases [OF False] Union_SetCompr_eq
  by (auto simp: le_Suc_eq hull_inc)
 qed
 
 lemma not_in_interior_convex_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "finite S" "card S Suc (DIM ('a))" "x S"
  shows "x interior(convex hull S)"
 using in_frontier_convex_hull [OF assms]
 by (metis Diff_iff frontier_def)
 
 lemma interior_convex_hull_eq_empty:
  fixes S :: "'a::euclidean_space set"
  assumes "card S = Suc (DIM ('a))"
  shows "interior(convex hull S) = {} affine_dependent S"
 proof
  show "affine_dependent S ==> interior (convex hull S) = {}"
  proof (clarsimp simp: affine_dependent_def)
  fix a b
  assume "b S" "b affine hull (S - {b})"
  then have "interior(affine hull S) = {}" using assms
  by (metis DIM_positive One_nat_def Suc_mono card.remove card.infinite empty_interior_affine_hull eq_iff hull_redundant insert_Diff not_less zero_le_one)
  then show "interior (convex hull S) = {}"
  using affine_hull_nonempty_interior by fastforce
  qed
 next
  show "interior (convex hull S) = {} ==> affine_dependent S"
  by (metis affine_hull_convex_hull affine_hull_empty affine_independent_span_eq assms convex_convex_hull empty_not_UNIV rel_interior_eq_empty rel_interior_interior)
 qed
 
 
 subsection Coplanarity, and collinearity in terms of affine hull
 
 definition🍋tag important coplanar where
  "coplanar S u v w. S affine hull {u,v,w}"
 
 lemma collinear_affine_hull:
  "collinear S (u v. S affine hull {u,v})"
 proof (cases "S={}")
  case True then show ?thesis
  by simp
 next
  case False
  then obtain x where x: "x S" by auto
  { fix u
  assume *: "x y. [xS; yS] ==> c. x - y = c *🪙R u"
  have "y c. x - y = c *🪙R u ==> a b. y = a *🪙R x + b *🪙R (x + u) a + b = 1"
  by (rule_tac x="1+c" in exI, rule_tac x="-c" in exI, simp add: algebra_simps)
  then have "u v. S {a *🪙R u + b *🪙R v |a b. a + b = 1}"
  using * [OF x] by (rule_tac x=x in exI, rule_tac x="x+u" in exI, force)
  } moreover
  { fix u v x y
  assume *: "S {a *🪙R u + b *🪙R v |a b. a + b = 1}"
  have "c. x - y = c *🪙R (v-u)" if "xS" "yS"
  proof -
  obtain a r where "a + r = 1" "x = a *🪙R u + r *🪙R v"
  using "*" x S by blast
  moreover
  obtain b s where "b + s = 1" "y = b *🪙R u + s *🪙R v"
  using "*" y S by blast
  ultimately have "x - y = (r-s) *🪙R (v-u)"
  by (simp add: algebra_simps) (metis scaleR_left.add)
  then show ?thesis
  by blast
  qed
  } ultimately
  show ?thesis
  unfolding collinear_def affine_hull_2
  by blast
 qed
 
 lemma collinear_closed_segment [simp]: "collinear (closed_segment a b)"
  by (metis affine_hull_convex_hull collinear_affine_hull hull_subset segment_convex_hull)
 
 lemma collinear_open_segment [simp]: "collinear (open_segment a b)"
  unfolding open_segment_def
  by (metis convex_hull_subset_affine_hull segment_convex_hull dual_order.trans
  convex_hull_subset_affine_hull Diff_subset collinear_affine_hull)
 
 lemma collinear_between_cases:
  fixes c :: "'a::euclidean_space"
  shows "collinear {a,b,c} between (b,c) a between (c,a) b between (a,b) c"
  (is "?lhs = ?rhs")
 proof
  assume ?lhs
  then obtain u v where uv: "x. x {a, b, c} ==> c. x = u + c *🪙R v"
  by (auto simp: collinear_alt)
  show ?rhs
  using uv [of a] uv [of b] uv [of c] by (auto simp: between_1)
 next
  assume ?rhs
  then show ?lhs
  unfolding between_mem_convex_hull
  by (metis (no_types, opaque_lifting) collinear_closed_segment collinear_subset hull_redundant hull_subset insert_commute segment_convex_hull)
 qed
 
 
 lemma subset_continuous_image_segment_1:
  fixes f :: "'a::euclidean_space ==> real"
  assumes "continuous_on (closed_segment a b) f"
  shows "closed_segment (f a) (f b) image f (closed_segment a b)"
 by (metis connected_segment convex_contains_segment ends_in_segment imageI
  is_interval_connected_1 is_interval_convex connected_continuous_image [OF assms])
 
 lemma continuous_injective_image_segment_1:
  fixes f :: "'a::euclidean_space ==> real"
  assumes contf: "continuous_on (closed_segment a b) f"
  and injf: "inj_on f (closed_segment a b)"
  shows "f ` (closed_segment a b) = closed_segment (f a) (f b)"
 proof
  show "closed_segment (f a) (f b) f ` closed_segment a b"
  by (metis subset_continuous_image_segment_1 contf)
  show "f ` closed_segment a b closed_segment (f a) (f b)"
  proof (cases "a = b")
  case True
  then show ?thesis by auto
  next
  case False
  then have fnot: "f a f b"
  using inj_onD injf by fastforce
  moreover
  have "f a open_segment (f c) (f b)" if c: "c closed_segment a b" for c
  proof (clarsimp simp add: open_segment_def)
  assume fa: "f a closed_segment (f c) (f b)"
  moreover have "closed_segment (f c) (f b) f ` closed_segment c b"
  by (meson closed_segment_subset contf continuous_on_subset convex_closed_segment ends_in_segment(2) subset_continuous_image_segment_1 that)
  ultimately have "f a f ` closed_segment c b"
  by blast
  then have a: "a closed_segment c b"
  by (meson ends_in_segment inj_on_image_mem_iff injf subset_closed_segment that)
  have cb: "closed_segment c b closed_segment a b"
  by (simp add: closed_segment_subset that)
  show "f a = f c"
  proof (rule between_antisym)
  show "between (f c, f b) (f a)"
  by (simp add: between_mem_segment fa)
  show "between (f a, f b) (f c)"
  by (metis a cb between_antisym between_mem_segment between_triv1 subset_iff)
  qed
  qed
  moreover
  have "f b open_segment (f a) (f c)" if c: "c closed_segment a b" for c
  proof (clarsimp simp add: open_segment_def fnot eq_commute)
  assume fb: "f b closed_segment (f a) (f c)"
  moreover have "closed_segment (f a) (f c) f ` closed_segment a c"
  by (meson contf continuous_on_subset ends_in_segment(1) subset_closed_segment subset_continuous_image_segment_1 that)
  ultimately have "f b f ` closed_segment a c"
  by blast
  then have b: "b closed_segment a c"
  by (meson ends_in_segment inj_on_image_mem_iff injf subset_closed_segment that)
  have ca: "closed_segment a c closed_segment a b"
  by (simp add: closed_segment_subset that)
  show "f b = f c"
  proof (rule between_antisym)
  show "between (f c, f a) (f b)"
  by (simp add: between_commute between_mem_segment fb)
  show "between (f b, f a) (f c)"
  by (metis b between_antisym between_commute between_mem_segment between_triv2 that)
  qed
  qed
  ultimately show ?thesis
  by (force simp: closed_segment_eq_real_ivl open_segment_eq_real_ivl split: if_split_asm)
  qed
 qed
 
 lemma continuous_injective_image_open_segment_1:
  fixes f :: "'a::euclidean_space ==> real"
  assumes contf: "continuous_on (closed_segment a b) f"
  and injf: "inj_on f (closed_segment a b)"
  shows "f ` (open_segment a b) = open_segment (f a) (f b)"
 proof -
  have "f ` (open_segment a b) = f ` (closed_segment a b) - {f a, f b}"
  by (metis (no_types, opaque_lifting) empty_subsetI ends_in_segment image_insert image_is_empty inj_on_image_set_diff injf insert_subset open_segment_def segment_open_subset_closed)
  also have "... = open_segment (f a) (f b)"
  using continuous_injective_image_segment_1 [OF assms]
  by (simp add: open_segment_def inj_on_image_set_diff [OF injf])
  finally show ?thesis .
 qed
 
 lemma collinear_imp_coplanar:
  "collinear s ==> coplanar s"
 by (metis collinear_affine_hull coplanar_def insert_absorb2)
 
 lemma collinear_small:
  assumes "finite s" "card s 2"
  shows "collinear s"
 proof -
  have "card s = 0 card s = 1 card s = 2"
  using assms by linarith
  then show ?thesis using assms
  using card_eq_SucD numeral_2_eq_2 by (force simp: card_1_singleton_iff)
 qed
 
 lemma coplanar_small:
  assumes "finite s" "card s 3"
  shows "coplanar s"
 proof -
  consider "card s 2" | "card s = Suc (Suc (Suc 0))"
  using assms by linarith
  then show ?thesis
  proof cases
  case 1
  then show ?thesis
  by (simp add: finite s collinear_imp_coplanar collinear_small)
  next
  case 2
  then show ?thesis
  using hull_subset [of "{_,_,_}"]
  by (fastforce simp: coplanar_def dest!: card_eq_SucD)
  qed
 qed
 
 lemma coplanar_empty: "coplanar {}"
  by (simp add: coplanar_small)
 
 lemma coplanar_sing: "coplanar {a}"
  by (simp add: coplanar_small)
 
 lemma coplanar_2: "coplanar {a,b}"
  by (auto simp: card_insert_if coplanar_small)
 
 lemma coplanar_3: "coplanar {a,b,c}"
  by (auto simp: card_insert_if coplanar_small)
 
 lemma collinear_affine_hull_collinear: "collinear(affine hull s) collinear s"
  unfolding collinear_affine_hull
  by (metis affine_affine_hull subset_hull hull_hull hull_mono)
 
 lemma coplanar_affine_hull_coplanar: "coplanar(affine hull s) coplanar s"
  unfolding coplanar_def
  by (metis affine_affine_hull subset_hull hull_hull hull_mono)
 
 lemma coplanar_linear_image:
  fixes f :: "'a::euclidean_space ==> 'b::real_normed_vector"
  assumes "coplanar S" "linear f" shows "coplanar(f ` S)"
 proof -
  { fix u v w
  assume "S affine hull {u, v, w}"
  then have "f ` S f ` (affine hull {u, v, w})"
  by (simp add: image_mono)
  then have "f ` S affine hull (f ` {u, v, w})"
  by (metis assms(2) linear_conv_bounded_linear affine_hull_linear_image)
  } then
  show ?thesis
  by auto (meson assms(1) coplanar_def)
 qed
 
 lemma coplanar_translation_imp:
  assumes "coplanar S" shows "coplanar ((λx. a + x) ` S)"
 proof -
  obtain u v w where "S affine hull {u,v,w}"
  by (meson assms coplanar_def)
  then have "(+) a ` S affine hull {u + a, v + a, w + a}"
  using affine_hull_translation [of a "{u,v,w}" for u v w]
  by (force simp: add.commute)
  then show ?thesis
  unfolding coplanar_def by blast
 qed
 
 lemma coplanar_translation_eq: "coplanar((λx. a + x) ` S) coplanar S"
  by (metis (no_types) coplanar_translation_imp translation_galois)
 
 lemma coplanar_linear_image_eq:
  fixes f :: "'a::euclidean_space ==> 'b::euclidean_space"
  assumes "linear f" "inj f" shows "coplanar(f ` S) = coplanar S"
 proof
  assume "coplanar S"
  then show "coplanar (f ` S)"
  using assms(1) coplanar_linear_image by blast
 next
  obtain g where g: "linear g" "g f = id"
  using linear_injective_left_inverse [OF assms]
  by blast
  assume "coplanar (f ` S)"
  then show "coplanar S"
  by (metis coplanar_linear_image g(1) g(2) id_apply image_comp image_id)
 qed
 
 lemma coplanar_subset: "[coplanar t; S t] ==> coplanar S"
  by (meson coplanar_def order_trans)
 
 lemma affine_hull_3_imp_collinear: "c affine hull {a,b} ==> collinear {a,b,c}"
  by (metis collinear_2 collinear_affine_hull_collinear hull_redundant insert_commute)
 
 lemma collinear_3_imp_in_affine_hull:
  assumes "collinear {a,b,c}" "a b" shows "c affine hull {a,b}"
 proof -
  obtain u x y where "b - a = y *🪙R u" "c - a = x *🪙R u"
  using assms unfolding collinear_def by auto
  with a b have "v. c = (1 - x / y) *🪙R a + v *🪙R b 1 - x / y + v = 1"
  by (simp add: algebra_simps)
  then show ?thesis
  by (simp add: hull_inc mem_affine)
 qed
 
 lemma collinear_3_affine_hull:
  assumes "a b"
  shows "collinear {a,b,c} c affine hull {a,b}"
  using affine_hull_3_imp_collinear assms collinear_3_imp_in_affine_hull by blast
 
 lemma collinear_3_eq_affine_dependent:
  "collinear{a,b,c} a = b a = c b = c affine_dependent {a,b,c}"
 proof (cases "a = b a = c b = c")
  case True
  then show ?thesis
  by (auto simp: insert_commute)
 next
  case False
  then have "collinear{a,b,c}" if "affine_dependent {a,b,c}"
  using that unfolding affine_dependent_def
  by (auto simp: insert_Diff_if; metis affine_hull_3_imp_collinear insert_commute)
  moreover
  have "affine_dependent {a,b,c}" if "collinear{a,b,c}"
  using False that by (auto simp: affine_dependent_def collinear_3_affine_hull insert_Diff_if)
  ultimately
  show ?thesis
  using False by blast
 qed
 
 lemma affine_dependent_imp_collinear_3:
  "affine_dependent {a,b,c} ==> collinear{a,b,c}"
  by (simp add: collinear_3_eq_affine_dependent)
 
 lemma collinear_3: "NO_MATCH 0 x ==> collinear {x,y,z} collinear {0, x-y, z-y}"
  by (auto simp add: collinear_def)
 
 lemma collinear_3_expand:
  "collinear{a,b,c} a = c (u. b = u *🪙R a + (1 - u) *🪙R c)"
 proof -
  have "collinear{a,b,c} = collinear{a,c,b}"
  by (simp add: insert_commute)
  also have "... = collinear {0, a - c, b - c}"
  by (simp add: collinear_3)
  also have "... (a = c b = c (ca. b - c = ca *🪙R (a - c)))"
  by (simp add: collinear_lemma)
  also have "... a = c (u. b = u *🪙R a + (1 - u) *🪙R c)"
  by (cases "a = c b = c") (auto simp: algebra_simps)
  finally show ?thesis .
 qed
 
 lemma collinear_aff_dim: "collinear S aff_dim S 1"
 proof
  assume "collinear S"
  then obtain u and v :: "'a" where "aff_dim S aff_dim {u,v}"
  by (metis collinear S aff_dim_affine_hull aff_dim_subset collinear_affine_hull)
  then show "aff_dim S 1"
  using order_trans by fastforce
 next
  assume "aff_dim S 1"
  then have le1: "aff_dim (affine hull S) 1"
  by simp
  obtain B where "B S" and B: "¬ affine_dependent B" "affine hull S = affine hull B"
  using affine_basis_exists [of S] by auto
  then have "finite B" "card B 2"
  using B le1 by (auto simp: affine_independent_iff_card)
  then have "collinear B"
  by (rule collinear_small)
  then show "collinear S"
  by (metis affine hull S = affine hull B collinear_affine_hull_collinear)
 qed
 
 lemma collinear_midpoint: "collinear{a, midpoint a b, b}"
 proof -
  have 🍋: "[a midpoint a b; b - midpoint a b - 1 *🪙R (a - midpoint a b)] ==> b = midpoint a b"
  by (simp add: algebra_simps)
  show ?thesis
  by (auto simp: collinear_3 collinear_lemma intro: 🍋)
 qed
 
 lemma midpoint_collinear:
  fixes a b c :: "'a::real_normed_vector"
  assumes "a c"
  shows "b = midpoint a c collinear{a,b,c} dist a b = dist b c"
 proof -
  have *: "a - (u *🪙R a + (1 - u) *🪙R c) = (1 - u) *🪙R (a - c)"
  "u *🪙R a + (1 - u) *🪙R c - c = u *🪙R (a - c)"
  "1 - u = u u = 1/2" for u::real
  by (auto simp: algebra_simps)
  have "b = midpoint a c ==> collinear{a,b,c}"
  using collinear_midpoint by blast
  moreover have "b = midpoint a c dist a b = dist b c" if "collinear{a,b,c}"
  proof -
  consider "a = c" | u where "b = u *🪙R a + (1 - u) *🪙R c"
  using collinear {a,b,c} unfolding collinear_3_expand by blast
  then show ?thesis
  proof cases
  case 2
  with assms have "dist a b = dist b c ==> b = midpoint a c"
  by (simp add: dist_norm * midpoint_def scaleR_add_right del: divide_const_simps)
  then show ?thesis
  by (auto simp: dist_midpoint)
  qed (use assms in auto)
  qed
  ultimately show ?thesis by blast
 qed
 
 lemma between_imp_collinear:
  fixes x :: "'a :: euclidean_space"
  assumes "between (a,b) x"
  shows "collinear {a,x,b}"
 proof (cases "x = a x = b a = b")
  case True with assms show ?thesis
  by (auto simp: dist_commute)
 next
  case False
  then have False if "c. b - x c *🪙R (a - x)"
  using that [of "-(norm(b - x) / norm(x - a))"] assms
  by (simp add: between_norm vector_add_divide_simps flip: real_vector.scale_minus_right)
  then show ?thesis
  by (auto simp: collinear_3 collinear_lemma)
 qed
 
 lemma midpoint_between:
  fixes a b :: "'a::euclidean_space"
  shows "b = midpoint a c between (a,c) b dist a b = dist b c"
 proof (cases "a = c")
  case False
  show ?thesis
  using False between_imp_collinear between_midpoint(1) midpoint_collinear by blast
 qed (auto simp: dist_commute)
 
 lemma collinear_triples:
  assumes "a b"
  shows "collinear(insert a (insert b S)) (x S. collinear{a,b,x})"
  (is "?lhs = ?rhs")
 proof safe
  fix x
  assume ?lhs and "x S"
  then show "collinear {a, b, x}"
  using collinear_subset by force
 next
  assume ?rhs
  then have "x S. collinear{a,x,b}"
  by (simp add: insert_commute)
  then have *: "u. x = u *🪙R a + (1 - u) *🪙R b" if "x insert a (insert b S)" for x
  using that assms collinear_3_expand by fastforce+
  have "c. x - y = c *🪙R (b - a)"
  if x: "x insert a (insert b S)" and y: "y insert a (insert b S)" for x y
  proof -
  obtain u v where "x = u *🪙R a + (1 - u) *🪙R b" "y = v *🪙R a + (1 - v) *🪙R b"
  using "*" x y by presburger
  then have "x - y = (v - u) *🪙R (b - a)"
  by (simp add: scale_left_diff_distrib scale_right_diff_distrib)
  then show ?thesis ..
  qed
  then show ?lhs
  unfolding collinear_def by metis
 qed
 
 lemma collinear_4_3:
  assumes "a b"
  shows "collinear {a,b,c,d} collinear{a,b,c} collinear{a,b,d}"
  using collinear_triples [OF assms, of "{c,d}"] by (force simp:)
 
 lemma collinear_3_trans:
  assumes "collinear{a,b,c}" "collinear{b,c,d}" "b c"
  shows "collinear{a,b,d}"
 proof -
  have "collinear{b,c,a,d}"
  by (metis (full_types) assms collinear_4_3 insert_commute)
  then show ?thesis
  by (simp add: collinear_subset)
 qed
 
 lemma affine_hull_2_alt:
  fixes a b :: "'a::real_vector"
  shows "affine hull {a,b} = range (λu. a + u *🪙R (b - a))"
 proof -
  have 1: "u *🪙R a + v *🪙R b = a + v *🪙R (b - a)" if "u + v = 1" for u v
  using that
  by (simp add: algebra_simps flip: scaleR_add_left)
  have 2: "a + u *🪙R (b - a) = (1 - u) *🪙R a + u *🪙R b" for u
  by (auto simp: algebra_simps)
  show ?thesis
  by (force simp add: affine_hull_2 dest: 1 intro!: 2)
 qed
 
 lemma interior_convex_hull_3_minimal:
  fixes a :: "'a::euclidean_space"
  assumes "¬ collinear{a,b,c}" and 2: "DIM('a) = 2"
  shows "interior(convex hull {a,b,c}) =
  {v. x y z. 0 🚫 0 🚫 0 🚫 x + y + z = 1 x *🪙R a + y *🪙R b + z *🪙R c = v}"
  (is "?lhs = ?rhs")
 proof
  have abc: "a b" "a c" "b c" "¬ affine_dependent {a, b, c}"
  using assms by (auto simp: collinear_3_eq_affine_dependent)
  with 2 show "?lhs ?rhs"
  by (fastforce simp add: interior_convex_hull_explicit_minimal)
  show "?rhs ?lhs"
  using abc 2
  apply (clarsimp simp add: interior_convex_hull_explicit_minimal)
  subgoal for x y z
  by (rule_tac x="λr. (if r=a then x else if r=b then y else if r=c then z else 0)" in exI) auto
  done
 qed
 
 
 subsection🍋tag unimportant\Basic lemmas about hyperplanes and halfspaces
 
 lemma halfspace_Int_eq:
  "{x. a x b} {x. b a x} = {x. a x = b}"
  "{x. b a x} {x. a x b} = {x. a x = b}"
  by auto
 
 lemma hyperplane_eq_Ex:
  assumes "a 0" obtains x where "a x = b"
  by (rule_tac x = "(b / (a a)) *🪙R a" in that) (simp add: assms)
 
 lemma hyperplane_eq_empty:
  "{x. a x = b} = {} a = 0 b 0"
  using hyperplane_eq_Ex
  by (metis (mono_tags, lifting) empty_Collect_eq inner_zero_left)
 
 lemma hyperplane_eq_UNIV:
  "{x. a x = b} = UNIV a = 0 b = 0"
 proof -
  have "a = 0 b = 0" if "UNIV {x. a x = b}"
  using subsetD [OF that, where c = "((b+1) / (a a)) *🪙R a"]
  by (simp add: field_split_simps split: if_split_asm)
  then show ?thesis by force
 qed
 
 lemma halfspace_eq_empty_lt:
  "{x. a x 🚫} = {} a = 0 b 0"
 proof -
  have "a = 0 b 0" if "{x. a x 🚫} {}"
  using subsetD [OF that, where c = "((b-1) / (a a)) *🪙R a"]
  by (force simp add: field_split_simps split: if_split_asm)
  then show ?thesis by force
 qed
 
 lemma halfspace_eq_empty_gt:
  "{x. a x > b} = {} a = 0 b 0"
  using halfspace_eq_empty_lt [of "-a" "-b"]
  by simp
 
 lemma halfspace_eq_empty_le:
  "{x. a x b} = {} a = 0 b 🚫"
 proof -
  have "a = 0 b 🚫" if "{x. a x b} {}"
  using subsetD [OF that, where c = "((b-1) / (a a)) *🪙R a"]
  by (force simp add: field_split_simps split: if_split_asm)
  then show ?thesis by force
 qed
 
 lemma halfspace_eq_empty_ge:
  "{x. a x b} = {} a = 0 b > 0"
  using halfspace_eq_empty_le [of "-a" "-b"] by simp
 
 subsection🍋tag unimportant\Use set distance for an easy proof of separation properties
 
 proposition🍋tag unimportant separation_closures:
  fixes S :: "'a::euclidean_space set"
  assumes "S closure T = {}" "T closure S = {}"
  obtains U V where "U V = {}" "open U" "open V" "S U" "T V"
 proof (cases "S = {} T = {}")
  case True with that show ?thesis by auto
 next
  case False
  define f where "f λx. setdist {x} T - setdist {x} S"
  have contf: "continuous_on UNIV f"
  unfolding f_def by (intro continuous_intros continuous_on_setdist)
  show ?thesis
  proof (rule_tac U = "{x. f x > 0}" and V = "{x. f x 🚫}" in that)
  show "{x. 0 🚫 x} {x. f x 🚫} = {}"
  by auto
  show "open {x. 0 🚫 x}"
  by (simp add: open_Collect_less contf)
  show "open {x. f x 🚫}"
  by (simp add: open_Collect_less contf)
  have "x. x S ==> setdist {x} T 0" "x. x T ==> setdist {x} S 0"
  by (meson False assms disjoint_iff setdist_eq_0_sing_1)+
  then show "S {x. 0 🚫 x}" "T {x. f x 🚫}"
  using less_eq_real_def by (fastforce simp add: f_def setdist_sing_in_set)+
  qed
 qed
 
 lemma separation_normal:
  fixes S :: "'a::euclidean_space set"
  assumes "closed S" "closed T" "S T = {}"
  obtains U V where "open U" "open V" "S U" "T V" "U V = {}"
 using separation_closures [of S T]
 by (metis assms closure_closed disjnt_def inf_commute)
 
 lemma separation_normal_local:
  fixes S :: "'a::euclidean_space set"
  assumes US: "closedin (top_of_set U) S"
  and UT: "closedin (top_of_set U) T"
  and "S T = {}"
  obtains S' T' where "openin (top_of_set U) S'"
  "openin (top_of_set U) T'"
  "S S'" "T T'" "S' T' = {}"
 proof (cases "S = {} T = {}")
  case True with that show ?thesis
  using UT US by (blast dest: closedin_subset)
 next
  case False
  define f where "f λx. setdist {x} T - setdist {x} S"
  have contf: "continuous_on U f"
  unfolding f_def by (intro continuous_intros)
  show ?thesis
  proof (rule_tac S' = "(U f -` {0🚫})" and T' = "(U f -` {..🚫)" in that)
  show "(U f -` {0🚫}) (U f -` {..🚫) = {}"
  by auto
  show "openin (top_of_set U) (U f -` {0🚫})"
  by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
  next
  show "openin (top_of_set U) (U f -` {..🚫)"
  by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
  next
  have "S U" "T U"
  using closedin_imp_subset assms by blast+
  then show "S U f -` {0🚫}" "T U f -` {..🚫"
  using assms False by (force simp add: f_def setdist_sing_in_set intro!: setdist_gt_0_closedin)+
  qed
 qed
 
 lemma separation_normal_compact:
  fixes S :: "'a::euclidean_space set"
  assumes "compact S" "closed T" "S T = {}"
  obtains U V where "open U" "compact(closure U)" "open V" "S U" "T V" "U V = {}"
 proof -
  have "closed S" "bounded S"
  using assms by (auto simp: compact_eq_bounded_closed)
  then obtain r where "r>0" and r: "S ball 0 r"
  by (auto dest!: bounded_subset_ballD)
  have **: "closed (T - ball 0 r)" "S (T - ball 0 r) = {}"
  using assms r by blast+
  then obtain U V where UV: "open U" "open V" "S U" "T - ball 0 r V" "U V = {}"
  by (meson closed S separation_normal)
  then have "compact(closure U)"
  by (meson bounded_ball bounded_subset compact_closure compl_le_swap2 disjoint_eq_subset_Compl le_sup_iff)
  with UV show thesis
  using that by auto
 qed
 
 subsectionConnectedness of the intersection of a chain
 
 proposition connected_chain:
  fixes F :: "'a :: euclidean_space set set"
  assumes cc: "S. S F ==> compact S connected S"
  and linear: "S T. S F T F ==> S T T S"
  shows "connected(F)"
 proof (cases "F = {}")
  case True then show ?thesis
  by auto
 next
  case False
  then have cf: "compact(F)"
  by (simp add: cc compact_Inter)
  have False if AB: "closed A" "closed B" "A B = {}"
  and ABeq: "A B = F" and "A {}" "B {}" for A B
  proof -
  obtain U V where "open U" "open V" "A U" "B V" "U V = {}"
  using separation_normal [OF AB] by metis
  obtain K where "K F" "compact K"
  using cc False by blast
  then obtain N where "open N" and "K N"
  by blast
  let ?C = "insert (U V) ((λS. N - S) ` F)"
  obtain D where "D ?C" "finite D" "K D"
  proof (rule compactE [OF compact K])
  show "K (insert (U V) ((-) N ` F))"
  using K N ABeq A U B V by auto
  show "B. B insert (U V) ((-) N ` F) ==> open B"
  by (auto simp: open U open V open_Un open N cc compact_imp_closed open_Diff)
  qed
  then have "finite(D - {U V})"
  by blast
  moreover have "D - {U V} (λS. N - S) ` F"
  using D ?C by blast
  ultimately obtain G where "G F" "finite G" and Deq: "D - {U V} = (λS. N-S) ` G"
  using finite_subset_image by metis
  obtain J where "J F" and J: "(SG. N - S) N - J"
  proof (cases "G = {}")
  case True
  with F {} that show ?thesis
  by auto
  next
  case False
  have "S T. [S G; T G] ==> S T T S"
  by (meson G F in_mono local.linear)
  with finite G G {}
  have "J G. (SG. N - S) N - J"
  proof induction
  case (insert X H)
  show ?case
  proof (cases "H = {}")
  case True then show ?thesis by auto
  next
  case False
  then have "S T. [S H; T H] ==> S T T S"
  by (simp add: insert.prems)
  with insert.IH False obtain J where "J H" and J: "(YH. N - Y) N - J"
  by metis
  have "N - J N - X N - X N - J"
  by (meson Diff_mono J H insert.prems(2) insert_iff order_refl)
  then show ?thesis
  proof
  assume "N - J N - X" with J show ?thesis
  by auto
  next
  assume "N - X N - J"
  with J have "N - X ((-) N ` H) N - J"
  by auto
  with J H show ?thesis
  by blast
  qed
  qed
  qed simp
  with G F show ?thesis by (blast intro: that)
  qed
  have "K (insert (U V) (D - {U V}))"
  using K D by auto
  also have "... (U V) (N - J)"
  by (metis (no_types, opaque_lifting) Deq Un_subset_iff Un_upper2 J Union_insert order_trans sup_ge1)
  finally have "J K U V"
  by blast
  moreover have "connected(J K)"
  by (metis Int_absorb1 J F K F cc inf.orderE local.linear)
  moreover have "U (J K) {}"
  using ABeq J F K F A {} A U by blast
  moreover have "V (J K) {}"
  using ABeq J F K F B {} B V by blast
  ultimately show False
  using connectedD [of "J K" U V] open U open V U V = {} by auto
  qed
  with cf show ?thesis
  by (auto simp: connected_closed_set compact_imp_closed)
 qed
 
 lemma connected_chain_gen:
  fixes F :: "'a :: euclidean_space set set"
  assumes X: "X F" "compact X"
  and cc: "T. T F ==> closed T connected T"
  and linear: "S T. S F T F ==> S T T S"
  shows "connected(F)"
 proof -
  have "F = (TF. X T)"
  using X by blast
  moreover have "connected (TF. X T)"
  proof (rule connected_chain)
  show "T. T () X ` F ==> compact T connected T"
  using cc X by auto (metis inf.absorb2 inf.orderE local.linear)
  show "S T. S () X ` F T () X ` F ==> S T T S"
  using local.linear by blast
  qed
  ultimately show ?thesis
  by metis
 qed
 
 lemma connected_nest:
  fixes S :: "'a::linorder ==> 'b::euclidean_space set"
  assumes S: "n. compact(S n)" "n. connected(S n)"
  and nest: "m n. m n ==> S n S m"
  shows "connected( (range S))"
 proof (rule connected_chain)
  show "A T. A range S T range S ==> A T T A"
  by (metis image_iff le_cases nest)
 qed (use S in blast)
 
 lemma connected_nest_gen:
  fixes S :: "'a::linorder ==> 'b::euclidean_space set"
  assumes S: "n. closed(S n)" "n. connected(S n)" "compact(S k)"
  and nest: "m n. m n ==> S n S m"
  shows "connected( (range S))"
 proof (rule connected_chain_gen [of "S k"])
  show "A T. A range S T range S ==> A T T A"
  by (metis imageE le_cases nest)
 qed (use S in auto)
 
 subsectionProper maps, including projections out of compact sets
 
 lemma finite_indexed_bound:
  assumes A: "finite A" "x. x A ==> n::'a::linorder. P x n"
  shows "m. x A. km. P x k"
 using A
 proof (induction A)
  case empty then show ?case by force
 next
  case (insert a A)
  then obtain m n where "x A. km. P x k" "P a n"
  by force
  then show ?case
  by (metis dual_order.trans insert_iff le_cases)
 qed
 
 proposition proper_map:
  fixes f :: "'a::heine_borel ==> 'b::heine_borel"
  assumes "closedin (top_of_set S) K"
  and com: "U. [U T; compact U] ==> compact (S f -` U)"
  and "f ` S T"
  shows "closedin (top_of_set T) (f ` K)"
 proof -
  have "K S"
  using assms closedin_imp_subset by metis
  obtain C where "closed C" and Keq: "K = S C"
  using assms by (auto simp: closedin_closed)
  have *: "y f ` K" if "y T" and y: "y islimpt f ` K" for y
  proof -
  obtain h where "n. (xK. h n = f x) h n y" "inj h" and hlim: "(h ---> y) sequentially"
  using y T y by (force simp: limpt_sequential_inj)
  then obtain X where X: "n. X n K h n = f (X n) h n y"
  by metis
  then have fX: "n. f (X n) = h n"
  by metis
  define Ψ where "Ψ λn. {a K. f a insert y (range (λi. f (X (n + i))))}"
  have "compact (C (S f -` insert y (range (λi. f(X(n + i))))))" for n
  proof (intro closed_Int_compact [OF closed C com] compact_sequence_with_limit)
  show "insert y (range (λi. f (X (n + i)))) T"
  using X K S f ` S T y T by blast
  show "(λi. f (X (n + i))) <---- y"
  by (simp add: fX add.commute [of n] LIMSEQ_ignore_initial_segment [OF hlim])
  qed
  then have comf: "compact (Ψ n)" for n
  by (simp add: Keq Int_def Ψ_def conj_commute)
  have ne: "F {}"
  if "finite F"
  and F: "t. t F ==> (n. t = Ψ n)"
  for F
  proof -
  obtain m where m: "t. t F ==> km. t = Ψ k"
  by (rule exE [OF finite_indexed_bound [OF finite F F]], force+)
  have "X m F"
  using X le_Suc_ex by (fastforce simp: Ψ_def dest: m)
  then show ?thesis by blast
  qed
  have "(n. Ψ n) {}"
  proof (rule compact_fip_Heine_Borel)
  show "F'. [finite F'; F' range Ψ] ==> F' {}"
  by (meson ne rangeE subset_eq)
  qed (use comf in blast)
  then obtain x where "x K" "n. (f x = y (u. f x = h (n + u)))"
  by (force simp add: Ψ_def fX)
  then show ?thesis
  unfolding image_iff by (metis inj h le_add1 not_less_eq_eq rangeI range_ex1_eq)
  qed
  with assms closedin_subset show ?thesis
  by (force simp: closedin_limpt)
 qed
 
 subsection Closure of conic hulls
 proposition closedin_conic_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "compact T" "0 T" "T S"
  shows "closedin (top_of_set (conic hull S)) (conic hull T)"
 proof -
  have **: "compact ({0..} × T (λz. fst z *🪙R snd z) -` K)" (is "compact ?L")
  if "K (λz. (fst z) *🪙R snd z) ` ({0..} × S)" "compact K" for K
  proof -
  obtain r where "r > 0" and r: "x. x K ==> norm x r"
  by (metis compact K bounded_normE compact_imp_bounded)
  show ?thesis
  unfolding compact_eq_bounded_closed
  proof
  have "bounded ({0..r / setdist{0}T} × T)"
  by (simp add: assms(1) bounded_Times compact_imp_bounded)
  moreover have "?L ({0..r / setdist{0}T} × T)"
  proof clarsimp
  fix a b
  assume "a *🪙R b K" and "b T" and "0 a"
  have "setdist {0} T 0"
  using b T assms compact_imp_closed setdist_eq_0_closed by auto
  then have T0: "setdist {0} T > 0"
  using less_eq_real_def by fastforce
  then have "a * setdist {0} T r"
  by (smt (verit, ccfv_SIG) 0 a a *🪙R b K b T dist_0_norm mult_mono' norm_scaleR r setdist_le_dist singletonI)
  with T0 r>0 show "a r / setdist {0} T"
  by (simp add: divide_simps)
  qed
  ultimately show "bounded ?L"
  by (meson bounded_subset)
  show "closed ?L"
  proof (rule continuous_closed_preimage)
  show "continuous_on ({0..} × T) (λz. fst z *🪙R snd z)"
  by (intro continuous_intros)
  show "closed ({0::real..} × T)"
  by (simp add: assms(1) closed_Times compact_imp_closed)
  show "closed K"
  by (simp add: compact_imp_closed that(2))
  qed
  qed
  qed
  show ?thesis
  unfolding conic_hull_as_image
  proof (rule proper_map)
  show "compact ({0..} × T (λz. fst z *🪙R snd z) -` K)" (is "compact ?L")
  if "K (λz. (fst z) *🪙R snd z) ` ({0..} × S)" "compact K" for K
  proof -
  obtain r where "r > 0" and r: "x. x K ==> norm x r"
  by (metis compact K bounded_normE compact_imp_bounded)
  show ?thesis
  unfolding compact_eq_bounded_closed
  proof
  have "bounded ({0..r / setdist{0}T} × T)"
  by (simp add: assms(1) bounded_Times compact_imp_bounded)
  moreover have "?L ({0..r / setdist{0}T} × T)"
  proof clarsimp
  fix a b
  assume "a *🪙R b K" and "b T" and "0 a"
  have "setdist {0} T 0"
  using b T assms compact_imp_closed setdist_eq_0_closed by auto
  then have T0: "setdist {0} T > 0"
  using less_eq_real_def by fastforce
  then have "a * setdist {0} T r"
  by (smt (verit, ccfv_SIG) 0 a a *🪙R b K b T dist_0_norm mult_mono' norm_scaleR r setdist_le_dist singletonI)
  with T0 r>0 show "a r / setdist {0} T"
  by (simp add: divide_simps)
  qed
  ultimately show "bounded ?L"
  by (meson bounded_subset)
  show "closed ?L"
  proof (rule continuous_closed_preimage)
  show "continuous_on ({0..} × T) (λz. fst z *🪙R snd z)"
  by (intro continuous_intros)
  show "closed ({0::real..} × T)"
  by (simp add: assms(1) closed_Times compact_imp_closed)
  show "closed K"
  by (simp add: compact_imp_closed that(2))
  qed
  qed
  qed
  show "(λz. fst z *🪙R snd z) ` ({0::real..} × T) (λz. fst z *🪙R snd z) ` ({0..} × S)"
  using T S by force
  qed auto
 qed
 
 lemma closed_conic_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "0 rel_interior S compact S 0 S"
  shows "closed(conic hull S)"
  using assms
 proof
  assume "0 rel_interior S"
  then show "closed (conic hull S)"
  by (simp add: conic_hull_eq_span)
 next
  assume "compact S 0 S"
  then have "closedin (top_of_set UNIV) (conic hull S)"
  using closedin_conic_hull by force
  then show "closed (conic hull S)"
  by simp
 qed
 
 lemma conic_closure:
  fixes S :: "'a::euclidean_space set"
  shows "conic S ==> conic(closure S)"
  by (meson Convex.cone_def cone_closure conic_def)
 
 lemma closure_conic_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "0 rel_interior S bounded S ~(0 closure S)"
  shows "closure(conic hull S) = conic hull (closure S)"
  using assms
 proof
  assume "0 rel_interior S"
  then show "closure (conic hull S) = conic hull closure S"
  by (metis closed_affine_hull closure_closed closure_same_affine_hull closure_subset conic_hull_eq_affine_hull subsetD subset_rel_interior)
 next
  have "x. x conic hull closure S ==> x closure (conic hull S)"
  by (metis (no_types, opaque_lifting) closure_mono conic_closure conic_conic_hull subset_eq subset_hull)
  moreover
  assume "bounded S 0 closure S"
  then have "x. x closure (conic hull S) ==> x conic hull closure S"
  by (metis closed_conic_hull closure_Un_frontier closure_closed closure_mono compact_closure hull_Un_subset le_sup_iff subsetD)
  ultimately show "closure (conic hull S) = conic hull closure S"
  by blast
 qed
 
 lemma compact_continuous_image_eq:
  fixes f :: "'a::heine_borel ==> 'b::heine_borel"
  assumes f: "inj_on f S"
  shows "continuous_on S f (T. compact T T S compact(f ` T))"
  (is "?lhs = ?rhs")
 proof
  assume ?lhs then show ?rhs
  by (metis continuous_on_subset compact_continuous_image)
 next
  assume RHS: ?rhs
  obtain g where gf: "x. x S ==> g (f x) = x"
  by (metis inv_into_f_f f)
  then have *: "(S f -` U) = g ` U" if "U f ` S" for U
  using that by fastforce
  have gfim: "g ` f ` S S" using gf by auto
  have **: "compact (f ` S g -` C)" if C: "C S" "compact C" for C
  proof -
  obtain h where "h C C h C S compact (f ` C)"
  by (force simp: C RHS)
  moreover have "f ` C = (f ` S g -` C)"
  using C gf by auto
  ultimately show ?thesis
  using C by auto
  qed
  show ?lhs
  using proper_map [OF _ _ gfim] **
  by (simp add: continuous_on_closed * closedin_imp_subset)
 qed
 
 subsection🍋tag unimportant\Trivial fact: convexity equals connectedness for collinear sets
 
 lemma convex_connected_collinear:
  fixes S :: "'a::euclidean_space set"
  assumes "collinear S"
  shows "convex S connected S"
 proof
  assume "convex S"
  then show "connected S"
  using convex_connected by blast
 next
  assume S: "connected S"
  show "convex S"
  proof (cases "S = {}")
  case True
  then show ?thesis by simp
  next
  case False
  then obtain a where "a S" by auto
  have "collinear (affine hull S)"
  by (simp add: assms collinear_affine_hull_collinear)
  then obtain z where "z 0" "x. x affine hull S ==> c. x - a = c *🪙R z"
  by (meson a S collinear hull_inc)
  then obtain f where f: "x. x affine hull S ==> x - a = f x *🪙R z"
  by metis
  then have inj_f: "inj_on f (affine hull S)"
  by (metis diff_add_cancel inj_onI)
  have diff: "x - y = (f x - f y) *🪙R z" if x: "x affine hull S" and y: "y affine hull S" for x y
  proof -
  have "f x *🪙R z = x - a"
  by (simp add: f hull_inc x)
  moreover have "f y *🪙R z = y - a"
  by (simp add: f hull_inc y)
  ultimately show ?thesis
  by (simp add: scaleR_left.diff)
  qed
  have cont_f: "continuous_on (affine hull S) f"
  proof (clarsimp simp: dist_norm continuous_on_iff diff)
  show "x e. 0 🚫 ==> d>0. y affine hull S. f y - f x * norm z 🚫 f y - f x 🚫"
  by (metis z 0 mult_pos_pos mult_less_cancel_right_pos zero_less_norm_iff)
  qed
  then have conn_fS: "connected (f ` S)"
  by (meson S connected_continuous_image continuous_on_subset hull_subset)
  show ?thesis
  proof (clarsimp simp: convex_contains_segment)
  fix x y z
  assume "x S" "y S" "z closed_segment x y"
  have False if "z S"
  proof -
  have "f ` (closed_segment x y) = closed_segment (f x) (f y)"
  proof (rule continuous_injective_image_segment_1)
  show "continuous_on (closed_segment x y) f"
  by (meson x S y S convex_affine_hull convex_contains_segment hull_inc continuous_on_subset [OF cont_f])
  show "inj_on f (closed_segment x y)"
  by (meson x S y S convex_affine_hull convex_contains_segment hull_inc inj_on_subset [OF inj_f])
  qed
  then have fz: "f z closed_segment (f x) (f y)"
  using z closed_segment x y by blast
  have "z affine hull S"
  by (meson x S y S z closed_segment x y convex_affine_hull convex_contains_segment hull_inc subset_eq)
  then have fz_notin: "f z f ` S"
  using hull_subset inj_f inj_onD that by fastforce
  moreover have "{..🚫z} f ` S {}" "{f z🚫} f ` S {}"
  proof -
  consider "f x f z f z f y" | "f y f z f z f x"
  using fz
  by (auto simp add: closed_segment_eq_real_ivl split: if_split_asm)
  then have "{..🚫z} f ` {x,y} {} {f z🚫} f ` {x,y} {}"
  by cases (use fz_notin x S y S in auto simp: image_iff)
  then show "{..🚫z} f ` S {}" "{f z🚫} f ` S {}"
  using x S y S by blast+
  qed
  ultimately show False
  using connectedD [OF conn_fS, of "{..🚫z}" "{f z🚫}"] by force
  qed
  then show "z S" by meson
  qed
  qed
 qed
 
 lemma compact_convex_collinear_segment_alt:
  fixes S :: "'a::euclidean_space set"
  assumes "S {}" "compact S" "connected S" "collinear S"
  obtains a b where "S = closed_segment a b"
 proof -
  obtain ξ where "ξ S" using S {} by auto
  have "collinear (affine hull S)"
  by (simp add: assms collinear_affine_hull_collinear)
  then obtain z where "z 0" "x. x affine hull S ==> c. x - ξ = c *🪙R z"
  by (meson ξ S collinear hull_inc)
  then obtain f where f: "x. x affine hull S ==> x - ξ = f x *🪙R z"
  by metis
  let ?g = "λr. r *🪙R z + ξ"
  have gf: "?g (f x) = x" if "x affine hull S" for x
  by (metis diff_add_cancel f that)
  then have inj_f: "inj_on f (affine hull S)"
  by (metis inj_onI)
  have diff: "x - y = (f x - f y) *🪙R z" if x: "x affine hull S" and y: "y affine hull S" for x y
  proof -
  have "f x *🪙R z = x - ξ"
  by (simp add: f hull_inc x)
  moreover have "f y *🪙R z = y - ξ"
  by (simp add: f hull_inc y)
  ultimately show ?thesis
  by (simp add: scaleR_left.diff)
  qed
  have cont_f: "continuous_on (affine hull S) f"
  proof (clarsimp simp: dist_norm continuous_on_iff diff)
  show "x e. 0 🚫 ==> d>0. y affine hull S. f y - f x * norm z 🚫 f y - f x 🚫"
  by (metis z 0 mult_pos_pos mult_less_cancel_right_pos zero_less_norm_iff)
  qed
  then have "connected (f ` S)"
  by (meson connected S connected_continuous_image continuous_on_subset hull_subset)
  moreover have "compact (f ` S)"
  by (meson compact S compact_continuous_image_eq cont_f hull_subset inj_f)
  ultimately obtain x y where "f ` S = {x..y}"
  by (meson connected_compact_interval_1)
  then have fS_eq: "f ` S = closed_segment x y"
  using S {} closed_segment_eq_real_ivl by auto
  obtain a b where "a S" "f a = x" "b S" "f b = y"
  by (metis (full_types) ends_in_segment fS_eq imageE)
  have "f ` (closed_segment a b) = closed_segment (f a) (f b)"
  proof (rule continuous_injective_image_segment_1)
  show "continuous_on (closed_segment a b) f"
  by (meson a S b S convex_affine_hull convex_contains_segment hull_inc continuous_on_subset [OF cont_f])
  show "inj_on f (closed_segment a b)"
  by (meson a S b S convex_affine_hull convex_contains_segment hull_inc inj_on_subset [OF inj_f])
  qed
  then have "f ` (closed_segment a b) = f ` S"
  by (simp add: f a = x f b = y fS_eq)
  then have "?g ` f ` (closed_segment a b) = ?g ` f ` S"
  by simp
  moreover have "(λx. f x *🪙R z + ξ) ` closed_segment a b = closed_segment a b"
  unfolding image_def using a S b S
  by (safe; metis (mono_tags, lifting) convex_affine_hull convex_contains_segment gf hull_subset subsetCE)
  ultimately have "closed_segment a b = S"
  using gf by (simp add: image_comp o_def hull_inc cong: image_cong)
  then show ?thesis
  using that by blast
 qed
 
 lemma compact_convex_collinear_segment:
  fixes S :: "'a::euclidean_space set"
  assumes "S {}" "compact S" "convex S" "collinear S"
  obtains a b where "S = closed_segment a b"
  using assms convex_connected_collinear compact_convex_collinear_segment_alt by blast
 
 
 lemma proper_map_from_compact:
  fixes f :: "'a::euclidean_space ==> 'b::euclidean_space"
  assumes contf: "continuous_on S f" and imf: "f S T" and "compact S"
  "closedin (top_of_set T) K"
  shows "compact (S f -` K)"
 by (rule closedin_compact [OF compact S] continuous_closedin_preimage_gen assms)+
 
 lemma proper_map_fst:
  assumes "compact T" "K S" "compact K"
  shows "compact (S × T fst -` K)"
 proof -
  have "(S × T fst -` K) = K × T"
  using assms by auto
  then show ?thesis by (simp add: assms compact_Times)
 qed
 
 lemma closed_map_fst:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "compact T" "closedin (top_of_set (S × T)) c"
  shows "closedin (top_of_set S) (fst ` c)"
 proof -
  have *: "fst ` (S × T) S"
  by auto
  show ?thesis
  using proper_map [OF _ _ *] by (simp add: proper_map_fst assms)
 qed
 
 lemma proper_map_snd:
  assumes "compact S" "K T" "compact K"
  shows "compact (S × T snd -` K)"
 proof -
  have "(S × T snd -` K) = S × K"
  using assms by auto
  then show ?thesis by (simp add: assms compact_Times)
 qed
 
 lemma closed_map_snd:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "compact S" "closedin (top_of_set (S × T)) c"
  shows "closedin (top_of_set T) (snd ` c)"
 proof -
  have *: "snd ` (S × T) T"
  by auto
  show ?thesis
  using proper_map [OF _ _ *] by (simp add: proper_map_snd assms)
 qed
 
 lemma closedin_compact_projection:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "compact S" and clo: "closedin (top_of_set (S × T)) U"
  shows "closedin (top_of_set T) {y. x. x S (x, y) U}"
 proof -
  have "U S × T"
  by (metis clo closedin_imp_subset)
  then have "{y. x. x S (x, y) U} = snd ` U"
  by force
  moreover have "closedin (top_of_set T) (snd ` U)"
  by (rule closed_map_snd [OF assms])
  ultimately show ?thesis
  by simp
 qed
 
 
 lemma closed_compact_projection:
  fixes S :: "'a::euclidean_space set"
  and T :: "('a * 'b::euclidean_space) set"
  assumes "compact S" and clo: "closed T"
  shows "closed {y. x. x S (x, y) T}"
 proof -
  have *: "{y. x. x S Pair x y T} = {y. x. x S Pair x y ((S × UNIV) T)}"
  by auto
  show ?thesis
  unfolding *
  by (intro clo closedin_closed_Int closedin_closed_trans [OF _ closed_UNIV] closedin_compact_projection [OF compact S])
 qed
 
 subsubsection🍋tag unimportant\Representing affine hull as a finite intersection of hyperplanes
 
 proposition🍋tag unimportant affine_hull_convex_Int_nonempty_interior:
  fixes S :: "'a::real_normed_vector set"
  assumes "convex S" "S interior T {}"
  shows "affine hull (S T) = affine hull S"
 proof
  show "affine hull (S T) affine hull S"
  by (simp add: hull_mono)
 next
  obtain a where "a S" "a T" and at: "a interior T"
  using assms interior_subset by blast
  then obtain e where "e > 0" and e: "cball a e T"
  using mem_interior_cball by blast
  have *: "x (+) a ` span ((λx. x - a) ` (S T))" if "x S" for x
  proof (cases "x = a")
  case True with that span_0 eq_add_iff image_def mem_Collect_eq show ?thesis
  by blast
  next
  case False
  define k where "k = min (1/2) (e / norm (x-a))"
  have k: "0 🚫" "k 🚫"
  using e > 0 False by (auto simp: k_def)
  then have xa: "(x-a) = inverse k *🪙R k *🪙R (x-a)"
  by simp
  have "e / norm (x - a) k"
  using k_def by linarith
  then have "a + k *🪙R (x - a) cball a e"
  using 0 🚫 False
  by (simp add: dist_norm) (simp add: field_simps)
  then have T: "a + k *🪙R (x - a) T"
  using e by blast
  have S: "a + k *🪙R (x - a) S"
  using k a S convexD [OF convex S a S x S, of "1-k" k]
  by (simp add: algebra_simps)
  have "inverse k *🪙R k *🪙R (x-a) span ((λx. x - a) ` (S T))"
  by (intro span_mul [OF span_base] image_eqI [where x = "a + k *🪙R (x - a)"]) (auto simp: S T)
  with xa image_iff show ?thesis by fastforce
  qed
  have "S affine hull (S T)"
  by (force simp: * a S a T hull_inc affine_hull_span_gen [of a])
  then show "affine hull S affine hull (S T)"
  by (simp add: subset_hull)
 qed
 
 corollary affine_hull_convex_Int_open:
  fixes S :: "'a::real_normed_vector set"
  assumes "convex S" "open T" "S T {}"
  shows "affine hull (S T) = affine hull S"
  using affine_hull_convex_Int_nonempty_interior assms interior_eq by blast
 
 corollary affine_hull_affine_Int_nonempty_interior:
  fixes S :: "'a::real_normed_vector set"
  assumes "affine S" "S interior T {}"
  shows "affine hull (S T) = affine hull S"
  by (simp add: affine_hull_convex_Int_nonempty_interior affine_imp_convex assms)
 
 corollary affine_hull_affine_Int_open:
  fixes S :: "'a::real_normed_vector set"
  assumes "affine S" "open T" "S T {}"
  shows "affine hull (S T) = affine hull S"
  by (simp add: affine_hull_convex_Int_open affine_imp_convex assms)
 
 corollary affine_hull_convex_Int_openin:
  fixes S :: "'a::real_normed_vector set"
  assumes "convex S" "openin (top_of_set (affine hull S)) T" "S T {}"
  shows "affine hull (S T) = affine hull S"
  using assms unfolding openin_open
  by (metis affine_hull_convex_Int_open hull_subset inf.orderE inf_assoc)
 
 corollary affine_hull_openin:
  fixes S :: "'a::real_normed_vector set"
  assumes "openin (top_of_set (affine hull T)) S" "S {}"
  shows "affine hull S = affine hull T"
  using assms unfolding openin_open
  by (metis affine_affine_hull affine_hull_affine_Int_open hull_hull)
 
 corollary affine_hull_open:
  fixes S :: "'a::real_normed_vector set"
  assumes "open S" "S {}"
  shows "affine hull S = UNIV"
  by (metis affine_hull_convex_Int_nonempty_interior assms convex_UNIV hull_UNIV inf_top.left_neutral interior_open)
 
 lemma aff_dim_convex_Int_nonempty_interior:
  fixes S :: "'a::euclidean_space set"
  shows "[convex S; S interior T {}] ==> aff_dim(S T) = aff_dim S"
  using aff_dim_affine_hull2 affine_hull_convex_Int_nonempty_interior by blast
 
 lemma aff_dim_convex_Int_open:
  fixes S :: "'a::euclidean_space set"
  shows "[convex S; open T; S T {}] ==> aff_dim(S T) = aff_dim S"
  using aff_dim_convex_Int_nonempty_interior interior_eq by blast
 
 lemma affine_hull_Diff:
  fixes S:: "'a::real_normed_vector set"
  assumes ope: "openin (top_of_set (affine hull S)) S" and "finite F" "F S"
  shows "affine hull (S - F) = affine hull S"
 proof -
  have clo: "closedin (top_of_set S) F"
  using assms finite_imp_closedin by auto
  moreover have "S - F {}"
  using assms by auto
  ultimately show ?thesis
  by (metis ope closedin_def topspace_euclidean_subtopology affine_hull_openin openin_trans)
 qed
 
 lemma affine_hull_halfspace_lt:
  fixes a :: "'a::euclidean_space"
  shows "affine hull {x. a x 🚫} = (if a = 0 r 0 then {} else UNIV)"
 using halfspace_eq_empty_lt [of a r]
 by (simp add: open_halfspace_lt affine_hull_open)
 
 lemma affine_hull_halfspace_le:
  fixes a :: "'a::euclidean_space"
  shows "affine hull {x. a x r} = (if a = 0 r 🚫 then {} else UNIV)"
 proof (cases "a = 0")
  case True then show ?thesis by simp
 next
  case False
  then have "affine hull closure {x. a x 🚫} = UNIV"
  using affine_hull_halfspace_lt closure_same_affine_hull by fastforce
  moreover have "{x. a x 🚫} {x. a x r}"
  by (simp add: Collect_mono)
  ultimately show ?thesis using False antisym_conv hull_mono top_greatest
  by (metis affine_hull_halfspace_lt)
 qed
 
 lemma affine_hull_halfspace_gt:
  fixes a :: "'a::euclidean_space"
  shows "affine hull {x. a x > r} = (if a = 0 r 0 then {} else UNIV)"
 using halfspace_eq_empty_gt [of r a]
 by (simp add: open_halfspace_gt affine_hull_open)
 
 lemma affine_hull_halfspace_ge:
  fixes a :: "'a::euclidean_space"
  shows "affine hull {x. a x r} = (if a = 0 r > 0 then {} else UNIV)"
 using affine_hull_halfspace_le [of "-a" "-r"] by simp
 
 lemma aff_dim_halfspace_lt:
  fixes a :: "'a::euclidean_space"
  shows "aff_dim {x. a x 🚫} =
  (if a = 0 r 0 then -1 else DIM('a))"
 by simp (metis aff_dim_open halfspace_eq_empty_lt open_halfspace_lt)
 
 lemma aff_dim_halfspace_le:
  fixes a :: "'a::euclidean_space"
  shows "aff_dim {x. a x r} =
  (if a = 0 r 🚫 then -1 else DIM('a))"
 proof -
  have "int (DIM('a)) = aff_dim (UNIV::'a set)"
  by (simp)
  then have "aff_dim (affine hull {x. a x r}) = DIM('a)" if "(a = 0 r 0)"
  using that by (simp add: affine_hull_halfspace_le not_less)
  then show ?thesis
  by (force)
 qed
 
 lemma aff_dim_halfspace_gt:
  fixes a :: "'a::euclidean_space"
  shows "aff_dim {x. a x > r} =
  (if a = 0 r 0 then -1 else DIM('a))"
 by simp (metis aff_dim_open halfspace_eq_empty_gt open_halfspace_gt)
 
 lemma aff_dim_halfspace_ge:
  fixes a :: "'a::euclidean_space"
  shows "aff_dim {x. a x r} =
  (if a = 0 r > 0 then -1 else DIM('a))"
 using aff_dim_halfspace_le [of "-a" "-r"] by simp
 
 proposition aff_dim_eq_hyperplane:
  fixes S :: "'a::euclidean_space set"
  shows "aff_dim S = DIM('a) - 1 (a b. a 0 affine hull S = {x. a x = b})"
  (is "?lhs = ?rhs")
 proof (cases "S = {}")
  case True then show ?thesis
  by (auto simp: dest: hyperplane_eq_Ex)
 next
  case False
  then obtain c where "c S" by blast
  show ?thesis
  proof (cases "c = 0")
  case True
  have "?lhs (a. a 0 span ((λx. x - c) ` S) = {x. a x = 0})"
  by (simp add: aff_dim_eq_dim [of c] c S hull_inc dim_eq_hyperplane del: One_nat_def)
  also have "... ?rhs"
  using span_zero [of S] True c S affine_hull_span_0 hull_inc
  by (fastforce simp add: affine_hull_span_gen [of c] c = 0)
  finally show ?thesis .
  next
  case False
  have xc_im: "x (+) c ` {y. a y = 0}" if "a x = a c" for a x
  proof -
  have "y. a y = 0 c + y = x"
  by (metis that add.commute diff_add_cancel inner_commute inner_diff_left right_minus_eq)
  then show "x (+) c ` {y. a y = 0}"
  by blast
  qed
  have 2: "span ((λx. x - c) ` S) = {x. a x = 0}"
  if "(+) c ` span ((λx. x - c) ` S) = {x. a x = b}" for a b
  proof -
  have "b = a c"
  using span_0 that by fastforce
  with that have "(+) c ` span ((λx. x - c) ` S) = {x. a x = a c}"
  by simp
  then have "span ((λx. x - c) ` S) = (λx. x - c) ` {x. a x = a c}"
  by (metis (no_types) image_cong translation_galois uminus_add_conv_diff)
  also have "... = {x. a x = 0}"
  by (force simp: inner_distrib inner_diff_right
  intro: image_eqI [where x="x+c" for x])
  finally show ?thesis .
  qed
  have "?lhs = (a. a 0 span ((λx. x - c) ` S) = {x. a x = 0})"
  by (simp add: aff_dim_eq_dim [of c] c S hull_inc dim_eq_hyperplane del: One_nat_def)
  also have "... = ?rhs"
  by (fastforce simp add: affine_hull_span_gen [of c] c S hull_inc inner_distrib intro: xc_im intro!: 2)
  finally show ?thesis .
  qed
 qed
 
 corollary aff_dim_hyperplane [simp]:
  fixes a :: "'a::euclidean_space"
  shows "a 0 ==> aff_dim {x. a x = r} = DIM('a) - 1"
 by (metis aff_dim_eq_hyperplane affine_hull_eq affine_hyperplane)
 
 subsection🍋tag unimportant\Some stepping theorems
 
 lemma aff_dim_insert:
  fixes a :: "'a::euclidean_space"
  shows "aff_dim (insert a S) = (if a affine hull S then aff_dim S else aff_dim S + 1)"
 proof (cases "S = {}")
  case True then show ?thesis
  by simp
 next
  case False
  then obtain x s' where S: "S = insert x s'" "x s'"
  by (meson Set.set_insert all_not_in_conv)
  show ?thesis using S
  by (force simp add: affine_hull_insert_span_gen span_zero insert_commute [of a] aff_dim_eq_dim [of x] dim_insert)
 qed
 
 lemma affine_dependent_choose:
  fixes a :: "'a :: euclidean_space"
  assumes "¬(affine_dependent S)"
  shows "affine_dependent(insert a S) a S a affine hull S"
  (is "?lhs = ?rhs")
 proof safe
  assume "affine_dependent (insert a S)" and "a S"
  then show "False"
  using a S assms insert_absorb by fastforce
 next
  assume lhs: "affine_dependent (insert a S)"
  then have "a S"
  by (metis (no_types) assms insert_absorb)
  moreover have "finite S"
  using affine_independent_iff_card assms by blast
  moreover have "aff_dim (insert a S) int (card S)"
  using finite S affine_independent_iff_card a S lhs by fastforce
  ultimately show "a affine hull S"
  by (metis aff_dim_affine_independent aff_dim_insert assms)
 next
  assume "a S" and "a affine hull S"
  show "affine_dependent (insert a S)"
  by (simp add: a affine hull S a S affine_dependent_def)
 qed
 
 lemma affine_independent_insert:
  fixes a :: "'a :: euclidean_space"
  shows "[¬ affine_dependent S; a affine hull S] ==> ¬ affine_dependent(insert a S)"
  by (simp add: affine_dependent_choose)
 
 lemma subspace_bounded_eq_trivial:
  fixes S :: "'a::real_normed_vector set"
  assumes "subspace S"
  shows "bounded S S = {0}"
 proof -
  have "False" if "bounded S" "x S" "x 0" for x
  proof -
  obtain B where B: "y. y S ==> norm y 🚫" "B > 0"
  using bounded S by (force simp: bounded_pos_less)
  have "(B / norm x) *🪙R x S"
  using assms subspace_mul x S by auto
  moreover have "norm ((B / norm x) *🪙R x) = B"
  using that B by (simp add: algebra_simps)
  ultimately show False using B by force
  qed
  then have "bounded S ==> S = {0}"
  using assms subspace_0 by fastforce
  then show ?thesis
  by blast
 qed
 
 lemma affine_bounded_eq_trivial:
  fixes S :: "'a::real_normed_vector set"
  assumes "affine S"
  shows "bounded S S = {} (a. S = {a})"
 proof (cases "S = {}")
  case True then show ?thesis
  by simp
 next
  case False
  then obtain b where "b S" by blast
  with False assms
  have "bounded S ==> S = {b}"
  using affine_diffs_subspace [OF assms b S]
  by (metis (no_types, lifting) ab_group_add_class.ab_left_minus bounded_translation image_empty image_insert subspace_bounded_eq_trivial translation_invert)
  then show ?thesis by auto
 qed
 
 lemma affine_bounded_eq_lowdim:
  fixes S :: "'a::euclidean_space set"
  assumes "affine S"
  shows "bounded S aff_dim S 0"
 proof
  show "aff_dim S 0 ==> bounded S"
  by (metis aff_dim_sing aff_dim_subset affine_dim_equal affine_sing all_not_in_conv assms bounded_empty bounded_insert dual_order.antisym empty_subsetI insert_subset)
 qed (use affine_bounded_eq_trivial assms in fastforce)
 
 
 lemma bounded_hyperplane_eq_trivial_0:
  fixes a :: "'a::euclidean_space"
  assumes "a 0"
  shows "bounded {x. a x = 0} DIM('a) = 1"
 proof
  assume "bounded {x. a x = 0}"
  then have 0: "aff_dim {x. a x = 0} 0"
  by (simp add: affine_bounded_eq_lowdim affine_hyperplane)
  with assms 0
  have "int DIM('a) = 1"
  using order_neq_le_trans by fastforce
  then show "DIM('a) = 1" by auto
 next
  assume "DIM('a) = 1"
  then show "bounded {x. a x = 0}"
  by (simp add: affine_bounded_eq_lowdim affine_hyperplane assms)
 qed
 
 lemma bounded_hyperplane_eq_trivial:
  fixes a :: "'a::euclidean_space"
  shows "bounded {x. a x = r} (if a = 0 then r 0 else DIM('a) = 1)"
 proof -
  { assume "r 0" "a 0"
  have "aff_dim {x. y x = 0} = aff_dim {x. a x = r}" if "y 0" for y::'a
  by (metis that a 0 aff_dim_hyperplane)
  then have "bounded {x. a x = r} = (DIM('a) = Suc 0)"
  by (metis One_nat_def a 0 affine_bounded_eq_lowdim affine_hyperplane bounded_hyperplane_eq_trivial_0)
  }
  then show ?thesis
  by (auto simp: bounded_hyperplane_eq_trivial_0)
 qed
 
 subsection🍋tag unimportant\General case without assuming closure and getting non-strict separation
 
 proposition🍋tag unimportant separating_hyperplane_closed_point_inset:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "closed S" "S {}" "z S"
  obtains a b where "a S" "(a - z) z 🚫" "x. x S ==> b 🚫a - z) x"
 proof -
  obtain y where "y S" and y: "u. u S ==> dist z y dist z u"
  using distance_attains_inf [of S z] assms by auto
  then have *: "(y - z) z 🚫y - z) z + (norm (y - z))🪙2 / 2"
  using y S z S by auto
  show ?thesis
  proof (rule that [OF y S *])
  fix x
  assume "x S"
  have yz: "0 🚫y - z) (y - z)"
  using y S z S by auto
  { assume 0: "0 🚫(z - y) (x - y))"
  with any_closest_point_dot [OF convex S closed S]
  have False
  using y x S y S not_less by blast
  }
  then have "0 ((y - z) (x - y))"
  by (force simp: not_less inner_diff_left)
  with yz have "0 🚫 * ((y - z) (x - y)) + (y - z) (y - z)"
  by (simp add: algebra_simps)
  then show "(y - z) z + (norm (y - z))🪙2 / 2 🚫y - z) x"
  by (simp add: field_simps inner_diff_left inner_diff_right dot_square_norm [symmetric])
  qed
 qed
 
 lemma separating_hyperplane_closed_0_inset:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "closed S" "S {}" "0 S"
  obtains a b where "a S" "a 0" "0 🚫" "x. x S ==> a x > b"
  using separating_hyperplane_closed_point_inset [OF assms] by simp (metis 0 S)
 
 
 proposition🍋tag unimportant separating_hyperplane_set_0_inspan:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "S {}" "0 S"
  obtains a where "a span S" "a 0" "x. x S ==> 0 a x"
 proof -
  define k where [abs_def]: "k c = {x. 0 c x}" for c :: 'a
  have "span S frontier (cball 0 1) f' {}"
  if f': "finite f'" "f' k ` S" for f'
  proof -
  obtain C where "C S" "finite C" and C: "f' = k ` C"
  using finite_subset_image [OF f'] by blast
  obtain a where "a S" "a 0"
  using S {} 0 S ex_in_conv by blast
  then have "norm (a /🪙R (norm a)) = 1"
  by simp
  moreover have "a /🪙R (norm a) span S"
  by (simp add: a S span_scale span_base)
  ultimately have ass: "a /🪙R (norm a) span S sphere 0 1"
  by simp
  show ?thesis
  proof (cases "C = {}")
  case True with C ass show ?thesis
  by auto
  next
  case False
  have "closed (convex hull C)"
  using finite C compact_eq_bounded_closed finite_imp_compact_convex_hull by auto
  moreover have "convex hull C {}"
  by (simp add: False)
  moreover have "0 convex hull C"
  by (metis C S convex S 0 S convex_hull_subset hull_same insert_absorb insert_subset)
  ultimately obtain a b
  where "a convex hull C" "a 0" "0 🚫"
  and ab: "x. x convex hull C ==> a x > b"
  using separating_hyperplane_closed_0_inset by blast
  then have "a S"
  by (metis C S assms(1) subsetCE subset_hull)
  moreover have "norm (a /🪙R (norm a)) = 1"
  using a 0 by simp
  moreover have "a /🪙R (norm a) span S"
  by (simp add: a S span_scale span_base)
  ultimately have ass: "a /🪙R (norm a) span S sphere 0 1"
  by simp
  have "x. [a 0; x C] ==> 0 x a"
  using ab 0 🚫 by (metis hull_inc inner_commute less_eq_real_def less_trans)
  then have aa: "a /🪙R (norm a) (cC. {x. 0 c x})"
  by (auto simp add: field_split_simps)
  show ?thesis
  unfolding C k_def
  using ass aa Int_iff empty_iff by force
  qed
  qed
  moreover have "T. T k ` S ==> closed T"
  using closed_halfspace_ge k_def by blast
  ultimately have "(span S frontier(cball 0 1)) ( (k ` S)) {}"
  by (metis compact_imp_fip closed_Int_compact closed_span compact_cball compact_frontier)
  then show ?thesis
  unfolding set_eq_iff k_def
  by simp (metis inner_commute norm_eq_zero that zero_neq_one)
 qed
 
 
 lemma separating_hyperplane_set_point_inaff:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "S {}" and zno: "z S"
  obtains a b where "(z + a) affine hull (insert z S)"
  and "a 0" and "a z b"
  and "x. x S ==> a x b"
 proof -
  from separating_hyperplane_set_0_inspan [of "image (λx. -z + x) S"]
  have "convex ((+) (- z) ` S)"
  using convex S by simp
  moreover have "(+) (- z) ` S {}"
  by (simp add: S {})
  moreover have "0 (+) (- z) ` S"
  using zno by auto
  ultimately obtain a where "a span ((+) (- z) ` S)" "a 0"
  and a: "x. x ((+) (- z) ` S) ==> 0 a x"
  using separating_hyperplane_set_0_inspan [of "image (λx. -z + x) S"]
  by blast
  then have szx: "x. x S ==> a z a x"
  by (metis (no_types, lifting) imageI inner_minus_right inner_right_distrib minus_add neg_le_0_iff_le neg_le_iff_le real_add_le_0_iff)
  moreover
  have "z + a affine hull insert z S"
  using a span ((+) (- z) ` S) affine_hull_insert_span_gen by blast
  ultimately show ?thesis
  using a 0 szx that by auto
 qed
 
 proposition🍋tag unimportant supporting_hyperplane_rel_boundary:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "x S" and xno: "x rel_interior S"
  obtains a where "a 0"
  and "y. y S ==> a x a y"
  and "y. y rel_interior S ==> a x 🚫 y"
 proof -
  obtain a b where aff: "(x + a) affine hull (insert x (rel_interior S))"
  and "a 0" and "a x b"
  and ageb: "u. u (rel_interior S) ==> a u b"
  using separating_hyperplane_set_point_inaff [of "rel_interior S" x] assms
  by (auto simp: rel_interior_eq_empty convex_rel_interior)
  have le_ay: "a x a y" if "y S" for y
  proof -
  have con: "continuous_on (closure (rel_interior S)) (() a)"
  by (rule continuous_intros continuous_on_subset | blast)+
  have y: "y closure (rel_interior S)"
  using convex S closure_def convex_closure_rel_interior y S
  by fastforce
  show ?thesis
  using continuous_ge_on_closure [OF con y] ageb a x b
  by fastforce
  qed
  have 3: "a x 🚫 y" if "y rel_interior S" for y
  proof -
  obtain e where "0 🚫" "y S" and e: "cball y e affine hull S S"
  using y rel_interior S by (force simp: rel_interior_cball)
  define y' where "y' = y - (e / norm a) *🪙R ((x + a) - x)"
  have "y' cball y e"
  unfolding y'_def using 0 🚫 by force
  moreover have "y' affine hull S"
  unfolding y'_def
  by (metis x S y S convex S aff affine_affine_hull hull_redundant
  rel_interior_same_affine_hull hull_inc mem_affine_3_minus2)
  ultimately have "y' S"
  using e by auto
  have "a x a y"
  using le_ay a 0 y S by blast
  moreover have "a x a y"
  using le_ay [OF y' S] a 0 0 🚫 not_le
  by (fastforce simp add: y'_def inner_diff dot_square_norm power2_eq_square)
  ultimately show ?thesis by force
  qed
  show ?thesis
  by (rule that [OF a 0 le_ay 3])
 qed
 
 lemma supporting_hyperplane_relative_frontier:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "x closure S" "x rel_interior S"
  obtains a where "a 0"
  and "y. y closure S ==> a x a y"
  and "y. y rel_interior S ==> a x 🚫 y"
 using supporting_hyperplane_rel_boundary [of "closure S" x]
 by (metis assms convex_closure convex_rel_interior_closure)
 
 
 subsection🍋tag unimportant\ Some results on decomposing convex hulls: intersections, simplicial subdivision
 
 lemma
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent(S T)"
  shows convex_hull_Int_subset: "convex hull S convex hull T convex hull (S T)" (is ?C)
  and affine_hull_Int_subset: "affine hull S affine hull T affine hull (S T)" (is ?A)
 proof -
  have [simp]: "finite S" "finite T"
  using aff_independent_finite assms by blast+
  have "sum u (S T) = 1
  (vS T. u v *🪙R v) = (vS. u v *🪙R v)"
  if [simp]: "sum u S = 1"
  "sum v T = 1"
  and eq: "(xT. v x *🪙R x) = (xS. u x *🪙R x)" for u v
  proof -
  define f where "f x = (if x S then u x else 0) - (if x T then v x else 0)" for x
  have "sum f (S T) = 0"
  by (simp add: f_def sum_Un sum_subtractf flip: sum.inter_restrict)
  moreover have "(x(S T). f x *🪙R x) = 0"
  by (simp add: eq f_def sum_Un scaleR_left_diff_distrib sum_subtractf if_smult flip: sum.inter_restrict cong: if_cong)
  ultimately have "v. v S T ==> f v = 0"
  using aff_independent_finite assms unfolding affine_dependent_explicit
  by blast
  then have u [simp]: "x. x S ==> u x = (if x T then v x else 0)"
  by (simp add: f_def) presburger
  have "sum u (S T) = sum u S"
  by (simp add: sum.inter_restrict)
  then have "sum u (S T) = 1"
  using that by linarith
  moreover have "(vS T. u v *🪙R v) = (vS. u v *🪙R v)"
  by (auto simp: sum.inter_restrict intro: sum.cong)
  ultimately show ?thesis
  by force
  qed
  then show ?A ?C
  by (auto simp: convex_hull_finite affine_hull_finite)
 qed
 
 
 proposition🍋tag unimportant affine_hull_Int:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent(S T)"
  shows "affine hull (S T) = affine hull S affine hull T"
  by (simp add: affine_hull_Int_subset assms hull_mono subset_antisym)
 
 proposition🍋tag unimportant convex_hull_Int:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent(S T)"
  shows "convex hull (S T) = convex hull S convex hull T"
  by (simp add: convex_hull_Int_subset assms hull_mono subset_antisym)
 
 proposition🍋tag unimportant
  fixes S :: "'a::euclidean_space set set"
  assumes "¬ affine_dependent (S)"
  shows affine_hull_Inter: "affine hull (S) = (TS. affine hull T)" (is "?A")
  and convex_hull_Inter: "convex hull (S) = (TS. convex hull T)" (is "?C")
 proof -
  have "finite S"
  using aff_independent_finite assms finite_UnionD by blast
  then have "?A ?C" using assms
  proof (induction S rule: finite_induct)
  case empty then show ?case by auto
  next
  case (insert T F)
  then show ?case
  proof (cases "F={}")
  case True then show ?thesis by simp
  next
  case False
  with "insert.prems" have [simp]: "¬ affine_dependent (T F)"
  by (auto intro: affine_dependent_subset)
  have [simp]: "¬ affine_dependent (F)"
  using affine_independent_subset insert.prems by fastforce
  show ?thesis
  by (simp add: affine_hull_Int convex_hull_Int insert.IH)
  qed
  qed
  then show "?A" "?C"
  by auto
 qed
 
 proposition🍋tag unimportant in_convex_hull_exchange_unique:
  fixes S :: "'a::euclidean_space set"
  assumes naff: "¬ affine_dependent S" and a: "a convex hull S"
  and S: "T S" "T' S"
  and x: "x convex hull (insert a T)"
  and x': "x convex hull (insert a T')"
  shows "x convex hull (insert a (T T'))"
 proof (cases "a S")
  case True
  then have "¬ affine_dependent (insert a T insert a T')"
  using affine_dependent_subset assms by auto
  then have "x convex hull (insert a T insert a T')"
  by (metis IntI convex_hull_Int x x')
  then show ?thesis
  by simp
 next
  case False
  then have anot: "a T" "a T'"
  using assms by auto
  have [simp]: "finite S"
  by (simp add: aff_independent_finite assms)
  then obtain b where b0: "s. s S ==> 0 b s"
  and b1: "sum b S = 1" and aeq: "a = (sS. b s *🪙R s)"
  using a by (auto simp: convex_hull_finite)
  have fin [simp]: "finite T" "finite T'"
  using assms infinite_super finite S by blast+
  then obtain c c' where c0: "t. t insert a T ==> 0 c t"
  and c1: "sum c (insert a T) = 1"
  and xeq: "x = (t insert a T. c t *🪙R t)"
  and c'0: "t. t insert a T' ==> 0 c' t"
  and c'1: "sum c' (insert a T') = 1"
  and x'eq: "x = (t insert a T'. c' t *🪙R t)"
  using x x' by (auto simp: convex_hull_finite)
  with fin anot
  have sumTT': "sum c T = 1 - c a" "sum c' T' = 1 - c' a"
  and wsumT: "(t T. c t *🪙R t) = x - c a *🪙R a"
  by simp_all
  have wsumT': "(t T'. c' t *🪙R t) = x - c' a *🪙R a"
  using x'eq fin anot by simp
  define cc where "cc λx. if x T then c x else 0"
  define cc' where "cc' λx. if x T' then c' x else 0"
  define dd where "dd λx. cc x - cc' x + (c a - c' a) * b x"
  have sumSS': "sum cc S = 1 - c a" "sum cc' S = 1 - c' a"
  unfolding cc_def cc'_def using S
  by (simp_all add: Int_absorb1 Int_absorb2 sum_subtractf sum.inter_restrict [symmetric] sumTT')
  have wsumSS: "(t S. cc t *🪙R t) = x - c a *🪙R a" "(t S. cc' t *🪙R t) = x - c' a *🪙R a"
  unfolding cc_def cc'_def using S
  by (simp_all add: Int_absorb1 Int_absorb2 if_smult sum.inter_restrict [symmetric] wsumT wsumT' cong: if_cong)
  have sum_dd0: "sum dd S = 0"
  unfolding dd_def using S
  by (simp add: sumSS' comm_monoid_add_class.sum.distrib sum_subtractf
  algebra_simps sum_distrib_right [symmetric] b1)
  have "(vS. (b v * x) *🪙R v) = x *🪙R (vS. b v *🪙R v)" for x
  by (simp add: pth_5 real_vector.scale_sum_right mult.commute)
  then have *: "(vS. (b v * x) *🪙R v) = x *🪙R a" for x
  using aeq by blast
  have "(v S. dd v *🪙R v) = 0"
  unfolding dd_def using S
  by (simp add: * wsumSS sum.distrib sum_subtractf algebra_simps)
  then have dd0: "dd v = 0" if "v S" for v
  using naff [unfolded affine_dependent_explicit not_ex, rule_format, of S dd]
  using that sum_dd0 by force
  consider "c' a c a" | "c a c' a" by linarith
  then show ?thesis
  proof cases
  case 1
  then have "sum cc S sum cc' S"
  by (simp add: sumSS')
  then have le: "cc x cc' x" if "x S" for x
  using dd0 [OF that] 1 b0 mult_left_mono that
  by (fastforce simp add: dd_def algebra_simps)
  have cc0: "cc x = 0" if "x S" "x T T'" for x
  using le [OF x S] that c0
  by (force simp: cc_def cc'_def split: if_split_asm)
  have ge0: "xT T'. 0 (cc(a := c a)) x"
  by (simp add: c0 cc_def)
  have "sum (cc(a := c a)) (insert a (T T')) = c a + sum (cc(a := c a)) (T T')"
  by (simp add: anot)
  also have "... = c a + sum (cc(a := c a)) S"
  using T S False cc0 cc_def a S by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
  also have "... = c a + (1 - c a)"
  by (metis a S fun_upd_other sum.cong sumSS'(1))
  finally have 1: "sum (cc(a := c a)) (insert a (T T')) = 1"
  by simp
  have "(xinsert a (T T'). (cc(a := c a)) x *🪙R x) = c a *🪙R a + (x T T'. (cc(a := c a)) x *🪙R x)"
  by (simp add: anot)
  also have "... = c a *🪙R a + (x S. (cc(a := c a)) x *🪙R x)"
  using T S False cc0 by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
  also have "... = c a *🪙R a + x - c a *🪙R a"
  by (simp add: wsumSS a S if_smult sum_delta_notmem)
  finally have self: "(xinsert a (T T'). (cc(a := c a)) x *🪙R x) = x"
  by simp
  show ?thesis
  by (force simp: convex_hull_finite c0 intro!: ge0 1 self exI [where x = "cc(a := c a)"])
  next
  case 2
  then have "sum cc' S sum cc S"
  by (simp add: sumSS')
  then have le: "cc' x cc x" if "x S" for x
  using dd0 [OF that] 2 b0 mult_left_mono that
  by (fastforce simp add: dd_def algebra_simps)
  have cc0: "cc' x = 0" if "x S" "x T T'" for x
  using le [OF x S] that c'0
  by (force simp: cc_def cc'_def split: if_split_asm)
  have ge0: "xT T'. 0 (cc'(a := c' a)) x"
  by (simp add: c'0 cc'_def)
  have "sum (cc'(a := c' a)) (insert a (T T')) = c' a + sum (cc'(a := c' a)) (T T')"
  by (simp add: anot)
  also have "... = c' a + sum (cc'(a := c' a)) S"
  using T S False cc0 by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
  also have "... = c' a + (1 - c' a)"
  by (metis a S fun_upd_other sum.cong sumSS')
  finally have 1: "sum (cc'(a := c' a)) (insert a (T T')) = 1"
  by simp
  have "(xinsert a (T T'). (cc'(a := c' a)) x *🪙R x) = c' a *🪙R a + (x T T'. (cc'(a := c' a)) x *🪙R x)"
  by (simp add: anot)
  also have "... = c' a *🪙R a + (x S. (cc'(a := c' a)) x *🪙R x)"
  using T S False cc0 by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
  also have "... = c a *🪙R a + x - c a *🪙R a"
  by (simp add: wsumSS a S if_smult sum_delta_notmem)
  finally have self: "(xinsert a (T T'). (cc'(a := c' a)) x *🪙R x) = x"
  by simp
  show ?thesis
  by (force simp: convex_hull_finite c'0 intro!: ge0 1 self exI [where x = "cc'(a := c' a)"])
  qed
 qed
 
 corollary🍋tag unimportant convex_hull_exchange_Int:
  fixes a :: "'a::euclidean_space"
  assumes "¬ affine_dependent S" "a convex hull S" "T S" "T' S"
  shows "(convex hull (insert a T)) (convex hull (insert a T')) =
  convex hull (insert a (T T'))" (is "?lhs = ?rhs")
 proof (rule subset_antisym)
  show "?lhs ?rhs"
  using in_convex_hull_exchange_unique assms by blast
  show "?rhs ?lhs"
  by (metis hull_mono inf_le1 inf_le2 insert_inter_insert le_inf_iff)
 qed
 
 lemma Int_closed_segment:
  fixes b :: "'a::euclidean_space"
  assumes "b closed_segment a c ¬ collinear{a,b,c}"
  shows "closed_segment a b closed_segment b c = {b}"
 proof (cases "c = a")
  case True
  then show ?thesis
  using assms collinear_3_eq_affine_dependent by fastforce
 next
  case False
  from assms show ?thesis
  proof
  assume "b closed_segment a c"
  moreover have "¬ affine_dependent {a, c}"
  by (simp)
  ultimately show ?thesis
  using False convex_hull_exchange_Int [of "{a,c}" b "{a}" "{c}"]
  by (simp add: segment_convex_hull insert_commute)
  next
  assume ncoll: "¬ collinear {a, b, c}"
  have False if "closed_segment a b closed_segment b c {b}"
  proof -
  have "b closed_segment a b" and "b closed_segment b c"
  by auto
  with that obtain d where "b d" "d closed_segment a b" "d closed_segment b c"
  by force
  then have d: "collinear {a, d, b}" "collinear {b, d, c}"
  by (auto simp: between_mem_segment between_imp_collinear)
  have "collinear {a, b, c}"
  by (metis (full_types) b d collinear_3_trans d insert_commute)
  with ncoll show False ..
  qed
  then show ?thesis
  by blast
  qed
 qed
 
 lemma affine_hull_finite_intersection_hyperplanes:
  fixes S :: "'a::euclidean_space set"
  obtains F where
  "finite F"
  "of_nat (card F) + aff_dim S = DIM('a)"
  "affine hull S = F"
  "h. h F ==> a b. a 0 h = {x. a x = b}"
 proof -
  obtain b where "b S"
  and indb: "¬ affine_dependent b"
  and eq: "affine hull S = affine hull b"
  using affine_basis_exists by blast
  obtain c where indc: "¬ affine_dependent c" and "b c"
  and affc: "affine hull c = UNIV"
  by (metis extend_to_affine_basis affine_UNIV hull_same indb subset_UNIV)
  then have "finite c"
  by (simp add: aff_independent_finite)
  then have fbc: "finite b" "card b card c"
  using b c infinite_super by (auto simp: card_mono)
  have imeq: "(λx. affine hull x) ` ((λa. c - {a}) ` (c - b)) = ((λa. affine hull (c - {a})) ` (c - b))"
  by blast
  have card_cb: "(card (c - b)) + aff_dim S = DIM('a)"
  proof -
  have aff: "aff_dim (UNIV::'a set) = aff_dim c"
  by (metis aff_dim_affine_hull affc)
  have "aff_dim b = aff_dim S"
  by (metis (no_types) aff_dim_affine_hull eq)
  then have "int (card b) = 1 + aff_dim S"
  by (simp add: aff_dim_affine_independent indb)
  then show ?thesis
  using fbc aff
  by (simp add: ¬ affine_dependent c b c aff_dim_affine_independent card_Diff_subset of_nat_diff)
  qed
  show ?thesis
  proof (cases "c = b")
  case True show ?thesis
  proof
  show "int (card {}) + aff_dim S = int DIM('a)"
  using True card_cb by auto
  show "affine hull S = {}"
  using True affc eq by blast
  qed auto
  next
  case False
  have ind: "¬ affine_dependent (ac - b. c - {a})"
  by (rule affine_independent_subset [OF indc]) auto
  have *: "1 + aff_dim (c - {t}) = int (DIM('a))" if t: "t c" for t
  proof -
  have "insert t c = c"
  using t by blast
  then show ?thesis
  by (metis (full_types) add.commute aff_dim_affine_hull aff_dim_insert aff_dim_UNIV affc affine_dependent_def indc insert_Diff_single t)
  qed
  let ?F = "(λx. affine hull x) ` ((λa. c - {a}) ` (c - b))"
  show ?thesis
  proof
  have "card ((λa. affine hull (c - {a})) ` (c - b)) = card (c - b)"
  proof (rule card_image)
  show "inj_on (λa. affine hull (c - {a})) (c - b)"
  unfolding inj_on_def
  by (metis Diff_eq_empty_iff Diff_iff indc affine_dependent_def hull_subset insert_iff)
  qed
  then show "int (card ?F) + aff_dim S = int DIM('a)"
  by (simp add: imeq card_cb)
  show "affine hull S = ?F"
  by (metis Diff_eq_empty_iff INT_simps(4) UN_singleton order_refl b c False eq double_diff affine_hull_Inter [OF ind])
  have "a. [a c; a b] ==> aff_dim (c - {a}) = int (DIM('a) - Suc 0)"
  by (metis "*" DIM_ge_Suc0 One_nat_def add_diff_cancel_left' int_ops(2) of_nat_diff)
  then show "h. h ?F ==> a b. a 0 h = {x. a x = b}"
  by (auto simp only: One_nat_def aff_dim_eq_hyperplane [symmetric])
  qed (use finite c in auto)
  qed
 qed
 
 lemma affine_hyperplane_sums_eq_UNIV_0:
  fixes S :: "'a :: euclidean_space set"
  assumes "affine S"
  and "0 S" and "w S"
  and "a w 0"
  shows "{x + y| x y. x S a y = 0} = UNIV"
 proof -
  have "subspace S"
  by (simp add: assms subspace_affine)
  have span1: "span {y. a y = 0} span {x + y |x y. x S a y = 0}"
  using 0 S add.left_neutral by (intro span_mono) force
  have "w span {y. a y = 0}"
  using a w 0 span_induct subspace_hyperplane by auto
  moreover have "w span {x + y |x y. x S a y = 0}"
  using w S
  by (metis (mono_tags, lifting) inner_zero_right mem_Collect_eq pth_d span_base)
  ultimately have span2: "span {y. a y = 0} span {x + y |x y. x S a y = 0}"
  by blast
  have "a 0" using assms inner_zero_left by blast
  then have "DIM('a) - 1 = dim {y. a y = 0}"
  by (simp add: dim_hyperplane)
  also have "... 🚫 {x + y |x y. x S a y = 0}"
  using span1 span2 by (blast intro: dim_psubset)
  finally have "DIM('a) - 1 🚫 {x + y |x y. x S a y = 0}" .
  then have DD: "dim {x + y |x y. x S a y = 0} = DIM('a)"
  using antisym dim_subset_UNIV lowdim_subset_hyperplane not_le by fastforce
  have subs: "subspace {x + y| x y. x S a y = 0}"
  using subspace_sums [OF subspace S subspace_hyperplane] by simp
  moreover have "span {x + y| x y. x S a y = 0} = UNIV"
  using DD dim_eq_full by blast
  ultimately show ?thesis
  by (simp add: subs) (metis (lifting) span_eq_iff subs)
 qed
 
 proposition🍋tag unimportant affine_hyperplane_sums_eq_UNIV:
  fixes S :: "'a :: euclidean_space set"
  assumes "affine S"
  and "S {v. a v = b} {}"
  and "S - {v. a v = b} {}"
  shows "{x + y| x y. x S a y = b} = UNIV"
 proof (cases "a = 0")
  case True with assms show ?thesis
  by (auto simp: if_splits)
 next
  case False
  obtain c where "c S" and c: "a c = b"
  using assms by force
  with affine_diffs_subspace [OF affine S]
  have "subspace ((+) (- c) ` S)" by blast
  then have aff: "affine ((+) (- c) ` S)"
  by (simp add: subspace_imp_affine)
  have 0: "0 (+) (- c) ` S"
  by (simp add: c S)
  obtain d where "d S" and "a d b" and dc: "d-c (+) (- c) ` S"
  using assms by auto
  then have adc: "a (d - c) 0"
  by (simp add: c inner_diff_right)
  define U where "U {x + y |x y. x (+) (- c) ` S a y = 0}"
  have "u + v (+) (c+c) ` U"
  if "u S" "b = a v" for u v
  proof
  show "u + v = c + c + (u + v - c - c)"
  by (simp add: algebra_simps)
  have "x y. u + v - c - c = x + y (xaS. x = xa - c) a y = 0"
  proof (intro exI conjI)
  show "u + v - c - c = (u-c) + (v-c)" "a (v - c) = 0"
  by (simp_all add: algebra_simps c that)
  qed (use that in auto)
  then show "u + v - c - c U"
  by (auto simp: U_def image_def)
  qed
  moreover have "[a v = 0; u S]
  ==> x ya. v + (u + c) = x + ya x S a ya = b" for v u
  by (metis add.left_commute c inner_right_distrib pth_d)
  ultimately have "{x + y |x y. x S a y = b} = (+) (c+c) ` U"
  by (fastforce simp: algebra_simps U_def)
  also have "... = range ((+) (c + c))"
  by (simp only: U_def affine_hyperplane_sums_eq_UNIV_0 [OF aff 0 dc adc])
  also have "... = UNIV"
  by simp
  finally show ?thesis .
 qed
 
 lemma aff_dim_sums_Int_0:
  assumes "affine S"
  and "affine T"
  and "0 S" "0 T"
  shows "aff_dim {x + y| x y. x S y T} = (aff_dim S + aff_dim T) - aff_dim(S T)"
 proof -
  have "0 {x + y |x y. x S y T}"
  using assms by force
  then have 0: "0 affine hull {x + y |x y. x S y T}"
  by (metis (lifting) hull_inc)
  have sub: "subspace S" "subspace T"
  using assms by (auto simp: subspace_affine)
  show ?thesis
  using dim_sums_Int [OF sub] by (simp add: aff_dim_zero assms 0 hull_inc)
 qed
 
 proposition aff_dim_sums_Int:
  assumes "affine S"
  and "affine T"
  and "S T {}"
  shows "aff_dim {x + y| x y. x S y T} = (aff_dim S + aff_dim T) - aff_dim(S T)"
 proof -
  obtain a where a: "a S" "a T" using assms by force
  have aff: "affine ((+) (-a) ` S)" "affine ((+) (-a) ` T)"
  using affine_translation [symmetric, of "- a"] assms by (simp_all cong: image_cong_simp)
  have zero: "0 ((+) (-a) ` S)" "0 ((+) (-a) ` T)"
  using a assms by auto
  have "{x + y |x y. x (+) (- a) ` S y (+) (- a) ` T} =
  (+) (- 2 *🪙R a) ` {x + y| x y. x S y T}"
  by (force simp: algebra_simps scaleR_2)
  moreover have "(+) (- a) ` S (+) (- a) ` T = (+) (- a) ` (S T)"
  by auto
  ultimately show ?thesis
  using aff_dim_sums_Int_0 [OF aff zero] aff_dim_translation_eq
  by (metis (lifting))
 qed
 
 lemma aff_dim_affine_Int_hyperplane:
  fixes a :: "'a::euclidean_space"
  assumes "affine S"
  shows "aff_dim(S {x. a x = b}) =
  (if S {v. a v = b} = {} then - 1
  else if S {v. a v = b} then aff_dim S
  else aff_dim S - 1)"
 proof (cases "a = 0")
  case True with assms show ?thesis
  by auto
 next
  case False
  then have "aff_dim (S {x. a x = b}) = aff_dim S - 1"
  if "x S" "a x b" and non: "S {v. a v = b} {}" for x
  proof -
  have [simp]: "{x + y| x y. x S a y = b} = UNIV"
  using affine_hyperplane_sums_eq_UNIV [OF assms non] that by blast
  show ?thesis
  using aff_dim_sums_Int [OF assms affine_hyperplane non]
  by (simp add: of_nat_diff False)
  qed
  then show ?thesis
  by (metis (mono_tags, lifting) inf.orderE aff_dim_empty_eq mem_Collect_eq subsetI)
 qed
 
 lemma aff_dim_lt_full:
  fixes S :: "'a::euclidean_space set"
  shows "aff_dim S 🚫('a) (affine hull S UNIV)"
 by (metis (no_types) aff_dim_affine_hull aff_dim_le_DIM aff_dim_UNIV affine_hull_UNIV less_le)
 
 lemma aff_dim_openin:
  fixes S :: "'a::euclidean_space set"
  assumes ope: "openin (top_of_set T) S" and "affine T" "S {}"
  shows "aff_dim S = aff_dim T"
 proof -
  show ?thesis
  proof (rule order_antisym)
  show "aff_dim S aff_dim T"
  by (blast intro: aff_dim_subset [OF openin_imp_subset] ope)
  next
  obtain a where "a S"
  using S {} by blast
  have "S T"
  using ope openin_imp_subset by auto
  then have "a T"
  using a S by auto
  then have subT': "subspace ((λx. - a + x) ` T)"
  using affine_diffs_subspace affine T by auto
  then obtain B where Bsub: "B ((λx. - a + x) ` T)" and po: "pairwise orthogonal B"
  and eq1: "x. x B ==> norm x = 1" and "independent B"
  and cardB: "card B = dim ((λx. - a + x) ` T)"
  and spanB: "span B = ((λx. - a + x) ` T)"
  by (rule orthonormal_basis_subspace) auto
  obtain e where "0 🚫" and e: "cball a e T S"
  by (meson a S openin_contains_cball ope)
  have "aff_dim T = aff_dim ((λx. - a + x) ` T)"
  by (metis aff_dim_translation_eq)
  also have "... = dim ((λx. - a + x) ` T)"
  using aff_dim_subspace subT' by blast
  also have "... = card B"
  by (simp add: cardB)
  also have "... = card ((λx. e *🪙R x) ` B)"
  using 0 🚫 by (force simp: inj_on_def card_image)
  also have "... dim ((λx. - a + x) ` S)"
  proof -
  have e': "cball 0 e (λx. x - a) ` T (λx. x - a) ` S"
  using e by (auto simp: dist_norm norm_minus_commute subset_eq)
  have "(λx. e *🪙R x) ` B cball 0 e (λx. x - a) ` T"
  using Bsub 0 🚫 eq1 subT' a T by (auto simp: subspace_def)
  then have "(λx. e *🪙R x) ` B (λx. x - a) ` S"
  using e' by blast
  moreover
  have "inj_on ((*🪙R) e) (span B)"
  using 0 🚫 inj_on_def by fastforce
  then have "independent ((λx. e *🪙R x) ` B)"
  using linear_scale_self independent B linear_dependent_inj_imageD by blast
  ultimately show ?thesis
  by (auto simp: intro!: independent_card_le_dim)
  qed
  also have "... = aff_dim S"
  using a S aff_dim_eq_dim hull_inc by (force cong: image_cong_simp)
  finally show "aff_dim T aff_dim S" .
  qed
 qed
 
 lemma dim_openin:
  fixes S :: "'a::euclidean_space set"
  assumes ope: "openin (top_of_set T) S" and "subspace T" "S {}"
  shows "dim S = dim T"
 proof (rule order_antisym)
  show "dim S dim T"
  by (metis ope dim_subset openin_subset topspace_euclidean_subtopology)
 next
  have "dim T = aff_dim S"
  using aff_dim_openin
  by (metis aff_dim_subspace subspace T S {} ope subspace_affine)
  also have "... dim S"
  by (metis aff_dim_subset aff_dim_subspace dim_span span_superset
  subspace_span)
  finally show "dim T dim S" by simp
 qed
 
 subsectionLower-dimensional affine subsets are nowhere dense
 
 proposition dense_complement_subspace:
  fixes S :: "'a :: euclidean_space set"
  assumes dim_less: "dim T 🚫 S" and "subspace S" shows "closure(S - T) = S"
 proof -
  have "closure(S - U) = S" if "dim U 🚫 S" "U S" for U
  proof -
  have "span U span S"
  by (metis neq_iff psubsetI span_eq_dim span_mono that)
  then obtain a where "a 0" "a span S" and a: "y. y span U ==> orthogonal a y"
  using orthogonal_to_subspace_exists_gen by metis
  show ?thesis
  proof
  have "closed S"
  by (simp add: subspace S closed_subspace)
  then show "closure (S - U) S"
  by (simp add: closure_minimal)
  show "S closure (S - U)"
  proof (clarsimp simp: closure_approachable)
  fix x and e::real
  assume "x S" "0 🚫"
  show "yS - U. dist y x 🚫"
  proof (cases "x U")
  case True
  let ?y = "x + (e/2 / norm a) *🪙R a"
  show ?thesis
  proof
  show "dist ?y x 🚫"
  using 0 🚫 by (simp add: dist_norm)
  next
  have "?y S"
  by (metis a span S x S assms(2) span_eq_iff subspace_add subspace_scale)
  moreover have "?y U"
  proof -
  have "e/2 / norm a 0"
  using 0 🚫 a 0 by auto
  then show ?thesis
  by (metis True a 0 a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_base)
  qed
  ultimately show "?y S - U" by blast
  qed
  next
  case False
  with 0 🚫 x S show ?thesis by force
  qed
  qed
  qed
  qed
  moreover have "S - S T = S-T"
  by blast
  moreover have "dim (S T) 🚫 S"
  by (metis dim_less dim_subset inf.cobounded2 inf.orderE inf.strict_boundedE not_le)
  ultimately show ?thesis
  by force
 qed
 
 corollary🍋tag unimportant dense_complement_affine:
  fixes S :: "'a :: euclidean_space set"
  assumes less: "aff_dim T 🚫 S" and "affine S" shows "closure(S - T) = S"
 proof (cases "S T = {}")
  case True
  then show ?thesis
  by (metis Diff_triv affine_hull_eq affine S closure_same_affine_hull closure_subset hull_subset subset_antisym)
 next
  case False
  then obtain z where z: "z S T" by blast
  then have "subspace ((+) (- z) ` S)"
  by (meson IntD1 affine_diffs_subspace affine S)
  moreover have "int (dim ((+) (- z) ` T)) 🚫 (dim ((+) (- z) ` S))"
 thm aff_dim_eq_dim
  using z less by (simp add: aff_dim_eq_dim_subtract [of z] hull_inc cong: image_cong_simp)
  ultimately have "closure(((+) (- z) ` S) - ((+) (- z) ` T)) = ((+) (- z) ` S)"
  by (simp add: dense_complement_subspace)
  then show ?thesis
  by (metis closure_translation translation_diff translation_invert)
 qed
 
 corollary🍋tag unimportant dense_complement_openin_affine_hull:
  fixes S :: "'a :: euclidean_space set"
  assumes less: "aff_dim T 🚫 S"
  and ope: "openin (top_of_set (affine hull S)) S"
  shows "closure(S - T) = closure S"
 proof -
  have "affine hull S - T affine hull S"
  by blast
  then have "closure (S closure (affine hull S - T)) = closure (S (affine hull S - T))"
  by (rule closure_openin_Int_closure [OF ope])
  then show ?thesis
  by (metis Int_Diff aff_dim_affine_hull affine_affine_hull dense_complement_affine hull_subset inf.orderE less)
 qed
 
 corollary🍋tag unimportant dense_complement_convex:
  fixes S :: "'a :: euclidean_space set"
  assumes "aff_dim T 🚫 S" "convex S"
  shows "closure(S - T) = closure S"
 proof
  show "closure (S - T) closure S"
  by (simp add: closure_mono)
  have "closure (rel_interior S - T) = closure (rel_interior S)"
  by (simp add: assms dense_complement_openin_affine_hull openin_rel_interior rel_interior_aff_dim rel_interior_same_affine_hull)
  then show "closure S closure (S - T)"
  by (metis Diff_mono convex S closure_mono convex_closure_rel_interior order_refl rel_interior_subset)
 qed
 
 corollary🍋tag unimportant dense_complement_convex_closed:
  fixes S :: "'a :: euclidean_space set"
  assumes "aff_dim T 🚫 S" "convex S" "closed S"
  shows "closure(S - T) = S"
  by (simp add: assms dense_complement_convex)
 
 
 subsection🍋tag unimportant\Parallel slices, etc
 
 text If we take a slice out of a set, we can do it perpendicularly,
  with the normal vector to the slice parallel to the affine hull.
 
 proposition🍋tag unimportant affine_parallel_slice:
  fixes S :: "'a :: euclidean_space set"
  assumes "affine S"
  and "S {x. a x b} {}"
  and "¬ (S {x. a x b})"
  obtains a' b' where "a' 0"
  "S {x. a' x b'} = S {x. a x b}"
  "S {x. a' x = b'} = S {x. a x = b}"
  "w. w S ==> (w + a') S"
 proof (cases "S {x. a x = b} = {}")
  case True
  then obtain u v where "u S" "v S" "a u b" "a v > b"
  using assms by (auto simp: not_le)
  define 🪙 where "🪙 = u + ((b - a u) / (a v - a u)) *🪙R (v - u)"
  have "🪙 S"
  by (simp add: 🪙_def u S v S affine S mem_affine_3_minus)
  moreover have "a 🪙 = b"
  using a u b b 🚫 v
  by (simp add: 🪙_def algebra_simps) (simp add: field_simps)
  ultimately have False
  using True by force
  then show ?thesis ..
 next
  case False
  then obtain z where "z S" and z: "a z = b"
  using assms by auto
  with affine_diffs_subspace [OF affine S]
  have sub: "subspace ((+) (- z) ` S)" by blast
  then have aff: "affine ((+) (- z) ` S)" and span: "span ((+) (- z) ` S) = ((+) (- z) ` S)"
  by (auto simp: subspace_imp_affine)
  obtain a' a'' where a': "a' span ((+) (- z) ` S)" and a: "a = a' + a''"
  and "w. w span ((+) (- z) ` S) ==> orthogonal a'' w"
  using orthogonal_subspace_decomp_exists [of "(+) (- z) ` S" "a"] by metis
  then have "w. w S ==> a'' (w-z) = 0"
  by (simp add: span_base orthogonal_def)
  then have a'': "w. w S ==> a'' w = (a - a') z"
  by (simp add: a inner_diff_right)
  then have ba'': "w. w S ==> a'' w = b - a' z"
  by (simp add: inner_diff_left z)
  show ?thesis
  proof (cases "a' = 0")
  case True
  with a assms True a'' diff_zero less_irrefl show ?thesis
  by auto
  next
  case False
  show ?thesis
  proof
  show "S {x. a' x a' z} = S {x. a x b}"
  "S {x. a' x = a' z} = S {x. a x = b}"
  by (auto simp: a ba'' inner_left_distrib)
  have "w. w (+) (- z) ` S ==> (w + a') (+) (- z) ` S"
  by (metis subspace_add a' span_eq_iff sub)
  then show "w. w S ==> (w + a') S"
  by fastforce
  qed (use False in auto)
  qed
 qed
 
 lemma diffs_affine_hull_span:
  assumes "a S"
  shows "(λx. x - a) ` (affine hull S) = span ((λx. x - a) ` S)"
 proof -
  have *: "((λx. x - a) ` (S - {a})) = ((λx. x - a) ` S) - {0}"
  by (auto simp: algebra_simps)
  show ?thesis
    by (auto simp add: algebra_simps affine_hull_span2 [OF assms] *)
qed

lemma aff_dim_dim_affine_diffs:
  fixes S :: "'a :: euclidean_space set"
  assumes "affine S" "a S"
    shows "aff_dim S = dim ((λx. x - a) ` S)"
proof -
  obtain B where aff: "affine hull B = affine hull S"
             and ind: "¬ affine_dependent B"
             and card: "of_nat (card B) = aff_dim S + 1"
    using aff_dim_basis_exists by blast
  then have "B {}" using assms
    by (metis affine_hull_eq_empty ex_in_conv)
  then obtain c where "c B" by auto
  then have "c S"
    by (metis aff affine_hull_eq affine S hull_inc)
  have xy: "x - c = y - a y = x + 1 *🪙R (a - c)" for x y c and a::'a
    by (auto simp: algebra_simps)
  have *: "(λx. x - c) ` S = (λx. x - a) ` S"
    using assms c S
    by (auto simp: image_iff xy; metis mem_affine_3_minus pth_1)
  have affS: "affine hull S = S"
    by (simp add: affine S)
  have "aff_dim S = of_nat (card B) - 1"
    using card by simp
  also have "... = dim ((λx. x - c) ` B)"
    using affine_independent_card_dim_diffs [OF ind c B]
    by (simp add: affine_independent_card_dim_diffs [OF ind c B])
  also have "... = dim ((λx. x - c) ` (affine hull B))"
    by (simp add: diffs_affine_hull_span c B)
  also have "... = dim ((λx. x - a) ` S)"
    by (simp add: affS aff *)
  finally show ?thesis .
qed

lemma aff_dim_linear_image_le:
  assumes "linear f"
    shows "aff_dim(f ` S) aff_dim S"
proof -
  have "aff_dim (f ` T) aff_dim T" if "affine T" for T
  proof (cases "T = {}")
    case True then show ?thesis by (simp add: aff_dim_geq)
  next
    case False
    then obtain a where "a T" by auto
    have 1: "((λx. x - f a) ` f ` T) = {x - f a |x. x f ` T}"
      by auto
    have 2: "{x - f a| x. x f ` T} = f ` ((λx. x - a) ` T)"
      by (force simp: linear_diff [OF assms])
    have "aff_dim (f ` T) = int (dim {x - f a |x. x f ` T})"
      by (simp add: a T hull_inc aff_dim_eq_dim [of "f a"] 1 cong: image_cong_simp)
    also have "... = int (dim (f ` ((λx. x - a) ` T)))"
      by (force simp: linear_diff [OF assms] 2)
    also have "... int (dim ((λx. x - a) ` T))"
      by (simp add: dim_image_le [OF assms])
    also have "... aff_dim T"
      by (simp add: aff_dim_dim_affine_diffs [symmetric] a T affine T)
    finally show ?thesis .
  qed
  then
  have "aff_dim (f ` (affine hull S)) aff_dim (affine hull S)"
    using affine_affine_hull [of S] by blast
  then show ?thesis
    using affine_hull_linear_image assms linear_conv_bounded_linear by fastforce
qed

lemma aff_dim_injective_linear_image [simp]:
  assumes "linear f" "inj f"
    shows "aff_dim (f ` S) = aff_dim S"
proof (rule antisym)
  show "aff_dim (f ` S) aff_dim S"
    by (simp add: aff_dim_linear_image_le assms(1))
next
  obtain g where "linear g" "g f = id"
    using assms(1) assms(2) linear_injective_left_inverse by blast
  then have "aff_dim S aff_dim(g ` f ` S)"
    by (simp add: image_comp)
  also have "... aff_dim (f ` S)"
    by (simp add: linear g aff_dim_linear_image_le)
  finally show "aff_dim S aff_dim (f ` S)" .
qed


lemma choose_affine_subset:
  assumes "affine S" "-1 d" and dle: "d aff_dim S"
  obtains T where "affine T" "T S" "aff_dim T = d"
proof (cases "d = -1 S={}")
  case True with assms show ?thesis
    by (metis aff_dim_empty affine_empty bot.extremum that eq_iff)
next
  case False
  with assms obtain a where "a S" "0 d" by auto
  with assms have ss: "subspace ((+) (- a) ` S)"
    by (simp add: affine_diffs_subspace_subtract cong: image_cong_simp)
  have "nat d dim ((+) (- a) ` S)"
    by (metis aff_dim_subspace aff_dim_translation_eq dle nat_int nat_mono ss)
  then obtain T where "subspace T" and Tsb: "T span ((+) (- a) ` S)"
                  and Tdim: "dim T = nat d"
    using choose_subspace_of_subspace [of "nat d" "(+) (- a) ` S"by blast
  then have "affine T"
    using subspace_affine by blast
  then have "affine ((+) a ` T)"
    by (metis affine_hull_eq affine_hull_translation)
  moreover have "(+) a ` T S"
  proof -
    have "T (+) (- a) ` S"
      by (metis (no_types) span_eq_iff Tsb ss)
    then show "(+) a ` T S"
      using add_ac by auto
  qed
  moreover have "aff_dim ((+) a ` T) = d"
    by (simp add: aff_dim_subspace Tdim 0 d subspace T aff_dim_translation_eq)
  ultimately show ?thesis
    by (rule that)
qed

subsectionParacompactness

proposition paracompact:
  fixes S :: "'a :: {metric_space,second_countable_topology} set"
  assumes "S C" and opC: "T. T C ==> open T"
  obtains Cwhere "S C'"
               and "U. U C' ==> open U (T. T C U T)"
               and "x. x S
                       ==> V. open V x V finite {U. U C' (U V {})}"
proof (cases "S = {}")
  case True with that show ?thesis by blast
next
  case False
  have "T U. x U open U closure U T T C" if "x S" for x
  proof -
    obtain T where "x T" "T C" "open T"
      using assms x S by blast
    then obtain e where "e > 0" "cball x e T"
      by (force simp: open_contains_cball)
    then show ?thesis
      by (meson open_ball T C ball_subset_cball centre_in_ball closed_cball closure_minimal dual_order.trans)
  qed
  then obtain F G where Gin: "x G x" and oG: "open (G x)"
    and clos: "closure (G x) F x" and Fin: "F x C"
  if "x S" for x
    by metis
  then obtain F where "F G ` S" "countable F" "F = (G ` S)"
    using Lindelof [of "G ` S"by (metis image_iff)
  then obtain K where K: "K S" "countable K" and eq: "(G ` K) = (G ` S)"
    by (metis countable_subset_image)
  with False Gin have "K {}" by force
  then obtain a :: "nat ==> 'a" where "range a = K"
    by (metis range_from_nat_into countable K)
  then have odif: "n. open (F (a n) - {closure (G (a m)) |m. m < n})"
    using K S Fin opC by (fastforce simp add:)
  let ?C = "range (λn. F(a n) - {closure(G(a m)) |m. m < n})"
  have enum_S: "n. x F(a n) x G(a n)" if "x S" for x
  proof -
    have "y K. x G y" using eq that Gin by fastforce
    then show ?thesis
      using clos K range a = K closure_subset by blast
  qed
  show ?thesis
  proof
    show "S Union ?C"
    proof
      fix x assume "x S"
      define n where "n LEAST n. x F(a n)"
      have n: "x F(a n)"
        using enum_S [OF x Sby (force simp: n_def intro: LeastI)
      have notn: "x F(a m)" if "m < n" for m
        using that not_less_Least by (force simp: n_def)
      then have "x {closure (G (a m)) |m. m < n}"
        using n K S range a = K clos notn by fastforce
      with n show "x Union ?C"
        by blast
    qed
    show "U. U ?C ==> open U (T. T C U T)"
      using Fin K S range a = K by (auto simp: odif)
    show "V. open V x V finite {U. U ?C (U V {})}" if "x S" for x
    proof -
      obtain n where n: "x F(a n)" "x G(a n)"
        using x S enum_S by auto
      have "{U ?C. U G (a n) {}} (λn. F(a n) - {closure(G(a m)) |m. m < n}) ` atMost n"
      proof clarsimp
        fix k  assume "(F (a k) - {closure (G (a m)) |m. m < k}) G (a n) {}"
        then have "k n"
          by auto (metis closure_subset not_le subsetCE)
        then show "F (a k) - {closure (G (a m)) |m. m < k}
                  (λn. F (a n) - {closure (G (a m)) |m. m < n}) ` {..n}"
          by force
      qed
      moreover have "finite ((λn. F(a n) - {closure(G(a m)) |m. m < n}) ` atMost n)"
        by force
      ultimately have *: "finite {U ?C. U G (a n) {}}"
        using finite_subset by blast
      have "a n S"
        using K S range a = K by blast
      then show ?thesis
        by (blast intro: oG n *)
    qed
  qed
qed

corollary paracompact_closedin:
  fixes S :: "'a :: {metric_space,second_countable_topology} set"
  assumes cin: "closedin (top_of_set U) S"
      and oin: "T. T C ==> openin (top_of_set U) T"
      and "S C"
  obtains Cwhere "S C'"
               and "V. V C' ==> openin (top_of_set U) V (T. T C V T)"
               and "x. x U
                       ==> V. openin (top_of_set U) V x V
                               finite {X. X C' (X V {})}"
proof -
  have "Z. open Z (T = U Z)" if "T C" for T
    using oin [OF that] by (auto simp: openin_open)
  then obtain F where opF: "open (F T)" and intF: "U F T = T" if "T C" for T
    by metis
  obtain K where K: "closed K" "U K = S"
    using cin by (auto simp: closedin_closed)
  have 1: "U (insert (- K) (F ` C))"
    by clarsimp (metis Int_iff Union_iff U K = S S C subsetD intF)
  have 2: "T. T insert (- K) (F ` C) ==> open T"
    using closed K by (auto simp: opF)
  obtain D where "U D"
             and D1: "U. U D ==> open U (T. T insert (- K) (F ` C) U T)"
             and D2: "x. x U ==> V. open V x V finite {U D. U V {}}"
    by (blast intro: paracompact [OF 1 2])
  let ?C = "{U V |V. V D (V K {})}"
  show ?thesis
  proof (rule_tac C' = "{U V |V. V D (V K {})}" in that)
    show "S ?C"
      using U K = S U Dby (blast dest!: subsetD)
    show "V. V ?C ==> openin (top_of_set U) V (T. T C V T)"
      using D1 intF by fastforce
    have *: "{X. (V. X = U V V D V K {}) X (U V) {}}
             (λx. U x) ` {U D. U V {}}" for V
      by blast
    show "V. openin (top_of_set U) V x V finite {X ?C. X V {}}"
      if "x U" for x
    proof -
      from D2 [OF that] obtain V where "open V" "x V" "finite {U D. U V {}}"
        by auto
      with * show ?thesis
        by (rule_tac x="U V" in exI) (auto intro: that finite_subset [OF *])
    qed
  qed
qed

corollary🍋tag unimportant paracompact_closed:
  fixes S :: "'a :: {metric_space,second_countable_topology} set"
  assumes "closed S"
      and opC: "T. T C ==> open T"
      and "S C"
  obtains Cwhere "S C'"
               and "U. U C' ==> open U (T. T C U T)"
               and "x. V. open V x V
                               finite {U. U C' (U V {})}"
  by (rule paracompact_closedin [of UNIV S C]) (auto simp: assms)

  
subsection🍋tag unimportant\<open>Closed-graph characterization of continuity

lemma continuous_closed_graph_gen:
  fixes T :: "'b::real_normed_vector set"
  assumes contf: "continuous_on S f" and fim: "f ` S T"
    shows "closedin (top_of_set (S × T)) ((λx. Pair x (f x)) ` S)"
proof -
  have eq: "((λx. Pair x (f x)) ` S) = (S × T (λz. (f fst)z - snd z) -` {0})"
    using fim by auto
  show ?thesis
    unfolding eq
    by (intro continuous_intros continuous_closedin_preimage continuous_on_subset [OF contf]) auto
qed

lemma continuous_closed_graph_eq:
  fixes f :: "'a::euclidean_space ==> 'b::euclidean_space"
  assumes "compact T" and fim: "f S T"
  shows "continuous_on S f
         closedin (top_of_set (S × T)) ((λx. Pair x (f x)) ` S)"
         (is "?lhs = ?rhs")
proof -
  have "?lhs" if ?rhs
  proof (clarsimp simp add: continuous_on_closed_gen [OF fim])
    fix U
    assume U: "closedin (top_of_set T) U"
    have eq: "(S f -` U) = fst ` (((λx. Pair x (f x)) ` S) (S × U))"
      by (force simp: image_iff)
    show "closedin (top_of_set S) (S f -` U)"
      by (simp add: U closedin_Int closedin_Times closed_map_fst [OF compact T] that eq)
  qed
  with continuous_closed_graph_gen assms show ?thesis by blast
qed

lemma continuous_closed_graph:
  fixes f :: "'a::topological_space ==> 'b::real_normed_vector"
  assumes "closed S" and contf: "continuous_on S f"
  shows "closed ((λx. Pair x (f x)) ` S)"
proof (rule closedin_closed_trans)
  show "closedin (top_of_set (S × UNIV)) ((λx. (x, f x)) ` S)"
    by (rule continuous_closed_graph_gen [OF contf subset_UNIV])
qed (simp add: closed S closed_Times)

lemma continuous_from_closed_graph:
  fixes f :: "'a::euclidean_space ==> 'b::euclidean_space"
  assumes "compact T" and fim: "f S T" and clo: "closed ((λx. Pair x (f x)) ` S)"
  shows "continuous_on S f"
    using fim clo
    by (auto intro: closed_subset simp: continuous_closed_graph_eq [OF compact T fim])

lemma continuous_on_Un_local_open:
  assumes opS: "openin (top_of_set (S T)) S"
      and opT: "openin (top_of_set (S T)) T"
      and contf: "continuous_on S f" and contg: "continuous_on T f"
    shows "continuous_on (S T) f"
  using pasting_lemma [of "{S,T}" "top_of_set (S T)" id euclidean "λi. f" f] contf contg opS opT
  by (simp add: subtopology_subtopology) (metis inf.absorb2 openin_imp_subset)  

lemma continuous_on_cases_local_open:
  assumes opS: "openin (top_of_set (S T)) S"
      and opT: "openin (top_of_set (S T)) T"
      and contf: "continuous_on S f" and contg: "continuous_on T g"
      and fg: "x. x S ¬P x x T P x ==> f x = g x"
    shows "continuous_on (S T) (λx. if P x then f x else g x)"
proof -
  have "x. x S ==> (if P x then f x else g x) = f x"  "x. x T ==> (if P x then f x else g x) = g x"
    by (simp_all add: fg)
  then have "continuous_on S (λx. if P x then f x else g x)" "continuous_on T (λx. if P x then f x else g x)"
    by (simp_all add: contf contg cong: continuous_on_cong)
  then show ?thesis
    by (rule continuous_on_Un_local_open [OF opS opT])
qed

subsection🍋tag unimportant\<open>The union of two collinear segments is another segment

proposition🍋tag unimportant in_convex_hull_exchange:
  fixes a :: "'a::euclidean_space"
  assumes a: "a convex hull S" and xS: "x convex hull S"
  obtains b where "b S" "x convex hull (insert a (S - {b}))"
proof (cases "a S")
  case True
  with xS insert_Diff that  show ?thesis by fastforce
next
  case False
  show ?thesis
  proof (cases "finite S card S Suc (DIM('a))")
    case True
    then obtain u where u0: "i. i S ==> 0 u i" and u1: "sum u S = 1"
                    and ua: "(iS. u i *🪙R i) = a"
        using a by (auto simp: convex_hull_finite)
    obtain v where v0: "i. i S ==> 0 v i" and v1: "sum v S = 1"
               and vx: "(iS. v i *🪙R i) = x"
      using True xS by (auto simp: convex_hull_finite)
    show ?thesis
    proof (cases "b. b S v b = 0")
      case True
      then obtain b where b: "b S" "v b = 0"
        by blast
      show ?thesis
      proof
        have fin: "finite (insert a (S - {b}))"
          using sum.infinite v1 by fastforce
        show "x convex hull insert a (S - {b})"
          unfolding convex_hull_finite [OF fin] mem_Collect_eq
        proof (intro conjI exI ballI)
          have "(x insert a (S - {b}). if x = a then 0 else v x) =
                (x S - {b}. if x = a then 0 else v x)"
            using fin by (force intro: sum.mono_neutral_right)
          also have "... = (x S - {b}. v x)"
            using b False by (auto intro!: sum.cong split: if_split_asm)
          also have "... = (xS. v x)"
            by (metis v b = 0 diff_zero sum.infinite sum_diff1 u1 zero_neq_one)
          finally show "(xinsert a (S - {b}). if x = a then 0 else v x) = 1"
            by (simp add: v1)
          show "x. x insert a (S - {b}) ==> 0 (if x = a then 0 else v x)"
            by (auto simp: v0)
          have "(x insert a (S - {b}). (if x = a then 0 else v x) *🪙R x) =
                (x S - {b}. (if x = a then 0 else v x) *🪙R x)"
            using fin by (force intro: sum.mono_neutral_right)
          also have "... = (x S - {b}. v x *🪙R x)"
            using b False by (auto intro!: sum.cong split: if_split_asm)
          also have "... = (xS. v x *🪙R x)"
            by (metis (no_types, lifting) b(2) diff_zero fin finite.emptyI finite_Diff2 finite_insert scale_eq_0_iff sum_diff1)
          finally show "(xinsert a (S - {b}). (if x = a then 0 else v x) *🪙R x) = x"
            by (simp add: vx)
        qed
      qed (rule b S)
    next
      case False
      have le_Max: "u i / v i Max ((λi. u i / v i) ` S)" if "i S" for i
        by (simp add: True that)
      have "Max ((λi. u i / v i) ` S) (λi. u i / v i) ` S"
        using True v1 by (auto intro: Max_in)
      then obtain b where "b S" and beq: "Max ((λb. u b / v b) ` S) = u b / v b"
        by blast
      then have "0 u b / v b"
        using le_Max beq divide_le_0_iff le_numeral_extra(2) sum_nonpos u1
        by (metis False eq_iff v0)
      then have  "0 < u b" "0 < v b"
        using False b S u0 v0 by force+
      have fin: "finite (insert a (S - {b}))"
        using sum.infinite v1 by fastforce
      show ?thesis
      proof
        show "x convex hull insert a (S - {b})"
          unfolding convex_hull_finite [OF fin] mem_Collect_eq
        proof (intro conjI exI ballI)
          have "(x insert a (S - {b}). if x=a then v b / u b else v x - (v b / u b) * u x) =
                v b / u b + (x S - {b}. v x - (v b / u b) * u x)"
            using a S b S True  
            by (auto intro!: sum.cong split: if_split_asm)
          also have "... = v b / u b + (x S - {b}. v x) - (v b / u b) * (x S - {b}. u x)"
            by (simp add: Groups_Big.sum_subtractf sum_distrib_left)
          also have "... = (xS. v x)"
            using 0 🚫 b True  by (simp add: Groups_Big.sum_diff1 u1 field_simps)
          finally show "sum (λx. if x=a then v b / u b else v x - (v b / u b) * u x) (insert a (S - {b})) = 1"
            by (simp add: v1)
          show "0 (if i = a then v b / u b else v i - v b / u b * u i)"
            if "i insert a (S - {b})" for i
            using 0 🚫 b 0 🚫 b v0 [of i] le_Max [of i] beq that False
            by (auto simp: field_simps split: if_split_asm)
          have "(xinsert a (S - {b}). (if x=a then v b / u b else v x - v b / u b * u x) *🪙R x) =
                (v b / u b) *🪙R a + (xS - {b}. (v x - v b / u b * u x) *🪙R x)"
            using a S b S True  by (auto intro!: sum.cong split: if_split_asm)
          also have "... = (v b / u b) *🪙R a + (x S - {b}. v x *🪙R x) - (v b / u b) *🪙R (x S - {b}. u x *🪙R x)"
            by (simp add: Groups_Big.sum_subtractf scaleR_left_diff_distrib sum_distrib_left scale_sum_right)
          also have "... = (xS. v x *🪙R x)"
            using 0 🚫 b True  by (simp add: ua vx Groups_Big.sum_diff1 algebra_simps)
          finally
          show "(xinsert a (S - {b}). (if x=a then v b / u b else v x - v b / u b * u x) *🪙R x) = x"
            by (simp add: vx)
        qed
      qed (rule b S)
    qed
  next
    case False
    obtain T where "finite T" "T S" and caT: "card T Suc (DIM('a))" and xT: "x convex hull T"
      using xS by (auto simp: caratheodory [of S])
    with False obtain b where b: "b S" "b T"
      by (metis antisym subsetI)
    show ?thesis
    proof
      show "x convex hull insert a (S - {b})"
        using  T Sby (blast intro: subsetD [OF hull_mono xT])
    qed (rule b S)
  qed
qed

lemma convex_hull_exchange_Union:
  fixes a :: "'a::euclidean_space"
  assumes "a convex hull S"
  shows "convex hull S = (b S. convex hull (insert a (S - {b})))" (is "?lhs = ?rhs")
proof
  show "?lhs ?rhs"
    by (blast intro: in_convex_hull_exchange [OF assms])
  show "?rhs ?lhs"
  proof clarify
    fix x b
    assume"b S" "x convex hull insert a (S - {b})"
    then show "x convex hull S" if "b S"
      by (metis (no_types) that assms order_refl hull_mono hull_redundant insert_Diff_single insert_subset subsetCE)
  qed
qed

lemma Un_closed_segment:
  fixes a :: "'a::euclidean_space"
  assumes "b closed_segment a c"
    shows "closed_segment a b closed_segment b c = closed_segment a c"
proof (cases "c = a")
  case True
  with assms show ?thesis by simp
next
  case False
  with assms have "convex hull {a, b} convex hull {b, c} = (ba{a, c}. convex hull insert b ({a, c} - {ba}))"
    by (auto simp: insert_Diff_if insert_commute)
  then show ?thesis
    using convex_hull_exchange_Union
    by (metis assms segment_convex_hull)
qed

lemma Un_open_segment:
  fixes a :: "'a::euclidean_space"
  assumes "b open_segment a c"
  shows "open_segment a b {b} open_segment b c = open_segment a c" (is "?lhs = ?rhs")
proof -
  have b: "b closed_segment a c"
    by (simp add: assms open_closed_segment)
  have *: "?rhs insert b (open_segment a b open_segment b c)"
          if "{b,c,a} open_segment a b open_segment b c = {c,a} ?rhs"
  proof -
    have "insert a (insert c (insert b (open_segment a b open_segment b c))) = insert a (insert c (?rhs))"
      using that by (simp add: insert_commute)
    then show ?thesis
      by (metis (no_types) Diff_cancel Diff_eq_empty_iff Diff_insert2 open_segment_def)
  qed
  show ?thesis
  proof
    show "?lhs ?rhs"
      by (simp add: assms b subset_open_segment)
    show "?rhs ?lhs"
      using Un_closed_segment [OF b] *
      by (simp add: closed_segment_eq_open insert_commute)
  qed
qed

subsectionCovering an open set by a countable chain of compact sets
  
proposition open_Union_compact_subsets:
  fixes S :: "'a::euclidean_space set"
  assumes "open S"
  obtains C where "n. compact(C n)" "n. C n S"
                  "n. C n interior(C(Suc n))"
                  "(range C) = S"
                  "K. [compact K; K S] ==> N. nN. K (C n)"
proof (cases "S = {}")
  case True
  then show ?thesis
    by (rule_tac C = "λn. {}" in that) auto
next
  case False
  then obtain a where "a S"
    by auto
  let ?C = "λn. cball a (real n) - (x -S. e ball 0 (1 / real(Suc n)). {x + e})"
  have "N. nN. K (f n)"
        if "n. compact(f n)" and sub_int: "n. f n interior (f(Suc n))"
            and eq: "(range f) = S" and "compact K" "K S" for f K
  proof -
    have *: "n. f n (n. interior (f n))"
      by (meson Sup_upper2 UNIV_I n. f n interior (f (Suc n)) image_iff)
    have mono: "m n. m n ==>f m f n"
      by (meson dual_order.trans interior_subset lift_Suc_mono_le sub_int)
    obtain I where "finite I" and I: "K (iI. interior (f i))"
    proof (rule compactE_image [OF compact K])
      show "K (n. interior (f n))"
        using K S (f ` UNIV) = Sby blast
    qed auto
    { fix n
      assume n: "Max I n"
      have "(iI. interior (f i)) f n"
        by (rule UN_least) (meson dual_order.trans interior_subset mono I Max_ge [OF finite I] n)
      then have "K f n"
        using I by auto
    }
    then show ?thesis
      by blast
  qed
  moreover have "f. (n. compact(f n)) (n. (f n) S) (n. (f n) interior(f(Suc n)))
                     (((range f) = S))"
  proof (intro exI conjI allI)
    show "n. compact (?C n)"
      by (auto simp: compact_diff open_sums)
    show "n. ?C n S"
      by auto
    show "?C n interior (?C (Suc n))" for n
    proof -
      have 🍋"cball a (real n) ball a (1 + real n)"
        by (simp add: cball_subset_ball_iff)
      have cl: "closed (x- S. ecball 0 (1 / (2 + real n)). {x + e})"
        using assms by (auto intro: closed_compact_sums)
      have "closure (x- S. yball 0 (1 / (2 + real n)). {x + y})
             (x -S. e cball 0 (1 / (2 + real n)). {x + e})"
        by (intro closure_minimal UN_mono ball_subset_cball order_refl cl)
      also have "... (x -S. yball 0 (1 / (1 + real n)). {x + y})"
        by (simp add: cball_subset_ball_iff field_split_simps UN_mono)
      finally have "closure (x- S. yball 0 (1 / (2 + real n)). {x + y})
                     (x -S. yball 0 (1 / (1 + real n)). {x + y})" .
      with 🍋 show ?thesis
        by (auto simp: interior_diff)
    qed
    have "S (range ?C)"
    proof
      fix x
      assume x: "x S"
      then obtain e where "e > 0" and e: "ball x e S"
        using assms open_contains_ball by blast
      then obtain N1 where "N1 > 0" and N1: "real N1 > 1/e"
        by (metis divide_less_0_1_iff gr0I of_nat_0 order_less_imp_triv reals_Archimedean2)
      obtain N2 where N2: "norm(x - a) real N2"
        by (meson real_arch_simple)
      have N12: "inverse((N1 + N2) + 1) inverse(N1)"
        using N1 > 0 by (auto simp: field_split_simps)
      have "x y + z" if "y S" "norm z < 1 / (1 + (real N1 + real N2))" for y z
      proof -
        have "e * real N1 < e * (1 + (real N1 + real N2))"
          by (simp add: 0 🚫)
        then have "1 / (1 + (real N1 + real N2)) < e"
          using N1 e > 0
          by (metis divide_less_eq less_trans mult.commute of_nat_add of_nat_less_0_iff of_nat_Suc)
        then have "x - z ball x e"
          using that by simp
        then have "x - z S"
          using e by blast
        with that show ?thesis
          by auto
      qed
      with N2 show "x (range ?C)"
        by (rule_tac a = "N1+N2" in UN_I) (auto simp: dist_norm norm_minus_commute)
    qed
    then show " (range ?C) = S" by auto
  qed
  ultimately show ?thesis
    using that by metis
qed


subsectionOrthogonal complement

definition🍋tag important orthogonal_comp ((open_block notation=postfix \??) [80] 80)
  where "orthogonal_comp W {x. y W. orthogonal y x}"

proposition subspace_orthogonal_comp: "subspace (W🪙)"
  unfolding subspace_def orthogonal_comp_def orthogonal_def
  by (auto simp: inner_right_distrib)

lemma orthogonal_comp_anti_mono:
  assumes "A B"
  shows "B🪙 A🪙"
  using assms by (force simp add: orthogonal_comp_def orthogonal_def)

lemma orthogonal_comp_null [simp]: "{0}🪙 = UNIV"
  by (auto simp: orthogonal_comp_def orthogonal_def)

lemma orthogonal_comp_UNIV [simp]: "UNIV🪙 = {0}"
  unfolding orthogonal_comp_def orthogonal_def
  by auto (use inner_eq_zero_iff in blast)

lemma orthogonal_comp_subset: "U U🪙🪙"
  by (auto simp: orthogonal_comp_def orthogonal_def inner_commute)

lemma subspace_sum_minimal:
  assumes "S U" "T U" "subspace U"
  shows "S + T U"
proof
  fix x
  assume "x S + T"
  then obtain xs xt where "xs S" "xt T" "x = xs+xt"
    by (meson set_plus_elim)
  then show "x U"
    by (meson assms subsetCE subspace_add)
qed

proposition subspace_sum_orthogonal_comp:
  fixes U :: "'a :: euclidean_space set"
  assumes "subspace U"
  shows "U + U🪙 = UNIV"
proof -
  obtain B where "B U"
    and ortho: "pairwise orthogonal B" "x. x B ==> norm x = 1"
    and "independent B" "card B = dim U" "span B = U"
    using orthonormal_basis_subspace [OF assms] by metis
  then have "finite B"
    by (simp add: indep_card_eq_dim_span)
  have *: "xB. yB. x y = (if x=y then 1 else 0)"
    using ortho norm_eq_1 by (auto simp: orthogonal_def pairwise_def)
  { fix v
    let ?u = "bB. (v b) *🪙R b"
    have "v = ?u + (v - ?u)"
      by simp
    moreover have "?u U"
      by (metis (no_types, lifting) span B = U assms subspace_sum span_base span_mul)
    moreover have "(v - ?u) U🪙"
      unfolding orthogonal_comp_def orthogonal_def mem_Collect_eq
    proof 
      fix y
      assume "y U"
      with span B = U span_finite [OF finite B]
      obtain u where u: "y = (bB. u b *🪙R b)"
        by auto
      have "b (v - ?u) = 0" if "b B" for b
        using that finite B
        by (simp add: * algebra_simps inner_sum_right if_distrib [of "(*)v" for v] inner_commute cong: if_cong)
      then show " (v - ?u) = 0"
        by (simp add: u inner_sum_left)
    qed
    ultimately have " U + U🪙"
      using set_plus_intro by fastforce
  } then show ?thesis
    by auto
qed

lemma orthogonal_Int_0:
  assumes "subspace U"
  shows " U🪙 = {0}"
  using orthogonal_comp_def orthogonal_self
  by (force simp: assms subspace_0 subspace_orthogonal_comp)

lemma orthogonal_comp_self:
  fixes U :: "'a :: euclidean_space set"
  assumes "subspace U"
  shows "U🪙🪙 = U"
proof
  have ssU': "subspace (U🪙)"
    by (simp add: subspace_orthogonal_comp)
  have " U" if " U🪙🪙" for u
  proof -
    obtain v w where "u = v+w" " U" " U🪙"
      using subspace_sum_orthogonal_comp [OF assms] set_plus_elim by blast
    then have "u-v  U🪙"
      by simp
    moreover have " U🪙🪙"
      using v U orthogonal_comp_subset by blast
    then have "u-v  U🪙🪙"
      by (simp add: subspace_diff subspace_orthogonal_comp that)
    ultimately have "u-v = 0"
      using orthogonal_Int_0 ssU' by blast
    with v U show ?thesis
      by auto
  qed
  then show "U🪙🪙  U"
    by auto
qed (use orthogonal_comp_subset in auto)

lemma ker_orthogonal_comp_adjoint:
  fixes f :: "'m::euclidean_space ==> 'n::euclidean_space"
  assumes "linear f"
  shows "f -` {0} = (range (adjoint f))🪙"
proof -
  have "x. [y. y  f x = 0] ==> f x = 0"
    using assms inner_commute all_zero_iff by metis
  then show ?thesis
    using assms
    by (auto simp: orthogonal_comp_def orthogonal_def adjoint_works inner_commute)
qed

subsection🍋tag unimportant A non-injective linear function maps into a hyperplane.

lemma linear_surj_adj_imp_inj:
  fixes f :: "'m::euclidean_space ==> 'n::euclidean_space"
  assumes "linear f" "surj (adjoint f)"
  shows "inj f"
proof -
  have "x. y = adjoint f x" for y
    using assms by (simp add: surjD)
  then show "inj f"
    using assms unfolding inj_on_def image_def
    by (metis (no_types) adjoint_works euclidean_eqI)
qed

\ 🪙https://mathonline.wikidot.com/injectivity-and-surjectivity-of-the-adjoint-of-a-linear-map\
lemma surj_adjoint_iff_inj [simp]:
  fixes f :: "'m::euclidean_space ==> 'n::euclidean_space"
  assumes "linear f"
  shows "surj (adjoint f)  inj f"
proof
  assume "surj (adjoint f)"
  then show "inj f"
    by (simp add: assms linear_surj_adj_imp_inj)
next
  assume "inj f"
  have "f -` {0} = {0}"
    using assms inj f linear_0 linear_injective_0 by fastforce
  moreover have "f -` {0} = range (adjoint f)🪙"
    by (intro ker_orthogonal_comp_adjoint assms)
  ultimately have "range (adjoint f)🪙🪙 = UNIV"
    by (metis orthogonal_comp_null)
  then show "surj (adjoint f)"
    using adjoint_linear linear f
    by (metis linear_subspace_image orthogonal_comp_self subspace_UNIV)
qed

lemma inj_adjoint_iff_surj [simp]:
  fixes f :: "'m::euclidean_space ==> 'n::euclidean_space"
  assumes "linear f"
  shows "inj (adjoint f)  surj f"
proof
  assume "inj (adjoint f)"
  have "(adjoint f) -` {0} = {0}"
    by (metis inj (adjoint f) adjoint_linear assms surj_adjoint_iff_inj ker_orthogonal_comp_adjoint orthogonal_comp_UNIV)
  then have "(range(f))🪙 = {0}"
    by (metis (no_types, opaque_lifting) adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint set_zero)
  then show "surj f"
    by (metis inj (adjoint f) adjoint_adjoint adjoint_linear assms surj_adjoint_iff_inj)
next
  assume "surj f"
  then have "range f = (adjoint f -` {0})🪙"
    by (simp add: adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint)
  then have "{0} = adjoint f -` {0}"
    using surj f adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint by force
  then show "inj (adjoint f)"
    by (simp add: surj f adjoint_adjoint adjoint_linear assms linear_surj_adj_imp_inj)
qed

lemma linear_singular_into_hyperplane:
  fixes f :: "'n::euclidean_space ==> 'n"
  assumes "linear f"
  shows "¬ inj f  (a. a  0  (x. a  f x = 0))" (is "_ = ?rhs")
proof
  assume "¬inj f"
  then show ?rhs
    using all_zero_iff
    by (metis (no_types, opaque_lifting) adjoint_clauses(2) adjoint_linear assms
        linear_injective_0 linear_injective_imp_surjective linear_surj_adj_imp_inj)
next
  assume ?rhs
  then show "¬inj f"
    by (metis assms linear_injective_isomorphism all_zero_iff)
qed

lemma linear_singular_image_hyperplane:
  fixes f :: "'n::euclidean_space ==> 'n"
  assumes "linear f" "¬inj f"
  obtains a where " 0" "S. f ` S  {x. a  x = 0}"
  using assms by (fastforce simp add: linear_singular_into_hyperplane)

end

Messung V0.5 in Prozent
C=33 H=22 G=26

¤ 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.3.383Bemerkung:  (vorverarbeitet am  2026-04-26) ¤

*Bot Zugriff






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.






                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge