# HG changeset patch
# User huffman
# Date 1272390864 25200
# Node ID b96d9dc6accaee08df9dac0c251b9c5ed4a789be
# Parent  1d7704c29af360ac22605c2c09187f050d71ad1b
generalize more continuity lemmas

diff -r 1d7704c29af3 -r b96d9dc6acca src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 27 10:39:52 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 27 10:54:24 2010 -0700
@@ -5187,15 +5187,19 @@
   unfolding tendsto_def
   by (auto simp add: eventually_within_Un)
 
+lemma Lim_topological:
+ "(f ---> l) net \<longleftrightarrow>
+        trivial_limit net \<or>
+        (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
+  unfolding tendsto_def trivial_limit_eq by auto
+
 lemma continuous_on_union:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
   shows "continuous_on (s \<union> t) f"
-  using assms unfolding continuous_on unfolding Lim_within_union
-  unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto
+  using assms unfolding continuous_on Lim_within_union
+  unfolding Lim_topological trivial_limit_within closed_limpt by auto
 
 lemma continuous_on_cases:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
           "\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
   shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"