Theory Topology_Euclidean_Space

(*  Author:     L C Paulson, University of Cambridge
    Author:     Amine Chaieb, University of Cambridge
    Author:     Robert Himmelmann, TU Muenchen
    Author:     Brian Huffman, Portland State University
*)

chapter ‹Vector Analysis›

theory Topology_Euclidean_Space
  imports
    Elementary_Normed_Spaces
    Linear_Algebra
    Norm_Arith
begin

section ‹Elementary Topology in Euclidean Space›

lemma euclidean_dist_l2:
  fixes x y :: "'a :: euclidean_space"
  shows "dist x y = L2_set (λi. dist (x  i) (y  i)) Basis"
  unfolding dist_norm norm_eq_sqrt_inner L2_set_def
  by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)

lemma norm_nth_le: "norm (x  i)  norm x" if "i  Basis"
proof -
  have "(x  i)2 = (i{i}. (x  i)2)"
    by simp
  also have "  (iBasis. (x  i)2)"
    by (intro sum_mono2) (auto simp: that)
  finally show ?thesis
    unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
    by (auto intro!: real_le_rsqrt)
qed

subsectiontag unimportant› ‹Continuity of the representation WRT an orthogonal basis›

lemma orthogonal_Basis: "pairwise orthogonal Basis"
  by (simp add: inner_not_same_Basis orthogonal_def pairwise_def)

lemma representation_bound:
  fixes B :: "'N::real_inner set"
  assumes "finite B" "independent B" "b  B" and orth: "pairwise orthogonal B"
  obtains m where "m > 0" "x. x  span B  ¦representation B x b¦  m * norm x"
proof 
  fix x
  assume x: "x  span B"
  have "b  0"
    using independent B b  B dependent_zero by blast
  have [simp]: "b  b' = (if b' = b then (norm b)2 else 0)"
    if "b  B" "b'  B" for b b'
    using orth by (simp add: orthogonal_def pairwise_def norm_eq_sqrt_inner that)
  have "norm x = norm (bB. representation B x b *R b)"
    using real_vector.sum_representation_eq [OF independent B x finite B order_refl]
    by simp
  also have " = sqrt ((bB. representation B x b *R b)  (bB. representation B x b *R b))"
    by (simp add: norm_eq_sqrt_inner)
  also have " = sqrt (bB. (representation B x b *R b)  (representation B x b *R b))"
    using finite B
    by (simp add: inner_sum_left inner_sum_right if_distrib [of "λx. _ * x"] cong: if_cong sum.cong_simp)
  also have " = sqrt (bB. (norm (representation B x b *R b))2)"
    by (simp add: mult.commute mult.left_commute power2_eq_square)
  also have " = sqrt (bB. (representation B x b)2 * (norm b)2)"
    by (simp add: norm_mult power_mult_distrib)
  finally have "norm x = sqrt (bB. (representation B x b)2 * (norm b)2)" .
  moreover
  have "sqrt ((representation B x b)2 * (norm b)2)  sqrt (bB. (representation B x b)2 * (norm b)2)"
    using b  B finite B by (auto intro: member_le_sum)
  then have "¦representation B x b¦  (1 / norm b) * sqrt (bB. (representation B x b)2 * (norm b)2)"
    using b  0 by (simp add: field_split_simps real_sqrt_mult del: real_sqrt_le_iff)
  ultimately show "¦representation B x b¦  (1 / norm b) * norm x"
    by simp
next
  show "0 < 1 / norm b"
    using independent B b  B dependent_zero by auto
qed 

lemma continuous_on_representation:
  fixes B :: "'N::euclidean_space set"
  assumes "finite B" "independent B" "b  B" "pairwise orthogonal B" 
  shows "continuous_on (span B) (λx. representation B x b)"
