Quelle  Elementary_Normed_Spaces.thy

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

section ‹Elementary Normed Vector Spaces›

theory Elementary_Normed_Spaces
  imports
  "HOL-Library.FuncSet"
  Elementary_Metric_Spaces Cartesian_Space
  Connected
begin
subsection ‹Orthogonal Transformation of Balls›

subsection🍋‹tag unimportant› ‹Various Lemmas Combining Imports›

lemma open_sums:
  fixes T :: "('b::real_normed_vector) set"
  assumes "open S ∨ open T"
  shows "open (∪x∈ S. ∪y ∈ T. {x + y})"
  using assms
proof
  assume S: "open S"
  show ?thesis
  proof (clarsimp simp: open_dist)
    fix x y
    assume "x ∈ S" "y ∈ T"
    with S obtain e where "e > 0" and e: "∧x'. dist x' x < e ==> x' ∈ S"
      by (auto simp: open_dist)
    then have "∧z. dist z (x + y) < e ==> ∃x∈S. ∃y∈T. z = x + y"
      by (metis ‹y ∈ T› diff_add_cancel dist_add_cancel2)
    then show "∃e>0. ∀z. dist z (x + y) < e ⟶ (∃x∈S. ∃y∈T. z = x + y)"
      using ‹0 🚫› ‹x ∈ S› by blast
  qed
next
  assume T: "open T"
  show ?thesis
  proof (clarsimp simp: open_dist)
    fix x y
    assume "x ∈ S" "y ∈ T"
    with T obtain e where "e > 0" and e: "∧x'. dist x' y < e ==> x' ∈ T"
      by (auto simp: open_dist)
    then have "∧z. dist z (x + y) < e ==> ∃x∈S. ∃y∈T. z = x + y"
      by (metis ‹x ∈ S› add_diff_cancel_left' add_diff_eq diff_diff_add dist_norm)
    then show "∃e>0. ∀z. dist z (x + y) < e ⟶ (∃x∈S. ∃y∈T. z = x + y)"
      using ‹0 🚫› ‹y ∈ T› by blast
  qed
qed

lemma image_orthogonal_transformation_ball:
  fixes f :: "'a::euclidean_space ==> 'a"
  assumes "orthogonal_transformation f"
  shows "f ` ball x r = ball (f x) r"
proof (intro equalityI subsetI)
  fix y assume "y ∈ f ` ball x r"
  with assms show "y ∈ ball (f x) r"
    by (auto simp: orthogonal_transformation_isometry)
next
  fix y assume y: "y ∈ ball (f x) r"
  then obtain z where z: "y = f z"
    using assms orthogonal_transformation_surj by blast
  with y assms show "y ∈ f ` ball x r"
    by (auto simp: orthogonal_transformation_isometry)
qed

lemma image_orthogonal_transformation_cball:
  fixes f :: "'a::euclidean_space ==> 'a"
  assumes "orthogonal_transformation f"
  shows "f ` cball x r = cball (f x) r"
proof (intro equalityI subsetI)
  fix y assume "y ∈ f ` cball x r"
  with assms show "y ∈ cball (f x) r"
    by (auto simp: orthogonal_transformation_isometry)
next
  fix y assume y: "y ∈ cball (f x) r"
  then obtain z where z: "y = f z"
    using assms orthogonal_transformation_surj by blast
  with y assms show "y ∈ f ` cball x r"
    by (auto simp: orthogonal_transformation_isometry)
qed


subsection ‹Support›

definition (in monoid_add) support_on :: "'b set ==> ('b ==> 'a) ==> 'b set"
  where "support_on S f = {x∈S. f x ≠ 0}"

lemma in_support_on: "x ∈ support_on S f ⟷ x ∈ S ∧ f x ≠ 0"
  by (simp add: support_on_def)

lemma support_on_simps[simp]:
  "support_on {} f = {}"
  "support_on (insert x S) f =
    (if f x = 0 then support_on S f else insert x (support_on S f))"
  "support_on (S ∪ T) f = support_on S f ∪ support_on T f"
  "support_on (S ∩ T) f = support_on S f ∩ support_on T f"
  "support_on (S - T) f = support_on S f - support_on T f"
  "support_on (f ` S) g = f ` (support_on S (g ∘ f))"
  unfolding support_on_def by auto

lemma support_on_cong:
  "(∧x. x ∈ S ==> f x = 0 ⟷ g x = 0) ==> support_on S f = support_on S g"
  by (auto simp: support_on_def)

lemma support_on_if: "a ≠ 0 ==> support_on A (λx. if P x then a else 0) = {x∈A. P x}"
  by (auto simp: support_on_def)

lemma support_on_if_subset: "support_on A (λx. if P x then a else 0) ⊆ {x ∈ A. P x}"
  by (auto simp: support_on_def)

lemma finite_support[intro]: "finite S ==> finite (support_on S f)"
  unfolding support_on_def by auto

(* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *)
definition (in comm_monoid_add) supp_sum :: "('b ==> 'a) ==> 'b set ==> 'a"
  where "supp_sum f S = (∑x∈support_on S f. f x)"

lemma supp_sum_empty[simp]: "supp_sum f {} = 0"
  unfolding supp_sum_def by auto

lemma supp_sum_insert[simp]:
  "finite (support_on S f) ==>
    supp_sum f (insert x S) = (if x ∈ S then supp_sum f S else f x + supp_sum f S)"
  by (simp add: supp_sum_def in_support_on insert_absorb)

lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (λn. f n / r) A"
  by (cases "r = 0")
     (auto simp: supp_sum_def sum_divide_distrib intro!: sum.cong support_on_cong)


subsection ‹Intervals›

lemma image_affinity_interval:
  fixes c :: "'a::ordered_real_vector"
  shows "((λx. m *🪙R x + c) ` {a..b}) =
           (if {a..b}={} then {}
            else if 0 ≤ m then {m *🪙R a + c .. m *🪙R b + c}
            else {m *🪙R b + c .. m *🪙R a + c})"
         (is "?lhs = ?rhs")
proof (cases "m=0")
  case True
  then show ?thesis
    by force
next
  case False
  show ?thesis
  proof
    show "?lhs ⊆ ?rhs"
      by (auto simp: scaleR_left_mono scaleR_left_mono_neg)
    show "?rhs ⊆ ?lhs"
    proof (clarsimp, intro conjI impI subsetI)
      show "[0 ≤ m; a ≤ b; x ∈ {m *🪙R a + c..m *🪙R b + c}]
            ==> x ∈ (λx. m *🪙R x + c) ` {a..b}" for x
        using False
        by (rule_tac x="inverse m *🪙R (x-c)" in image_eqI)
           (auto simp: pos_le_divideR_eq pos_divideR_le_eq le_diff_eq diff_le_eq)
      show "[¬ 0 ≤ m; a ≤ b; x ∈ {m *🪙R b + c..m *🪙R a + c}]
            ==> x ∈ (λx. m *🪙R x + c) ` {a..b}" for x
        by (rule_tac x="inverse m *🪙R (x-c)" in image_eqI)
           (auto simp add: neg_le_divideR_eq neg_divideR_le_eq le_diff_eq diff_le_eq)
    qed
  qed
qed

subsection ‹Limit Points›

lemma islimpt_ball:
  fixes x y :: "'a::{real_normed_vector,perfect_space}"
  shows "y islimpt ball x e ⟷ 0 < e ∧ y ∈ cball x e"
  (is "?lhs ⟷ ?rhs")
proof
  show ?rhs if ?lhs
  proof
    {
      assume "e ≤ 0"
      then have *: "ball x e = {}"
        using ball_eq_empty[of x e] by auto
      have False using ‹?lhs›
        unfolding * using islimpt_EMPTY[of y] by auto
    }
    then show "e > 0" by (metis not_less)
    show "y ∈ cball x e"
      using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"]
        ball_subset_cball[of x e] ‹?lhs›
      unfolding closed_limpt by auto
  qed
  show ?lhs if ?rhs
  proof -
    from that have "e > 0" by auto
    {
      fix d :: real
      assume "d > 0"
      have "∃x'∈ball x e. x' ≠ y ∧ dist x' y < d"
      proof (cases "d ≤ dist x y")
        case True
        then show ?thesis
        proof (cases "x = y")
          case True
          then have False
            using ‹d ≤ dist x y› ‹d>0› by auto
          then show ?thesis
            by auto
        next
          case False
          have "dist x (y - (d / (2 * dist y x)) *🪙R (y - x)) =
            norm (x - y + (d / (2 * norm (y - x))) *🪙R (y - x))"
            unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric]
            by auto
          also have "… = ∣- 1 + d / (2 * norm (x - y))∣ * norm (x - y)"
            using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"]
            unfolding scaleR_minus_left scaleR_one
            by (auto simp: norm_minus_commute)
          also have "… = ∣- norm (x - y) + d / 2∣"
            unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
            unfolding distrib_right using ‹x≠y›  by auto
          also have "… ≤ e - d/2" using ‹d ≤ dist x y› and ‹d>0› and ‹?rhs›
            by (auto simp: dist_norm)
          finally have "y - (d / (2 * dist y x)) *🪙R (y - x) ∈ ball x e" using ‹d>0›
            by auto
          moreover
          have "(d / (2*dist y x)) *🪙R (y - x) ≠ 0"
            using ‹x≠y›[unfolded dist_nz] ‹d>0› unfolding scaleR_eq_0_iff
            by (auto simp: dist_commute)
          moreover
          have "dist (y - (d / (2 * dist y x)) *🪙R (y - x)) y < d"
            using ‹0 🚫› by (fastforce simp: dist_norm)
          ultimately show ?thesis
            by (rule_tac x = "y - (d / (2*dist y x)) *🪙R (y - x)" in bexI) auto
        qed
      next
        case False
        then have "d > dist x y" by auto
        show "∃x' ∈ ball x e. x' ≠ y ∧ dist x' y < d"
        proof (cases "x = y")
          case True
          obtain z where z: "z ≠ y" "dist z y < min e d"
            using perfect_choose_dist[of "min e d" y]
            using ‹d > 0› ‹e>0› by auto
          show ?thesis
            by (metis True z dist_commute mem_ball min_less_iff_conj)
        next
          case False
          then show ?thesis
            using ‹d>0› ‹d > dist x y› ‹?rhs› by force
        qed
      qed
    }
    then show ?thesis
      unfolding mem_cball islimpt_approachable mem_ball by auto
  qed
