src/HOL/Topological_Spaces.thy

 lemma filterlim_subseq: "strict_mono f \<Longrightarrow> filterlim f sequentially sequentially"
   unfolding filterlim_iff by (metis eventually_subseq)
 
 lemma strict_mono_o: "strict_mono r \<Longrightarrow> strict_mono s \<Longrightarrow> strict_mono (r \<circ> s)"
   unfolding strict_mono_def by simp
+
+lemma strict_mono_compose: "strict_mono r \<Longrightarrow> strict_mono s \<Longrightarrow> strict_mono (\<lambda>x. r (s x))"
+  using strict_mono_o[of r s] by (simp add: o_def)
 
 lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
   by (simp add: incseq_def monoseq_def)
 
 lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"

   using continuous_on_open_Union [of "{s,t}"] by auto
 
 lemma continuous_on_closed_Un:
   "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
   by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)
+
+lemma continuous_on_closed_Union:
+  assumes "finite I"
+    "\<And>i. i \<in> I \<Longrightarrow> closed (U i)"
+    "\<And>i. i \<in> I \<Longrightarrow> continuous_on (U i) f"
+  shows "continuous_on (\<Union> i \<in> I. U i) f"
+  using assms
+  by (induction I) (auto intro!: continuous_on_closed_Un)
 
 lemma continuous_on_If:
   assumes closed: "closed s" "closed t"
     and cont: "continuous_on s f" "continuous_on t g"
     and P: "\<And>x. x \<in> s \<Longrightarrow> \<not> P x \<Longrightarrow> f x = g x" "\<And>x. x \<in> t \<Longrightarrow> P x \<Longrightarrow> f x = g x"