hasDerivWithinAt_abs_pos

Mathlib.Analysis.Calculus.Deriv.Abs

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

English

If s is a set of real numbers and x ∈ s with x > 0, then HasDerivWithinAt abs 1 s x.

Русский

Если s — множество вещественных чисел и x ∈ s с x > 0, тогда HasDerivWithinAt(abs, 1, s, x).

LaTeX

$$HasDerivWithinAt abs 1 s x$$

Lean4

theorem hasDerivWithinAt_abs_pos (s : Set ℝ) {x : ℝ} (hx : 0 < x) : HasDerivWithinAt (|·|) 1 s x :=
  (hasDerivAt_abs_pos hx).hasDerivWithinAt

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

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

Разделы

Аффилиация

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