qed

lemma closure_ball_lemma:
  fixes x y :: "'a::real_normed_vector"
  assumes "x ≠ y"
  shows "y islimpt ball x (dist x y)"
proof (rule islimptI)
  fix T
  assume "y ∈ T" "open T"
  then obtain r where "0 < r" "∀z. dist z y < r ⟶ z ∈ T"
    unfolding open_dist by fast
  🍋‹choose point between @{term x} and @{term y}, within distance @{term r} of @{term y}.›
  define k where "k = min 1 (r / (2 * dist x y))"
  define z where "z = y + scaleR k (x - y)"
  have z_def2: "z = x + scaleR (1 - k) (y - x)"
    unfolding z_def by (simp add: algebra_simps)
  have "dist z y < r"
    unfolding z_def k_def using ‹0 🚫›
    by (simp add: dist_norm min_def)
  then have "z ∈ T"
    using ‹∀z. dist z y 🚫 ⟶ z ∈ T› by simp
  have "dist x z < dist x y"
    using ‹0 🚫› assms by (simp add: z_def2 k_def dist_norm norm_minus_commute) 
  then have "z ∈ ball x (dist x y)"
    by simp
  have "z ≠ y"
    unfolding z_def k_def using ‹x ≠ y› ‹0 🚫›
    by (simp add: min_def)
  show "∃z∈ball x (dist x y). z ∈ T ∧ z ≠ y"
    using ‹z ∈ ball x (dist x y)› ‹z ∈ T› ‹z ≠ y›
    by fast
qed


subsection ‹Balls and Spheres in Normed Spaces›

lemma mem_ball_0 [simp]: "x ∈ ball 0 e ⟷ norm x < e"
  for x :: "'a::real_normed_vector"
  by simp

lemma mem_cball_0 [simp]: "x ∈ cball 0 e ⟷ norm x ≤ e"
  for x :: "'a::real_normed_vector"
  by simp

lemma closure_ball [simp]:
  fixes x :: "'a::real_normed_vector"
  assumes "0 < e"
  shows "closure (ball x e) = cball x e"
proof
  show "closure (ball x e) ⊆ cball x e"
    using closed_cball closure_minimal by blast
  have "∧y. dist x y < e ∨ dist x y = e ==> y ∈ closure (ball x e)"
    by (metis Un_iff assms closure_ball_lemma closure_def dist_eq_0_iff mem_Collect_eq mem_ball)
  then show "cball x e ⊆ closure (ball x e)"
    by force
qed

lemma mem_sphere_0 [simp]: "x ∈ sphere 0 e ⟷ norm x = e"
  for x :: "'a::real_normed_vector"
  by simp

(* In a trivial vector space, this fails for e = 0. *)
lemma interior_cball [simp]:
  fixes x :: "'a::{real_normed_vector, perfect_space}"
  shows "interior (cball x e) = ball x e"
proof (cases "e ≥ 0")
  case False note cs = this
  from cs have null: "ball x e = {}"
    using ball_empty[of e x] by auto
  moreover
  have "cball x e = {}"
  proof (rule equals0I)
    fix y
    assume "y ∈ cball x e"
    then show False
      by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball
          subset_antisym subset_ball)
  qed
  then have "interior (cball x e) = {}"
    using interior_empty by auto
  ultimately show ?thesis by blast
next
  case True note cs = this
  have "ball x e ⊆ cball x e"
    using ball_subset_cball by auto
  moreover
  {
    fix S y
    assume as: "S ⊆ cball x e" "open S" "y∈S"
    then obtain d where "d>0" and d: "∀x'. dist x' y < d ⟶ x' ∈ S"
      unfolding open_dist by blast
    then obtain xa where xa_y: "xa ≠ y" and xa: "dist xa y < d"
      using perfect_choose_dist [of d] by auto
    have "xa ∈ S"
      using d[THEN spec[where x = xa]]
      using xa by (auto simp: dist_commute)
    then have xa_cball: "xa ∈ cball x e"
      using as(1) by auto
    then have "y ∈ ball x e"
    proof (cases "x = y")
      case True
      then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce
      then show "y ∈ ball x e"
        using ‹x = y › by simp
    next
      case False
      have "dist (y + (d / 2 / dist y x) *🪙R (y - x)) y < d"
        unfolding dist_norm
        using ‹d>0› norm_ge_zero[of "y - x"] ‹x ≠ y› by auto
      then have *: "y + (d / 2 / dist y x) *🪙R (y - x) ∈ cball x e"
        using d as(1)[unfolded subset_eq] by blast
      have "y - x ≠ 0" using ‹x ≠ y› by auto
      hence **:"d / (2 * norm (y - x)) > 0"
        unfolding zero_less_norm_iff[symmetric] using ‹d>0› by auto
      have "dist (y + (d / 2 / dist y x) *🪙R (y - x)) x =
        norm (y + (d / (2 * norm (y - x))) *🪙R y - (d / (2 * norm (y - x))) *🪙R x - x)"
        by (auto simp: dist_norm algebra_simps)
      also have "… = norm ((1 + d / (2 * norm (y - x))) *🪙R (y - x))"
        by (auto simp: algebra_simps)
      also have "… = ∣1 + d / (2 * norm (y - x))∣ * norm (y - x)"
        using ** by auto
      also have "… = (dist y x) + d/2"
        using ** by (auto simp: distrib_right dist_norm)
      finally have "e ≥ dist x y +d/2"
        using *[unfolded mem_cball] by (auto simp: dist_commute)
      then show "y ∈ ball x e"
        unfolding mem_ball using ‹d>0› by auto
    qed
  }
  then have "∀S ⊆ cball x e. open S ⟶ S ⊆ ball x e"
    by auto
  ultimately show ?thesis
    using interior_unique[of "ball x e" "cball x e"]
    using open_ball[of x e]
    by auto
qed

lemma frontier_ball [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "0 < e ==> frontier (ball a e) = sphere a e"
  by (force simp: frontier_def)

lemma frontier_cball [simp]:
  fixes a :: "'a::{real_normed_vector, perfect_space}"
  shows "frontier (cball a e) = sphere a e"
  by (force simp: frontier_def)

corollary compact_sphere [simp]:
  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
  shows "compact (sphere a r)"
using compact_frontier [of "cball a r"] by simp

corollary bounded_sphere [simp]:
  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
  shows "bounded (sphere a r)"
by (simp add: compact_imp_bounded)

corollary closed_sphere  [simp]:
  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
  shows "closed (sphere a r)"
by (simp add: compact_imp_closed)

lemma image_add_ball [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "(+) b ` ball a r = ball (a+b) r"
proof -
  { fix x :: 'a
    assume "dist (a + b) x < r"
    moreover
    have "b + (x - b) = x"
      by simp
    ultimately have "x ∈ (+) b ` ball a r"
      by (metis add.commute dist_add_cancel image_eqI mem_ball) }
  then show ?thesis
    by (auto simp: add.commute)
qed

lemma image_add_cball [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "(+) b ` cball a r = cball (a+b) r"
proof -
  have "∧x. dist (a + b) x ≤ r ==> ∃y∈cball a r. x = b + y"
    by (metis (no_types) add.commute diff_add_cancel dist_add_cancel2 mem_cball)
  then show ?thesis
    by (force simp: add.commute)
qed


subsection🍋‹tag unimportant› ‹Various Lemmas on Normed Algebras›


lemma closed_of_nat_image: "closed (of_nat ` A :: 'a::real_normed_algebra_1 set)"
  by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_nat)

lemma closed_of_int_image: "closed (of_int ` A :: 'a::real_normed_algebra_1 set)"
  by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_int)

lemma closed_Nats [simp]: "closed (ℕ :: 'a :: real_normed_algebra_1 set)"
  unfolding Nats_def by (rule closed_of_nat_image)

lemma closed_Ints [simp]: "closed (ℤ :: 'a :: real_normed_algebra_1 set)"
  unfolding Ints_def by (rule closed_of_int_image)

lemma closed_subset_Ints:
  fixes A :: "'a :: real_normed_algebra_1 set"
  assumes "A ⊆ ℤ"
  shows   "closed A"
proof (intro discrete_imp_closed[OF zero_less_one] ballI impI, goal_cases)
  case (1 x y)
  with assms have "x ∈ ℤ" and "y ∈ ℤ" by auto
  with ‹dist y x 🚫› show "y = x"
    by (auto elim!: Ints_cases simp: dist_of_int)
qed

subsection ‹Filters›

definition indirection :: "'a::real_normed_vector ==> 'a ==> 'a filter"  (infixr ‹indirection› 70)
  where "a indirection v = at a within {b. ∃c≥0. b - a = scaleR c v}"


subsection ‹Trivial Limits›

lemma trivial_limit_at_infinity:
  "¬ trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) filter)"
proof -
  obtain x::'a where "x ≠ 0"
    by (meson perfect_choose_dist zero_less_one)
  then have "b ≤ norm ((b / norm x) *🪙R x)" for b
    by simp
  then show ?thesis
    unfolding trivial_limit_def eventually_at_infinity
    by blast
qed

lemma at_within_ball_bot_iff:
  fixes x y :: "'a::{real_normed_vector,perfect_space}"
  shows "at x within ball y r = bot ⟷ (r=0 ∨ x ∉ cball y r)"
  unfolding trivial_limit_within
  by (metis (no_types) cball_empty equals0D islimpt_ball less_linear) 


subsection ‹Limits›

proposition Lim_at_infinity: "(f ---> l) at_infinity ⟷ (∀e>0. ∃b. ∀x. norm x ≥ b ⟶ dist (f x) l < e)"
  by (auto simp: tendsto_iff eventually_at_infinity)

corollary Lim_at_infinityI [intro?]:
  assumes "∧e. e > 0 ==> ∃B. ∀x. norm x ≥ B ⟶ dist (f x) l ≤ e"
  shows "(f ---> l) at_infinity"
proof -
  have "∧e. e > 0 ==> ∃B. ∀x. norm x ≥ B ⟶ dist (f x) l < e"
    by (meson assms dense le_less_trans)
  then show ?thesis
    using Lim_at_infinity by blast
qed

lemma Lim_transform_within_set_eq:
  fixes a :: "'a::metric_space" and l :: "'b::metric_space"
  shows "eventually (λx. x ∈ S ⟷ x ∈ T) (at a)
         ==> ((f ---> l) (at a within S) ⟷ (f ---> l) (at a within T))"
  by (force intro: Lim_transform_within_set elim: eventually_mono)

lemma Lim_null:
  fixes f :: "'a ==> 'b::real_normed_vector"
  shows "(f ---> l) net ⟷ ((λx. f(x) - l) ---> 0) net"
  by (simp add: Lim dist_norm)

lemma Lim_null_comparison:
  fixes f :: "'a ==> 'b::real_normed_vector"
  assumes "eventually (λx. norm (f x) ≤ g x) net" "(g ---> 0) net"
  shows "(f ---> 0) net"
  using assms(2)
proof (rule metric_tendsto_imp_tendsto)
  show "eventually (λx. dist (f x) 0 ≤ dist (g x) 0) net"
    using assms(1) by (rule eventually_mono) (simp add: dist_norm)
qed

lemma Lim_transform_bound:
  fixes f :: "'a ==> 'b::real_normed_vector"
    and g :: "'a ==> 'c::real_normed_vector"
  assumes "eventually (λn. norm (f n) ≤ norm (g n)) net"
    and "(g ---> 0) net"
  shows "(f ---> 0) net"
  using assms(1) tendsto_norm_zero [OF assms(2)]
  by (rule Lim_null_comparison)

lemma lim_null_mult_right_bounded:
  fixes f :: "'a ==> 'b::real_normed_div_algebra"
  assumes f: "(f ---> 0) F" and g: "eventually (λx. norm(g x) ≤ B) F"
    shows "((λz. f z * g z) ---> 0) F"
proof -
  have "((λx. norm (f x) * norm (g x)) ---> 0) F"
  proof (rule Lim_null_comparison)
    show "∀🪙F x in F. norm (norm (f x) * norm (g x)) ≤ norm (f x) * B"
      by (simp add: eventually_mono [OF g] mult_left_mono)
    show "((λx. norm (f x) * B) ---> 0) F"
      by (simp add: f tendsto_mult_left_zero tendsto_norm_zero)
  qed
  then show ?thesis
    by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult)
