src/HOL/Lim.thy
 changeset 44205 18da2a87421c parent 44194 0639898074ae child 44217 5cdad94bdc29
equal inserted replaced
44195:f5363511b212 44205:18da2a87421c
`   179   by (rule tendsto_rabs_zero_cancel)`
`   179   by (rule tendsto_rabs_zero_cancel)`
`   180 `
`   180 `
`   181 lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"`
`   181 lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"`
`   182   by (rule tendsto_rabs_zero_iff)`
`   182   by (rule tendsto_rabs_zero_iff)`
`   183 `
`   183 `
`   184 lemma at_neq_bot:`
`   184 lemma trivial_limit_at:`
`   185   fixes a :: "'a::real_normed_algebra_1"`
`   185   fixes a :: "'a::real_normed_algebra_1"`
`   186   shows "at a \<noteq> bot"  -- {* TODO: find a more appropriate class *}`
`   186   shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}`
`   187 unfolding eventually_False [symmetric]`
`   187 unfolding trivial_limit_def`
`   188 unfolding eventually_at dist_norm`
`   188 unfolding eventually_at dist_norm`
`   189 by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)`
`   189 by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)`
`   190 `
`   190 `
`   191 lemma LIM_const_not_eq:`
`   191 lemma LIM_const_not_eq:`
`   192   fixes a :: "'a::real_normed_algebra_1"`
`   192   fixes a :: "'a::real_normed_algebra_1"`
`   193   fixes k L :: "'b::metric_space"`
`   193   fixes k L :: "'b::t2_space"`
`   194   shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"`
`   194   shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"`
`   195 by (simp add: tendsto_const_iff at_neq_bot)`
`   195 by (simp add: tendsto_const_iff trivial_limit_at)`
`   196 `
`   196 `
`   197 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]`
`   197 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]`
`   198 `
`   198 `
`   199 lemma LIM_const_eq:`
`   199 lemma LIM_const_eq:`
`   200   fixes a :: "'a::real_normed_algebra_1"`
`   200   fixes a :: "'a::real_normed_algebra_1"`
`   201   fixes k L :: "'b::metric_space"`
`   201   fixes k L :: "'b::t2_space"`
`   202   shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"`
`   202   shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"`
`   203 by (simp add: tendsto_const_iff at_neq_bot)`
`   203   by (simp add: tendsto_const_iff trivial_limit_at)`
`   204 `
`   204 `
`   205 lemma LIM_unique:`
`   205 lemma LIM_unique:`
`   206   fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}`
`   206   fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}`
`   207   fixes L M :: "'b::metric_space"`
`   207   fixes L M :: "'b::t2_space"`
`   208   shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"`
`   208   shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"`
`   209 by (drule (1) tendsto_dist, simp add: tendsto_const_iff at_neq_bot)`
`   209   using trivial_limit_at by (rule tendsto_unique)`
`   210 `
`   210 `
`   211 lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"`
`   211 lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"`
`   212 by (rule tendsto_ident_at)`
`   212 by (rule tendsto_ident_at)`
`   213 `
`   213 `
`   214 text{*Limits are equal for functions equal except at limit point*}`
`   214 text{*Limits are equal for functions equal except at limit point*}`