1847 |
1847 |
1848 lemma metric_LIMSEQ_D: "X \<longlonglongrightarrow> L \<Longrightarrow> 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r" |
1848 lemma metric_LIMSEQ_D: "X \<longlonglongrightarrow> L \<Longrightarrow> 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r" |
1849 for L :: "'a::metric_space" |
1849 for L :: "'a::metric_space" |
1850 by (simp add: lim_sequentially) |
1850 by (simp add: lim_sequentially) |
1851 |
1851 |
|
1852 lemma LIMSEQ_norm_0: |
|
1853 assumes "\<And>n::nat. norm (f n) < 1 / real (Suc n)" |
|
1854 shows "f \<longlonglongrightarrow> 0" |
|
1855 proof (rule metric_LIMSEQ_I) |
|
1856 fix \<epsilon> :: "real" |
|
1857 assume "\<epsilon> > 0" |
|
1858 then obtain N::nat where "\<epsilon> > inverse N" "N > 0" |
|
1859 by (metis neq0_conv real_arch_inverse) |
|
1860 then have "norm (f n) < \<epsilon>" if "n \<ge> N" for n |
|
1861 proof - |
|
1862 have "1 / (Suc n) \<le> 1 / N" |
|
1863 using \<open>0 < N\<close> inverse_of_nat_le le_SucI that by blast |
|
1864 also have "\<dots> < \<epsilon>" |
|
1865 by (metis (no_types) \<open>inverse (real N) < \<epsilon>\<close> inverse_eq_divide) |
|
1866 finally show ?thesis |
|
1867 by (meson assms less_eq_real_def not_le order_trans) |
|
1868 qed |
|
1869 then show "\<exists>no. \<forall>n\<ge>no. dist (f n) 0 < \<epsilon>" |
|
1870 by auto |
|
1871 qed |
|
1872 |
1852 |
1873 |
1853 subsubsection \<open>Limits of Functions\<close> |
1874 subsubsection \<open>Limits of Functions\<close> |
1854 |
1875 |
1855 lemma LIM_def: "f \<midarrow>a\<rightarrow> L \<longleftrightarrow> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)" |
1876 lemma LIM_def: "f \<midarrow>a\<rightarrow> L \<longleftrightarrow> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)" |
1856 for a :: "'a::metric_space" and L :: "'b::metric_space" |
1877 for a :: "'a::metric_space" and L :: "'b::metric_space" |