src/HOL/Library/Liminf_Limsup.thy
changeset 62343 24106dc44def
parent 62049 b0f941e207cf
child 62624 59ceeb6f3079
--- a/src/HOL/Library/Liminf_Limsup.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -380,7 +380,7 @@
   note * = this
 
   have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))"
-    unfolding Liminf_def SUP_def
+    unfolding Liminf_def
     by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
   also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
@@ -405,7 +405,7 @@
   note * = this
 
   have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))"
-    unfolding Limsup_def INF_def
+    unfolding Limsup_def
     by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
   also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
@@ -429,7 +429,7 @@
       by auto
   qed
   have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
-    unfolding Limsup_def INF_def
+    unfolding Limsup_def
     by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
   also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
@@ -455,7 +455,7 @@
   note * = this
 
   have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))"
-    unfolding Liminf_def SUP_def
+    unfolding Liminf_def
     by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
   also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"