src/HOL/Lim.thy
 changeset 44568 e6f291cb5810 parent 44532 a2e9b39df938 child 44570 b93d1b3ee300
```     1.1 --- a/src/HOL/Lim.thy	Sat Aug 27 17:26:14 2011 +0200
1.2 +++ b/src/HOL/Lim.thy	Sun Aug 28 09:20:12 2011 -0700
1.3 @@ -211,51 +211,6 @@
1.4    finally show "norm (g x - 0) \<le> norm (f x - 0)" .
1.5  qed
1.6
1.7 -text {* Bounded Linear Operators *}
1.8 -
1.9 -lemma (in bounded_linear) LIM:
1.10 -  "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
1.11 -by (rule tendsto)
1.12 -
1.13 -lemma (in bounded_linear) LIM_zero:
1.14 -  "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
1.15 -  by (rule tendsto_zero)
1.16 -
1.17 -text {* Bounded Bilinear Operators *}
1.18 -
1.19 -lemma (in bounded_bilinear) LIM:
1.20 -  "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
1.21 -by (rule tendsto)
1.22 -
1.23 -lemma (in bounded_bilinear) LIM_prod_zero:
1.24 -  fixes a :: "'d::metric_space"
1.25 -  assumes f: "f -- a --> 0"
1.26 -  assumes g: "g -- a --> 0"
1.27 -  shows "(\<lambda>x. f x ** g x) -- a --> 0"
1.28 -  using f g by (rule tendsto_zero)
1.29 -
1.30 -lemma (in bounded_bilinear) LIM_left_zero:
1.31 -  "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
1.32 -  by (rule tendsto_left_zero)
1.33 -
1.34 -lemma (in bounded_bilinear) LIM_right_zero:
1.35 -  "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
1.36 -  by (rule tendsto_right_zero)
1.37 -
1.38 -lemmas LIM_mult_zero =
1.39 -  bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
1.40 -
1.41 -lemmas LIM_mult_left_zero =
1.42 -  bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
1.43 -
1.44 -lemmas LIM_mult_right_zero =
1.45 -  bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
1.46 -
1.47 -lemma LIM_inverse_fun:
1.48 -  assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
1.49 -  shows "inverse -- a --> inverse a"
1.50 -  by (rule tendsto_inverse [OF tendsto_ident_at a])
1.51 -
1.52
1.53  subsection {* Continuity *}
1.54
1.55 @@ -495,29 +450,4 @@
1.56     (X -- a --> (L::'b::topological_space))"
1.57    using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
1.58
1.59 -subsection {* Legacy theorem names *}
1.60 -
1.61 -lemmas LIM_ident [simp] = tendsto_ident_at
1.62 -lemmas LIM_const [simp] = tendsto_const [where F="at x", standard]
1.63 -lemmas LIM_add = tendsto_add [where F="at x", standard]
1.64 -lemmas LIM_add_zero = tendsto_add_zero [where F="at x", standard]
1.65 -lemmas LIM_minus = tendsto_minus [where F="at x", standard]
1.66 -lemmas LIM_diff = tendsto_diff [where F="at x", standard]
1.67 -lemmas LIM_norm = tendsto_norm [where F="at x", standard]
1.68 -lemmas LIM_norm_zero = tendsto_norm_zero [where F="at x", standard]
1.69 -lemmas LIM_norm_zero_cancel = tendsto_norm_zero_cancel [where F="at x", standard]
1.70 -lemmas LIM_norm_zero_iff = tendsto_norm_zero_iff [where F="at x", standard]
1.71 -lemmas LIM_rabs = tendsto_rabs [where F="at x", standard]
1.72 -lemmas LIM_rabs_zero = tendsto_rabs_zero [where F="at x", standard]
1.73 -lemmas LIM_rabs_zero_cancel = tendsto_rabs_zero_cancel [where F="at x", standard]
1.74 -lemmas LIM_rabs_zero_iff = tendsto_rabs_zero_iff [where F="at x", standard]
1.75 -lemmas LIM_compose = tendsto_compose [where F="at x", standard]
1.76 -lemmas LIM_mult = tendsto_mult [where F="at x", standard]
1.77 -lemmas LIM_scaleR = tendsto_scaleR [where F="at x", standard]
1.78 -lemmas LIM_of_real = tendsto_of_real [where F="at x", standard]
1.79 -lemmas LIM_power = tendsto_power [where F="at x", standard]
1.80 -lemmas LIM_inverse = tendsto_inverse [where F="at x", standard]
1.81 -lemmas LIM_sgn = tendsto_sgn [where F="at x", standard]
1.82 -lemmas isCont_LIM_compose = isCont_tendsto_compose [where F="at x", standard]
1.83 -
1.84  end
```