1797 shows "((\<lambda>x. f x) \<longlongrightarrow> x) (at a) \<longleftrightarrow> ((g \<longlongrightarrow> y) (at a))" |
1797 shows "((\<lambda>x. f x) \<longlongrightarrow> x) (at a) \<longleftrightarrow> ((g \<longlongrightarrow> y) (at a))" |
1798 unfolding tendsto_def eventually_at_topological |
1798 unfolding tendsto_def eventually_at_topological |
1799 using assms by simp |
1799 using assms by simp |
1800 |
1800 |
1801 text \<open>An unbounded sequence's inverse tends to 0.\<close> |
1801 text \<open>An unbounded sequence's inverse tends to 0.\<close> |
1802 lemma LIMSEQ_inverse_zero: "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0" |
1802 lemma LIMSEQ_inverse_zero: |
|
1803 assumes "\<And>r::real. \<exists>N. \<forall>n\<ge>N. r < X n" |
|
1804 shows "(\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0" |
1803 apply (rule filterlim_compose[OF tendsto_inverse_0]) |
1805 apply (rule filterlim_compose[OF tendsto_inverse_0]) |
1804 apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially) |
1806 apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially) |
1805 apply (metis abs_le_D1 linorder_le_cases linorder_not_le) |
1807 apply (metis assms abs_le_D1 linorder_le_cases linorder_not_le) |
1806 done |
1808 done |
1807 |
1809 |
1808 text \<open>The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity.\<close> |
1810 text \<open>The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity.\<close> |
1809 lemma LIMSEQ_inverse_real_of_nat: "(\<lambda>n. inverse (real (Suc n))) \<longlonglongrightarrow> 0" |
1811 lemma LIMSEQ_inverse_real_of_nat: "(\<lambda>n. inverse (real (Suc n))) \<longlonglongrightarrow> 0" |
1810 by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc |
1812 by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc |
2187 lemma LIM_offset_zero_iff: "f \<midarrow>a\<rightarrow> L \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L" |
2189 lemma LIM_offset_zero_iff: "f \<midarrow>a\<rightarrow> L \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L" |
2188 for f :: "'a :: real_normed_vector \<Rightarrow> _" |
2190 for f :: "'a :: real_normed_vector \<Rightarrow> _" |
2189 using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto |
2191 using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto |
2190 |
2192 |
2191 lemma LIM_zero: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. f x - l) \<longlongrightarrow> 0) F" |
2193 lemma LIM_zero: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. f x - l) \<longlongrightarrow> 0) F" |
2192 for f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
2194 for f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2193 unfolding tendsto_iff dist_norm by simp |
2195 unfolding tendsto_iff dist_norm by simp |
2194 |
2196 |
2195 lemma LIM_zero_cancel: |
2197 lemma LIM_zero_cancel: |
2196 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
2198 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2197 shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F" |
2199 shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F" |
2198 unfolding tendsto_iff dist_norm by simp |
2200 unfolding tendsto_iff dist_norm by simp |
2199 |
2201 |
2200 lemma LIM_zero_iff: "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F = (f \<longlongrightarrow> l) F" |
2202 lemma LIM_zero_iff: "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F = (f \<longlongrightarrow> l) F" |
2201 for f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
2203 for f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2202 unfolding tendsto_iff dist_norm by simp |
2204 unfolding tendsto_iff dist_norm by simp |
2203 |
2205 |
2204 lemma LIM_imp_LIM: |
2206 lemma LIM_imp_LIM: |
2205 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
2207 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
2206 fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector" |
2208 fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector" |