src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 51773 9328c6681f3c
parent 51641 cd05e9fcc63d
child 52141 eff000cab70f
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Apr 25 10:31:10 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Apr 24 13:28:30 2013 +0200
     1.3 @@ -1364,8 +1364,8 @@
     1.4    by (simp add: sequentially_imp_eventually_within)
     1.5  
     1.6  lemma Lim_right_bound:
     1.7 -  fixes f :: "'a :: {linorder_topology, conditional_complete_linorder, no_top} \<Rightarrow>
     1.8 -    'b::{linorder_topology, conditional_complete_linorder}"
     1.9 +  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow>
    1.10 +    'b::{linorder_topology, conditionally_complete_linorder}"
    1.11    assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
    1.12    assumes bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
    1.13    shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"