not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi

English

Under hypotheses akin to MVT with differentiability on (a,b), there exists c ∈ Ioo(a,b) with (lgb-lga) deriv f c = (lfb-lfa) deriv g c.

Русский

При условиях, аналогичных MVT и касающихся производной, существует c ∈ Ioo(a,b) такое, что (lgb-lga) deriv f c = (lfb-lfa) deriv g c.

LaTeX

$$$\\exists c\\in I^{oo}_{a,b}, (lgb-lga) \\ deriv f\\ c = (lfb-lfa) \\ deriv g\\ c$$$

Lean4

/-- A real function whose derivative tends to minus infinity from the right at a point is not
differentiable on the right at that point -/
theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi (f : ℝ → ℝ) {a : ℝ}
    (hf : Tendsto (deriv f) (𝓝[>] a) atBot) : ¬DifferentiableWithinAt ℝ f (Ioi a) a :=
  by
  intro h
  have hf' : Tendsto (deriv (-f)) (𝓝[>] a) atTop := by
    rw [deriv.neg']
    exact tendsto_neg_atBot_atTop.comp hf
  exact not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi (-f) hf' h.neg

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