# HG changeset patch # User huffman # Date 1314574087 25200 # Node ID b93d1b3ee30088a70938d3eab1eca1ecb63ea638 # Parent 44525dd281d43bb830eeecf62d9de6c2a9259655 generalize LIM_zero lemmas to arbitrary filters diff -r 44525dd281d4 -r b93d1b3ee300 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Sun Aug 28 09:22:42 2011 -0700 +++ b/src/HOL/Lim.thy Sun Aug 28 16:28:07 2011 -0700 @@ -85,17 +85,17 @@ lemma LIM_zero: fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "f -- a --> l \ (\x. f x - l) -- a --> 0" + shows "(f ---> l) F \ ((\x. f x - l) ---> 0) F" unfolding tendsto_iff dist_norm by simp lemma LIM_zero_cancel: fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "(\x. f x - l) -- a --> 0 \ f -- a --> l" + shows "((\x. f x - l) ---> 0) F \ (f ---> l) F" unfolding tendsto_iff dist_norm by simp lemma LIM_zero_iff: fixes f :: "'a::metric_space \ 'b::real_normed_vector" - shows "(\x. f x - l) -- a --> 0 = f -- a --> l" + shows "((\x. f x - l) ---> 0) F = (f ---> l) F" unfolding tendsto_iff dist_norm by simp lemma metric_LIM_imp_LIM: