hasStrictDerivAt_abs_pos

Mathlib.Analysis.Calculus.Deriv.Abs

URI: https://scilib.ai/kg/mathlib#hasStrictDerivAt_abs_pos

← MathLib Explorer

English

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

Русский

Если x > 0, то производная mодуля равна 1 в точке x.

LaTeX

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

Lean4

theorem hasStrictDerivAt_abs_pos {x : ℝ} (hx : 0 < x) : HasStrictDerivAt (|·|) 1 x :=
  (hasStrictDerivAt_id x).congr_of_eventuallyEq <|
    EqOn.eventuallyEq_of_mem (fun _ hy ↦ (abs_of_pos (mem_Iio.1 hy)).symm) (Ioi_mem_nhds hx)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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