equal
deleted
inserted
replaced
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 filter_lim} and @{term NSLIM} *} |
136 subsubsection {* Equivalence of @{term filterlim} 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 |