src/HOL/Analysis/Uniform_Limit.thy
changeset 65037 2cf841ff23be
parent 65036 ab7e11730ad8
child 65204 d23eded35a33
     1.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Tue Feb 21 15:04:01 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Tue Feb 21 17:12:10 2017 +0000
     1.3 @@ -519,7 +519,7 @@
     1.4      using lte by (force intro: eventually_mono)
     1.5  qed
     1.6  
     1.7 -lemma uniform_lim_div:
     1.8 +lemma uniform_lim_divide:
     1.9    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_field"
    1.10    assumes f: "uniform_limit S f l F"
    1.11        and g: "uniform_limit S g m F"