image_hasDerivWithinAt — Mathlib

English

If s is convex and HasDerivWithinAt holds for all x ∈ s, then the image of dslope under f' is convex.

Русский

Если множество выпукло и выполняются условия HasDerivWithinAt, образ dslope под f' выпукл.

LaTeX

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

Lean4

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

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