# 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 (\x. c)"
unfolding continuous_def by (rule tendsto_const)
+lemma continuous_fst: "continuous F f \ continuous F (\x. fst (f x))"
+ unfolding continuous_def by (rule tendsto_fst)
+
+lemma continuous_snd: "continuous F f \ continuous F (\x. snd (f x))"
+ unfolding continuous_def by (rule tendsto_snd)
+
+lemma continuous_Pair: "continuous F f \ continuous F g \ continuous F (\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 (\x. dist (f x) (g x))"