src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 51344 b3d246c92dfb
parent 51343 b61b32f62c78
child 51345 e7dd577cb053
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:14 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:15 2013 +0100
     1.3 @@ -4037,6 +4037,15 @@
     1.4  lemma continuous_const: "continuous F (\<lambda>x. c)"
     1.5    unfolding continuous_def by (rule tendsto_const)
     1.6  
     1.7 +lemma continuous_fst: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
     1.8 +  unfolding continuous_def by (rule tendsto_fst)
     1.9 +
    1.10 +lemma continuous_snd: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
    1.11 +  unfolding continuous_def by (rule tendsto_snd)
    1.12 +
    1.13 +lemma continuous_Pair: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
    1.14 +  unfolding continuous_def by (rule tendsto_Pair)
    1.15 +
    1.16  lemma continuous_dist:
    1.17    assumes "continuous F f" and "continuous F g"
    1.18    shows "continuous F (\<lambda>x. dist (f x) (g x))"