src/HOL/Library/Topology_Euclidean_Space.thy
 changeset 31531 fc78714d14e1 parent 31530 e31d63c66f55 child 31532 43e8d4bfde26
equal 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`