differentiableWithinAt_abs_neg — Mathlib

English

For real numbers, the absolute value is differentiable within any set at points x<0.

Русский

Для действительных чисел модуль дифференцируем внутри любого множества в точках x<0.

LaTeX

$$$$\text{DifferentiableWithinAt}_{\mathbb{R}} |·| s x \quad\text{for } x<0.$$$$

Lean4

theorem differentiableWithinAt_abs_neg (s : Set ℝ) {x : ℝ} (hx : x < 0) : DifferentiableWithinAt ℝ (|·|) s x :=
  (differentiableAt_abs_neg hx).differentiableWithinAt

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