image_deriv — Mathlib

English

If s is convex and f is differentiable on s, then the image of deriv f on s is convex.

Русский

Если s выпукло и f дифференцируема на s, образ deriv f на s выпукл.

LaTeX

$$Convex (deriv f '' s)$$

Lean4

/-- **Darboux's theorem**: the image of a convex set under `f'` is a convex set,
`deriv` version. -/
theorem image_deriv {s : Set ℝ} (hs : Convex ℝ s) (hf : ∀ x ∈ s, DifferentiableAt ℝ f x) : Convex ℝ (deriv f '' s) :=
  (hs.ordConnected.image_deriv hf).convex

Похожие утверждения