qed

lemma lim_null_mult_left_bounded:
  fixes f :: "'a ==> 'b::real_normed_div_algebra"
  assumes g: "eventually (λx. norm(g x) ≤ B) F" and f: "(f ---> 0) F"
    shows "((λz. g z * f z) ---> 0) F"
proof -
  have "((λx. norm (g x) * norm (f x)) ---> 0) F"
  proof (rule Lim_null_comparison)
    show "∀🪙F x in F. norm (norm (g x) * norm (f x)) ≤ B * norm (f x)"
      by (simp add: eventually_mono [OF g] mult_right_mono)
    show "((λx. B * norm (f x)) ---> 0) F"
      by (simp add: f tendsto_mult_right_zero tendsto_norm_zero)
  qed
  then show ?thesis
    by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult)
qed

lemma lim_null_scaleR_bounded:
  assumes f: "(f ---> 0) net" and gB: "eventually (λa. f a = 0 ∨ norm(g a) ≤ B) net"
    shows "((λn. f n *🪙R g n) ---> 0) net"
proof
  fix ε::real
  assume "0 < ε"
  then have B: "0 < ε / (abs B + 1)" by simp
  have *: "∣f x∣ * norm (g x) < ε" if f: "∣f x∣ * (∣B∣ + 1) < ε" and g: "norm (g x) ≤ B" for x
  proof -
    have "∣f x∣ * norm (g x) ≤ ∣f x∣ * B"
      by (simp add: mult_left_mono g)
    also have "… ≤ ∣f x∣ * (∣B∣ + 1)"
      by (simp add: mult_left_mono)
    also have "… < ε"
      by (rule f)
    finally show ?thesis .
  qed
  have "∧x. [∣f x∣ < ε / (∣B∣ + 1); norm (g x) ≤ B] ==> ∣f x∣ * norm (g x) < ε"
    by (simp add: "*" pos_less_divide_eq)
  then show "∀🪙F x in net. dist (f x *🪙R g x) 0 < ε"
    using ‹0 🚫ε› by (auto intro: eventually_mono [OF eventually_conj [OF tendstoD [OF f B] gB]])
qed

lemma Lim_norm_ubound:
  fixes f :: "'a ==> 'b::real_normed_vector"
  assumes "¬(trivial_limit net)" "(f ---> l) net" "eventually (λx. norm(f x) ≤ e) net"
  shows "norm(l) ≤ e"
  using assms by (fast intro: tendsto_le tendsto_intros)

lemma Lim_norm_lbound:
  fixes f :: "'a ==> 'b::real_normed_vector"
  assumes "¬ trivial_limit net"
    and "(f ---> l) net"
    and "eventually (λx. e ≤ norm (f x)) net"
  shows "e ≤ norm l"
  using assms by (fast intro: tendsto_le tendsto_intros)

text‹Limit under bilinear function›

lemma Lim_bilinear:
  assumes "(f ---> l) net"
    and "(g ---> m) net"
    and "bounded_bilinear h"
  shows "((λx. h (f x) (g x)) ---> (h l m)) net"
  using ‹bounded_bilinear h› ‹(f ---> l) net› ‹(g ---> m) net›
  by (rule bounded_bilinear.tendsto)

lemma Lim_at_zero:
  fixes a :: "'a::real_normed_vector"
    and l :: "'b::topological_space"
  shows "(f ---> l) (at a) ⟷ ((λx. f(a + x)) ---> l) (at 0)"
  using LIM_offset_zero LIM_offset_zero_cancel ..


subsection🍋‹tag unimportant› ‹Limit Point of Filter›

lemma netlimit_at_vector:
  fixes a :: "'a::real_normed_vector"
  shows "netlimit (at a) = a"
proof (cases "∃x. x ≠ a")
  case True then obtain x where x: "x ≠ a" ..
  have "∧d. 0 < d ==> ∃x. x ≠ a ∧ norm (x - a) < d"
    by (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI) (simp add: norm_sgn sgn_zero_iff x)
  then have "¬ trivial_limit (at a)"
    by (auto simp: trivial_limit_def eventually_at dist_norm)
  then show ?thesis
    by (rule Lim_ident_at [of a UNIV])
qed simp

subsection ‹Boundedness›

lemma continuous_on_closure_norm_le:
  fixes f :: "'a::metric_space ==> 'b::real_normed_vector"
  assumes "continuous_on (closure s) f"
    and "∀y ∈ s. norm(f y) ≤ b"
    and "x ∈ (closure s)"
  shows "norm (f x) ≤ b"
proof -
  have *: "f ` s ⊆ cball 0 b"
    using assms(2)[unfolded mem_cball_0[symmetric]] by auto
  show ?thesis
    by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0)
qed

lemma bounded_pos: "bounded S ⟷ (∃b>0. ∀x∈ S. norm x ≤ b)"
  unfolding bounded_iff 
  by (meson less_imp_le not_le order_trans zero_less_one)

lemma bounded_pos_less: "bounded S ⟷ (∃b>0. ∀x∈ S. norm x < b)"
  by (metis bounded_pos le_less_trans less_imp_le linordered_field_no_ub)

lemma bounded_normE:
  assumes "bounded A"
  obtains B where "B > 0" "∧z. z ∈ A ==> norm z ≤ B"
  by (meson assms bounded_pos)

lemma bounded_normE_less:
  assumes "bounded A"
  obtains B where "B > 0" "∧z. z ∈ A ==> norm z < B"
  by (meson assms bounded_pos_less)

lemma Bseq_eq_bounded:
  fixes f :: "nat ==> 'a::real_normed_vector"
  shows "Bseq f ⟷ bounded (range f)"
  unfolding Bseq_def bounded_pos by auto

lemma bounded_linear_image:
  assumes "bounded S"
    and "bounded_linear f"
  shows "bounded (f ` S)"
proof -
  from assms(1) obtain b where "b > 0" and b: "∀x∈S. norm x ≤ b"
    unfolding bounded_pos by auto
  from assms(2) obtain B where B: "B > 0" "∀x. norm (f x) ≤ B * norm x"
    using bounded_linear.pos_bounded by (auto simp: ac_simps)
  show ?thesis
    unfolding bounded_pos
  proof (intro exI, safe)
    show "norm (f x) ≤ B * b" if "x ∈ S" for x
      by (meson B b less_imp_le mult_left_mono order_trans that)
  qed (use ‹b > 0› ‹B > 0› in auto)
qed

lemma bounded_scaling:
  fixes S :: "'a::real_normed_vector set"
  shows "bounded S ==> bounded ((λx. c *🪙R x) ` S)"
  by (simp add: bounded_linear_image bounded_linear_scaleR_right)

lemma bounded_scaleR_comp:
  fixes f :: "'a ==> 'b::real_normed_vector"
  assumes "bounded (f ` S)"
  shows "bounded ((λx. r *🪙R f x) ` S)"
  using bounded_scaling[of "f ` S" r] assms
  by (auto simp: image_image)

lemma bounded_translation:
  fixes S :: "'a::real_normed_vector set"
  assumes "bounded S"
  shows "bounded ((λx. a + x) ` S)"
proof -
  from assms obtain b where b: "b > 0" "∀x∈S. norm x ≤ b"
    unfolding bounded_pos by auto
  {
    fix x
    assume "x ∈ S"
    then have "norm (a + x) ≤ b + norm a"
      using norm_triangle_ineq[of a x] b by auto
  }
  then show ?thesis
    unfolding bounded_pos
    using norm_ge_zero[of a] b(1) and add_strict_increasing[of b 0 "norm a"]
    by (auto intro!: exI[of _ "b + norm a"])
