src/HOL/Analysis/Connected.thy

 (*  Author:     L C Paulson, University of Cambridge
     Material split off from Topology_Euclidean_Space
 *)
 
-section \<open>Connected Components, Homeomorphisms, Baire property, etc.\<close>
+section \<open>Connected Components, Homeomorphisms, Baire property, etc\<close>
 
 theory Connected
 imports Topology_Euclidean_Space
 begin
 
-subsection%unimportant \<open>More properties of closed balls, spheres, etc.\<close>
+subsection%unimportant \<open>More properties of closed balls, spheres, etc\<close>
 
 lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
   apply (simp add: interior_def, safe)
   apply (force simp: open_contains_cball)
   apply (rule_tac x="ball x e" in exI)

     ultimately show "\<exists>y \<in> \<Inter>\<G>. dist y x < e"
       by auto
   qed
 qed
 
-subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded".\<close>
+subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded"\<close>
 
 lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
   by (simp add: bounded_iff)
 
 lemma bounded_imp_bdd_above: "bounded S \<Longrightarrow> bdd_above (S :: real set)"

     by (metis continuous_attains_inf)
   with that show ?thesis by fastforce
 qed
 
 
-subsection%unimportant\<open>Relations among convergence and absolute convergence for power series.\<close>
+subsection%unimportant\<open>Relations among convergence and absolute convergence for power series\<close>
 
 lemma summable_imp_bounded:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "summable f \<Longrightarrow> bounded (range f)"
 by (frule summable_LIMSEQ_zero) (simp add: convergent_imp_bounded)

     by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
   ultimately show "compact {x. infdist x A \<le> e}"
     by (simp add: compact_eq_bounded_closed)
 qed
 
-subsection%unimportant \<open>Equality of continuous functions on closure and related results.\<close>
+subsection%unimportant \<open>Equality of continuous functions on closure and related results\<close>
 
 lemma continuous_closedin_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   shows "continuous_on S f \<Longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x = a}"
   using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)

   fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
   assumes "uniformly_continuous_on S f" "bounded S"
   shows "bounded(f ` S)"
   by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
 
-subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
+subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood\<close>
 
 lemma continuous_within_avoid:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
   assumes "continuous (at x within s) f"
     and "f x \<noteq> a"

     unfolding subset_eq by auto
   then show "x \<in> interior ((+) a ` S)"
     unfolding mem_interior using \<open>e > 0\<close> by auto
 qed
 
-subsection \<open>Continuity implies uniform continuity on a compact domain.\<close>
+subsection \<open>Continuity implies uniform continuity on a compact domain\<close>
 
 text\<open>From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of
 J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)\<close>
 
 lemma Heine_Borel_lemma:

   ultimately show ?thesis
     using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
 qed
 
 
-subsection \<open>The diameter of a set.\<close>
+subsection \<open>The diameter of a set\<close>
 
 definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where
   "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
 
 lemma diameter_empty [simp]: "diameter{} = 0"

     finally show False by simp
   qed
 qed
 
 
-subsection%unimportant \<open>Compact sets and the closure operation.\<close>
+subsection%unimportant \<open>Compact sets and the closure operation\<close>
 
 lemma closed_scaling:
   fixes S :: "'a::real_normed_vector set"
   assumes "closed S"
   shows "closed ((\<lambda>x. c *\<^sub>R x) ` S)"

       and "a \<in> s \<Longrightarrow> f a = g a"
     shows "continuous_on s (\<lambda>t. if t \<le> a then f(t) else g(t))"
 using assms
 by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified])
 
-subsubsection\<open>Some more convenient intermediate-value theorem formulations.\<close>
+subsubsection\<open>Some more convenient intermediate-value theorem formulations\<close>
 
 lemma connected_ivt_hyperplane:
   assumes "connected S" and xy: "x \<in> S" "y \<in> S" and b: "inner a x \<le> b" "b \<le> inner a y"
   shows "\<exists>z \<in> S. inner a z = b"
 proof (rule ccontr)

   ultimately show ?thesis
     by (simp add: continuous_on_closed oo)
 qed
 
 
-subsection \<open>"Isometry" (up to constant bounds) of injective linear map etc.\<close>
+subsection \<open>"Isometry" (up to constant bounds) of injective linear map etc\<close>
 
 lemma cauchy_isometric:
   assumes e: "e > 0"
     and s: "subspace s"
     and f: "bounded_linear f"

   qed
 qed
 
 
 
-subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4).\<close>
+subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4)\<close>
 
 
 lemma connected_Un_clopen_in_complement:
   fixes S U :: "'a::metric_space set"
   assumes "connected S" "connected U" "S \<subseteq> U"