src/HOL/Lim.thy
 changeset 44571 bd91b77c4cd6 parent 44570 b93d1b3ee300 child 45031 9583f2b56f85
equal inserted replaced
44570:b93d1b3ee300 44571:bd91b77c4cd6
`   112   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"`
`   112   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"`
`   113   shows "g -- a --> m"`
`   113   shows "g -- a --> m"`
`   114   by (rule metric_LIM_imp_LIM [OF f],`
`   114   by (rule metric_LIM_imp_LIM [OF f],`
`   115     simp add: dist_norm le)`
`   115     simp add: dist_norm le)`
`   116 `
`   116 `
`   124 lemma LIM_const_not_eq:`
`   117 lemma LIM_const_not_eq:`
`   125   fixes a :: "'a::real_normed_algebra_1"`
`   118   fixes a :: "'a::perfect_space"`
`   126   fixes k L :: "'b::t2_space"`
`   119   fixes k L :: "'b::t2_space"`
`   127   shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"`
`   120   shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"`
`   128 by (simp add: tendsto_const_iff trivial_limit_at)`
`   121   by (simp add: tendsto_const_iff)`
`   129 `
`   122 `
`   130 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]`
`   123 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]`
`   131 `
`   124 `
`   132 lemma LIM_const_eq:`
`   125 lemma LIM_const_eq:`
`   133   fixes a :: "'a::real_normed_algebra_1"`
`   126   fixes a :: "'a::perfect_space"`
`   134   fixes k L :: "'b::t2_space"`
`   127   fixes k L :: "'b::t2_space"`
`   135   shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"`
`   128   shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"`
`   136   by (simp add: tendsto_const_iff trivial_limit_at)`
`   129   by (simp add: tendsto_const_iff)`
`   137 `
`   130 `
`   138 lemma LIM_unique:`
`   131 lemma LIM_unique:`
`   139   fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}`
`   132   fixes a :: "'a::perfect_space"`
`   140   fixes L M :: "'b::t2_space"`
`   133   fixes L M :: "'b::t2_space"`
`   141   shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"`
`   134   shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"`
`   142   using trivial_limit_at by (rule tendsto_unique)`
`   135   using at_neq_bot by (rule tendsto_unique)`
`   143 `
`   136 `
`   144 text{*Limits are equal for functions equal except at limit point*}`
`   137 text{*Limits are equal for functions equal except at limit point*}`
`   145 lemma LIM_equal:`
`   138 lemma LIM_equal:`
`   146      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"`
`   139      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"`
`   147 unfolding tendsto_def eventually_at_topological by simp`
`   140 unfolding tendsto_def eventually_at_topological by simp`