# HG changeset patch # User huffman # Date 1163027956 -3600 # Node ID b7f090c5057de1f25ee398efd5ea4c117627dd03 # Parent 47195501ecf7054b2a7278d8608610d81443c3aa added LIM_norm and related lemmas diff -r 47195501ecf7 -r b7f090c5057d src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Wed Nov 08 23:11:13 2006 +0100 +++ b/src/HOL/Hyperreal/Lim.thy Thu Nov 09 00:19:16 2006 +0100 @@ -107,6 +107,10 @@ qed qed +lemma LIM_add_zero: + "\f -- a --> 0; g -- a --> 0\ \ (\x. f x + g x) -- a --> 0" +by (drule (1) LIM_add, simp) + lemma minus_diff_minus: fixes a b :: "'a::ab_group_add" shows "(- a) - (- b) = - (a - b)" @@ -129,6 +133,25 @@ lemma LIM_zero_cancel: "(\x. f x - l) -- a --> 0 \ f -- a --> l" by (simp add: LIM_def) +lemma LIM_imp_LIM: + assumes f: "f -- a --> l" + assumes le: "\x. x \ a \ norm (g x - m) \ norm (f x - l)" + shows "g -- a --> m" +apply (rule LIM_I, drule LIM_D [OF f], safe) +apply (rule_tac x="s" in exI, safe) +apply (drule_tac x="x" in spec, safe) +apply (erule (1) order_le_less_trans [OF le]) +done + +lemma LIM_norm: "f -- a --> l \ (\x. norm (f x)) -- a --> norm l" +by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3) + +lemma LIM_norm_zero: "f -- a --> 0 \ (\x. norm (f x)) -- a --> 0" +by (drule LIM_norm, simp) + +lemma LIM_norm_zero_cancel: "(\x. norm (f x)) -- a --> 0 \ f -- a --> 0" +by (erule LIM_imp_LIM, simp) + lemma LIM_const_not_eq: fixes a :: "'a::real_normed_div_algebra" shows "k \ L ==> ~ ((%x. k) -- a --> L)"