exists_hasDerivWithinAt_eq_of_lt_of_gt

English

Darboux's theorem in the reverse orientation: if a ≤ b and f' b < m < f' a, then m lies in the image f' on (a,b).

Русский

Дарбок в обратном виде: если a ≤ b и f'(b) < m < f'(a), то m достигается как значение производной на (a,b).

LaTeX

$$let c,d denote points with a ≤ b and m between f'(b) and f'(a); then m ∈ f' '' Ioo a b$$

Lean4

/-- **Darboux's theorem**: if `a ≤ b` and `f' b < m < f' a`, then `f' c = m` for some `c ∈ (a, b)`.
-/
theorem exists_hasDerivWithinAt_eq_of_lt_of_gt (hab : a ≤ b) (hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x)
    {m : ℝ} (hma : m < f' a) (hmb : f' b < m) : m ∈ f' '' Ioo a b :=
  let ⟨c, cmem, hc⟩ :=
    exists_hasDerivWithinAt_eq_of_gt_of_lt hab (fun x hx => (hf x hx).neg) (neg_lt_neg hma) (neg_lt_neg hmb)
  ⟨c, cmem, neg_injective hc⟩

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