English
If s is an ordinally connected set and HasDerivWithinAt f (f' x) s x for all x ∈ s, then the image f'(s) is OrdConnected.
Русский
Пусть s ордометрически связно; если HasDerivWithinAt f (f'(x)) для всех x ∈ s, то образ f'(s) орд Connected.
LaTeX
$$OrdConnected (f' '' s)$$
Lean4
/-- **Darboux's theorem**: the image of a `Set.OrdConnected` set under `f'` is a `Set.OrdConnected`
set, `HasDerivWithinAt` version. -/
theorem image_hasDerivWithinAt {s : Set ℝ} (hs : OrdConnected s) (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) :
OrdConnected (f' '' s) := by
apply ordConnected_of_Ioo
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ - m ⟨hma, hmb⟩
rcases le_total a b with hab | hab
· have : Icc a b ⊆ s := hs.out ha hb
rcases exists_hasDerivWithinAt_eq_of_gt_of_lt hab (fun x hx => (hf x <| this hx).mono this) hma hmb with
⟨c, cmem, hc⟩
exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩
· have : Icc b a ⊆ s := hs.out hb ha
rcases exists_hasDerivWithinAt_eq_of_lt_of_gt hab (fun x hx => (hf x <| this hx).mono this) hmb hma with
⟨c, cmem, hc⟩
exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩
