equal
deleted
inserted
replaced
4034 lemma continuous_at_id: "continuous (at a) (\<lambda>x. x)" 
4034 lemma continuous_at_id: "continuous (at a) (\<lambda>x. x)" 
4035 unfolding continuous_at by (rule tendsto_ident_at) 
4035 unfolding continuous_at by (rule tendsto_ident_at) 
4036 
4036 
4037 lemma continuous_const: "continuous F (\<lambda>x. c)" 
4037 lemma continuous_const: "continuous F (\<lambda>x. c)" 
4038 unfolding continuous_def by (rule tendsto_const) 
4038 unfolding continuous_def by (rule tendsto_const) 

4039 

4040 lemma continuous_fst: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))" 

4041 unfolding continuous_def by (rule tendsto_fst) 

4042 

4043 lemma continuous_snd: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))" 

4044 unfolding continuous_def by (rule tendsto_snd) 

4045 

4046 lemma continuous_Pair: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))" 

4047 unfolding continuous_def by (rule tendsto_Pair) 
4039 
4048 
4040 lemma continuous_dist: 
4049 lemma continuous_dist: 
4041 assumes "continuous F f" and "continuous F g" 
4050 assumes "continuous F f" and "continuous F g" 
4042 shows "continuous F (\<lambda>x. dist (f x) (g x))" 
4051 shows "continuous F (\<lambda>x. dist (f x) (g x))" 
4043 using assms unfolding continuous_def by (rule tendsto_dist) 
4052 using assms unfolding continuous_def by (rule tendsto_dist) 