src/HOL/Analysis/Borel_Space.thy
changeset 63952 354808e9f44b
parent 63627 6ddb43c6b711
child 64008 17a20ca86d62
     1.1 --- a/src/HOL/Analysis/Borel_Space.thy	Mon Sep 26 07:56:54 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Wed Sep 28 17:01:01 2016 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4    assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
     1.5    assumes "x \<in> interior A"
     1.6    shows "D \<ge> 0"
     1.7 -proof (rule tendsto_le_const)
     1.8 +proof (rule tendsto_lowerbound)
     1.9    let ?A' = "(\<lambda>y. y - x) ` interior A"
    1.10    from deriv show "((\<lambda>h. (f (x + h) - f x) / h) \<longlongrightarrow> D) (at 0)"
    1.11        by (simp add: field_has_derivative_at has_field_derivative_def)