Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Limits.thy
changeset 70532 fcf3b891ccb1
parent 70365 4df0628e8545
child 70688 3d894e1cfc75 
--- a/src/HOL/Limits.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Limits.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -1981,7 +1981,7 @@
   using Lim_transform Lim_transform2 by blast
 
 lemma Lim_transform_eventually:
-  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f \<longlongrightarrow> l) net \<Longrightarrow> (g \<longlongrightarrow> l) net"
+  "\<lbrakk>(f \<longlongrightarrow> l) F; eventually (\<lambda>x. f x = g x) F\<rbrakk> \<Longrightarrow> (g \<longlongrightarrow> l) F"
   using eventually_elim2 by (fastforce simp add: tendsto_def)
 
 lemma Lim_transform_within:
isabelle