proof
  show "d>0. x'span B. dist x' x < d  dist (representation B x' b) (representation B x b)  e"
    if "e > 0" "x  span B" for x e
  proof -
    obtain m where "m > 0" and m: "x. x  span B  ¦representation B x b¦  m * norm x"
      using assms representation_bound by blast
    show ?thesis
      unfolding dist_norm
    proof (intro exI conjI ballI impI)
      show "e/m > 0"
        by (simp add: e > 0 m > 0)
      show "norm (representation B x' b - representation B x b)  e"
        if x': "x'  span B" and less: "norm (x'-x) < e/m" for x' 
      proof -
        have "¦representation B (x'-x) b¦  m * norm (x'-x)"
          using m [of "x'-x"] x  span B span_diff x' by blast
        also have " < e"
          by (metis m > 0 less mult.commute pos_less_divide_eq)
        finally have "¦representation B (x'-x) b¦  e" by simp
        then show ?thesis
          by (simp add: x  span B independent B representation_diff x')
      qed
    qed
  qed
qed

subsectiontag unimportant›‹Balls in Euclidean Space›

lemma cball_subset_cball_iff:
  fixes a :: "'a :: euclidean_space"
  shows "cball a r  cball a' r'  dist a a' + r  r'  r < 0"
    (is "?lhs  ?rhs")
proof
  assume ?lhs
  then show ?rhs
  proof (cases "r < 0")
    case True
    then show ?rhs by simp
  next
    case False
    then have [simp]: "r  0" by simp
    have "norm (a - a') + r  r'"
    proof (cases "a = a'")
      case True
      then show ?thesis
        using subsetD [where c = "a + r *R (SOME i. i  Basis)", OF ?lhs] subsetD [where c = a, OF ?lhs]
        by (force simp: SOME_Basis dist_norm)
    next
      case False
      have "norm (a' - (a + (r / norm (a - a')) *R (a - a'))) = norm ((-1 - (r / norm (a - a'))) *R (a - a'))"
        by (simp add: algebra_simps)
      also from a  a' have "... = ¦- norm (a - a') - r¦"
        by (simp add: divide_simps)
      finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *R (a - a'))) = ¦norm (a - a') + r¦"
        by linarith
      from a  a' show ?thesis
        using subsetD [where c = "a' + (1 + r / norm(a - a')) *R (a - a')", OF ?lhs]
        by (simp add: dist_norm scaleR_add_left)
    qed
    then show ?rhs
      by (simp add: dist_norm)
  qed
qed metric

lemma cball_subset_ball_iff: "cball a r  ball a' r'  dist a a' + r < r'  r < 0"
  (is "?lhs  ?rhs")
  for a :: "'a::euclidean_space"
proof
  assume ?lhs
  then show ?rhs
  proof (cases "r < 0")
    case True then
    show ?rhs by simp
  next
    case False
    then have [simp]: "r  0" by simp
    have "norm (a - a') + r < r'"
    proof (cases "a = a'")
      case True
      then show ?thesis
        using subsetD [where c = "a + r *R (SOME i. i  Basis)", OF ?lhs] subsetD [where c = a, OF ?lhs]
        by (force simp: SOME_Basis dist_norm)
    next
      case False
      have False if "norm (a - a') + r  r'"
      proof -
        from that have "¦r' - norm (a - a')¦  r"
          by (smt (verit, best) 0  r ?lhs ball_subset_cball cball_subset_cball_iff dist_norm order_trans)
        then show ?thesis
          using subsetD [where c = "a + (r' / norm(a - a') - 1) *R (a - a')", OF ?lhs] a  a'
          apply (simp add: dist_norm)
          apply (simp add: scaleR_left_diff_distrib)
          apply (simp add: field_simps)
          done
      qed
      then show ?thesis by force
    qed
    then show ?rhs by (simp add: dist_norm)
  qed
next
  assume ?rhs
  then show ?lhs
    by metric
qed

lemma ball_subset_cball_iff: "ball a r  cball a' r'  dist a a' + r  r'  r  0"
  (is "?lhs = ?rhs")
  for a :: "'a::euclidean_space"
proof (cases "r  0")
  case True
  then show ?thesis
    by metric
next
  case False
  show ?thesis
  proof
    assume ?lhs
    then have "(cball a r  cball a' r')"
      by (metis False closed_cball closure_ball closure_closed closure_mono not_less)
    with False show ?rhs
      by (fastforce iff: cball_subset_cball_iff)
  next
    assume ?rhs
    with False show ?lhs
      by metric
  qed
qed

lemma ball_subset_ball_iff:
  fixes a :: "'a :: euclidean_space"
  shows "ball a r  ball a' r'  dist a a' + r  r'  r  0"
        (is "?lhs = ?rhs")
proof (cases "r  0")
  case True then show ?thesis
    by metric
next
  case False show ?thesis
  proof
    assume ?lhs
    then have "0 < r'"
      using False by metric
    then have "cball a r  cball a' r'"
      by (metis False ?lhs closure_ball closure_mono not_less)
    then show ?rhs
      using False cball_subset_cball_iff by fastforce
  qed metric
qed


lemma ball_eq_ball_iff:
  fixes x :: "'a :: euclidean_space"
  shows "ball x d = ball y e  d  0  e  0  x=y  d=e"
  by (smt (verit, del_insts) ball_empty ball_subset_cball_iff dist_norm norm_pths(2))

lemma cball_eq_cball_iff:
  fixes x :: "'a :: euclidean_space"
  shows "cball x d = cball y e  d < 0  e < 0  x=y  d=e"
  by (smt (verit, ccfv_SIG) cball_empty cball_subset_cball_iff dist_norm norm_pths(2) zero_le_dist)

lemma ball_eq_cball_iff:
  fixes x :: "'a :: euclidean_space"
  shows "ball x d = cball y e  d  0  e < 0" (is "?lhs = ?rhs")
  by (smt (verit) ball_eq_empty ball_subset_cball_iff cball_eq_empty cball_subset_ball_iff order.refl)

lemma cball_eq_ball_iff:
  fixes x :: "'a :: euclidean_space"
  shows "cball x d = ball y e  d < 0  e  0"
  using ball_eq_cball_iff by blast

lemma finite_ball_avoid:
  fixes S :: "'a :: euclidean_space set"
  assumes "open S" "finite X" "p  S"
  shows "e>0. wball p e. wS  (wp  wX)"
proof -
  obtain e1 where "0 < e1" and e1_b:"ball p e1  S"
    using open_contains_ball_eq[OF open S] assms by auto
  obtain e2 where "0 < e2" and "xX. x  p  e2  dist p x"
    using finite_set_avoid[OF finite X,of p] by auto
  hence "wball p (min e1 e2). wS  (wp  wX)" using e1_b by auto
  thus "e>0. wball p e. w  S  (w  p  w  X)" 
    using e2>0 e1>0 by (rule_tac x="min e1 e2" in exI) auto
qed

lemma finite_cball_avoid:
  fixes S :: "'a :: euclidean_space set"
  assumes "open S" "finite X" "p  S"
  shows "e>0. wcball p e. wS  (wp  wX)"
proof -
  obtain e1 where "e1>0" and e1: "wball p e1. wS  (wp  wX)"
    using finite_ball_avoid[OF assms] by auto
  define e2 where "e2  e1/2"
  have "e2>0" and "e2 < e1" unfolding e2_def using e1>0 by auto
  then have "cball p e2  ball p e1" by (subst cball_subset_ball_iff,auto)
  then show "e>0. wcball p e. w  S  (w  p  w  X)" using e2>0 e1 by auto
qed

lemma dim_cball:
  assumes "e > 0"
  shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)"
proof -
  {
    fix x :: "'n::euclidean_space"
    define y where "y = (e / norm x) *R x"
    then have "y  cball 0 e"
      using assms by auto
    moreover have *: "x = (norm x / e) *R y"
      using y_def assms by simp
    moreover from * have "x = (norm x/e) *R y"
      by auto
    ultimately have "x  span (cball 0 e)"
      using span_scale[of y "cball 0 e" "norm x/e"]
        span_superset[of "cball 0 e"]
      by (simp add: span_base)
  }
  then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)"
    by auto
  then show ?thesis
    using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto)
qed


subsection ‹Boxes›

abbreviationtag important› One :: "'a::euclidean_space" where
"One  Basis"

lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
proof -
  have "dependent (Basis :: 'a set)"
    apply (simp add: dependent_finite)
    apply (rule_tac x="λi. 1" in exI)
    using SOME_Basis apply (auto simp: assms)
    done
  with independent_Basis show False by force
qed

corollarytag unimportant› One_neq_0[iff]: "One  0"
  by (metis One_non_0)

corollarytag unimportant› Zero_neq_One[iff]: "0  One"
  by (metis One_non_0)

definitiontag important› (in euclidean_space) eucl_less (infix "<e" 50) where 
"eucl_less a b  (iBasis. a  i < b  i)"

definitiontag important› box_eucl_less: "box a b = {x. a <e x  x <e b}"
definitiontag important› "cbox a b = {x. iBasis. a  i  x  i  x  i  b  i}"

