hasStrictFDerivAt_add_const_iff — Mathlib

English

HasStrictFDerivAt of (f + c) equals HasStrictFDerivAt f for constant c; translation via isLittleO.

Русский

Строгая производная от суммы с константой равна строгой производной f без константы.

LaTeX

$$$\forall c,\ HasStrictFDerivAt (f + c) f' x \iff HasStrictFDerivAt f f' x.$$$

Lean4

@[simp]
theorem hasStrictFDerivAt_add_const_iff (c : F) : HasStrictFDerivAt (f · + c) f' x ↔ HasStrictFDerivAt f f' x := by
  simp [hasStrictFDerivAt_iff_isLittleO]

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