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