src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
changeset 44125 230a8665c919
parent 43923 ab93d0190a5d
child 44142 8e27e0177518
     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Aug 09 08:53:12 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Aug 09 10:30:00 2011 -0700
     1.3 @@ -248,7 +248,7 @@
     1.4      show "eventually (\<lambda>x. a * X x \<in> S) net"
     1.5        by (rule eventually_mono[OF _ *]) auto
     1.6    qed
     1.7 -qed auto
     1.8 +qed (auto intro: tendsto_const)
     1.9  
    1.10  lemma ereal_lim_uminus:
    1.11    fixes X :: "'a \<Rightarrow> ereal" shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net"
    1.12 @@ -460,12 +460,12 @@
    1.13    assumes inc: "incseq X" and lim: "X ----> L"
    1.14    shows "X N \<le> L"
    1.15    using inc
    1.16 -  by (intro ereal_lim_mono[of N, OF _ Lim_const lim]) (simp add: incseq_def)
    1.17 +  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
    1.18  
    1.19  lemma decseq_ge_ereal: assumes dec: "decseq X"
    1.20    and lim: "X ----> (L::ereal)" shows "X N >= L"
    1.21    using dec
    1.22 -  by (intro ereal_lim_mono[of N, OF _ lim Lim_const]) (simp add: decseq_def)
    1.23 +  by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
    1.24  
    1.25  lemma liminf_bounded_open:
    1.26    fixes x :: "nat \<Rightarrow> ereal"
    1.27 @@ -519,7 +519,7 @@
    1.28  lemma lim_ereal_increasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
    1.29    obtains l where "f ----> (l::ereal)"
    1.30  proof(cases "f = (\<lambda>x. - \<infinity>)")
    1.31 -  case True then show thesis using Lim_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
    1.32 +  case True then show thesis using tendsto_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
    1.33  next
    1.34    case False
    1.35    from this obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
    1.36 @@ -1138,7 +1138,7 @@
    1.37        by (induct i) (insert assms, auto) }
    1.38    note this[simp]
    1.39    show ?thesis unfolding sums_def
    1.40 -    by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan)
    1.41 +    by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan intro: tendsto_const)
    1.42  qed
    1.43  
    1.44  lemma suminf_finite:
    1.45 @@ -1298,4 +1298,4 @@
    1.46      apply (subst SUP_commute) ..
    1.47  qed
    1.48  
    1.49 -end
    1.50 \ No newline at end of file
    1.51 +end