lemma box_def: "box a b = {x. iBasis. a  i < x  i  x  i < b  i}"
  and in_box_eucl_less: "x  box a b  a <e x  x <e b"
  and mem_box: "x  box a b  (iBasis. a  i < x  i  x  i < b  i)"
    "x  cbox a b  (iBasis. a  i  x  i  x  i  b  i)"
  by (auto simp: box_eucl_less eucl_less_def cbox_def)

lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b × cbox c d"
  by (force simp: cbox_def Basis_prod_def)

lemma cbox_Pair_iff [iff]: "(x, y)  cbox (a, c) (b, d)  x  cbox a b  y  cbox c d"
  by (force simp: cbox_Pair_eq)

lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (λ(x,y). Complex x y) ` (cbox a b × cbox c d)"
  by (force simp: cbox_def Basis_complex_def)

lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {}  cbox a b = {}  cbox c d = {}"
  by (force simp: cbox_Pair_eq)

lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)"
  by auto

lemma mem_box_real[simp]:
  "(x::real)  box a b  a < x  x < b"
  "(x::real)  cbox a b  a  x  x  b"
  by (auto simp: mem_box)

lemma box_real[simp]:
  fixes a b:: real
  shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
  by auto

lemma box_Int_box:
  fixes a :: "'a::euclidean_space"
  shows "box a b  box c d =
    box (iBasis. max (ai) (ci) *R i) (iBasis. min (bi) (di) *R i)"
  unfolding set_eq_iff and Int_iff and mem_box by auto

lemma rational_boxes:
  fixes x :: "'a::euclidean_space"
  assumes "e > 0"
  shows "a b. (iBasis. a  i    b  i  )  x  box a b  box a b  ball x e"
proof -
  define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
  then have e: "e' > 0"
    using assms by (auto)
  have "y. y    y < x  i  x  i - y < e'" for i
    using Rats_dense_in_real[of "x  i - e'" "x  i"] e by force
  then obtain a where
    a: "u. a u    a u < x  u  x  u - a u < e'" by metis
  have "y. y    x  i < y  y - x  i < e'" for i
    using Rats_dense_in_real[of "x  i" "x  i + e'"] e by force
  then obtain b where
    b: "u. b u    x  u < b u  b u - x  u < e'" by metis
  let ?a = "iBasis. a i *R i" and ?b = "iBasis. b i *R i"
  show ?thesis
  proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
    fix y :: 'a
    assume *: "y  box ?a ?b"
    have "dist x y = sqrt (iBasis. (dist (x  i) (y  i))2)"
      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
    also have " < sqrt ((i::'a)Basis. e^2 / real (DIM('a)))"
    proof (rule real_sqrt_less_mono, rule sum_strict_mono)
      fix i :: "'a"
      assume i: "i  Basis"
      have "a i < yi  yi < b i"
        using * i by (auto simp: box_def)
      moreover have "a i < xi" "xi - a i < e'" "xi < b i" "b i - xi < e'"
        using a b by auto
      ultimately have "¦xi - yi¦ < 2 * e'"
        by auto
      then have "dist (x  i) (y  i) < e/sqrt (real (DIM('a)))"
        unfolding e'_def by (auto simp: dist_real_def)
      then have "(dist (x  i) (y  i))2 < (e/sqrt (real (DIM('a))))2"
        by (rule power_strict_mono) auto
      then show "(dist (x  i) (y  i))2 < e2 / real DIM('a)"
        by (simp add: power_divide)
    qed auto
    also have " = e"
      using 0 < e by simp
    finally show "y  ball x e"
      by (auto simp: ball_def)
  qed (use a b in auto simp: box_def)
qed

lemma open_UNION_box:
  fixes M :: "'a::euclidean_space set"
  assumes "open M"
  defines "a'  λf :: 'a  real × real. ((i::'a)Basis. fst (f i) *R i)"
  defines "b'  λf :: 'a  real × real. ((i::'a)Basis. snd (f i) *R i)"
  defines "I  {fBasis E  × . box (a' f) (b' f)  M}"
  shows "M = (fI. box (a' f) (b' f))"
proof -
  have "x  (fI. box (a' f) (b' f))" if "x  M" for x
  proof -
    obtain e where e: "e > 0" "ball x e  M"
      using openE[OF open M x  M] by auto
    moreover obtain a b where ab:
      "x  box a b"
      "i  Basis. a  i  "
      "iBasis. b  i  "
      "box a b  ball x e"
      using rational_boxes[OF e(1)] by metis
    ultimately show ?thesis
       by (intro UN_I[of "λiBasis. (a  i, b  i)"])
          (auto simp: euclidean_representation I_def a'_def b'_def)
  qed
  then show ?thesis by (auto simp: I_def)
qed

corollary open_countable_Union_open_box:
  fixes S :: "'a :: euclidean_space set"
  assumes "open S"
  obtains 𝒟 where "countable 𝒟" "𝒟  Pow S" "X. X  𝒟  a b. X = box a b" "𝒟 = S"
proof -
  let ?a = "λf. ((i::'a)Basis. fst (f i) *R i)"
  let ?b = "λf. ((i::'a)Basis. snd (f i) *R i)"
  let ?I = "{fBasis E  × . box (?a f) (?b f)  S}"
  let ?𝒟 = "(λf. box (?a f) (?b f)) ` ?I"
  show ?thesis
  proof
    have "countable ?I"
      by (simp add: countable_PiE countable_rat)
    then show "countable ?𝒟"
      by blast
    show "?𝒟 = S"
      using open_UNION_box [OF assms] by metis
  qed auto
qed

lemma rational_cboxes:
  fixes x :: "'a::euclidean_space"
  assumes "e > 0"
  shows "a b. (iBasis. a  i    b  i  )  x  cbox a b  cbox a b  ball x e"
