# HG changeset patch
# User hoelzl
# Date 1362494595 -3600
# Node ID b3d246c92dfb4540c1fb87ae3e85063a6265e9b7
# Parent  b61b32f62c7862c6210195463d6828ae27adc90d
continuity of pair operations

diff -r b61b32f62c78 -r b3d246c92dfb src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:14 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:15 2013 +0100
@@ -4037,6 +4037,15 @@
 lemma continuous_const: "continuous F (\<lambda>x. c)"
   unfolding continuous_def by (rule tendsto_const)
 
+lemma continuous_fst: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
+  unfolding continuous_def by (rule tendsto_fst)
+
+lemma continuous_snd: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
+  unfolding continuous_def by (rule tendsto_snd)
+
+lemma continuous_Pair: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
+  unfolding continuous_def by (rule tendsto_Pair)
+
 lemma continuous_dist:
   assumes "continuous F f" and "continuous F g"
   shows "continuous F (\<lambda>x. dist (f x) (g x))"