src/HOL/Topological_Spaces.thy
changeset 61204 3e491e34a62e
parent 61169 4de9ff3ea29a
child 61234 a9e6052188fa
     1.1 --- a/src/HOL/Topological_Spaces.thy	Mon Sep 21 14:44:32 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Sep 21 19:52:13 2015 +0100
     1.3 @@ -1392,6 +1392,10 @@
     1.4    "(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
     1.5    unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
     1.6  
     1.7 +lemma continuous_on_open_Un:
     1.8 +  "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
     1.9 +  using continuous_on_open_Union [of "{s,t}"] by auto
    1.10 +
    1.11  lemma continuous_on_closed_Un:
    1.12    "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
    1.13    by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)