proof -
  define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
  then have e: "e' > 0"
    using assms by auto
  have "y. y    y < x  i  x  i - y < e'" for i
    using Rats_dense_in_real[of "x  i - e'" "x  i"] e by force
  then obtain a where
    a: "u. a u    a u < x  u  x  u - a u < e'" by metis
  have "y. y    x  i < y  y - x  i < e'" for i
    using Rats_dense_in_real[of "x  i" "x  i + e'"] e by force
  then obtain b where
    b: "u. b u    x  u < b u  b u - x  u < e'" by metis
  let ?a = "iBasis. a i *R i" and ?b = "iBasis. b i *R i"
  show ?thesis
  proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
    fix y :: 'a
    assume *: "y  cbox ?a ?b"
    have "dist x y = sqrt (iBasis. (dist (x  i) (y  i))2)"
      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
    also have " < sqrt ((i::'a)Basis. e^2 / real (DIM('a)))"
    proof (rule real_sqrt_less_mono, rule sum_strict_mono)
      fix i :: "'a"
      assume i: "i  Basis"
      have "a i  yi  yi  b i"
        using * i by (auto simp: cbox_def)
      moreover have "a i < xi" "xi - a i < e'" "xi < b i" "b i - xi < e'"
        using a b by auto
      ultimately have "¦xi - yi¦ < 2 * e'"
        by auto
      then have "dist (x  i) (y  i) < e/sqrt (real (DIM('a)))"
        unfolding e'_def by (auto simp: dist_real_def)
      then have "(dist (x  i) (y  i))2 < (e/sqrt (real (DIM('a))))2"
        by (rule power_strict_mono) auto
      then show "(dist (x  i) (y  i))2 < e2 / real DIM('a)"
        by (simp add: power_divide)
    qed auto
    also have " = e"
      using 0 < e by simp
    finally show "y  ball x e"
      by (auto simp: ball_def)
  next
    show "x  cbox (iBasis. a i *R i) (iBasis. b i *R i)"
      using a b less_imp_le by (auto simp: cbox_def)
  qed (use a b cbox_def in auto)
qed

lemma open_UNION_cbox:
  fixes M :: "'a::euclidean_space set"
  assumes "open M"
  defines "a'  λf. ((i::'a)Basis. fst (f i) *R i)"
  defines "b'  λf. ((i::'a)Basis. snd (f i) *R i)"
  defines "I  {fBasis E  × . cbox (a' f) (b' f)  M}"
  shows "M = (fI. cbox (a' f) (b' f))"
proof -
  have "x  (fI. cbox (a' f) (b' f))" if "x  M" for x
  proof -
    obtain e where e: "e > 0" "ball x e  M"
      using openE[OF open M x  M] by auto
    moreover obtain a b where ab: "x  cbox a b" "i  Basis. a  i  "
                                  "i  Basis. b  i  " "cbox a b  ball x e"
      using rational_cboxes[OF e(1)] by metis
    ultimately show ?thesis
       by (intro UN_I[of "λiBasis. (a  i, b  i)"])
          (auto simp: euclidean_representation I_def a'_def b'_def)
  qed
  then show ?thesis by (auto simp: I_def)
qed

corollary open_countable_Union_open_cbox:
  fixes S :: "'a :: euclidean_space set"
  assumes "open S"
  obtains 𝒟 where "countable 𝒟" "𝒟  Pow S" "X. X  𝒟  a b. X = cbox a b" "𝒟 = S"
proof -
  let ?a = "λf. ((i::'a)Basis. fst (f i) *R i)"
  let ?b = "λf. ((i::'a)Basis. snd (f i) *R i)"
  let ?I = "{fBasis E  × . cbox (?a f) (?b f)  S}"
  let ?𝒟 = "(λf. cbox (?a f) (?b f)) ` ?I"
  show ?thesis
  proof
    have "countable ?I"
      by (simp add: countable_PiE countable_rat)
    then show "countable ?𝒟"
      by blast
    show "?𝒟 = S"
      using open_UNION_cbox [OF assms] by metis
  qed auto
qed

lemma box_eq_empty:
  fixes a :: "'a::euclidean_space"
  shows "(box a b = {}  (iBasis. bi  ai))" (is ?th1)
    and "(cbox a b = {}  (iBasis. bi < ai))" (is ?th2)
proof -
  have False if "i  Basis" and "bi  ai" and "x  box a b" for i x
    by (smt (verit, ccfv_SIG) mem_box(1) that)
  moreover
  { assume as: "iBasis. ¬ (bi  ai)"
    let ?x = "(1/2) *R (a + b)"
    { fix i :: 'a
      assume i: "i  Basis"
      have "ai < bi"
        using as i by fastforce
      then have "ai < ((1/2) *R (a+b))  i" "((1/2) *R (a+b))  i < bi"
        by (auto simp: inner_add_left)
    }
    then have "box a b  {}"
      by (metis (no_types, opaque_lifting) emptyE mem_box(1))
  }
  ultimately show ?th1 by blast

  have False if "iBasis" and "bi < ai" and "x  cbox a b" for i x
    using mem_box(2) that by force
  moreover
  have "cbox a b  {}" if "iBasis. ¬ (bi < ai)"
    by (metis emptyE linorder_linear mem_box(2) order.strict_iff_not that)
  ultimately show ?th2 by blast
qed

lemma box_ne_empty:
  fixes a :: "'a::euclidean_space"
  shows "cbox a b  {}  (iBasis. ai  bi)"
  and "box a b  {}  (iBasis. ai < bi)"
  unfolding box_eq_empty[of a b] by fastforce+

lemma
  fixes a :: "'a::euclidean_space"
  shows cbox_idem [simp]: "cbox a a = {a}"
    and box_idem [simp]: "box a a = {}"
  unfolding set_eq_iff mem_box eq_iff [symmetric] using euclidean_eq_iff by fastforce+

lemma subset_box_imp:
  fixes a :: "'a::euclidean_space"
  shows "(iBasis. ai  ci  di  bi)  cbox c d  cbox a b"
    and "(iBasis. ai < ci  di < bi)  cbox c d  box a b"
    and "(iBasis. ai  ci  di  bi)  box c d  cbox a b"
     and "(iBasis. ai  ci  di  bi)  box c d  box a b"
  unfolding subset_eq[unfolded Ball_def] unfolding mem_box
  by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+

lemma box_subset_cbox:
  fixes a :: "'a::euclidean_space"
  shows "box a b  cbox a b"
  unfolding subset_eq [unfolded Ball_def] mem_box
  by (fast intro: less_imp_le)

lemma subset_box:
  fixes a :: "'a::euclidean_space"
  shows "cbox c d  cbox a b  (iBasis. ci  di)  (iBasis. ai  ci  di  bi)" (is ?th1)
    and "cbox c d  box a b  (iBasis. ci  di)  (iBasis. ai < ci  di < bi)" (is ?th2)
    and "box c d  cbox a b  (iBasis. ci < di)  (iBasis. ai  ci  di  bi)" (is ?th3)
    and "box c d  box a b  (iBasis. ci < di)  (iBasis. ai  ci  di  bi)" (is ?th4)
