src/HOL/Analysis/Topology_Euclidean_Space.thy

 lemma continuous_on_cases:
   "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow>
     \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow>
     continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
   by (rule continuous_on_If) auto
+
+lemma open_sums:
+  fixes T :: "('b::real_normed_vector) set"
+  assumes "open S \<or> open T"
+  shows "open (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
+  using assms
+proof
+  assume S: "open S"
+  show ?thesis
+  proof (clarsimp simp: open_dist)
+    fix x y
+    assume "x \<in> S" "y \<in> T"
+    with S obtain e where "e > 0" and e: "\<And>x'. dist x' x < e \<Longrightarrow> x' \<in> S"
+      by (auto simp: open_dist)
+    then have "\<And>z. dist z (x + y) < e \<Longrightarrow> \<exists>x\<in>S. \<exists>y\<in>T. z = x + y"
+      by (metis \<open>y \<in> T\<close> diff_add_cancel dist_add_cancel2)
+    then show "\<exists>e>0. \<forall>z. dist z (x + y) < e \<longrightarrow> (\<exists>x\<in>S. \<exists>y\<in>T. z = x + y)"
+      using \<open>0 < e\<close> \<open>x \<in> S\<close> by blast
+  qed
+next
+  assume T: "open T"
+  show ?thesis
+  proof (clarsimp simp: open_dist)
+    fix x y
+    assume "x \<in> S" "y \<in> T"
+    with T obtain e where "e > 0" and e: "\<And>x'. dist x' y < e \<Longrightarrow> x' \<in> T"
+      by (auto simp: open_dist)
+    then have "\<And>z. dist z (x + y) < e \<Longrightarrow> \<exists>x\<in>S. \<exists>y\<in>T. z = x + y"
+      by (metis \<open>x \<in> S\<close> add_diff_cancel_left' add_diff_eq diff_diff_add dist_norm)
+    then show "\<exists>e>0. \<forall>z. dist z (x + y) < e \<longrightarrow> (\<exists>x\<in>S. \<exists>y\<in>T. z = x + y)"
+      using \<open>0 < e\<close> \<open>y \<in> T\<close> by blast
+  qed
+qed
 
 
 subsection \<open>Topological Basis\<close>
 
 context topological_space

   assume H: ?rhs
   let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
   have "openin U ?t" by (force simp add: openin_Union)
   also have "?t = S" using H by auto
   finally show "openin U S" .
+qed
+
+lemma openin_INT [intro]:
+  assumes "finite I"
+          "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
+  shows "openin T ((\<Inter>i \<in> I. U i) \<inter> topspace T)"
+using assms by (induct, auto simp add: inf_sup_aci(2) openin_Int)
+
+lemma openin_INT2 [intro]:
+  assumes "finite I" "I \<noteq> {}"
+          "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
+  shows "openin T (\<Inter>i \<in> I. U i)"
+proof -
+  have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
+    using `I \<noteq> {}` openin_subset[OF assms(3)] by auto
+  then show ?thesis
+    using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
 qed
 
 
 subsubsection \<open>Closed sets\<close>
 

 lemma closure_complement: "closure (- S) = - interior S"
   by (simp add: closure_interior)
 
 lemma interior_complement: "interior (- S) = - closure S"
   by (simp add: closure_interior)
+   
+lemma interior_diff: "interior(S - T) = interior S - closure T"
+  by (simp add: Diff_eq interior_complement)
 
 lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
 proof (rule closure_unique)
   show "A \<times> B \<subseteq> closure A \<times> closure B"
     by (intro Sigma_mono closure_subset)