qed

lemma bounded_translation_minus:
  fixes S :: "'a::real_normed_vector set"
  shows "bounded S ==> bounded ((λx. x - a) ` S)"
using bounded_translation [of S "-a"] by simp

lemma bounded_uminus [simp]:
  fixes X :: "'a::real_normed_vector set"
  shows "bounded (uminus ` X) ⟷ bounded X"
by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp: add.commute norm_minus_commute)

lemma uminus_bounded_comp [simp]:
  fixes f :: "'a ==> 'b::real_normed_vector"
  shows "bounded ((λx. - f x) ` S) ⟷ bounded (f ` S)"
  using bounded_uminus[of "f ` S"]
  by (auto simp: image_image)

lemma bounded_plus_comp:
  fixes f g::"'a ==> 'b::real_normed_vector"
  assumes "bounded (f ` S)"
  assumes "bounded (g ` S)"
  shows "bounded ((λx. f x + g x) ` S)"
proof -
  {
    fix B C
    assume "∧x. x∈S ==> norm (f x) ≤ B" "∧x. x∈S ==> norm (g x) ≤ C"
    then have "∧x. x ∈ S ==> norm (f x + g x) ≤ B + C"
      by (auto intro!: norm_triangle_le add_mono)
  } then show ?thesis
    using assms by (fastforce simp: bounded_iff)
qed

lemma bounded_plus:
  fixes S ::"'a::real_normed_vector set"
  assumes "bounded S" "bounded T"
  shows "bounded ((λ(x,y). x + y) ` (S × T))"
  using bounded_plus_comp [of fst "S × T" snd] assms
  by (auto simp: split_def split: if_split_asm)

lemma bounded_minus_comp:
  "bounded (f ` S) ==> bounded (g ` S) ==> bounded ((λx. f x - g x) ` S)"
  for f g::"'a ==> 'b::real_normed_vector"
  using bounded_plus_comp[of "f" S "λx. - g x"]
  by auto

lemma bounded_minus:
  fixes S ::"'a::real_normed_vector set"
  assumes "bounded S" "bounded T"
  shows "bounded ((λ(x,y). x - y) ` (S × T))"
  using bounded_minus_comp [of fst "S × T" snd] assms
  by (auto simp: split_def split: if_split_asm)

lemma bounded_sums:
  fixes S :: "'a::real_normed_vector set"
  assumes "bounded S" and "bounded T"
  shows "bounded (∪x∈ S. ∪y ∈ T. {x + y})"
  using assms by (simp add: bounded_iff) (meson norm_triangle_mono)

lemma bounded_differences:
  fixes S :: "'a::real_normed_vector set"
  assumes "bounded S" and "bounded T"
  shows "bounded (∪x∈ S. ∪y ∈ T. {x - y})"
  using assms by (simp add: bounded_iff) (meson add_mono norm_triangle_le_diff)

lemma not_bounded_UNIV[simp]:
  "¬ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)"
proof (auto simp: bounded_pos not_le)
  obtain x :: 'a where "x ≠ 0"
    using perfect_choose_dist [OF zero_less_one] by fast
  fix b :: real
  assume b: "b >0"
  have b1: "b +1 ≥ 0"
    using b by simp
  with ‹x ≠ 0› have "b < norm (scaleR (b + 1) (sgn x))"
    by (simp add: norm_sgn)
  then show "∃x::'a. b < norm x" ..
qed

corollary cobounded_imp_unbounded:
    fixes S :: "'a::{real_normed_vector, perfect_space} set"
    shows "bounded (- S) ==> ¬ bounded S"
  using bounded_Un [of S "-S"]  by (simp)

subsection🍋‹tag unimportant›\<open>Relations among convergence and absolute convergence for power series›

lemma summable_imp_bounded:
  fixes f :: "nat ==> 'a::real_normed_vector"
  shows "summable f ==> bounded (range f)"
by (frule summable_LIMSEQ_zero) (simp add: convergent_imp_bounded)

lemma summable_imp_sums_bounded:
   "summable f ==> bounded (range (λn. sum f {..
by (auto simp: summable_def sums_def dest: convergent_imp_bounded)

lemma power_series_conv_imp_absconv_weak:
  fixes a:: "nat ==> 'a::{real_normed_div_algebra,banach}" and w :: 'a
  assumes sum: "summable (λn. a n * z ^ n)" and no: "norm w < norm z"
    shows "summable (λn. of_real(norm(a n)) * w ^ n)"
proof -
  obtain M where M: "∧x. norm (a x * z ^ x) ≤ M"
    using summable_imp_bounded [OF sum] by (force simp: bounded_iff)
  show ?thesis
  proof (rule series_comparison_complex)
    have "∧n. norm (a n) * norm z ^ n ≤ M"
      by (metis (no_types) M norm_mult norm_power)
    then show "summable (λn. complex_of_real (norm (a n) * norm w ^ n))"
      using Abel_lemma no norm_ge_zero summable_of_real by blast
  qed (auto simp: norm_mult norm_power)
qed


subsection ‹Normed spaces with the Heine-Borel property›

lemma not_compact_UNIV[simp]:
  fixes s :: "'a::{real_normed_vector,perfect_space,heine_borel} set"
  shows "¬ compact (UNIV::'a set)"
    by (simp add: compact_eq_bounded_closed)

lemma not_compact_space_euclideanreal [simp]: "¬ compact_space euclideanreal"
  by (simp add: compact_space_def)

text‹Representing sets as the union of a chain of compact sets.›
lemma closed_Union_compact_subsets:
  fixes S :: "'a::{heine_borel,real_normed_vector} set"
  assumes "closed S"
  obtains F where "∧n. compact(F n)" "∧n. F n ⊆ S" "∧n. F n ⊆ F(Suc n)"
                  "(∪n. F n) = S" "∧K. [compact K; K ⊆ S] ==> ∃N. ∀n ≥ N. K ⊆ F n"
proof
  show "compact (S ∩ cball 0 (of_nat n))" for n
    using assms compact_eq_bounded_closed by auto
next
  show "(∪n. S ∩ cball 0 (real n)) = S"
    by (auto simp: real_arch_simple)
next
  fix K :: "'a set"
  assume "compact K" "K ⊆ S"
  then obtain N where "K ⊆ cball 0 N"
    by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI)
  then show "∃N. ∀n≥N. K ⊆ S ∩ cball 0 (real n)"
    by (metis of_nat_le_iff Int_subset_iff ‹K ⊆ S› real_arch_simple subset_cball subset_trans)
qed auto

subsection ‹Intersecting chains of compact sets and the Baire property›

proposition bounded_closed_chain:
  fixes F :: "'a::heine_borel set set"
  assumes "B ∈ F" "bounded B" and F: "∧S. S ∈ F ==> closed S" and "{} ∉ F"
      and chain: "∧S T. S ∈ F ∧ T ∈ F ==> S ⊆ T ∨ T ⊆ S"
    shows "∩F ≠ {}"
proof -
  have "B ∩ ∩F ≠ {}"
  proof (rule compact_imp_fip)
    show "compact B" "∧T. T ∈ F ==> closed T"
      by (simp_all add: assms compact_eq_bounded_closed)
    show "[finite G; G ⊆ F] ==> B ∩ ∩G ≠ {}" for G
    proof (induction G rule: finite_induct)
      case empty
      with assms show ?case by force
    next
      case (insert U G)
      then have "U ∈ F" and ne: "B ∩ ∩G ≠ {}" by auto
      then consider "B ⊆ U" | "U ⊆ B"
          using ‹B ∈ F› chain by blast
        then show ?case
        proof cases
          case 1
          then show ?thesis
            using Int_left_commute ne by auto
        next
          case 2
          have "U ≠ {}"
            using ‹U ∈ F› ‹{} ∉ F› by blast
          moreover
          have False if "∧x. x ∈ U ==> ∃Y∈G. x ∉ Y"
          proof -
            have "∧x. x ∈ U ==> ∃Y∈G. Y ⊆ U"
              by (metis chain contra_subsetD insert.prems insert_subset that)
            then obtain Y where "Y ∈ G" "Y ⊆ U"
              by (metis all_not_in_conv ‹U ≠ {}›)
            moreover obtain x where "x ∈ ∩G"
              by (metis Int_emptyI ne)
            ultimately show ?thesis
              by (metis Inf_lower subset_eq that)
          qed
          with 2 show ?thesis
            by blast
        qed
      qed
  qed
  then show ?thesis by blast
qed

corollary compact_chain:
  fixes F :: "'a::heine_borel set set"
  assumes "∧S. S ∈ F ==> compact S" "{} ∉ F"
          "∧S T. S ∈ F ∧ T ∈ F ==> S ⊆ T ∨ T ⊆ S"
    shows "∩ F ≠ {}"
proof (cases "F = {}")
  case True
  then show ?thesis by auto
next
  case False
  show ?thesis
    by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain)
qed

lemma compact_nest:
  fixes F :: "'a::linorder ==> 'b::heine_borel set"
  assumes F: "∧n. compact(F n)" "∧n. F n ≠ {}" and mono: "∧m n. m ≤ n ==> F n ⊆ F m"
  shows "∩(range F) ≠ {}"
proof -
  have *: "∧S T. S ∈ range F ∧ T ∈ range F ==> S ⊆ T ∨ T ⊆ S"
    by (metis mono image_iff le_cases)
  show ?thesis
    using F by (intro compact_chain [OF _ _ *]; blast dest: *)
qed

text‹The Baire property of dense sets›
theorem Baire:
  fixes S::"'a::{real_normed_vector,heine_borel} set"
  assumes "closed S" "countable G"
      and ope: "∧T. T ∈ G ==> openin (top_of_set S) T ∧ S ⊆ closure T"
 shows "S ⊆ closure(∩G)"
proof (cases "G = {}")
  case True
  then show ?thesis
    using closure_subset by auto