proof -
  let ?lesscd = "iBasis. ci < di"
  let ?lerhs = "iBasis. ai  ci  di  bi"
  show ?th1 ?th2
    by (fastforce simp: mem_box)+
  have acdb: "ai  ci  di  bi"
    if i: "i  Basis" and box: "box c d  cbox a b" and cd: "i. i  Basis  ci < di" for i
  proof -
    have "box c d  {}"
      using that
      unfolding box_eq_empty by force
    { let ?x = "(jBasis. (if j=i then ((min (aj) (dj))+cj)/2 else (cj+dj)/2) *R j)::'a"
      assume *: "ai > ci"
      then have "c  j < ?x  j  ?x  j < d  j" if "j  Basis" for j
        using cd that by (fastforce simp add: i *)
      then have "?x  box c d"
        unfolding mem_box by auto
      moreover have "?x  cbox a b"
        using i cd * by (force simp: mem_box)
      ultimately have False using box by auto
    }
    then have "ai  ci" by force
    moreover
    { let ?x = "(jBasis. (if j=i then ((max (bj) (cj))+dj)/2 else (cj+dj)/2) *R j)::'a"
      assume *: "bi < di"
      then have "d  j > ?x  j  ?x  j > c  j" if "j  Basis" for j
        using cd that by (fastforce simp add: i *)
      then have "?x  box c d"
        unfolding mem_box by auto
      moreover have "?x  cbox a b"
        using i cd * by (force simp: mem_box)
      ultimately have False using box by auto
    }
    then have "bi  di" by (rule ccontr) auto
    ultimately show ?thesis by auto
  qed
  show ?th3
    using acdb by (fastforce simp add: mem_box)
  have acdb': "ai  ci  di  bi"
    if "i  Basis" "box c d  box a b" "i. i  Basis  ci < di" for i
      using box_subset_cbox[of a b] that acdb by auto
  show ?th4
    using acdb' by (fastforce simp add: mem_box)
qed

lemma eq_cbox: "cbox a b = cbox c d  cbox a b = {}  cbox c d = {}  a = c  b = d"
      (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have "cbox a b  cbox c d" "cbox c d  cbox a b"
    by auto
  then show ?rhs
    by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI)
qed auto

lemma eq_cbox_box [simp]: "cbox a b = box c d  cbox a b = {}  box c d = {}"
  (is "?lhs  ?rhs")
proof
  assume L: ?lhs
  then have "cbox a b  box c d" "box c d  cbox a b"
    by auto
  with L subset_box show ?rhs
    by (smt (verit) SOME_Basis box_ne_empty(1))
qed force

lemma eq_box_cbox [simp]: "box a b = cbox c d  box a b = {}  cbox c d = {}"
  by (metis eq_cbox_box)

lemma eq_box: "box a b = box c d  box a b = {}  box c d = {}  a = c  b = d"
  (is "?lhs  ?rhs")
proof
  assume L: ?lhs
  then have "box a b  box c d" "box c d  box a b"
    by auto
  then show ?rhs
    unfolding subset_box by (smt (verit) box_ne_empty(2) euclidean_eq_iff)+
qed force

lemma subset_box_complex:
   "cbox a b  cbox c d 
      (Re a  Re b  Im a  Im b)  Re a  Re c  Im a  Im c  Re b  Re d  Im b  Im d"
   "cbox a b  box c d 
      (Re a  Re b  Im a  Im b)  Re a > Re c  Im a > Im c  Re b < Re d  Im b < Im d"
   "box a b  cbox c d 
      (Re a < Re b  Im a < Im b)  Re a  Re c  Im a  Im c  Re b  Re d  Im b  Im d"
   "box a b  box c d 
      (Re a < Re b  Im a < Im b)  Re a  Re c  Im a  Im c  Re b  Re d  Im b  Im d"
  by (subst subset_box; force simp: Basis_complex_def)+

lemma in_cbox_complex_iff:
  "x  cbox a b  Re x  {Re a..Re b}  Im x  {Im a..Im b}"
  by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)

lemma cbox_complex_of_real: "cbox (complex_of_real x) (complex_of_real y) = complex_of_real ` {x..y}"
proof -
  have "(x  Re z  Re z  y  Im z = 0) = (z  complex_of_real ` {x..y})" for z
    by (cases z) (simp add: complex_eq_cancel_iff2 image_iff)
  then show ?thesis
    by (auto simp: in_cbox_complex_iff)
qed

lemma box_Complex_eq:
  "box (Complex a c) (Complex b d) = (λ(x,y). Complex x y) ` (box a b × box c d)"
  by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)

lemma in_box_complex_iff:
  "x  box a b  Re x  {Re a<..<Re b}  Im x  {Im a<..<Im b}"
  by (cases x; cases a; cases b) (auto simp: box_Complex_eq)

lemma box_complex_of_real [simp]: "box (complex_of_real x) (complex_of_real y) = {}"
  by (auto simp: in_box_complex_iff)

lemma Int_interval:
  fixes a :: "'a::euclidean_space"
  shows "cbox a b  cbox c d =
    cbox (iBasis. max (ai) (ci) *R i) (iBasis. min (bi) (di) *R i)"
  unfolding set_eq_iff and Int_iff and mem_box
  by auto

lemma disjoint_interval:
  fixes a::"'a::euclidean_space"
  shows "cbox a b  cbox c d = {}  (iBasis. (bi < ai  di < ci  bi < ci  di < ai))" (is ?th1)
    and "cbox a b  box c d = {}  (iBasis. (bi < ai  di  ci  bi  ci  di  ai))" (is ?th2)
    and "box a b  cbox c d = {}  (iBasis. (bi  ai  di < ci  bi  ci  di  ai))" (is ?th3)
    and "box a b  box c d = {}  (iBasis. (bi  ai  di  ci  bi  ci  di  ai))" (is ?th4)
