src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 51344 b3d246c92dfb
parent 51343 b61b32f62c78
child 51345 e7dd577cb053
equal deleted inserted replaced
51343:b61b32f62c78 51344:b3d246c92dfb
  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)