src/HOL/Library/Liminf_Limsup.thy
 changeset 61810 3c5040d5694a parent 61806 d2e62ae01cd8 child 61880 ff4d33058566
```--- a/src/HOL/Library/Liminf_Limsup.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -100,7 +100,7 @@
lemma Liminf_eq:
assumes "eventually (\<lambda>x. f x = g x) F"
shows "Liminf F f = Liminf F g"
-  by (intro antisym Liminf_mono eventually_mono'[OF assms]) auto
+  by (intro antisym Liminf_mono eventually_mono[OF assms]) auto

lemma Limsup_mono:
assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
@@ -116,7 +116,7 @@
lemma Limsup_eq:
assumes "eventually (\<lambda>x. f x = g x) net"
shows "Limsup net f = Limsup net g"
-  by (intro antisym Limsup_mono eventually_mono'[OF assms]) auto
+  by (intro antisym Limsup_mono eventually_mono[OF assms]) auto

lemma Liminf_le_Limsup:
assumes ntriv: "\<not> trivial_limit F"
@@ -167,7 +167,7 @@
proof -
have "eventually (\<lambda>x. y < X x) F"
if "eventually P F" "y < INFIMUM (Collect P) X" for y P
-    using that by (auto elim!: eventually_elim1 dest: less_INF_D)
+    using that by (auto elim!: eventually_mono dest: less_INF_D)
moreover
have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
@@ -218,7 +218,7 @@
then have "eventually (\<lambda>x. y < f x) F"
using lim[THEN topological_tendstoD, of "{y <..}"] by auto
then have "eventually (\<lambda>x. f0 \<le> f x) F"
-        using discrete by (auto elim!: eventually_elim1)
+        using discrete by (auto elim!: eventually_mono)
then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
by (rule upper)
moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
@@ -257,7 +257,7 @@
then have "eventually (\<lambda>x. f x < y) F"
using lim[THEN topological_tendstoD, of "{..< y}"] by auto
then have "eventually (\<lambda>x. f x \<le> f0) F"
-        using False by (auto elim!: eventually_elim1 simp: not_less)
+        using False by (auto elim!: eventually_mono simp: not_less)
then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
by (rule lower)
moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
@@ -278,14 +278,14 @@
then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
unfolding Limsup_def INF_less_iff by auto
then show "eventually (\<lambda>x. f x < a) F"
-    by (auto elim!: eventually_elim1 dest: SUP_lessD)
+    by (auto elim!: eventually_mono dest: SUP_lessD)
next
fix a assume "a < f0"
with assms have "a < Liminf F f" by simp
then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
unfolding Liminf_def less_SUP_iff by auto
then show "eventually (\<lambda>x. a < f x) F"
-    by (auto elim!: eventually_elim1 dest: less_INF_D)
+    by (auto elim!: eventually_mono dest: less_INF_D)
qed

lemma tendsto_iff_Liminf_eq_Limsup:```