proof -
  let ?z = "(iBasis. (((max (ai) (ci)) + (min (bi) (di))) / 2) *R i)::'a"
  have **: "P Q. (i :: 'a. i  Basis  Q ?z i  P i) 
      (i x :: 'a. i  Basis  P i  Q x i)  (x. iBasis. Q x i)  (iBasis. P i)"
    by blast
  note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
  show ?th1 unfolding * by (intro **) auto
  show ?th2 unfolding * by (intro **) auto
  show ?th3 unfolding * by (intro **) auto
  show ?th4 unfolding * by (intro **) auto
qed

lemma UN_box_eq_UNIV: "(i::nat. box (- (real i *R One)) (real i *R One)) = UNIV"
proof -
  have "¦x  b¦ < real_of_int (Max ((λb. ¦x  b¦)`Basis) + 1)"
    if [simp]: "b  Basis" for x b :: 'a
  proof -
    have "¦x  b¦  real_of_int ¦x  b¦"
      by (rule le_of_int_ceiling)
    also have "  real_of_int Max ((λb. ¦x  b¦)`Basis)"
      by (auto intro!: ceiling_mono)
    also have " < real_of_int (Max ((λb. ¦x  b¦)`Basis) + 1)"
      by simp
    finally show ?thesis .
  qed
  then have "n::nat. bBasis. ¦x  b¦ < real n" for x :: 'a
    by (metis order.strict_trans reals_Archimedean2)
  moreover have "x b::'a. n::nat.  ¦x  b¦ < real n  - real n < x  b  x  b < real n"
    by auto
  ultimately show ?thesis
    by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
qed

lemma image_affinity_cbox: fixes m::real
  fixes a b c :: "'a::euclidean_space"
  shows "(λx. m *R x + c) ` cbox a b =
    (if cbox a b = {} then {}
     else (if 0  m then cbox (m *R a + c) (m *R b + c)
     else cbox (m *R b + c) (m *R a + c)))"
proof (cases "m = 0")
  case True
  {
    fix x
    assume "iBasis. x  i  c  i" "iBasis. c  i  x  i"
    then have "x = c"
      by (simp add: dual_order.antisym euclidean_eqI)
  }
  moreover have "c  cbox (m *R a + c) (m *R b + c)"
    unfolding True by auto
  ultimately show ?thesis using True by (auto simp: cbox_def)
next
  case False
  {
    fix y
    assume "iBasis. a  i  y  i" "iBasis. y  i  b  i" "m > 0"
    then have "iBasis. (m *R a + c)  i  (m *R y + c)  i" 
          and "iBasis. (m *R y + c)  i  (m *R b + c)  i"
      by (auto simp: inner_distrib)
  }
  moreover
  {
    fix y
    assume "iBasis. a  i  y  i" "iBasis. y  i  b  i" "m < 0"
    then have "iBasis. (m *R b + c)  i  (m *R y + c)  i"
         and  "iBasis. (m *R y + c)  i  (m *R a + c)  i"
      by (auto simp: mult_left_mono_neg inner_distrib)
  }
  moreover
  {
    fix y
    assume "m > 0" and "iBasis. (m *R a + c)  i  y  i"
      and  "iBasis. y  i  (m *R b + c)  i"
    then have "y  (λx. m *R x + c) ` cbox a b"
      unfolding image_iff Bex_def mem_box
      apply (intro exI[where x="(1 / m) *R (y - c)"])
      apply (auto simp: pos_le_divide_eq pos_divide_le_eq mult.commute inner_distrib inner_diff_left)
      done
  }
  moreover
  {
    fix y
    assume "iBasis. (m *R b + c)  i  y  i" "iBasis. y  i  (m *R a + c)  i" "m < 0"
    then have "y  (λx. m *R x + c) ` cbox a b"
      unfolding image_iff Bex_def mem_box
      apply (intro exI[where x="(1 / m) *R (y - c)"])
      apply (auto simp: neg_le_divide_eq neg_divide_le_eq mult.commute inner_distrib inner_diff_left)
      done
  }
  ultimately show ?thesis using False by (auto simp: cbox_def)
qed

lemma image_smult_cbox:"(λx. m *R (x::_::euclidean_space)) ` cbox a b =
  (if cbox a b = {} then {} else if 0  m then cbox (m *R a) (m *R b) else cbox (m *R b) (m *R a))"
  using image_affinity_cbox[of m 0 a b] by auto

lemma swap_continuous:
  assumes "continuous_on (cbox (a,c) (b,d)) (λ(x,y). f x y)"
    shows "continuous_on (cbox (c,a) (d,b)) (λ(x, y). f y x)"
proof -
  have "(λ(x, y). f y x) = (λ(x, y). f x y)  prod.swap"
    by auto
  then show ?thesis
    by (metis assms continuous_on_compose continuous_on_swap swap_cbox_Pair)
qed

lemma open_contains_cbox:
  fixes x :: "'a :: euclidean_space"
  assumes "open A" "x  A"
  obtains a b where "cbox a b  A" "x  box a b" "iBasis. a  i < b  i"
proof -
  from assms obtain R where R: "R > 0" "ball x R  A"
    by (auto simp: open_contains_ball)
  define r :: real where "r = R / (2 * sqrt DIM('a))"
  from R > 0 have [simp]: "r > 0" by (auto simp: r_def)
  define d :: 'a where "d = r *R Topology_Euclidean_Space.One"
  have "cbox (x - d) (x + d)  A"
  proof safe
    fix y assume y: "y  cbox (x - d) (x + d)"
    have "dist x y = sqrt (iBasis. (dist (x  i) (y  i))2)"
      by (subst euclidean_dist_l2) (auto simp: L2_set_def)
    also from y have "sqrt (iBasis. (dist (x  i) (y  i))2)  sqrt (i(Basis::'a set). r2)"
      by (intro real_sqrt_le_mono sum_mono power_mono)
         (auto simp: dist_norm d_def cbox_def algebra_simps)
    also have " = sqrt (DIM('a) * r2)" by simp
    also have "DIM('a) * r2 = (R / 2) ^ 2"
      by (simp add: r_def power_divide)
    also have "sqrt  = R / 2"
      using R > 0 by simp
    also from R > 0 have " < R" by simp
    finally have "y  ball x R" by simp
    with R show "y  A" by blast
  qed
  thus ?thesis
    using that[of "x - d" "x + d"] by (auto simp: algebra_simps d_def box_def)
qed

lemma open_contains_box:
  fixes x :: "'a :: euclidean_space"
  assumes "open A" "x  A"
  obtains a b where "box a b  A" "x  box a b" "iBasis. a  i < b  i"
  by (meson assms box_subset_cbox dual_order.trans open_contains_cbox)

lemma inner_image_box:
  assumes "(i :: 'a :: euclidean_space)  Basis"
  assumes "iBasis. a  i < b  i"
  shows   "(λx. x  i) ` box a b = {a  i<..<b  i}"
proof safe
  fix x assume x: "x  {a  i<..<b  i}"
  let ?y = "(jBasis. (if i = j then x else (a + b)  j / 2) *R j)"
  from x assms have "?y  i  (λx. x  i) ` box a b"
    by (intro imageI) (auto simp: box_def algebra_simps)
  also have "?y  i = (jBasis. (if i = j then x else (a + b)  j / 2) * (j  i))"
    by (simp add: inner_sum_left)
  also have " = (jBasis. if i = j then x else 0)"
    by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
  also have " = x" using assms by simp
  finally show "x  (λx. x  i) ` box a b"  .
qed (insert assms, auto simp: box_def)

lemma inner_image_cbox:
  assumes "(i :: 'a :: euclidean_space)  Basis"
  assumes "iBasis. a  i  b  i"
  shows   "(λx. x  i) ` cbox a b = {a  i..b  i}"
proof safe
  fix x assume x: "x  {a  i..b  i}"
  let ?y = "(jBasis. (if i = j then x else a  j) *R j)"
  from x assms have "?y  i  (λx. x  i) ` cbox a b"
    by (intro imageI) (auto simp: cbox_def)
  also have "?y  i = (jBasis. (if i = j then x else a  j) * (j  i))"
    by (simp add: inner_sum_left)
  also have " = (jBasis. if i = j then x else 0)"
    by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
  also have " = x" using assms by simp
  finally show "x  (λx. x  i) ` cbox a b"  .
qed (insert assms, auto simp: cbox_def)

subsection ‹General Intervals›

definitiontag important› "is_interval (s::('a::euclidean_space) set) 
  (as. bs. x. (iBasis. ((ai  xi  xi  bi)  (bi  xi  xi  ai)))  x  s)"

lemma is_interval_1:
  "is_interval (s::real set)  (as. bs.  x. a  x  x  b  x  s)"
  unfolding is_interval_def by auto

lemma is_interval_Int: "is_interval X  is_interval Y  is_interval (X  Y)"
  unfolding is_interval_def
  by blast

lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
  and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
  unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
  by (meson order_trans le_less_trans less_le_trans less_trans)+

lemma is_interval_empty [iff]: "is_interval {}"
  unfolding is_interval_def  by simp

lemma is_interval_univ [iff]: "is_interval UNIV"
  unfolding is_interval_def  by simp

lemma mem_is_intervalI:
  assumes "is_interval S"
    and "a  S" "b  S"
    and "i. i  Basis  a  i  x  i  x  i  b  i  b  i  x  i  x  i  a  i"
  shows "x  S"
  using assms is_interval_def by force

lemma interval_subst:
  fixes S::"'a::euclidean_space set"
  assumes "is_interval S"
    and "x  S" "y j  S"
    and "j  Basis"
  shows "(iBasis. (if i = j then y i  i else x  i) *R i)  S"
  by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)

