English
Lagrange’s Mean Value Theorem on convex domains: If f: E → R is differentiable along a convex domain s with HasFDerivWithinAt f at each point in s, then there exists z in the segment between x and y such that f(y) − f(x) equals the derivative at z applied to (y − x).
Русский
Теорема среднего значения Лагранжа на выпуклой области: для f: E→R, дифференцируемой на s, существует z ∈ отрезка x y таких, что f(y) − f(x) = f'(z)·(y − x).
LaTeX
$$$\exists z \in \operatorname{segment}(x,y)\;:\; f(y) - f(x) = f'(z)(y-x)$ (in the appropriate generalized sense for E).$$
Lean4
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is strictly positive, then
`f` is a strictly monotone function. -/
theorem strictAnti_of_hasDerivAt_neg {f f' : ℝ → ℝ} (hf : ∀ x, HasDerivAt f (f' x) x) (hf' : ∀ x, f' x < 0) :
StrictAnti f :=
strictAnti_of_deriv_neg fun x ↦ by rw [(hf _).deriv]; exact hf' _
