hasFDerivAt_add_const_iff

Mathlib.Analysis.Calculus.FDeriv.Add

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

English

DifferentiableAt of (f + c) equals DifferentiableAt f for constant c.

Русский

Дифференцируемость в точке для f + константа равна дифференцируемости f.

LaTeX

$$$\forall f, x, c,\ DifferentiableAt 𝕜 (f+ c) x \iff DifferentiableAt 𝕜 f x.$$$

Lean4

@[simp]
theorem hasFDerivAt_add_const_iff (c : F) : HasFDerivAt (f · + c) f' x ↔ HasFDerivAt f f' x :=
  hasFDerivAtFilter_add_const_iff c

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

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

Разделы

Аффилиация

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