lemma mem_box_componentwiseI:
  fixes S::"'a::euclidean_space set"
  assumes "is_interval S"
  assumes "i. i  Basis  x  i  ((λx. x  i) ` S)"
  shows "x  S"
proof -
  from assms have "i  Basis. s  S. x  i = s  i"
    by auto
  with finite_Basis obtain s and bs::"'a list"
    where s: "i. i  Basis  x  i = s i  i" "i. i  Basis  s i  S"
      and bs: "set bs = Basis" "distinct bs"
    by (metis finite_distinct_list)
  from nonempty_Basis s obtain j where j: "j  Basis" "s j  S"
    by blast
  define y where
    "y = rec_list (s j) (λj _ Y. (iBasis. (if i = j then s i  i else Y  i) *R i))"
  have "x = (iBasis. (if i  set bs then s i  i else s j  i) *R i)"
    using bs by (auto simp: s(1)[symmetric] euclidean_representation)
  also have [symmetric]: "y bs = "
    using bs(2) bs(1)[THEN equalityD1]
    by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
  also have "y bs  S"
    using bs(1)[THEN equalityD1]
  proof (induction bs)
    case Nil
    then show ?case
      by (simp add: j y_def)
  next
    case (Cons a bs)
    then show ?case
      using interval_subst[OF assms(1)] s by (simp add: y_def)
  qed
  finally show ?thesis .
qed

lemma cbox01_nonempty [simp]: "cbox 0 One  {}"
  by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg)

lemma box01_nonempty [simp]: "box 0 One  {}"
  by (simp add: box_ne_empty inner_Basis inner_sum_left)

lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
  using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast

lemma interval_subset_is_interval:
  assumes "is_interval S"
  shows "cbox a b  S  cbox a b = {}  a  S  b  S" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs  using box_ne_empty(1) mem_box(2) by fastforce
next
  assume ?rhs
  have "cbox a b  S" if "a  S" "b  S"
    using assms that 
    by (force simp: mem_box intro: mem_is_intervalI)
  with ?rhs show ?lhs
    by blast
qed

lemma is_real_interval_union:
  "is_interval (X  Y)"
  if X: "is_interval X" and Y: "is_interval Y" and I: "(X  {}  Y  {}  X  Y  {})"
  for X Y::"real set"
proof -
  consider "X  {}" "Y  {}" | "X = {}" | "Y = {}" by blast
  then show ?thesis
  proof cases
    case 1
    then obtain r where "r  X  X  Y = {}" "r  Y  X  Y = {}"
      by blast
    then show ?thesis
      using I 1 X Y unfolding is_interval_1
      by (metis (full_types) Un_iff le_cases)
  qed (use that in auto)
qed

lemma is_interval_translationI:
  assumes "is_interval X"
  shows "is_interval ((+) x ` X)"
  unfolding is_interval_def
proof safe
  fix b d e
  assume "b  X" "d  X"
    "iBasis. (x + b)  i  e  i  e  i  (x + d)  i 
       (x + d)  i  e  i  e  i  (x + b)  i"
  hence "e - x  X"
    by (intro mem_is_intervalI[OF assms b  X d  X, of "e - x"])
      (auto simp: algebra_simps)
  thus "e  (+) x ` X" by force
qed

lemma is_interval_uminusI:
  assumes "is_interval X"
  shows "is_interval (uminus ` X)"
  unfolding is_interval_def
