differentiableWithinAt_abs_pos

Mathlib.Analysis.Calculus.Deriv.Abs

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

← MathLib Explorer

English

If x > 0, then |·| is differentiable within any set s at x.

Русский

Если x > 0, то |·| дифференцируема внутри любого множества s в x.

LaTeX

$$$\text{differentiableWithinAt}_{\mathbb{R}} (|\cdot|)\ s x \quad \text{ при } x>0$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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