equal
deleted
inserted
replaced
698 by (rule F3) |
698 by (rule F3) |
699 with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r" by fast |
699 with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r" by fast |
700 } |
700 } |
701 then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp |
701 then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp |
702 with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto |
702 with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto |
703 thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less) |
703 thus ?thesis by (unfold LIMSEQ_iff, auto simp add: linorder_not_less) |
704 qed |
704 qed |
705 ultimately show False by simp |
705 ultimately show False by simp |
706 qed |
706 qed |
707 |
707 |
708 lemma LIMSEQ_SEQ_conv: |
708 lemma LIMSEQ_SEQ_conv: |