hasFDerivAtFilter_add_const_iff — Mathlib

English

HasFDerivAt of (f + c) equals HasFDerivAt f when c is constant, i.e., adding a constant does not change derivative.

Русский

Утверждение о производной: добавление константы не меняет производную.

LaTeX

$$$\forall c\in F,\ HasFDerivAt (f+ c) f' x \iff HasFDerivAt f f' x.$$$

Lean4

@[simp]
theorem hasFDerivAtFilter_add_const_iff (c : F) : HasFDerivAtFilter (f · + c) f' x L ↔ HasFDerivAtFilter f f' x L := by
  simp [hasFDerivAtFilter_iff_isLittleOTVS]

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