equal
deleted
inserted
replaced
455 apply (induct_tac "no") |
455 apply (induct_tac "no") |
456 apply simp |
456 apply simp |
457 apply (auto intro: order_trans simp add: diff_minus abs_if) |
457 apply (auto intro: order_trans simp add: diff_minus abs_if) |
458 done |
458 done |
459 |
459 |
460 lemma lim_uminus: "convergent g ==> lim (%x. - g x) = - (lim g)" |
460 lemma lim_uminus: |
|
461 fixes g :: "nat \<Rightarrow> 'a::real_normed_vector" |
|
462 shows "convergent g ==> lim (%x. - g x) = - (lim g)" |
461 apply (rule LIMSEQ_minus [THEN limI]) |
463 apply (rule LIMSEQ_minus [THEN limI]) |
462 apply (simp add: convergent_LIMSEQ_iff) |
464 apply (simp add: convergent_LIMSEQ_iff) |
463 done |
465 done |
464 |
466 |
465 lemma g_dec_imp_lim_le: |
467 lemma g_dec_imp_lim_le: |