src/HOL/NSA/HLim.thy
changeset 50249 3f0920f8a24e
parent 41959 b460124855b8
child 50322 b06b95a5fda2
equal deleted inserted replaced
50248:9a65279b5d27 50249:3f0920f8a24e
   131 by (drule NSLIM_mult, auto)
   131 by (drule NSLIM_mult, auto)
   132 
   132 
   133 lemma NSLIM_self: "(%x. x) -- a --NS> a"
   133 lemma NSLIM_self: "(%x. x) -- a --NS> a"
   134 by (simp add: NSLIM_def)
   134 by (simp add: NSLIM_def)
   135 
   135 
   136 subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
   136 subsubsection {* Equivalence of @{term filter_lim} and @{term NSLIM} *}
   137 
   137 
   138 lemma LIM_NSLIM:
   138 lemma LIM_NSLIM:
   139   assumes f: "f -- a --> L" shows "f -- a --NS> L"
   139   assumes f: "f -- a --> L" shows "f -- a --NS> L"
   140 proof (rule NSLIM_I)
   140 proof (rule NSLIM_I)
   141   fix x
   141   fix x