image_derivWithin — Mathlib

English

If s is convex and f is differentiable on s, then the image of derivWithin f s under f' is convex.

Русский

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

LaTeX

$$Convex (derivWithin f s '' s)$$

Lean4

/-- **Darboux's theorem**: the image of a convex set under `f'` is a convex set,
`derivWithin` version. -/
theorem image_derivWithin {s : Set ℝ} (hs : Convex ℝ s) (hf : DifferentiableOn ℝ f s) :
    Convex ℝ (derivWithin f s '' s) :=
  (hs.ordConnected.image_derivWithin hf).convex

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