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