src/HOL/Analysis/Infinite_Products.thy
changeset 68426 e0b5f2d14bf9
parent 68424 02e5a44ffe7d
child 68452 c027dfbfad30
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Mon Jun 11 15:53:22 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Mon Jun 11 16:23:21 2018 +0100
     1.3 @@ -1431,7 +1431,7 @@
     1.4  
     1.5  subsection\<open>Embeddings from the reals into some complete real normed field\<close>
     1.6  
     1.7 -lemma tendsto_of_real:
     1.8 +lemma tendsto_eq_of_real_lim:
     1.9    assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
    1.10    shows "q = of_real (lim f)"
    1.11  proof -
    1.12 @@ -1444,10 +1444,10 @@
    1.13      by (metis LIMSEQ_unique assms convergentD sequentially_bot tendsto_Lim tendsto_of_real)
    1.14  qed
    1.15  
    1.16 -lemma tendsto_of_real':
    1.17 +lemma tendsto_eq_of_real:
    1.18    assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
    1.19    obtains r where "q = of_real r"
    1.20 -  using tendsto_of_real assms by blast
    1.21 +  using tendsto_eq_of_real_lim assms by blast
    1.22  
    1.23  lemma has_prod_of_real_iff:
    1.24    "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) has_prod of_real c \<longleftrightarrow> f has_prod c"
    1.25 @@ -1456,7 +1456,7 @@
    1.26    assume ?lhs
    1.27    then show ?rhs
    1.28      apply (auto simp: prod_defs LIMSEQ_prod_0 tendsto_of_real_iff simp flip: of_real_prod)
    1.29 -    using tendsto_of_real'
    1.30 +    using tendsto_eq_of_real
    1.31      by (metis of_real_0 tendsto_of_real_iff)
    1.32  next
    1.33    assume ?rhs