src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 70688 3d894e1cfc75
parent 70630 2402aa499ffe
child 70690 8518a750f7bb
equal deleted inserted replaced
70682:4c53227f4b73 70688:3d894e1cfc75
  1098   shows "uniformly_continuous_on s (\<lambda>x. f x - g x)"
  1098   shows "uniformly_continuous_on s (\<lambda>x. f x - g x)"
  1099   using assms uniformly_continuous_on_add [of s f "- g"]
  1099   using assms uniformly_continuous_on_add [of s f "- g"]
  1100     by (simp add: fun_Compl_def uniformly_continuous_on_minus)
  1100     by (simp add: fun_Compl_def uniformly_continuous_on_minus)
  1101 
  1101 
  1102 
  1102 
  1103 subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological properties of linear functions\<close>
       
  1104 
       
  1105 lemma linear_lim_0:
       
  1106   assumes "bounded_linear f"
       
  1107   shows "(f \<longlongrightarrow> 0) (at (0))"
       
  1108 proof -
       
  1109   interpret f: bounded_linear f by fact
       
  1110   have "(f \<longlongrightarrow> f 0) (at 0)"
       
  1111     using tendsto_ident_at by (rule f.tendsto)
       
  1112   then show ?thesis unfolding f.zero .
       
  1113 qed
       
  1114 
       
  1115 lemma linear_continuous_at:
       
  1116   assumes "bounded_linear f"
       
  1117   shows "continuous (at a) f"
       
  1118   unfolding continuous_at using assms
       
  1119   apply (rule bounded_linear.tendsto)
       
  1120   apply (rule tendsto_ident_at)
       
  1121   done
       
  1122 
       
  1123 lemma linear_continuous_within:
       
  1124   "bounded_linear f \<Longrightarrow> continuous (at x within s) f"
       
  1125   using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
       
  1126 
       
  1127 lemma linear_continuous_on:
       
  1128   "bounded_linear f \<Longrightarrow> continuous_on s f"
       
  1129   using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
       
  1130 
       
  1131 subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic Preserves Topological Properties\<close>
  1103 subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic Preserves Topological Properties\<close>
  1132 
  1104 
  1133 lemma open_scaling[intro]:
  1105 lemma open_scaling[intro]:
  1134   fixes s :: "'a::real_normed_vector set"
  1106   fixes s :: "'a::real_normed_vector set"
  1135   assumes "c \<noteq> 0"
  1107   assumes "c \<noteq> 0"