not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio

English

If the derivative tends to −∞ from the left at a, then the function is not differentiable on the left at a.

Русский

Если производная стремится к минус бесконечности слева от a, то функция не дифференцируема слева от a.

LaTeX

$$$\\text{not }\\text{DifferentiableWithinAt} \\big(\\mathbb{R} \\to \\mathbb{R},\\ I^{o}_{a}, a\\big)$$$

Lean4

/-- A real function whose derivative tends to infinity from the left at a point is not
differentiable on the left at that point -/
theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio (f : ℝ → ℝ) {a : ℝ}
    (hf : Tendsto (deriv f) (𝓝[<] a) atTop) : ¬DifferentiableWithinAt ℝ f (Iio a) a :=
  by
  intro h
  have hf' : Tendsto (deriv (-f)) (𝓝[<] a) atBot := by
    rw [deriv.neg']
    exact tendsto_neg_atTop_atBot.comp hf
  exact not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio (-f) hf' h.neg

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