src/HOL/Library/Topology_Euclidean_Space.thy
changeset 31531 fc78714d14e1
parent 31530 e31d63c66f55
child 31532 43e8d4bfde26
equal deleted inserted replaced
31530:e31d63c66f55 31531:fc78714d14e1
  1128 
  1128 
  1129 lemma Lim_at_iff_LIM: "(f ---> l) (at a) \<longleftrightarrow> f -- a --> l"
  1129 lemma Lim_at_iff_LIM: "(f ---> l) (at a) \<longleftrightarrow> f -- a --> l"
  1130   unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
  1130   unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
  1131 
  1131 
  1132 lemma Lim_at_infinity:
  1132 lemma Lim_at_infinity:
  1133   "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x::real^'n::finite. norm x >= b \<longrightarrow> dist (f x) l < e)"
  1133   "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)"
  1134   by (auto simp add: tendsto_iff eventually_at_infinity)
  1134   by (auto simp add: tendsto_iff eventually_at_infinity)
  1135 
  1135 
  1136 lemma Lim_sequentially:
  1136 lemma Lim_sequentially:
  1137  "(S ---> l) sequentially \<longleftrightarrow>
  1137  "(S ---> l) sequentially \<longleftrightarrow>
  1138           (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
  1138           (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
  2030 done
  2030 done
  2031 
  2031 
  2032 lemma bounded_insert[intro]:"bounded(insert x S) \<longleftrightarrow> bounded S"
  2032 lemma bounded_insert[intro]:"bounded(insert x S) \<longleftrightarrow> bounded S"
  2033   by (metis Diff_cancel Un_empty_right Un_insert_right bounded_Un bounded_subset finite.emptyI finite_imp_bounded infinite_remove subset_insertI)
  2033   by (metis Diff_cancel Un_empty_right Un_insert_right bounded_Un bounded_subset finite.emptyI finite_imp_bounded infinite_remove subset_insertI)
  2034 
  2034 
  2035 lemma bot_bounded_UNIV[simp, intro]: "~(bounded (UNIV:: (real^'n::finite) set))"
  2035 lemma not_bounded_UNIV[simp, intro]:
       
  2036   "\<not> bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)"
  2036 proof(auto simp add: bounded_pos not_le)
  2037 proof(auto simp add: bounded_pos not_le)
       
  2038   obtain x :: 'a where "x \<noteq> 0"
       
  2039     using perfect_choose_dist [OF zero_less_one] by fast
  2037   fix b::real  assume b: "b >0"
  2040   fix b::real  assume b: "b >0"
  2038   have b1: "b +1 \<ge> 0" using b by simp
  2041   have b1: "b +1 \<ge> 0" using b by simp
  2039   then obtain x:: "real^'n" where "norm x = b + 1" using vector_choose_size[of "b+1"] by blast
  2042   with `x \<noteq> 0` have "b < norm (scaleR (b + 1) (sgn x))"
  2040   hence "norm x > b" using b by simp
  2043     by (simp add: norm_scaleR norm_sgn)
  2041   then show "\<exists>(x::real^'n). b < norm x"  by blast
  2044   then show "\<exists>x::'a. b < norm x" ..
  2042 qed
  2045 qed
  2043 
  2046 
  2044 lemma bounded_linear_image:
  2047 lemma bounded_linear_image:
  2045   fixes f :: "real^'m::finite \<Rightarrow> real^'n::finite"
  2048   fixes f :: "real^'m::finite \<Rightarrow> real^'n::finite"
  2046   assumes "bounded S" "linear f"
  2049   assumes "bounded S" "linear f"
  3355   fixes x y :: "'a::real_normed_vector"
  3358   fixes x y :: "'a::real_normed_vector"
  3356   shows "dist (- x) (- y) = dist x y"
  3359   shows "dist (- x) (- y) = dist x y"
  3357   unfolding dist_norm minus_diff_minus norm_minus_cancel ..
  3360   unfolding dist_norm minus_diff_minus norm_minus_cancel ..
  3358 
  3361 
  3359 lemma uniformly_continuous_on_neg:
  3362 lemma uniformly_continuous_on_neg:
  3360   fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" (* FIXME: generalize *)
  3363   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
  3361   shows "uniformly_continuous_on s f
  3364   shows "uniformly_continuous_on s f
  3362          ==> uniformly_continuous_on s (\<lambda>x. -(f x))"
  3365          ==> uniformly_continuous_on s (\<lambda>x. -(f x))"
  3363   unfolding uniformly_continuous_on_def dist_minus .
  3366   unfolding uniformly_continuous_on_def dist_minus .
  3364 
  3367 
  3365 lemma uniformly_continuous_on_add:
  3368 lemma uniformly_continuous_on_add:
  3366   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  3369   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
  3367   assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
  3370   assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
  3368   shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
  3371   shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
  3369 proof-
  3372 proof-
  3370   {  fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
  3373   {  fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
  3371                     "((\<lambda>n. g (x n) - g (y n)) ---> 0) sequentially"
  3374                     "((\<lambda>n. g (x n) - g (y n)) ---> 0) sequentially"
  3374     hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and add_diff_add [symmetric] by auto  }
  3377     hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and add_diff_add [symmetric] by auto  }
  3375   thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
  3378   thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
  3376 qed
  3379 qed
  3377 
  3380 
  3378 lemma uniformly_continuous_on_sub:
  3381 lemma uniformly_continuous_on_sub:
  3379   fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" (* FIXME: generalize *)
  3382   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
  3380   shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
  3383   shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
  3381            ==> uniformly_continuous_on s  (\<lambda>x. f x - g x)"
  3384            ==> uniformly_continuous_on s  (\<lambda>x. f x - g x)"
  3382   unfolding ab_diff_minus
  3385   unfolding ab_diff_minus
  3383   using uniformly_continuous_on_add[of s f "\<lambda>x. - g x"]
  3386   using uniformly_continuous_on_add[of s f "\<lambda>x. - g x"]
  3384   using uniformly_continuous_on_neg[of s g] by auto
  3387   using uniformly_continuous_on_neg[of s g] by auto