src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
changeset 54257 5c7a3b6b05a9
parent 53788 b319a0c8b8a2
child 54258 adfc759263ab
     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 05 05:48:08 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 05 09:44:57 2013 +0100
     1.3 @@ -1193,12 +1193,12 @@
     1.4  qed
     1.5  
     1.6  lemma Liminf_at:
     1.7 -  fixes f :: "'a::metric_space \<Rightarrow> _"
     1.8 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
     1.9    shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
    1.10    using Liminf_within[of x UNIV f] by simp
    1.11  
    1.12  lemma Limsup_at:
    1.13 -  fixes f :: "'a::metric_space \<Rightarrow> _"
    1.14 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
    1.15    shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
    1.16    using Limsup_within[of x UNIV f] by simp
    1.17