hasStrictDerivAt_abs_neg — Mathlib

English

If x < 0, then the absolute value has strict derivative -1 at x.

Русский

Если x < 0, то для функции abs(x) существует строго производная -1 в точке x.

LaTeX

$${x ∈ ℝ, x < 0} ⇒ HasStrictDerivAt (|·|) (-1) x$$

Lean4

theorem hasStrictDerivAt_abs_neg {x : ℝ} (hx : x < 0) : HasStrictDerivAt (|·|) (-1) x :=
  (hasStrictDerivAt_neg x).congr_of_eventuallyEq <|
    EqOn.eventuallyEq_of_mem (fun _ hy ↦ (abs_of_neg (mem_Iio.1 hy)).symm) (Iio_mem_nhds hx)

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