Theorems · Theorem · real analysis

strictAnti_of_deriv_neg

∀ {f : ℝ → ℝ}, (∀ (x : ℝ), deriv f x < 0) → StrictAnti f

Let f : ℝ → ℝ be a differentiable function. If f' is negative, then f is a strictly antitone function. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly negative.

Defined in

Mathlib.Analysis.Calculus.Deriv.MeanValue

Cited by

1 results in Mathlib

Foundations

Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound