equal
deleted
inserted
replaced
402 lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] |
402 lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] |
403 |
403 |
404 lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F" |
404 lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F" |
405 by (simp only: tendsto_iff Zfun_def dist_norm) |
405 by (simp only: tendsto_iff Zfun_def dist_norm) |
406 |
406 |
|
407 lemma tendsto_0_le: "\<lbrakk>(f ---> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk> |
|
408 \<Longrightarrow> (g ---> 0) F" |
|
409 by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff) |
|
410 |
407 subsubsection {* Distance and norms *} |
411 subsubsection {* Distance and norms *} |
408 |
412 |
409 lemma tendsto_dist [tendsto_intros]: |
413 lemma tendsto_dist [tendsto_intros]: |
410 fixes l m :: "'a :: metric_space" |
414 fixes l m :: "'a :: metric_space" |
411 assumes f: "(f ---> l) F" and g: "(g ---> m) F" |
415 assumes f: "(f ---> l) F" and g: "(g ---> m) F" |