image_deriv — Mathlib

English

If s is OrdConnected and f is differentiable on s, then the image of the derivatives under derivWithin is OrdConnected.

Русский

Если s орд connected и f дифференцируема на s, то образ производной derivWithin по s является OrdConnected.

LaTeX

$$OrdConnected (derivWithin f s '' s)$$

Lean4

/-- **Darboux's theorem**: the image of a `Set.OrdConnected` set under `f'` is a `Set.OrdConnected`
set, `deriv` version. -/
theorem image_deriv {s : Set ℝ} (hs : OrdConnected s) (hf : ∀ x ∈ s, DifferentiableAt ℝ f x) :
    OrdConnected (deriv f '' s) :=
  hs.image_hasDerivWithinAt fun x hx => (hf x hx).hasDerivAt.hasDerivWithinAt

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