next
  let ?g = "from_nat_into G"
  case False
  then have gin: "?g n ∈ G" for n
    by (simp add: from_nat_into)
  show ?thesis
  proof (clarsimp simp: closure_approachable)
    fix x and e::real
    assume "x ∈ S" "0 < e"
    obtain TF where opeF: "∧n. openin (top_of_set S) (TF n)"
               and ne: "∧n. TF n ≠ {}"
               and subg: "∧n. S ∩ closure(TF n) ⊆ ?g n"
               and subball: "∧n. closure(TF n) ⊆ ball x e"
               and decr: "∧n. TF(Suc n) ⊆ TF n"
    proof -
      have *: "∃Y. (openin (top_of_set S) Y ∧ Y ≠ {} ∧
                   S ∩ closure Y ⊆ ?g n ∧ closure Y ⊆ ball x e) ∧ Y ⊆ U"
        if opeU: "openin (top_of_set S) U" and "U ≠ {}" and cloU: "closure U ⊆ ball x e" for U n
      proof -
        obtain T where T: "open T" "U = T ∩ S"
          using ‹openin (top_of_set S) U› by (auto simp: openin_subtopology)
        with ‹U ≠ {}› have "T ∩ closure (?g n) ≠ {}"
          using gin ope by fastforce
        then have "T ∩ ?g n ≠ {}"
          using ‹open T› open_Int_closure_eq_empty by blast
        then obtain y where "y ∈ U" "y ∈ ?g n"
          using T ope [of "?g n", OF gin] by (blast dest:  openin_imp_subset)
        moreover have "openin (top_of_set S) (U ∩ ?g n)"
          using gin ope opeU by blast
        ultimately obtain d where U: "U ∩ ?g n ⊆ S" and "d > 0" and d: "ball y d ∩ S ⊆ U ∩ ?g n"
          by (force simp: openin_contains_ball)
        show ?thesis
        proof (intro exI conjI)
          show "openin (top_of_set S) (S ∩ ball y (d/2))"
            by (simp add: openin_open_Int)
          show "S ∩ ball y (d/2) ≠ {}"
            using ‹0 🚫› ‹y ∈ U› opeU openin_imp_subset by fastforce
          have "S ∩ closure (S ∩ ball y (d/2)) ⊆ S ∩ closure (ball y (d/2))"
            using closure_mono by blast
          also have "... ⊆ ?g n"
            using ‹d > 0› d by force
          finally show "S ∩ closure (S ∩ ball y (d/2)) ⊆ ?g n" .
          have "closure (S ∩ ball y (d/2)) ⊆ S ∩ ball y d"
          proof -
            have "closure (ball y (d/2)) ⊆ ball y d"
              using ‹d > 0› by auto
            then have "closure (S ∩ ball y (d/2)) ⊆ ball y d"
              by (meson closure_mono inf.cobounded2 subset_trans)
            then show ?thesis
              by (simp add: ‹closed S› closure_minimal)
          qed
          also have "... ⊆ ball x e"
            using cloU closure_subset d by blast
          finally show "closure (S ∩ ball y (d/2)) ⊆ ball x e" .
          show "S ∩ ball y (d/2) ⊆ U"
            using ball_divide_subset_numeral d by blast
        qed
      qed
      let ?Φ = "λn X. openin (top_of_set S) X ∧ X ≠ {} ∧
                      S ∩ closure X ⊆ ?g n ∧ closure X ⊆ ball x e"
      have "closure (S ∩ ball x (e/2)) ⊆ closure(ball x (e/2))"
        by (simp add: closure_mono)
      also have "... ⊆ ball x e"
        using ‹e > 0› by auto
      finally have "closure (S ∩ ball x (e/2)) ⊆ ball x e" .
      moreover have"openin (top_of_set S) (S ∩ ball x (e/2))" "S ∩ ball x (e/2) ≠ {}"
        using ‹0 🚫› ‹x ∈ S› by auto
      ultimately obtain Y where Y: "?Φ 0 Y ∧ Y ⊆ S ∩ ball x (e/2)"
            using * [of "S ∩ ball x (e/2)" 0] by metis
      show thesis
      proof (rule exE [OF dependent_nat_choice])
        show "∃x. ?Φ 0 x"
          using Y by auto
        show "∃Y. ?Φ (Suc n) Y ∧ Y ⊆ X" if "?Φ n X" for X n
          using that by (blast intro: *)
      qed (use that in metis)
    qed
    have "(∩n. S ∩ closure (TF n)) ≠ {}"
    proof (rule compact_nest)
      show "∧n. compact (S ∩ closure (TF n))"
        by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF ‹closed S›])
      show "∧n. S ∩ closure (TF n) ≠ {}"
        by (metis Int_absorb1 opeF ‹closed S› closure_eq_empty closure_minimal ne openin_imp_subset)
      show "∧m n. m ≤ n ==> S ∩ closure (TF n) ⊆ S ∩ closure (TF m)"
        by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le)
    qed
    moreover have "(∩n. S ∩ closure (TF n)) ⊆ {y ∈ ∩G. dist y x < e}"
    proof (clarsimp, intro conjI)
      fix y
      assume "y ∈ S" and y: "∀n. y ∈ closure (TF n)"
      then show "∀T∈G. y ∈ T"
        by (metis Int_iff from_nat_into_surj [OF ‹countable G›] subsetD subg)
      show "dist y x < e"
        by (metis y dist_commute mem_ball subball subsetCE)
    qed
    ultimately show "∃y ∈ ∩G. dist y x < e"
      by auto
  qed
qed


subsection ‹Continuity›

subsubsection🍋‹tag unimportant› ‹Structural rules for uniform continuity›

lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]:
  fixes g :: "_::metric_space ==> _"
  assumes "uniformly_continuous_on s g"
  shows "uniformly_continuous_on s (λx. f (g x))"
  using assms unfolding uniformly_continuous_on_sequentially
  unfolding dist_norm tendsto_norm_zero_iff diff[symmetric]
  by (auto intro: tendsto_zero)

lemma uniformly_continuous_on_dist[continuous_intros]:
  fixes f g :: "'a::metric_space ==> 'b::metric_space"
  assumes "uniformly_continuous_on s f"
    and "uniformly_continuous_on s g"
  shows "uniformly_continuous_on s (λx. dist (f x) (g x))"
proof -
  {
    fix a b c d :: 'b
    have "∣dist a b - dist c d∣ ≤ dist a c + dist b d"
      using dist_triangle2 [of a b c] dist_triangle2 [of b c d]
      using dist_triangle3 [of c d a] dist_triangle [of a d b]
      by arith
  } note le = this
  {
    fix x y
    assume f: "(λn. dist (f (x n)) (f (y n))) <---- 0"
    assume g: "(λn. dist (g (x n)) (g (y n))) <---- 0"
    have "(λn. ∣dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))∣) <---- 0"
      by (rule Lim_transform_bound [OF _ tendsto_add_zero [OF f g]],
        simp add: le)
  }
  then show ?thesis
    using assms unfolding uniformly_continuous_on_sequentially
    unfolding dist_real_def by simp
qed

lemma uniformly_continuous_on_cmul_right [continuous_intros]:
  fixes f :: "'a::real_normed_vector ==> 'b::real_normed_algebra"
  shows "uniformly_continuous_on s f ==> uniformly_continuous_on s (λx. f x * c)"
  using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] .

lemma uniformly_continuous_on_cmul_left[continuous_intros]:
  fixes f :: "'a::real_normed_vector ==> 'b::real_normed_algebra"
  assumes "uniformly_continuous_on s f"
    shows "uniformly_continuous_on s (λx. c * f x)"
by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right)

lemma uniformly_continuous_on_norm[continuous_intros]:
  fixes f :: "'a :: metric_space ==> 'b :: real_normed_vector"
  assumes "uniformly_continuous_on s f"
  shows "uniformly_continuous_on s (λx. norm (f x))"
  unfolding norm_conv_dist using assms
  by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)

lemma uniformly_continuous_on_cmul[continuous_intros]:
  fixes f :: "'a::metric_space ==> 'b::real_normed_vector"
  assumes "uniformly_continuous_on s f"
  shows "uniformly_continuous_on s (λx. c *🪙R f(x))"
  using bounded_linear_scaleR_right assms
  by (rule bounded_linear.uniformly_continuous_on)

lemma dist_minus:
  fixes x y :: "'a::real_normed_vector"
  shows "dist (- x) (- y) = dist x y"
  unfolding dist_norm minus_diff_minus norm_minus_cancel ..

lemma uniformly_continuous_on_minus[continuous_intros]:
  fixes f :: "'a::metric_space ==> 'b::real_normed_vector"
  shows "uniformly_continuous_on s f ==> uniformly_continuous_on s (λx. - f x)"
  unfolding uniformly_continuous_on_def dist_minus .

lemma uniformly_continuous_on_add[continuous_intros]:
  fixes f g :: "'a::metric_space ==> 'b::real_normed_vector"
  assumes "uniformly_continuous_on s f"
    and "uniformly_continuous_on s g"
  shows "uniformly_continuous_on s (λx. f x + g x)"
  using assms
  unfolding uniformly_continuous_on_sequentially
  unfolding dist_norm tendsto_norm_zero_iff add_diff_add
  by (auto intro: tendsto_add_zero)

lemma uniformly_continuous_on_diff[continuous_intros]:
  fixes f :: "'a::metric_space ==> 'b::real_normed_vector"
  assumes "uniformly_continuous_on s f"
    and "uniformly_continuous_on s g"
  shows "uniformly_continuous_on s (λx. f x - g x)"
  using assms uniformly_continuous_on_add [of s f "- g"]
    by (simp add: fun_Compl_def uniformly_continuous_on_minus)

lemma uniformly_continuous_on_sum [continuous_intros]:
  fixes f :: "'a ==> 'b::metric_space ==> 'c::real_normed_vector"
  shows "(∧i. i ∈ I ==> uniformly_continuous_on S (f i)) ==> uniformly_continuous_on S (λx. ∑i∈I. f i x)"
  by (induction I rule: infinite_finite_induct)
     (auto simp: uniformly_continuous_on_add uniformly_continuous_on_const)


