hasFDerivWithinAt_add_const_iff — Mathlib

English

Derivative within s of (f + c) equals derivative within s of f, with constant c.

Русский

Производная внутри s от f + константа равна производной внутри s от f.

LaTeX

$$$\forall c,\ fderivWithin 𝕜 (f \,+ c) s x = fderivWithin 𝕜 f s x.$$$

Lean4

@[simp]
theorem hasFDerivWithinAt_add_const_iff (c : F) : HasFDerivWithinAt (f · + c) f' s x ↔ HasFDerivWithinAt f f' s x :=
  hasFDerivAtFilter_add_const_iff c

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