proof safe
  fix b d e
  assume "b  X" "d  X"
    "iBasis. (- b)  i  e  i  e  i  (- d)  i 
       (- d)  i  e  i  e  i  (- b)  i"
  hence "- e  X"
    by (smt (verit, ccfv_threshold) assms inner_minus_left mem_is_intervalI)
  thus "e  uminus ` X" by force
qed

lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
  using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
  by (auto simp: image_image)

lemma is_interval_neg_translationI:
  assumes "is_interval X"
  shows "is_interval ((-) x ` X)"
proof -
  have "(-) x ` X = (+) x ` uminus ` X"
    by (force simp: algebra_simps)
  also have "is_interval "
    by (metis is_interval_uminusI is_interval_translationI assms)
  finally show ?thesis .
qed

lemma is_interval_translation[simp]:
  "is_interval ((+) x ` X) = is_interval X"
  using is_interval_neg_translationI[of "(+) x ` X" x]
  by (auto intro!: is_interval_translationI simp: image_image)

lemma is_interval_minus_translation[simp]:
  shows "is_interval ((-) x ` X) = is_interval X"
proof -
  have "(-) x ` X = (+) x ` uminus ` X"
    by (force simp: algebra_simps)
  also have "is_interval  = is_interval X"
    by simp
  finally show ?thesis .
qed

lemma is_interval_minus_translation'[simp]:
  shows "is_interval ((λx. x - c) ` X) = is_interval X"
  using is_interval_translation[of "-c" X]
  by (metis image_cong uminus_add_conv_diff)

lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
  by (simp add: cball_eq_atLeastAtMost is_interval_def)

lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
  by (simp add: ball_eq_greaterThanLessThan is_interval_def)


subsectiontag unimportant› ‹Bounded Projections›

lemma bounded_inner_imp_bdd_above:
  assumes "bounded s"
    shows "bdd_above ((λx. x  a) ` s)"
by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)

lemma bounded_inner_imp_bdd_below:
  assumes "bounded s"
    shows "bdd_below ((λx. x  a) ` s)"
by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)


subsectiontag unimportant› ‹Structural rules for pointwise continuity›

lemma continuous_infnorm[continuous_intros]:
  "continuous F f  continuous F (λx. infnorm (f x))"
  unfolding continuous_def by (rule tendsto_infnorm)

lemma continuous_inner[continuous_intros]:
  assumes "continuous F f"
    and "continuous F g"
  shows "continuous F (λx. inner (f x) (g x))"
  using assms unfolding continuous_def by (rule tendsto_inner)


subsectiontag unimportant› ‹Structural rules for setwise continuity›

lemma continuous_on_infnorm[continuous_intros]:
  "continuous_on s f  continuous_on s (λx. infnorm (f x))"
  unfolding continuous_on by (fast intro: tendsto_infnorm)

lemma continuous_on_inner[continuous_intros]:
  fixes g :: "'a::topological_space  'b::real_inner"
  assumes "continuous_on s f"
    and "continuous_on s g"
  shows "continuous_on s (λx. inner (f x) (g x))"
  using bounded_bilinear_inner assms
  by (rule bounded_bilinear.continuous_on)


subsectiontag unimportant› ‹Openness of halfspaces.›

lemma open_halfspace_lt: "open {x. inner a x < b}"
  by (simp add: open_Collect_less continuous_on_inner)

lemma open_halfspace_gt: "open {x. inner a x > b}"
  by (simp add: open_Collect_less continuous_on_inner)

lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. xi < a}"
  by (simp add: open_Collect_less continuous_on_inner)

lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. xi > a}"
  by (simp add: open_Collect_less continuous_on_inner)

lemma eucl_less_eq_halfspaces:
  fixes a :: "'a::euclidean_space"
  shows "{x. x <e a} = (iBasis. {x. x  i < a  i})"
        "{x. a <e x} = (iBasis. {x. a  i < x  i})"
  by (auto simp: eucl_less_def)

lemma open_Collect_eucl_less[simp, intro]:
  fixes a :: "'a::euclidean_space"
  shows "open {x. x <e a}" "open {x. a <e x}"
  by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)

subsectiontag unimportant› ‹Closure and Interior of halfspaces and hyperplanes›

lemma continuous_at_inner: "continuous (at x) (inner a)"
  unfolding continuous_at by (intro tendsto_intros)

lemma closed_halfspace_le: "closed {x. inner a x  b}"
  by (simp add: closed_Collect_le continuous_on_inner)

lemma closed_halfspace_ge: "closed {x. inner a x  b}"
  by (simp add: closed_Collect_le continuous_on_inner)

lemma closed_hyperplane: "closed {x. inner a x = b}"
  by (simp add: closed_Collect_eq continuous_on_inner)

lemma closed_halfspace_component_le: "closed {x::'a::euclidean_space. xi  a}"
  by (simp add: closed_Collect_le continuous_on_inner)

lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. xi  a}"
  by (simp add: closed_Collect_le continuous_on_inner)

lemma closed_interval_left:
  fixes b :: "'a::euclidean_space"
  shows "closed {x::'a. iBasis. xi  bi}"
  by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner)

lemma closed_interval_right:
  fixes a :: "'a::euclidean_space"
  shows "closed {x::'a. iBasis. ai  xi}"
  by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner)

lemma interior_halfspace_le [simp]:
  assumes "a  0"
    shows "interior {x. a  x  b} = {x. a  x < b}"
proof -
  have *: "a  x < b" if x: "x  S" and S: "S  {x. a  x  b}" and "open S" for S x
  proof -
    obtain e where "e>0" and e: "cball x e  S"
      using open S open_contains_cball x by blast
    then have "x + (e / norm a) *R a  cball x e"
      by (simp add: dist_norm)
    then have "x + (e / norm a) *R a  S"
      using e by blast
    then have "x + (e / norm a) *R a  {x. a  x  b}"
      using S by blast
    moreover have "e * (a  a) / norm a > 0"
      by (simp add: 0 < e assms)
    ultimately show ?thesis
      by (simp add: algebra_simps)
  qed
  show ?thesis
    by (rule interior_unique) (auto simp: open_halfspace_lt *)
qed

lemma interior_halfspace_ge [simp]:
   "a  0  interior {x. a  x  b} = {x. a  x > b}"
using interior_halfspace_le [of "-a" "-b"] by simp

lemma closure_halfspace_lt [simp]:
  assumes "a  0"
    shows "closure {x. a  x < b} = {x