# 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 \ + trivial_limit net \ + (\S. open S \ l \ S \ eventually (\x. f x \ S) net)" + unfolding tendsto_def trivial_limit_eq by auto + lemma continuous_on_union: - fixes f :: "'a::metric_space \ 'b::metric_space" (* TODO: generalize *) assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f" shows "continuous_on (s \ 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 \ 'b::metric_space" (* TODO: generalize *) assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g" "\x. (x\s \ \ P x) \ (x \ t \ P x) \ f x = g x" shows "continuous_on (s \ t) (\x. if P x then f x else g x)"