author hoelzl Tue, 09 Apr 2013 15:07:35 +0200 changeset 51644 8c38147d404e parent 51643 b6675f4549d8 child 51645 86e8c87e1f1b
```--- 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)
```