abs

Mathlib.Analysis.Calculus.Deriv.Abs

URI: https://scilib.ai/kg/mathlib#DifferentiableAt.abs

English

If f is differentiable at x and f(x) ≠ 0, then |f| is differentiable at x.

Русский

Если f дифференцируема в x и f(x) ≠ 0, то |f| дифференцируемо в x.

LaTeX

$$$$\text{DifferentiableAt } f x \land f(x) \neq 0 \Rightarrow \text{DifferentiableAt } |f| x.$$$$

Lean4

theorem abs (hf : DifferentiableAt ℝ f x) (h₀ : f x ≠ 0) : DifferentiableAt ℝ (fun x ↦ |f x|) x :=
  (differentiableAt_abs h₀).comp x hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru