src/HOL/Library/Liminf_Limsup.thy
changeset 54257 5c7a3b6b05a9
parent 53381 355a4cac5440
child 54261 89991ef58448
     1.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Tue Nov 05 05:48:08 2013 +0100
     1.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Nov 05 09:44:57 2013 +0100
     1.3 @@ -21,11 +21,13 @@
     1.4    by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
     1.5  
     1.6  lemma SUPR_pair:
     1.7 -  "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
     1.8 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
     1.9 +  shows "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
    1.10    by (rule antisym) (auto intro!: SUP_least SUP_upper2)
    1.11  
    1.12  lemma INFI_pair:
    1.13 -  "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    1.14 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    1.15 +  shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    1.16    by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    1.17  
    1.18  subsubsection {* @{text Liminf} and @{text Limsup} *}
    1.19 @@ -41,12 +43,14 @@
    1.20  abbreviation "limsup \<equiv> Limsup sequentially"
    1.21  
    1.22  lemma Liminf_eqI:
    1.23 -  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
    1.24 +  fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
    1.25 +  shows "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
    1.26      (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    1.27    unfolding Liminf_def by (auto intro!: SUP_eqI)
    1.28  
    1.29  lemma Limsup_eqI:
    1.30 -  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
    1.31 +  fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
    1.32 +  shows "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
    1.33      (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    1.34    unfolding Limsup_def by (auto intro!: INF_eqI)
    1.35