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
```