image_derivWithin — Mathlib

English

Alternative formalization: the image of an OrdConnected set under a function whose HasDerivWithinAt holds is OrdConnected.

Русский

Альтернатива: образ OrdConnected множества под функцией, у которой выполняется HasDerivWithinAt, остаётся OrdConnected.

LaTeX

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

Lean4

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

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