equal
deleted
inserted
replaced
192 |
192 |
193 |
193 |
194 subsection {* Limits of Sequences *} |
194 subsection {* Limits of Sequences *} |
195 |
195 |
196 lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially" |
196 lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially" |
197 unfolding LIMSEQ_def tendsto_def eventually_sequentially .. |
197 unfolding LIMSEQ_def tendsto_iff eventually_sequentially .. |
198 |
198 |
199 lemma LIMSEQ_iff: |
199 lemma LIMSEQ_iff: |
200 fixes L :: "'a::real_normed_vector" |
200 fixes L :: "'a::real_normed_vector" |
201 shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)" |
201 shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)" |
202 unfolding LIMSEQ_def dist_norm .. |
202 unfolding LIMSEQ_def dist_norm .. |