subsection🍋‹tag unimportant› ‹Arithmetic Preserves Topological Properties›

lemma open_scaling[intro]:
  fixes S :: "'a::real_normed_vector set"
  assumes "c ≠ 0"
    and "open S"
  shows "open((λx. c *🪙R x) ` S)"
proof -
  {
    fix x
    assume "x ∈ S"
    then obtain ε where "ε>0"
      and ε: "∀x'. dist x' x < ε ⟶ x' ∈ S" using assms(2)[unfolded open_dist, THEN bspec[where x=x]]
      by auto
    have "ε * ∣c∣ > 0"
      using assms(1)[unfolded zero_less_abs_iff[symmetric]] ‹ε>0› by auto
    moreover
    {
      fix y
      assume "dist y (c *🪙R x) < ε * ∣c∣"
      then have "norm (c *🪙R ((1 / c) *🪙R y - x)) < ε * norm c"
        by (simp add: ‹c ≠ 0› dist_norm scale_right_diff_distrib)
      then have "norm ((1 / c) *🪙R y - x) < ε"
        by (simp add: ‹c ≠ 0›)
      then have "y ∈ (*🪙R) c ` S"
        using rev_image_eqI[of "(1 / c) *🪙R y" S y "(*\<^sub>R) c"]
        by (simp add: ‹c ≠ 0› dist_norm ε)
    }
    ultimately have "∃e>0. ∀x'. dist x' (c *🪙R x) < e ⟶ x' ∈ (*\<^sub>R) c ` S"
  by (rule_tac x="ε * ∣c∣" in exI, auto)
  }
  then show ?thesis unfolding open_dist by auto
 qed
 
 lemma open_times_image:
  fixes S::"'a::real_normed_field set"
  assumes "c≠0" "open S"
  shows "open (((*)
proof -
  let ?f = "λx. x/c" and ?g="((*) c)"
  have "continuous_on UNIV ?f" using ‹c≠0› by (auto intro:continuous_intros)
  then have "open (?f -` S)" using ‹open S› by (auto elim:open_vimage)
  moreover have "?g ` S = ?f -` S" using ‹c≠0›
    using image_iff by fastforce
  ultimately show ?thesis by auto
qed   

lemma minus_image_eq_vimage:
  fixes A :: "'a::ab_group_add set"
  shows "(λx. - x) ` A = (λx. - x) -` A"
  by (auto intro!: image_eqI [where f="λx. - x"])

lemma open_negations:
  fixes S :: "'a::real_normed_vector set"
  shows "open S ==> open ((λx. - x) ` S)"
  using open_scaling [of "- 1" S] by simp

lemma open_translation:
  fixes S :: "'a::real_normed_vector set"
  assumes "open S"
  shows "open((λx. a + x) ` S)"
proof -
  {
    fix x
    have "continuous (at x) (λx. x - a)"
      by (intro continuous_diff continuous_ident continuous_const)
  }
  moreover have "{x. x - a ∈ S} = (+) a ` S"
    by force
  ultimately show ?thesis
    by (metis assms continuous_open_vimage vimage_def)
qed

lemma open_translation_subtract:
  fixes S :: "'a::real_normed_vector set"
  assumes "open S"
  shows "open ((λx. x - a) ` S)" 
  using assms open_translation [of S "- a"] by (simp cong: image_cong_simp)

lemma open_neg_translation:
  fixes S :: "'a::real_normed_vector set"
  assumes "open S"
  shows "open((λx. a - x) ` S)"
  using open_translation[OF open_negations[OF assms], of a]
  by (auto simp: image_image)

lemma open_affinity:
  fixes S :: "'a::real_normed_vector set"
  assumes "open S"  "c ≠ 0"
  shows "open ((λx. a + c *🪙R x) ` S)"
proof -
  have *: "(λx. a + c *🪙R x) = (λx. a + x) ∘ (λx. c *🪙R x)"
    unfolding o_def ..
  have "(+) a ` (*🪙R) c ` S = ((+) a ∘ (*🪙R) c) ` S"
    by auto
  then show ?thesis
    using assms open_translation[of "(*\<^sub>R) c ` S" a]
    unfolding *
    by auto
qed

lemma interior_translation:
  "interior ((+) a ` S) = (+) a ` (interior S)" for S :: "'a::real_normed_vector set"
proof (rule set_eqI, rule)
  fix x
  assume "x ∈ interior ((+) a ` S)"
  then obtain e where "e > 0" and e: "ball x e ⊆ (+) a ` S"
    unfolding mem_interior by auto
  then have "ball (x - a) e ⊆ S"
    unfolding subset_eq Ball_def mem_ball dist_norm
    by (auto simp: diff_diff_eq)
  then show "x ∈ (+) a ` interior S"
    unfolding image_iff
    by (metis ‹0 < e› add.commute diff_add_cancel mem_interior)
next
  fix x
  assume "x ∈ (+) a ` interior S"
  then obtain y e where "e > 0" and e: "ball y e ⊆ S" and y: "x = a + y"
    unfolding image_iff Bex_def mem_interior by auto
  {
    fix z
    have *: "a + y - z = y + a - z" by auto
    assume "z ∈ ball x e"
    then have "z - a ∈ S"
      using e[unfolded subset_eq, THEN bspec[where x="z - a"]]
      unfolding mem_ball dist_norm y group_add_class.diff_diff_eq2 *
      by auto
    then have "z ∈ (+) a ` S"
      unfolding image_iff by (auto intro!: bexI[where x="z - a"])
  }
  then have "ball x e ⊆ (+) a ` S"
    unfolding subset_eq by auto
  then show "x ∈ interior ((+) a ` S)"
    unfolding mem_interior using ‹e > 0› by auto
qed

lemma interior_translation_subtract:
  "interior ((λx. x - a) ` S) = (λx. x - a) ` interior S" for S :: "'a::real_normed_vector set"
  using interior_translation [of "- a"] by (simp cong: image_cong_simp)


lemma compact_scaling:
  fixes s :: "'a::real_normed_vector set"
  assumes "compact s"
  shows "compact ((λx. c *🪙R x) ` s)"
proof -
  let ?f = "λx. scaleR c x"
  have *: "bounded_linear ?f" by (rule bounded_linear_scaleR_right)
  show ?thesis
    using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
    using linear_continuous_at[OF *] assms
    by auto
qed

lemma compact_negations:
  fixes s :: "'a::real_normed_vector set"
  assumes "compact s"
  shows "compact ((λx. - x) ` s)"
  using compact_scaling [OF assms, of "- 1"] by auto

lemma compact_sums:
  fixes s t :: "'a::real_normed_vector set"
  assumes "compact s"
    and "compact t"
  shows "compact {x + y | x y. x ∈ s ∧ y ∈ t}"
proof -
  have *: "{x + y | x y. x ∈ s ∧ y ∈ t} = (λz. fst z + snd z) ` (s × t)"
    by (fastforce simp: image_iff)
  have "continuous_on (s × t) (λz. fst z + snd z)"
    unfolding continuous_on by (rule ballI) (intro tendsto_intros)
  then show ?thesis
    unfolding * using compact_continuous_image compact_Times [OF assms] by auto
qed

lemma compact_differences:
  fixes s t :: "'a::real_normed_vector set"
  assumes "compact s"
    and "compact t"
  shows "compact {x - y | x y. x ∈ s ∧ y ∈ t}"
proof-
  have "{x - y | x y. x∈s ∧ y ∈ t} = {x + y | x y. x ∈ s ∧ y ∈ (uminus ` t)}"
    using diff_conv_add_uminus by force
  then show ?thesis
    using compact_sums[OF assms(1) compact_negations[OF assms(2)]] by auto
qed

lemma compact_sums':
  fixes S :: "'a::real_normed_vector set"
  assumes "compact S" and "compact T"
  shows "compact (∪x∈ S. ∪y ∈ T. {x + y})"
proof -
  have "(∪x∈S. ∪y∈T. {x + y}) = {x + y |x y. x ∈ S ∧ y ∈ T}"
    by blast
  then show ?thesis
    using compact_sums [OF assms] by simp
qed

lemma compact_differences':
  fixes S :: "'a::real_normed_vector set"
  assumes "compact S" and "compact T"
  shows "compact (∪x∈ S. ∪y ∈ T. {x - y})"
proof -
  have "(∪x∈S. ∪y∈T. {x - y}) = {x - y |x y. x ∈ S ∧ y ∈ T}"
    by blast
  then show ?thesis
    using compact_differences [OF assms] by simp
qed

lemma compact_translation:
  "compact ((+) a ` s)" if "compact s" for s :: "'a::real_normed_vector set"
proof -
  have "{x + y |x y. x ∈ s ∧ y ∈ {a}} = (λx. a + x) ` s"
    by auto
  then show ?thesis
    using compact_sums [OF that compact_sing [of a]] by auto
qed

lemma compact_translation_subtract:
  "compact ((λx. x - a) ` s)" if "compact s" for s :: "'a::real_normed_vector set"
  using that compact_translation [of s "- a"] by (simp cong: image_cong_simp)

lemma compact_affinity:
  fixes s :: "'a::real_normed_vector set"
  assumes "compact s"
  shows "compact ((λx. a + c *🪙R x) ` s)"
