# HG changeset patch
# User hoelzl
# Date 1365512855 -7200
# Node ID 8c38147d404e903f47c51840b76767be4fcb2620
# Parent  b6675f4549d8ce33d8b2e5bb5eeb685a3a631542
add continuous_on rules for products

diff -r b6675f4549d8 -r 8c38147d404e src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Tue Apr 09 14:13:13 2013 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Tue Apr 09 15:07:35 2013 +0200
@@ -202,6 +202,15 @@
 lemma continuous_Pair[continuous_intros]: "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_on_fst[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_fst)
+
+lemma continuous_on_snd[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_snd)
+
+lemma continuous_on_Pair[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
+  unfolding continuous_on_def by (auto intro: tendsto_Pair)
+
 lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
   by (fact continuous_fst)