author | huffman |
Mon, 15 Aug 2011 16:18:13 -0700 | |
changeset 44217 | 5cdad94bdc29 |
parent 44216 | 903bfe95fece |
child 44218 | f0e442e24816 |
src/HOL/Lim.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Lim.thy Mon Aug 15 15:11:55 2011 -0700 +++ b/src/HOL/Lim.thy Mon Aug 15 16:18:13 2011 -0700 @@ -386,8 +386,6 @@ shows "(\<lambda>x. f x ^ n) -- a --> l ^ n" using assms by (rule tendsto_power) -subsubsection {* Derived theorems about @{term LIM} *} - lemma LIM_inverse: fixes L :: "'a::real_normed_div_algebra" shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"