proof -
  have "(+) a ` (*\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s"
  by auto
  then show ?thesis
  using compact_translation[OF compact_scaling[OF assms], of a c] by auto
 qed
 
 lemma closed_scaling:
  fixes S :: "'a::real_normed_vector set"
  assumes "closed S"
  shows "closed ((λx. c *🪙R x) ` S)"
 proof (cases "c = 0")
  case True then show ?thesis
  by (auto simp: image_constant_conv)
 next
  case False
  from assms have "closed ((λx. inverse c *🪙R x) -` S)"
  by (simp add: continuous_closed_vimage)
  also have "(λx. inverse c *🪙R x) -` S = (λx. c *🪙R x) ` S"
  using ‹c ≠ 0› by (auto elim: image_eqI [rotated])
  finally show ?thesis .
 qed
 
 lemma closed_negations:
  fixes S :: "'a::real_normed_vector set"
  assumes "closed S"
  shows "closed ((λx. -x) ` S)"
  using closed_scaling[OF assms, of "- 1"] by simp
 
 lemma compact_closed_sums:
  fixes S :: "'a::real_normed_vector set"
  assumes "compact S" and "closed T"
  shows "closed (∪x∈ S. ∪y ∈ T. {x + y})"
 proof -
  let ?S = "{x + y |x y. x ∈ S ∧ y ∈ T}"
  {
  fix x l
  assume as: "∀n. x n ∈ ?S" "(x ---> l) sequentially"
  from as(1) obtain f where f: "∀n. x n = fst (f n) + snd (f n)" "∀n. fst (f n) ∈ S" "∀n. snd (f n) ∈ T"
  using choice[of "λn y. x n = (fst y) + (snd y) ∧ fst y ∈ S ∧ snd y ∈ T"] by auto
  obtain l' r where "l'∈S" and r: "strict_mono r" and lr: "(((λn. fst (f n)) ∘ r) ---> l') sequentially"
  using assms(1)[unfolded compact_def, THEN spec[where x="λ n. fst (f n)"]] using f(2) by auto
  have "((λn. snd (f (r n))) ---> l - l') sequentially"
  using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1)
  unfolding o_def
  by auto
  then have "l - l' ∈ T"
  using assms(2)[unfolded closed_sequential_limits,
  THEN spec[where x="λ n. snd (f (r n))"],
  THEN spec[where x="l - l'"]]
  using f(3)
  by auto
  then have "l ∈ ?S"
  using ‹l' ∈ S› by force
  }
  moreover have "?S = (∪x∈ S. ∪y ∈ T. {x + y})"
  by force
  ultimately show ?thesis
  unfolding closed_sequential_limits
  by (metis (no_types, lifting))
 qed
 
 lemma closed_compact_sums:
  fixes S T :: "'a::real_normed_vector set"
  assumes "closed S" "compact T"
  shows "closed (∪x∈ S. ∪y ∈ T. {x + y})"
 proof -
  have "(∪x∈ T. ∪y ∈ S. {x + y}) = (∪x∈ S. ∪y ∈ T. {x + y})"
  by auto
  then show ?thesis
  using compact_closed_sums[OF assms(2,1)] by simp
 qed
 
 lemma compact_closed_differences:
  fixes S T :: "'a::real_normed_vector set"
  assumes "compact S" "closed T"
  shows "closed (∪x∈ S. ∪y ∈ T. {x - y})"
 proof -
  have "(∪x∈ S. ∪y ∈ uminus ` T. {x + y}) = (∪x∈ S. ∪y ∈ T. {x - y})"
  by force
  then show ?thesis
  by (metis assms closed_negations compact_closed_sums)
 qed
 
 lemma closed_compact_differences:
  fixes S T :: "'a::real_normed_vector set"
  assumes "closed S" "compact T"
  shows "closed (∪x∈ S. ∪y ∈ T. {x - y})"
 proof -
  have "(∪x∈ S. ∪y ∈ uminus ` T. {x + y}) = {x - y |x y. x ∈ S ∧ y ∈ T}"
  by auto
  then show ?thesis
  using closed_compact_sums[OF assms(1) compact_negations[OF assms(2)]] by simp
 qed
 
 lemma closed_translation:
  "closed ((+) a ` S)" if "closed S" for a :: "'a::real_normed_vector"
 proof -
  have "(∪x∈ {a}. ∪y ∈ S. {x + y}) = ((+) a ` S)" by auto
  then show ?thesis
  using compact_closed_sums [OF compact_sing [of a] that] by auto
 qed
 
 lemma closed_translation_subtract:
  "closed ((λx. x - a) ` S)" if "closed S" for a :: "'a::real_normed_vector"
  using that closed_translation [of S "- a"] by (simp cong: image_cong_simp)
 
 lemma closure_translation:
  "closure ((+) a ` s) = (+) a ` closure s" for a :: "'a::real_normed_vector"
 proof -
  have *: "(+) a ` (- s) = - (+) a ` s"
  by (auto intro!: image_eqI [where x = "x - a" for x])
  show ?thesis
  using interior_translation [of a "- s", symmetric]
    by (simp add: closure_interior translation_Compl *)
qed

lemma closure_translation_subtract:
  "closure ((λx. x - a) ` s) = (λx. x - a) ` closure s" for a :: "'a::real_normed_vector"
  using closure_translation [of "- a" s] by (simp cong: image_cong_simp)

lemma frontier_translation:
  "frontier ((+) a ` s) = (+) a ` frontier s" for a :: "'a::real_normed_vector"
  by (auto simp add: frontier_def translation_diff interior_translation closure_translation)

lemma frontier_translation_subtract:
  "frontier ((+) a ` s) = (+) a ` frontier s" for a :: "'a::real_normed_vector"
  by (auto simp add: frontier_def translation_diff interior_translation closure_translation)

lemma sphere_translation:
  "sphere (a + c) r = (+) a ` sphere c r" for a :: "'n::real_normed_vector"
  by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x])

lemma sphere_translation_subtract:
  "sphere (c - a) r = (λx. x - a) ` sphere c r" for a :: "'n::real_normed_vector"
  using sphere_translation [of "- a" c] by (simp cong: image_cong_simp)

lemma cball_translation:
  "cball (a + c) r = (+) a ` cball c r" for a :: "'n::real_normed_vector"
  by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x])

lemma cball_translation_subtract:
  "cball (c - a) r = (λx. x - a) ` cball c r" for a :: "'n::real_normed_vector"
  using cball_translation [of "- a" c] by (simp cong: image_cong_simp)

lemma ball_translation:
  "ball (a + c) r = (+) a ` ball c r" for a :: "'n::real_normed_vector"
  by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x])

lemma ball_translation_subtract:
  "ball (c - a) r = (λx. x - a) ` ball c r" for a :: "'n::real_normed_vector"
  using ball_translation [of "- a" c] by (simp cong: image_cong_simp)


subsection🍋‹tag unimportant›\<open>Homeomorphisms›

lemma homeomorphic_scaling:
  fixes S :: "'a::real_normed_vector set"
  assumes "c ≠ 0"
  shows "S homeomorphic ((λx. c *🪙R x) ` S)"
  unfolding homeomorphic_minimal
  apply (rule_tac x="λx. c *🪙R x" in exI)
  apply (rule_tac x="λx. (1 / c) *🪙R x" in exI)
  using assms by (auto simp: continuous_intros)

lemma homeomorphic_translation:
  fixes S :: "'a::real_normed_vector set"
  shows "S homeomorphic ((λx. a + x) ` S)"
  unfolding homeomorphic_minimal
  apply (rule_tac x="λx. a + x" in exI)
  apply (rule_tac x="λx. -a + x" in exI)
  by (auto simp: continuous_intros)

lemma homeomorphic_affinity:
  fixes S :: "'a::real_normed_vector set"
  assumes "c ≠ 0"
  shows "S homeomorphic ((λx. a + c *🪙R x) ` S)"
proof -
  have *: "(+) a ` (*🪙R) c ` S = (λx. a + c *🪙R x) ` S" by auto
  show ?thesis
    by (metis "*" assms homeomorphic_scaling homeomorphic_trans homeomorphic_translation)
qed

lemma homeomorphic_balls:
  fixes a b ::"'a::real_normed_vector"
  assumes "0 < d"  "0 < e"
  shows "(ball a d) homeomorphic (ball b e)" (is ?th)
    and "(cball a d) homeomorphic (cball b e)" (is ?cth)
proof -
  show ?th unfolding homeomorphic_minimal
    apply(rule_tac x="λx. b + (e/d) *🪙R (x - a)" in exI)
    apply(rule_tac x="λx. a + (d/e) *🪙R (x - b)" in exI)
    using assms
    by (auto intro!: continuous_intros simp: dist_commute dist_norm pos_divide_less_eq)
  show ?cth unfolding homeomorphic_minimal
    apply(rule_tac x="λx. b + (e/d) *🪙R (x - a)" in exI)
    apply(rule_tac x="λx. a + (d/e) *🪙R (x - b)" in exI)
    using assms
    by (auto intro!: continuous_intros simp: dist_commute dist_norm pos_divide_le_eq)
qed

lemma homeomorphic_spheres:
  fixes a b ::"'a::real_normed_vector"
  assumes "0 < d"  "0 < e"
  shows "(sphere a d) homeomorphic (sphere b e)"
unfolding homeomorphic_minimal
    apply(rule_tac x="λx. b + (e/d) *🪙R (x - a)" in exI)
    apply(rule_tac x="λx. a + (d/e) *🪙R (x - b)" in exI)
    using assms
    by (auto intro!: continuous_intros simp: dist_commute dist_norm pos_divide_less_eq)

lemma homeomorphic_ball01_UNIV:
  "ball (0::'a::real_normed_vector) 1 homeomorphic (UNIV:: 'a set)"
  (is "?B homeomorphic ?U")
proof
  have "x ∈ (λz. z /🪙R (1 - norm z)) ` ball 0 1" for x::'a
    apply (rule_tac x="x /🪙R (1 + norm x)" in image_eqI)
     apply (auto simp: field_split_simps)
    using norm_ge_zero [of x] apply linarith+
    done
  then show "(λz::'a. z /🪙R (1 - norm z)) ` ?B = ?U"
    by blast
  have "x ∈ range (λz. (1 / (1 + norm z)) *🪙R z)" if "norm x < 1" for x::'a
    using that
    by (rule_tac x="x /🪙R (1 - norm x)" in image_eqI) (auto simp: field_split_simps)
  then show "(λz::'a. z /🪙R (1 + norm z)) ` ?U = ?B"
    by (force simp: field_split_simps dest: add_less_zeroD)
  show "continuous_on (ball 0 1) (λz. z /🪙R (1 - norm z))"
    by (rule continuous_intros | force)+
  have 0: "∧z. 1 + norm z ≠ 0"
    by (metis (no_types) le_add_same_cancel1 norm_ge_zero not_one_le_zero)
  then show "continuous_on UNIV (λz. z /🪙R (1 + norm z))"
    by (auto intro!: continuous_intros)
  show "∧x. x ∈ ball 0 1 ==>
         x /🪙R (1 - norm x) /🪙R (1 + norm (x /🪙R (1 - norm x))) = x"
    by (auto simp: field_split_simps)
  show "∧y. y /🪙R (1 + norm y) /🪙R (1 - norm (y /🪙R (1 + norm y))) = y"
    using 0 by (auto simp: field_split_simps)
qed

proposition homeomorphic_ball_UNIV:
  fixes a ::"'a::real_normed_vector"
  assumes "0 < r" shows "ball a r homeomorphic (UNIV:: 'a set)"
  using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast


subsection🍋‹tag unimportant› ‹Discrete›

lemma finite_implies_discrete:
  fixes S :: "'a::topological_space set"
  assumes "finite (f ` S)"
  shows "(∀x ∈ S. ∃e>0. ∀y. y ∈ S ∧ f y ≠ f x ⟶ e ≤ norm (f y - f x))"
proof -
  have "∃e>0. ∀y. y ∈ S ∧ f y ≠ f x ⟶ e ≤ norm (f y - f x)" if "x ∈ S" for x
  proof (cases "f ` S - {f x} = {}")
    case True
    with zero_less_numeral show ?thesis
      by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
  next
    case False
    then obtain z where "z ∈ S" "f z ≠ f x"
      by blast
    moreover have finn: "finite {norm (z - f x) |z. z ∈ f ` S - {f x}}"
      using assms by simp
    ultimately have *: "0 < Inf{norm(z - f x) | z. z ∈ f ` S - {f x}}"
      by (force intro: finite_imp_less_Inf)
    show ?thesis
      by (force intro!: * cInf_le_finite [OF finn])
  qed
  with assms show ?thesis
    by blast
qed


subsection🍋‹tag unimportant› ‹Completeness of "Isometry" (up to constant bounds)›

lemma cauchy_isometric:🍋 ‹TODO: rename lemma to ‹Cauchy_isometric›\   assumes e: "e > 0"
    and s: "subspace s"
    and f: "bounded_linear f"
    and normf: "∀x∈s. norm (f x) ≥ e * norm x"
    and xs: "∀n. x n ∈ s"
    and cf: "Cauchy (f ∘ x)"
  shows "Cauchy x"
proof -
  interpret f: bounded_linear f by fact
  have "∃N. ∀n≥N. norm (x n - x N) < d" if "d > 0" for d :: real
  proof -
    from that obtain N where N: "∀n≥N. norm (f (x n) - f (x N)) < e * d"
      using cf[unfolded Cauchy_def o_def dist_norm, THEN spec[where x="e*d"]] e
      by auto
    have "norm (x n - x N) < d" if "n ≥ N" for n
    proof -
      have "e * norm (x n - x N) ≤ norm (f (x n - x N))"
        using subspace_diff[OF s, of "x n" "x N"]
        using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
        using normf[THEN bspec[where x="x n - x N"]]
        by auto
      also have "norm (f (x n - x N)) < e * d"
        using ‹N ≤ n› N unfolding f.diff[symmetric] by auto
      finally show ?thesis
        using ‹e>0› by simp
    qed
    then show ?thesis by auto
  qed
  then show ?thesis
    by (simp add: Cauchy_altdef2 dist_norm)
qed

lemma complete_isometric_image:
  assumes "0 < e"
    and s: "subspace s"
    and f: "bounded_linear f"
    and normf: "∀x∈s. norm(f x) ≥ e * norm(x)"
    and cs: "complete s"
  shows "complete (f ` s)"
proof -
  have "∃l∈f ` s. (g ---> l) sequentially"
    if as:"∀n::nat. g n ∈ f ` s" and cfg:"Cauchy g" for g
  proof -
    from that obtain x where "∀n. x n ∈ s ∧ g n = f (x n)"
      using choice[of "λ n xa. xa ∈ s ∧ g n = f xa"] by auto
    then have x: "∀n. x n ∈ s" "∀n. g n = f (x n)" by auto
    then have "f ∘ x = g" by (simp add: fun_eq_iff)
    then obtain l where "l∈s" and l:"(x ---> l) sequentially"
      using cs[unfolded complete_def, THEN spec[where x=x]]
      using cauchy_isometric[OF ‹0 🚫› s f normf] and cfg and x(1)
      by auto
    then show ?thesis
      using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l]
      by (auto simp: ‹f ∘ x = g›)
  qed
  then show ?thesis
    unfolding complete_def by auto
qed

subsection ‹Connected Normed Spaces›

lemma compact_components:
  fixes s :: "'a::heine_borel set"
  shows "[compact s; c ∈ components s] ==> compact c"
by (meson bounded_subset closed_components in_components_subset compact_eq_bounded_closed)

lemma discrete_subset_disconnected:
  fixes S :: "'a::topological_space set"
  fixes t :: "'b::real_normed_vector set"
  assumes conf: "continuous_on S f"
      and no: "∧x. x ∈ S ==> ∃e>0. ∀y. y ∈ S ∧ f y ≠ f x ⟶ e ≤ norm (f y - f x)"
   shows "f ` S ⊆ {y. connected_component_set (f ` S) y = {y}}"
proof -
  { fix x assume x: "x ∈ S"
    then obtain e where "e>0" and ele: "∧y. [y ∈ S; f y ≠ f x] ==> e ≤ norm (f y - f x)"
      using conf no [OF x] by auto
    then have e2: "0 ≤ e/2"
      by simp
    define F where "F ≡ connected_component_set (f ` S) (f x)"
    have False if "y ∈ S" and ccs: "f y ∈ F" and not: "f y ≠ f x" for y 
    proof -
      define C where "C ≡ cball (f x) (e/2)"
      define D where "D ≡ - ball (f x) e"
      have disj: "C ∩ D = {}"
        unfolding C_def D_def using ‹0 🚫› by fastforce
      moreover have FCD: "F ⊆ C ∪ D"
      proof -
        have "t ∈ C ∨ t ∈ D" if "t ∈ F" for t
        proof -
          obtain y where "y ∈ S" "t = f y"
            using F_def ‹t ∈ F› connected_component_in by blast
          then show ?thesis
            by (metis C_def ComplI D_def centre_in_cball dist_norm e2 ele mem_ball norm_minus_commute not_le)
        qed
        then show ?thesis
          by auto
      qed
      ultimately have "C ∩ F = {} ∨ D ∩ F = {}"
        using connected_closed [of "F"] ‹e>0› not
        unfolding C_def D_def
        by (metis Elementary_Metric_Spaces.open_ball F_def closed_cball connected_connected_component inf_bot_left open_closed)
      moreover have "C ∩ F ≠ {}"
        unfolding disjoint_iff
        by (metis FCD ComplD image_eqI mem_Collect_eq subsetD x  D_def F_def Un_iff ‹0 🚫› centre_in_ball connected_component_refl_eq)
      moreover have "D ∩ F ≠ {}"
        unfolding disjoint_iff
        by (metis ComplI D_def ccs dist_norm ele mem_ball norm_minus_commute not not_le that(1))
      ultimately show ?thesis by metis
    qed
    moreover have "connected_component_set (f ` S) (f x) ⊆ f ` S"
      by (auto simp: connected_component_in)
    ultimately have "connected_component_set (f ` S) (f x) = {f x}"
      by (auto simp: x F_def)
  }
  with assms show ?thesis
    by blast
qed

lemma continuous_disconnected_range_constant_eq:
      "(connected S ⟷
           (∀f::'a::topological_space ==> 'b::real_normed_algebra_1.
            ∀t. continuous_on S f ∧ f ` S ⊆ t ∧ (∀y ∈ t. connected_component_set t y = {y})
            ⟶ f constant_on S))" (is ?thesis1)
  and continuous_discrete_range_constant_eq:
      "(connected S ⟷
         (∀f::'a::topological_space ==> 'b::real_normed_algebra_1.
          continuous_on S f ∧
          (∀x ∈ S. ∃e. 0 < e ∧ (∀y. y ∈ S ∧ (f y ≠ f x) ⟶ e ≤ norm(f y - f x)))
          ⟶ f constant_on S))" (is ?thesis2)
  and continuous_finite_range_constant_eq:
      "(connected S ⟷
         (∀f::'a::topological_space ==> 'b::real_normed_algebra_1.
          continuous_on S f ∧ finite (f ` S)
          ⟶ f constant_on S))" (is ?thesis3)
proof -
  have *: "∧s t u v. [s ==> t; t ==> u; u ==> v; v ==> s]
    ==> (s ⟷ t) ∧ (s ⟷ u) ∧ (s ⟷ v)"
    by blast
  have "?thesis1 ∧ ?thesis2 ∧ ?thesis3"
    apply (rule *)
    using continuous_disconnected_range_constant
    apply (metis image_subset_iff_funcset)
    apply (smt (verit, best) discrete_subset_disconnected mem_Collect_eq subsetD subsetI)
    apply (blast dest: finite_implies_discrete)
    apply (blast intro!: finite_range_constant_imp_connected)
    done
  then show ?thesis1 ?thesis2 ?thesis3
    by blast+
qed

lemma continuous_discrete_range_constant:
  fixes f :: "'a::topological_space ==> 'b::real_normed_algebra_1"
  assumes S: "connected S"
      and "continuous_on S f"
      and "∧x. x ∈ S ==> ∃e>0. ∀y. y ∈ S ∧ f y ≠ f x ⟶ e ≤ norm (f y - f x)"
    shows "f constant_on S"
  using continuous_discrete_range_constant_eq [THEN iffD1, OF S] assms by blast

lemma continuous_finite_range_constant:
  fixes f :: "'a::topological_space ==> 'b::real_normed_algebra_1"
  assumes "connected S"
      and "continuous_on S f"
      and "finite (f ` S)"
    shows "f constant_on S"
  using assms continuous_finite_range_constant_eq  by blast

end